NF weak partition development: Flypitch4.ToMathlib.

Lean 3 → Lean 4 Port: Renames and Drops

Renames (for downstream file porters, search counts in src/)

1. imp_self → ba_imp_self (renamed to avoid collision with Lean 4 core imp_self)

   • Call sites: src/henkin.lean:210, src/fol.lean:2097 (2 sites)

2. le_trans' → le_trans_inf (renamed to avoid collision with mathlib4 ge_trans alias and Lean 4 core le_trans' for lists)

   • Call sites: src/bfol.lean:706, src/bvm.lean:64, :2475, :2481, src/bvm_extras.lean:2121, :2124 (6 sites)

3. mk_union_le → mk_union_le_impl (kept as wrapper; mathlib4 has Cardinal.mk_union_le)

   • Call site: src/collapse.lean:570 — when collapse is ported, prefer Cardinal.mk_union_le over our wrapper

4. nontrivial.bot_lt_top → nontrivial_bot_lt_top (flattened from sub-namespace dot notation; class accessor pattern changes in Lean 4)

   • Call sites: src/bfol.lean:790, src/bvm.lean:1596, src/zfc.lean:519, :534 (4 sites)

Drops (declarations removed because they exist in mathlib4)

1. congr1 and rexact tactics (src/to_mathlib.lean:492-510)

   • congr1 was a custom tactic used in ~10 downstream Lean 3 proof sites
   • In Lean 4, congr 1 (with a space) is a built-in tactic
   • When porting fol, henkin, language_extension, etc., translate congr1 (no space) to congr 1 (with space) inline rather than re-implementing

2. complete_degenerate_boolean_algebra (src/to_mathlib.lean:756)

   • Replaced by mathlib4's PUnit.instCompleteBooleanAlgebra in Mathlib/Order/CompleteBooleanAlgebra.lean
   • No downstream src/ file uses this directly

function namespace

Function.Injective.ne_iff already exists in mathlib4. No redeclaration needed.

dvector type and namespace

inductive NFChoice.DVec (α : Type u) : ℕ → Type u

Dependent-length vector: a list of exactly n elements of type α.

• nil {α : Type u} : DVec α 0
• cons {α : Type u} {n : ℕ} (_x : α) (_xs : DVec α n) : DVec α (n + 1)

inductive NFChoice.DFin : ℕ → Type

Finite type with n elements, used with DVec.

• fz {n : ℕ} : DFin (n + 1)
• fs {n : ℕ} : DFin n → DFin (n + 1)

@[instance_reducible]

instance NFChoice.haszeroDFin {n : ℕ} : Zero (DFin (n + 1))

Equations

• NFChoice.haszeroDFin = { zero := NFChoice.DFin.fz }

theorem NFChoice.DVec.zero_eq {α : Type u} (xs : DVec α 0) : xs = nil

def NFChoice.DVec.concat {α : Type u} {n : ℕ} : DVec α n → α → DVec α (n + 1)

Flypitch construction concat, retained by the first-order soundness and completeness development.

Equations

• NFChoice.DVec.nil.concat x✝ = NFChoice.DVec.cons x✝ NFChoice.DVec.nil
• (NFChoice.DVec.cons x_3 xs).concat x✝ = NFChoice.DVec.cons x_3 (xs.concat x✝)

def NFChoice.DVec.nth {α : Type u} {n : ℕ} : DVec α n → (m : ℕ) → m < n → α

Flypitch construction nth, retained by the first-order soundness and completeness development.

Equations

• NFChoice.DVec.nil.nth x✝¹ x✝ = absurd x✝ ⋯
• (NFChoice.DVec.cons x_4 _xs).nth 0 x_5 = x_4
• (NFChoice.DVec.cons _x xs).nth m.succ h = xs.nth m ⋯

theorem NFChoice.DVec.nth_cons {α : Type u} {n : ℕ} (x : α) (xs : DVec α n) (m : ℕ) (h : m < n) : (cons x xs).nth (m + 1) ⋯ = xs.nth m h

@[reducible]

def NFChoice.DVec.last {α : Type u} {n : ℕ} (xs : DVec α (n + 1)) : α

Flypitch construction last, retained by the first-order soundness and completeness development.

Equations

• xs.last = xs.nth n ⋯

def NFChoice.DVec.nth' {α : Type u} {n : ℕ} (xs : DVec α n) (m : Fin n) : α

Flypitch construction nth', retained by the first-order soundness and completeness development.

Equations

• xs.nth' m = xs.nth ↑m ⋯

def NFChoice.DVec.nth'' {α : Type u} {n : ℕ} : DVec α n → DFin n → α

Flypitch construction nth'', retained by the first-order soundness and completeness development.

Equations

• (NFChoice.DVec.cons x_3 _xs).nth'' NFChoice.DFin.fz = x_3
• (NFChoice.DVec.cons _x xs).nth'' m.fs = xs.nth'' m

def NFChoice.DVec.mem {α : Type u} {n : ℕ} : α → DVec α n → Prop

Flypitch construction mem, retained by the first-order soundness and completeness development.

Equations

• NFChoice.DVec.mem x✝ NFChoice.DVec.nil = False
• NFChoice.DVec.mem x✝ (NFChoice.DVec.cons x' xs) = (x✝ = x' ∨ NFChoice.DVec.mem x✝ xs)

@[instance_reducible]

instance NFChoice.DVec.membershipDVec {α : Type u} {n : ℕ} : Membership α (DVec α n)

Equations

• NFChoice.DVec.membershipDVec = { mem := fun (xs : NFChoice.DVec α n) (a : α) => NFChoice.DVec.mem a xs }

def NFChoice.DVec.pmem {α : Type u} {n : ℕ} : α → DVec α n → Type

Flypitch construction pmem, retained by the first-order soundness and completeness development.

Equations

• NFChoice.DVec.pmem x✝ NFChoice.DVec.nil = Empty
• NFChoice.DVec.pmem x✝ (NFChoice.DVec.cons x' xs) = (x✝ = x' ⊕' NFChoice.DVec.pmem x✝ xs)

theorem NFChoice.DVec.mem_of_pmem {α : Type u} {n : ℕ} {x : α} {xs : DVec α n} : ∀ (a : DVec.pmem x xs), x ∈ xs

def NFChoice.DVec.map {α : Type u} {β : Type v} (f : α → β) {n : ℕ} : DVec α n → DVec β n

Flypitch construction map, retained by the first-order soundness and completeness development.

Equations

• NFChoice.DVec.map f NFChoice.DVec.nil = NFChoice.DVec.nil
• NFChoice.DVec.map f (NFChoice.DVec.cons x_2 xs) = NFChoice.DVec.cons (f x_2) (NFChoice.DVec.map f xs)

def NFChoice.DVec.map2 {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) {n : ℕ} : DVec α n → DVec β n → DVec γ n

Flypitch construction map2, retained by the first-order soundness and completeness development.

Equations

• NFChoice.DVec.map2 f NFChoice.DVec.nil NFChoice.DVec.nil = NFChoice.DVec.nil
• NFChoice.DVec.map2 f (NFChoice.DVec.cons x_3 xs) (NFChoice.DVec.cons y ys) = NFChoice.DVec.cons (f x_3 y) (NFChoice.DVec.map2 f xs ys)

@[simp]

theorem NFChoice.DVec.map_id {α : Type u} {n : ℕ} (xs : DVec α n) : DVec.map (fun (x : α) => x) xs = xs

theorem NFChoice.DVec.map_congr_pmem {α : Type u} {β : Type v} {f g : α → β} {n : ℕ} {xs : DVec α n} : (∀ (x : α) (a : DVec.pmem x xs), f x = g x) → DVec.map f xs = DVec.map g xs

theorem NFChoice.DVec.map_congr_mem {α : Type u} {β : Type v} {f g : α → β} {n : ℕ} {xs : DVec α n} (h : ∀ x ∈ xs, f x = g x) : DVec.map f xs = DVec.map g xs

theorem NFChoice.DVec.map_congr {α : Type u} {β : Type v} {f g : α → β} (h : ∀ (x : α), f x = g x) {n : ℕ} (xs : DVec α n) : DVec.map f xs = DVec.map g xs

@[simp]

theorem NFChoice.DVec.map_map {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) {n : ℕ} (xs : DVec α n) : DVec.map g (DVec.map f xs) = DVec.map (fun (x : α) => g (f x)) xs

theorem NFChoice.DVec.map_inj {α : Type u} {β : Type v} {f : α → β} (hf : ∀ {x x' : α}, f x = f x' → x = x') {n : ℕ} {xs xs' : DVec α n} (h : DVec.map f xs = DVec.map f xs') : xs = xs'

@[simp]

theorem NFChoice.DVec.map_concat {α : Type u} {β : Type v} (f : α → β) {n : ℕ} (xs : DVec α n) (x : α) : DVec.map f (xs.concat x) = (DVec.map f xs).concat (f x)

@[simp]

theorem NFChoice.DVec.map_nth {α : Type u} {β : Type v} (f : α → β) {n : ℕ} (xs : DVec α n) (m : ℕ) (h : m < n) : (DVec.map f xs).nth m h = f (xs.nth m h)

theorem NFChoice.DVec.concat_nth {α : Type u} {n : ℕ} (xs : DVec α n) (x : α) (m : ℕ) (h' : m < n + 1) (h : m < n) : (xs.concat x).nth m h' = xs.nth m h

@[simp]

theorem NFChoice.DVec.concat_nth_last {α : Type u} {n : ℕ} (xs : DVec α n) (x : α) (h : n < n + 1) : (xs.concat x).nth n h = x

theorem NFChoice.DVec.concat_nth_last' {α : Type u} {n : ℕ} (xs : DVec α n) (x : α) (_h : n < n + 1) : (xs.concat x).last = x

def NFChoice.DVec.append {α : Type u} {n m : ℕ} : DVec α n → DVec α m → DVec α (m + n)

Flypitch construction append, retained by the first-order soundness and completeness development.

Equations

• NFChoice.DVec.nil.append x✝ = x✝
• (NFChoice.DVec.cons x' xs).append x✝ = NFChoice.DVec.cons x' (xs.append x✝)

def NFChoice.DVec.insert {α : Type u} {n : ℕ} : α → ℕ → DVec α n → DVec α (n + 1)

Flypitch construction insert, retained by the first-order soundness and completeness development.

Equations

• NFChoice.DVec.insert x✝¹ 0 x✝ = NFChoice.DVec.cons x✝¹ x✝
• NFChoice.DVec.insert x✝¹ x✝ x_6 = NFChoice.DVec.cons x✝¹ NFChoice.DVec.nil
• NFChoice.DVec.insert x✝ k.succ (NFChoice.DVec.cons y ys) = NFChoice.DVec.cons y (NFChoice.DVec.insert x✝ k ys)

@[simp]

theorem NFChoice.DVec.insert_at_zero {α : Type u} {n : ℕ} (x : α) (xs : DVec α n) : DVec.insert x 0 xs = cons x xs

@[simp]

theorem NFChoice.DVec.insert_nth {α : Type u} {n : ℕ} (x : α) (k : ℕ) (xs : DVec α n) (h : k < n + 1) : (DVec.insert x k xs).nth k h = x

theorem NFChoice.DVec.insert_cons {α : Type u} {n k : ℕ} {x y : α} {v : DVec α n} : cons x (DVec.insert y k v) = DVec.insert y (k + 1) (cons x v)

def NFChoice.DVec.trunc {α : Type u} (n : ℕ) {m : ℕ} : n ≤ m → DVec α m → DVec α n

The n-th initial segment of a vector, given a proof that n ≤ m.

Equations

• NFChoice.DVec.trunc 0 x_4 x_5 = NFChoice.DVec.nil
• NFChoice.DVec.trunc 0 x_4 x_5 = NFChoice.DVec.nil
• NFChoice.DVec.trunc n.succ h x_4 = absurd h ⋯
• NFChoice.DVec.trunc n.succ h (NFChoice.DVec.cons x_4 xs) = NFChoice.DVec.cons x_4 (NFChoice.DVec.trunc n ⋯ xs)

@[simp]

theorem NFChoice.DVec.trunc_n_n {α : Type u} {n : ℕ} {h : n ≤ n} {v : DVec α n} : DVec.trunc n h v = v

@[simp]

theorem NFChoice.DVec.trunc_0_n {α : Type u} {n : ℕ} {h : 0 ≤ n} {v : DVec α n} : DVec.trunc 0 h v = nil

@[simp]

theorem NFChoice.DVec.trunc_nth {α : Type u} {n m l : ℕ} {h : n ≤ m} {h' : l < n} {v : DVec α m} : (DVec.trunc n h v).nth l h' = v.nth l ⋯

theorem NFChoice.DVec.nth_irrel1 {α : Type u} {n k : ℕ} {h : k < n + 1} {h' : k < n + 1 + 1} (v : DVec α (n + 1)) (x : α) : (cons x (DVec.trunc n ⋯ v)).nth k h = (cons x v).nth k h'

def NFChoice.DVec.cast {α : Type u} {n m : ℕ} (p : n = m) (v : DVec α n) : DVec α m

Flypitch construction cast, retained by the first-order soundness and completeness development.

Equations

• NFChoice.DVec.cast p v = p ▸ v

@[simp]

theorem NFChoice.DVec.cast_irrel {α : Type u} {n m : ℕ} {p p' : n = m} {v : DVec α n} : DVec.cast p v = DVec.cast p' v

theorem NFChoice.DVec.cast_rfl {α : Type u} {n m : ℕ} {p : n = m} {q : m = n} {v : DVec α n} : DVec.cast q (DVec.cast p v) = v

theorem NFChoice.DVec.cast_hrfl {α : Type u} {n m : ℕ} {p : n = m} {v : DVec α n} : DVec.cast p v ≍ v

@[simp]

theorem NFChoice.DVec.cast_trans {α : Type u} {n m o : ℕ} {p : n = m} {q : m = o} {v : DVec α n} : DVec.cast q (DVec.cast p v) = DVec.cast ⋯ v

@[simp]

theorem NFChoice.DVec.cast_cons {α : Type u} {n m : ℕ} (h : n + 1 = m + 1) (x : α) (v : DVec α n) : DVec.cast h (cons x v) = cons x (DVec.cast ⋯ v)

@[simp]

theorem NFChoice.DVec.cast_append_nil {α : Type u} {n : ℕ} (v : DVec α n) (h : 0 + n = n) : DVec.cast h (v.append nil) = v

def NFChoice.DVec.removeMth {α : Type u} {n : ℕ} : ℕ → DVec α (n + 1) → DVec α n

Flypitch construction remove_mth, retained by the first-order soundness and completeness development.

Equations

• NFChoice.DVec.removeMth x✝ x_4 = NFChoice.DVec.nil
• NFChoice.DVec.removeMth 0 (NFChoice.DVec.cons _x ys) = ys
• NFChoice.DVec.removeMth k.succ (NFChoice.DVec.cons y ys) = NFChoice.DVec.cons y (NFChoice.DVec.removeMth k ys)

def NFChoice.DVec.replace {α : Type u} {n : ℕ} : α → ℕ → DVec α n → DVec α n

Flypitch construction replace, retained by the first-order soundness and completeness development.

Equations

• NFChoice.DVec.replace x✝ 0 (NFChoice.DVec.cons _x ys) = NFChoice.DVec.cons x✝ ys
• NFChoice.DVec.replace x✝¹ x✝ ys = ys
• NFChoice.DVec.replace x✝ k.succ (NFChoice.DVec.cons y ys) = NFChoice.DVec.cons y (NFChoice.DVec.replace x✝ k ys)

theorem NFChoice.DVec.insert_nth_lt {α : Type u} {n k l : ℕ} (x : α) (xs : DVec α n) (h : l < n) (h' : l < n + 1) (h2 : l < k) : (DVec.insert x k xs).nth l h' = xs.nth l h

theorem NFChoice.DVec.insert_nth_gt' {α : Type u} {n k l : ℕ} (x : α) (xs : DVec α n) (h : l - 1 < n) (h' : l < n + 1) (h2 : k < l) : (DVec.insert x k xs).nth l h' = xs.nth (l - 1) h

@[simp]

theorem NFChoice.DVec.insert_nth_gt_simp {α : Type u} {n k l : ℕ} (x : α) (xs : DVec α n) (h' : l < n + 1) (h2 : k < l) : (DVec.insert x k xs).nth l h' = xs.nth (l - 1) ⋯

theorem NFChoice.DVec.insert_nth_gt {α : Type u} {n k l : ℕ} (x : α) (xs : DVec α n) (h : l < n) (h' : l + 1 < n + 1) (h2 : k < l + 1) : (DVec.insert x k xs).nth (l + 1) h' = xs.nth l h

@[simp]

theorem NFChoice.DVec.replace_head {α : Type u} {n : ℕ} {x z : α} {xs : DVec α n} : DVec.replace z 0 (cons x xs) = cons z xs

@[simp]

theorem NFChoice.DVec.replace_neck {α : Type u} {n : ℕ} {x y z : α} {xs : DVec α n} : DVec.replace z 1 (cons x (cons y xs)) = cons x (cons z xs)

def NFChoice.DVec.foldr {α : Type u} {β : Type v} (f : α → β → β) (b : β) {n : ℕ} : DVec α n → β

Flypitch construction foldr, retained by the first-order soundness and completeness development.

Equations

• NFChoice.DVec.foldr f b NFChoice.DVec.nil = b
• NFChoice.DVec.foldr f b (NFChoice.DVec.cons x_2 xs) = f x_2 (NFChoice.DVec.foldr f b xs)

def NFChoice.DVec.zip {α : Type u} {β : Type v} {n : ℕ} : DVec α n → DVec β n → DVec (α × β) n

Flypitch construction zip, retained by the first-order soundness and completeness development.

Equations

• NFChoice.DVec.nil.zip NFChoice.DVec.nil = NFChoice.DVec.nil
• (NFChoice.DVec.cons x_3 xs).zip (NFChoice.DVec.cons y ys) = NFChoice.DVec.cons (x_3, y) (xs.zip ys)

def NFChoice.DVec.fInf {α : Type u} {n : ℕ} [SemilatticeInf α] [OrderTop α] (xs : DVec α n) : α

The finitary infimum

Equations

• xs.fInf = NFChoice.DVec.foldr (fun (x b : α) => x ⊓ b) ⊤ xs

@[simp]

theorem NFChoice.DVec.fInf_nil {α : Type u} [SemilatticeInf α] [OrderTop α] : nil.fInf = ⊤

@[simp]

theorem NFChoice.DVec.fInf_cons {α : Type u} {n : ℕ} [SemilatticeInf α] [OrderTop α] (x : α) (xs : DVec α n) : (cons x xs).fInf = x ⊓ xs.fInf

def NFChoice.DVec.fSup {α : Type u} {n : ℕ} [SemilatticeSup α] [OrderBot α] (xs : DVec α n) : α

The finitary supremum

Equations

• xs.fSup = NFChoice.DVec.foldr (fun (x b : α) => x ⊔ b) ⊥ xs

@[simp]

theorem NFChoice.DVec.fSup_nil {α : Type u} [SemilatticeSup α] [OrderBot α] : nil.fSup = ⊥

@[simp]

theorem NFChoice.DVec.fSup_cons {α : Type u} {n : ℕ} [SemilatticeSup α] [OrderBot α] (x : α) (xs : DVec α n) : (cons x xs).fSup = x ⊔ xs.fSup

inductive NFChoice.DVec.DVecRel {α : Type u} [Setoid α] {n : ℕ} : DVec α n → DVec α n → Prop

Pointwise relation on DVec, given a setoid on the element type

• rnil {α : Type u} [Setoid α] : nil.DVecRel nil
• rcons {α : Type u} [Setoid α] {x x' : α} {n : ℕ} {xs xs' : DVec α n} (hx : x ≈ x') (hxs : xs.DVecRel xs') : (cons x xs).DVecRel (cons x' xs')

theorem NFChoice.DVec.rel_refl {α : Type u} [Setoid α] {n : ℕ} (xs : DVec α n) : xs.DVecRel xs

theorem NFChoice.DVec.rel_symm {α : Type u} [Setoid α] {n : ℕ} {xs xs' : DVec α n} (h : xs.DVecRel xs') : xs'.DVecRel xs

theorem NFChoice.DVec.rel_trans {α : Type u} [Setoid α] {n : ℕ} {xs₁ xs₂ xs₃ : DVec α n} (h₁ : xs₁.DVecRel xs₂) (h₂ : xs₂.DVecRel xs₃) : xs₁.DVecRel xs₃

@[instance_reducible]

instance NFChoice.DVec.setoidInst {α : Type u} [Setoid α] {n : ℕ} : Setoid (DVec α n)

Equations

• NFChoice.DVec.setoidInst = { r := NFChoice.DVec.DVecRel, iseqv := ⋯ }

noncomputable def NFChoice.DVec.quotientLift {α : Type u} {β : Sort v} {R : Setoid α} {n : ℕ} (f : DVec α n → β) (_h : ∀ {xs xs' : DVec α n}, xs ≈ xs' → f xs = f xs') (_qs : DVec (Quotient R) n) : β

Flypitch construction quotient_lift, retained by the first-order soundness and completeness development.

Equations

• NFChoice.DVec.quotientLift f x_4 NFChoice.DVec.nil = f NFChoice.DVec.nil
• NFChoice.DVec.quotientLift f h (NFChoice.DVec.cons q qs) = Quotient.lift (fun (x : α) => NFChoice.DVec.quotientLift (fun (xs : NFChoice.DVec α n) => f (NFChoice.DVec.cons x xs)) ⋯ qs) ⋯ q

theorem NFChoice.DVec.quotient_beta {α : Type u} {β : Sort v} {R : Setoid α} {n : ℕ} (f : DVec α n → β) (h : ∀ {xs xs' : DVec α n}, xs ≈ xs' → f xs = f xs') (xs : DVec α n) : quotientLift f ⋯ (DVec.map Quotient.mk'' xs) = f xs

set namespace

theorem NFChoice.Set.disjoint_iff_eq_empty {α : Type u_1} {s t : Set α} : Disjoint s t ↔ s ∩ t = ∅

theorem NFChoice.Set.not_nonempty_iff {α : Type u_1} {s : Set α} : ¬Nonempty ↑s ↔ s = ∅

theorem NFChoice.Set.neq_neg_of_nonempty {α : Type u_1} {P : Set α} (H_nonempty : Nonempty α) : P ≠ Pᶜ

theorem NFChoice.Set.subset_biInter_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {u : α → Set β} : t ⊆ ⋂ x ∈ s, u x ↔ ∀ x ∈ s, t ⊆ u x

theorem NFChoice.Set.ne_empty_of_subset {α : Type u_1} {s t : Set α} (h : s ⊆ t) (hs : s ≠ ∅) : t ≠ ∅

nat namespace

theorem NFChoice.Nat.pred_lt_iff_lt_succ {m n : ℕ} (H : 1 ≤ m) : m.pred < n ↔ m < n.succ

@[simp]

theorem NFChoice.Nat.le_of_le_and_ne_succ {x y : ℕ} (H : x ≤ y + 1) (H' : x ≠ y + 1) : x ≤ y

classical namespace (logic helpers)

noncomputable def NFChoice.Classical.psigmaOfExists {α : Type u} {p : α → Prop} (h : ∃ (x : α), p x) : (x : α) ×' p x

Flypitch construction psigma_of_exists, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Classical.psigmaOfExists h = ⟨Classical.choose h, ⋯⟩

theorem NFChoice.Classical.some_eq {α : Type u} {p : α → Prop} {h : ∃ (a : α), p a} (x : α) (hx : ∀ (y : α), p y → y = x) : Classical.choose h = x

theorem NFChoice.Classical.or_not_iff_true (p : Prop) : p ∨ ¬p ↔ True

theorem NFChoice.Classical.nonempty_of_not_empty {α : Type u} (s : Set α) (h : ¬s = ∅) : Nonempty ↑s

theorem NFChoice.Classical.nonempty_of_not_empty_finset {α : Type u} (s : Finset α) (h : ¬s = ∅) : Nonempty ↑↑s

list namespace

def NFChoice.List.toSet {α : Type u} (l : List α) : Set α

Flypitch construction toSet, retained by the first-order soundness and completeness development.

Equations

• NFChoice.List.toSet l = {x : α | x ∈ l}

theorem NFChoice.List.toSet_map {α : Type u} {β : Type v} (f : α → β) (l : List α) : List.toSet (List.map f l) = f '' List.toSet l

theorem NFChoice.List.exists_of_toSet_subset_image {α : Type u} {β : Type v} {f : α → β} {l : List β} {t : Set α} (h : List.toSet l ⊆ f '' t) : ∃ (l' : List α), List.toSet l' ⊆ t ∧ List.map f l' = l

additional nat lemmas

theorem NFChoice.Nat.add_sub_swap {n k : ℕ} (h : k ≤ n) (m : ℕ) : n + m - k = n - k + m

misc prop lemmas

theorem NFChoice.imp_eq_congr {a b c d : Prop} (h₁ : a = b) (h₂ : c = d) : (a → c) = (b → d)

theorem NFChoice.forall_eq_congr {α : Sort u} {p q : α → Prop} (h : ∀ (a : α), p a = q a) : (∀ (a : α), p a) = ∀ (a : α), q a

additional set lemmas

theorem NFChoice.Set.ne_empty_of_exists_mem {α : Type u} {s : Set α} : (∃ (x : α), x ∈ s) → s ≠ ∅

theorem NFChoice.Set.inter_sUnion_ne_empty_of_exists_mem {α : Type u} {b : Set α} {𝓕 : Set (Set α)} (H : ∃ f ∈ 𝓕, b ∩ f ≠ ∅) : b ∩ ⋃₀ 𝓕 ≠ ∅

theorem NFChoice.Set.mem_image_univ {α : Type u} {β : Type v} {f : α → β} {x : α} : f x ∈ f '' Set.univ

theorem NFChoice.Set.image_preimage_eq_of_subset_image {α : Type u} {β : Type v} {f : α → β} {s : Set β} {t : Set α} (h : s ⊆ f '' t) : f '' f ⁻¹' s = s

theorem NFChoice.Set.subset_union_left_of_subset {α : Type u} {s t : Set α} (h : s ⊆ t) (u : Set α) : s ⊆ t ∪ u

theorem NFChoice.Set.subset_union_right_of_subset {α : Type u} {s u : Set α} (h : s ⊆ u) (t : Set α) : s ⊆ t ∪ u

theorem NFChoice.Set.subset_sUnion {α : Type u} {s : Set α} {t : Set (Set α)} (h : s ∈ t) : s ⊆ ⋃₀ t

theorem NFChoice.Set.subset_union2_left {α : Type u} {s t u : Set α} : s ⊆ s ∪ t ∪ u

theorem NFChoice.Set.subset_union2_middle {α : Type u} {s t u : Set α} : t ⊆ s ∪ t ∪ u

def NFChoice.Set.change {α : Type u} {π : α → Type u_1} [DecidableEq α] (f : (a : α) → π a) {x : α} (z : π x) (y : α) : π y

Flypitch construction change, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Set.change f z y = if h : x = y then h ▸ z else f y

theorem NFChoice.Set.dif_mem_pi {α : Type u} {π : α → Type u_1} (i : Set α) (s : (a : α) → Set (π a)) [DecidableEq α] (f : (a : α) → π a) (hf : f ∈ i.pi s) {x : α} (z : π x) (h : x ∈ i → z ∈ s x) : change f z ∈ i.pi s

theorem NFChoice.Set.image_pi_pos {α : Type u} {π : α → Type u_1} (i : Set α) (s : (a : α) → Set (π a)) (hp : (i.pi s).Nonempty) (x : α) (hx : x ∈ i) : (fun (f : (a : α) → π a) => f x) '' i.pi s = s x

theorem NFChoice.Set.image_pi_neg {α : Type u} {π : α → Type u_1} (i : Set α) (s : (a : α) → Set (π a)) (hp : (i.pi s).Nonempty) (x : α) (hx : x ∉ i) : (fun (f : (a : α) → π a) => f x) '' i.pi s = Set.univ

nonempty namespace

theorem NFChoice.Nonempty.iff {α : Sort u} {β : Sort v} (mp : α → β) (mpr : β → α) : Nonempty α ↔ Nonempty β

arity' type and namespace

def NFChoice.Arity' (α β : Type u) : ℕ → Type u

The type α → (α → ... (α → β)...) with n α's.

Equations

• NFChoice.Arity' α β 0 = β
• NFChoice.Arity' α β n.succ = (α → NFChoice.Arity' α β n)

def NFChoice.Arity'.arity'Constant {α β : Type u} {n : ℕ} : β → Arity' α β n

Flypitch construction arity'_constant, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Arity'.arity'Constant x✝ = x✝
• NFChoice.Arity'.arity'Constant x✝ = fun (x : α) => NFChoice.Arity'.arity'Constant x✝

def NFChoice.Arity'.ofDvectorMap {α β : Type u} {l : ℕ} (_f : DVec α l → β) : Arity' α β l

Flypitch construction of_dvector_map, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Arity'.ofDvectorMap f = f NFChoice.DVec.nil
• NFChoice.Arity'.ofDvectorMap f = fun (x : α) => NFChoice.Arity'.ofDvectorMap fun (xs : NFChoice.DVec α _l) => f (NFChoice.DVec.cons x xs)

def NFChoice.Arity'.arity'App {α β : Type u} {l : ℕ} : Arity' α β l → DVec α l → β

Flypitch construction arity'_app, retained by the first-order soundness and completeness development.

Equations

• b.arity'App NFChoice.DVec.nil = b
• f.arity'App (NFChoice.DVec.cons x_3 xs) = (f x_3).arity'App xs

@[simp]

theorem NFChoice.Arity'.arity'_app_zero {α β : Type u} (f : Arity' α β 0) (xs : DVec α 0) : f.arity'App xs = f

def NFChoice.Arity'.arity'Postcompose {α β γ : Type u} (g : β → γ) {n : ℕ} (_f : Arity' α β n) : Arity' α γ n

Flypitch construction arity'_postcompose, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Arity'.arity'Postcompose g b = g b
• NFChoice.Arity'.arity'Postcompose g f = fun (x : α) => NFChoice.Arity'.arity'Postcompose g (f x)

def NFChoice.Arity'.arity'Postcompose2 {α β γ δ : Type u} (h : β → γ → δ) {n : ℕ} (_f : Arity' α β n) (_g : Arity' α γ n) : Arity' α δ n

Flypitch construction arity'_postcompose2, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Arity'.arity'Postcompose2 h b c = h b c
• NFChoice.Arity'.arity'Postcompose2 h f g = fun (x : α) => NFChoice.Arity'.arity'Postcompose2 h (f x) (g x)

def NFChoice.Arity'.arity'Precompose {α β γ : Type u} {n : ℕ} (_g : Arity' β γ n) (_f : α → β) : Arity' α γ n

Flypitch construction arity'_precompose, retained by the first-order soundness and completeness development.

Equations

• c.arity'Precompose x✝ = c
• g.arity'Precompose x✝ = fun (x : α) => (g (x✝ x)).arity'Precompose x✝

inductive NFChoice.Arity'.Arity'RespectSetoid {α β : Type u} [R : Setoid α] {n : ℕ} : Arity' α β n → Type u

Flypitch construction arity'_respect_setoid, retained by the first-order soundness and completeness development.

• r_zero {α β : Type u} [R : Setoid α] (b : β) : Arity'RespectSetoid b
• r_succ {α β : Type u} [R : Setoid α] (n : ℕ) (f : Arity' α β (n + 1)) (h₁ : ∀ {a a' : α}, a ≈ a' → f a = f a') (h₂ : (a : α) → (f a).Arity'RespectSetoid) : f.Arity'RespectSetoid

instance NFChoice.Arity'.subsingleton_arity'_respect_setoid {α β : Type u} [R : Setoid α] {n : ℕ} (f : Arity' α β n) : Subsingleton f.Arity'RespectSetoid

def NFChoice.Arity'.forAll {α : Type u} (P : α → Prop) : Prop

Flypitch construction for_all, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Arity'.forAll P = ∀ (x : α), P x

def NFChoice.Arity'.arity'Map2 {α β : Type u} (q : (α → β) → β) (f : β → β → β) {n : ℕ} : Arity' α β n → Arity' α β n → β

Flypitch construction arity'_map2, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Arity'.arity'Map2 q f x_3 y = f x_3 y
• NFChoice.Arity'.arity'Map2 q f x_3 y = q fun (z : α) => NFChoice.Arity'.arity'Map2 q f (x_3 z) (y z)

@[simp]

theorem NFChoice.Arity'.arity'_map2_refl {α : Type} {f : Prop → Prop → Prop} (r : ∀ (A : Prop), f A A) {n : ℕ} (x : Arity' α Prop n) : arity'Map2 forAll f x x

def NFChoice.Arity'.arity'Imp {α : Type} {n : ℕ} (f₁ f₂ : Arity' α Prop n) : Prop

Flypitch construction arity'_imp, retained by the first-order soundness and completeness development.

Equations

• f₁.arity'Imp f₂ = NFChoice.Arity'.arity'Map2 NFChoice.Arity'.forAll (fun (P Q : Prop) => P → Q) f₁ f₂

def NFChoice.Arity'.arity'Iff {α : Type} {n : ℕ} (f₁ f₂ : Arity' α Prop n) : Prop

Flypitch construction arity'_iff, retained by the first-order soundness and completeness development.

Equations

• f₁.arity'Iff f₂ = NFChoice.Arity'.arity'Map2 NFChoice.Arity'.forAll Iff f₁ f₂

theorem NFChoice.Arity'.arity'_iff_refl {α : Type} {n : ℕ} (f : Arity' α Prop n) : f.arity'Iff f

theorem NFChoice.Arity'.arity'_iff_rfl {α : Type} {n : ℕ} {f : Arity' α Prop n} : f.arity'Iff f

Miscellaneous lemmas

theorem NFChoice.lt_irrefl' {α : Type u_1} [Preorder α] {Γ : α} (H_lt : Γ < Γ) : False