awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
F : Type u_4
inst_2 : FunLike F M N
inst_3 : L.HomClass F M N
g : F
t : L.Term α
v : α → M
⊢ Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) t : N) ((g : (a : M) → N) (Term.realize v t) : N)
have var : ∀ (a : α),
  Eq.{u_1 + 1} (α := N) (Term.realize.{u, v, u_1, u'} (L := L) ((⇑g : (a : M) → N) ∘ v) (var a) : N)
    ((g : (a : M) → N) (Term.realize.{u, v, w, u'} (L := L) v (var a)) : N)
Tactic: induction t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
F : Type u_4
inst_2 : FunLike F M N
inst_3 : L.HomClass F M N
g : F
t : L.Term α
v : α → M
var :
  ∀ (a : α),
    Eq.{u_1 + 1} (α := N) (Term.realize.{u, v, u_1, u'} (L := L) ((⇑g : (a : M) → N) ∘ v) (Language.var a) : N)
      ((g : (a : M) → N) (Term.realize.{u, v, w, u'} (L := L) v (Language.var a)) : N)
⊢ Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) t : N) ((g : (a : M) → N) (Term.realize v t) : N)
have func : ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α),
  (∀ (a : Fin l),
      Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts a) : N)
        ((g : (a : M) → N) (Term.realize v (_ts a)) : N)) →
    Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) (func _f _ts) : N)
      ((g : (a : M) → N) (Term.realize v (func _f _ts)) : N)
Tactic: induction t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
F : Type u_4
inst_2 : FunLike F M N
inst_3 : L.HomClass F M N
g : F
v : α → M
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
_ts_ih :
  ∀ (a : Fin l),
    Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts a) : N)
      ((g : (a : M) → N) (Term.realize v (_ts a)) : N)
⊢ Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) (func _f _ts) : N)
    ((g : (a : M) → N) (Term.realize v (func _f _ts)) : N)
have func : Eq.{u_1 + 1} (α := N) (funMap _f fun (i : Fin l) ↦ Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts i))
  (funMap _f (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) fun (i : Fin l) ↦ Term.realize v (_ts i)))
Tactic: rw [Term.realize, Term.realize, HomClass.map_fun]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
F : Type u_4
inst_2 : FunLike F M N
inst_3 : L.HomClass F M N
g : F
v : α → M
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
_ts_ih :
  ∀ (a : Fin l),
    Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts a) : N)
      ((g : (a : M) → N) (Term.realize v (_ts a)) : N)
⊢ Eq.{u_1 + 1} (α := N) (funMap _f fun (i : Fin l) ↦ Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts i))
    (funMap _f (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) fun (i : Fin l) ↦ Term.realize v (_ts i)))
have func : Eq.{u_1 + 1} (α := (i : Fin l) → N) (fun (i : Fin l) ↦ Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts i))
  (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) fun (i : Fin l) ↦ Term.realize v (_ts i))
Tactic: refine congr rfl ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
F : Type u_4
inst_2 : FunLike F M N
inst_3 : L.HomClass F M N
g : F
v : α → M
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
_ts_ih :
  ∀ (a : Fin l),
    Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts a) : N)
      ((g : (a : M) → N) (Term.realize v (_ts a)) : N)
⊢ Eq.{u_1 + 1} (α := (i : Fin l) → N) (fun (i : Fin l) ↦ Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts i))
    (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) fun (i : Fin l) ↦ Term.realize v (_ts i))
have func : ∀ (x : Fin l),
  Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts x))
    (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) (fun (i : Fin l) ↦ Term.realize v (_ts i)) x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
l : List (L.BoundedFormula α n)
v : α → M
xs : Fin n → M
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊓ x2) ⊤ l) v xs ↔
    ∀ φ ∈ l, φ.Realize v xs
have nil : Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊓ x2) ⊤ []) v xs ↔
  ∀ (φ : L.BoundedFormula α n), Membership.mem (γ := List (L.BoundedFormula α n)) [] φ → φ.Realize v xs
Tactic: induction l with
  | nil => simp
  | cons φ l ih => simp [ih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
l : List (L.BoundedFormula α n)
v : α → M
xs : Fin n → M
nil :
  Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊓ x2) ⊤ []) v xs ↔
    ∀ (φ : L.BoundedFormula α n), Membership.mem (γ := List (L.BoundedFormula α n)) [] φ → φ.Realize v xs
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊓ x2) ⊤ l) v xs ↔
    ∀ φ ∈ l, φ.Realize v xs
have cons : ∀ (φ : L.BoundedFormula α n) (l : List (L.BoundedFormula α n))
  (ih :
    Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊓ x2) ⊤ l) v xs ↔
      ∀ φ ∈ l, φ.Realize v xs),
  Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊓ x2) ⊤ (φ :: l)) v xs ↔
    ∀ φ_1 ∈ φ :: l, φ_1.Realize v xs
Tactic: induction l with
  | nil => simp
  | cons φ l ih => simp [ih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
k : ℕ
l : List (L.BoundedFormula α k)
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
⊢ (List.foldr imp f l).Realize v xs = ((∀ i ∈ l, i.Realize v xs) → f.Realize v xs)
have induction : (List.foldr imp f []).Realize v xs =
  ((∀ (i : L.BoundedFormula α k), Membership.mem (γ := List (L.BoundedFormula α k)) [] i → i.Realize v xs) →
    f.Realize v xs)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
k : ℕ
l : List (L.BoundedFormula α k)
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
induction :
  (List.foldr imp f []).Realize v xs =
    ((∀ (i : L.BoundedFormula α k), Membership.mem (γ := List (L.BoundedFormula α k)) [] i → i.Realize v xs) →
      f.Realize v xs)
⊢ (List.foldr imp f l).Realize v xs = ((∀ i ∈ l, i.Realize v xs) → f.Realize v xs)
have cons : ∀ (head : L.BoundedFormula α k) (tail : List (L.BoundedFormula α k)),
  (List.foldr imp f tail).Realize v xs = ((∀ i ∈ tail, i.Realize v xs) → f.Realize v xs) →
    (List.foldr imp f (head :: tail)).Realize v xs = ((∀ i ∈ head :: tail, i.Realize v xs) → f.Realize v xs)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
f' : L.BoundedFormula α k
tail : List (L.BoundedFormula α k)
tail_ih : (List.foldr imp f tail).Realize v xs = ((∀ i ∈ tail, i.Realize v xs) → f.Realize v xs)
⊢ (List.foldr imp f (f' :: tail)).Realize v xs = ((∀ i ∈ f' :: tail, i.Realize v xs) → f.Realize v xs)
have pos : f'.Realize v xs → (List.foldr imp f (f' :: tail)).Realize v xs = ((∀ i ∈ f' :: tail, i.Realize v xs) → f.Realize v xs)
Tactic: by_cases f'.Realize v xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
f' : L.BoundedFormula α k
tail : List (L.BoundedFormula α k)
tail_ih : (List.foldr imp f tail).Realize v xs = ((∀ i ∈ tail, i.Realize v xs) → f.Realize v xs)
pos :
  f'.Realize v xs → (List.foldr imp f (f' :: tail)).Realize v xs = ((∀ i ∈ f' :: tail, i.Realize v xs) → f.Realize v xs)
⊢ (List.foldr imp f (f' :: tail)).Realize v xs = ((∀ i ∈ f' :: tail, i.Realize v xs) → f.Realize v xs)
have neg : ¬f'.Realize v xs → (List.foldr imp f (f' :: tail)).Realize v xs = ((∀ i ∈ f' :: tail, i.Realize v xs) → f.Realize v xs)
Tactic: by_cases f'.Realize v xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : Term.{u, v, u'} L (α ⊕ Fin l)
⊢ (R.boundedFormula₁ t).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t]
have rw : (RelMap.{u, v, w} (M := M) R fun (i : Fin 1) ↦ realize (Sum.elim v xs) (![t] i)) = RelMap R ![realize (Sum.elim v xs) t]
Tactic: rw [Relations.boundedFormula₁, realize_rel, iff_eq_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : Term.{u, v, u'} L (α ⊕ Fin l)
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin 1) ↦ realize (Sum.elim v xs) (![t] i)) =
    RelMap R ![realize (Sum.elim v xs) t]
have refine : ∀ (x : Fin 1), realize (Sum.elim v xs) (![t] x) = ![realize (Sum.elim v xs) t] x
Tactic: refine congr rfl (funext fun _ => ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin l)
⊢ (R.boundedFormula₂ t₁ t₂).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]
have rw : (RelMap.{u, v, w} (M := M) R fun (i : Fin 2) ↦ realize (Sum.elim v xs) (![t₁, t₂] i)) =
  RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]
Tactic: rw [Relations.boundedFormula₂, realize_rel, iff_eq_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin l)
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin 2) ↦ realize (Sum.elim v xs) (![t₁, t₂] i)) =
    RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]
have refine_1 : realize (Sum.elim v xs) (![t₁, t₂] 0) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] 0
Tactic: refine congr rfl (funext (Fin.cases ?_ ?_))
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin l)
refine_1 : realize (Sum.elim v xs) (![t₁, t₂] 0) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] 0
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin 2) ↦ realize (Sum.elim v xs) (![t₁, t₂] i)) =
    RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]
have refine_2 : ∀ (i : Fin 1),
  realize (Sum.elim v xs) (![t₁, t₂] i.succ) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] i.succ
Tactic: refine congr rfl (funext (Fin.cases ?_ ?_))
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (∼φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs
have mp : (∼φ ⟹ ψ).Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
Tactic: tauto
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
mp : (∼φ ⟹ ψ).Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
⊢ (∼φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs
have mpr : φ.Realize v xs ∨ ψ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
Tactic: tauto
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
mp : (∼φ ⟹ ψ).Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
mpr : φ.Realize v xs ∨ ψ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mp₁ mp₂ : (∼φ ⟹ ψ).Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
⊢ (∼φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs
have mp₃ : (∼φ ⟹ ψ).Realize v xs → ¬φ.Realize v xs → ψ.Realize v xs
Tactic: tauto
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
mp : (∼φ ⟹ ψ).Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
mpr : φ.Realize v xs ∨ ψ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mp₁ mp₂ : (∼φ ⟹ ψ).Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
mp₃ : (∼φ ⟹ ψ).Realize v xs → ¬φ.Realize v xs → ψ.Realize v xs
⊢ (∼φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs
have mpr₁ : φ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
Tactic: tauto
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
mp : (∼φ ⟹ ψ).Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
mpr : φ.Realize v xs ∨ ψ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mp₁ mp₂ : (∼φ ⟹ ψ).Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
mp₃ : (∼φ ⟹ ψ).Realize v xs → ¬φ.Realize v xs → ψ.Realize v xs
mpr₁ : φ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
⊢ (∼φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs
have mpr₂ : ψ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
Tactic: tauto
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
mp : (∼φ ⟹ ψ).Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
mpr : φ.Realize v xs ∨ ψ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mp₁ mp₂ : (∼φ ⟹ ψ).Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
mp₃ : (∼φ ⟹ ψ).Realize v xs → ¬φ.Realize v xs → ψ.Realize v xs
mpr₁ : φ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mpr₂ : ψ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mpr₃ : φ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mpr₄ : ψ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
⊢ (∼φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs
have mpr₅ : φ.Realize v xs → (∼φ).Realize v xs → ψ.Realize v xs
Tactic: tauto
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
mp : (∼φ ⟹ ψ).Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
mpr : φ.Realize v xs ∨ ψ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mp₁ mp₂ : (∼φ ⟹ ψ).Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
mp₃ : (∼φ ⟹ ψ).Realize v xs → ¬φ.Realize v xs → ψ.Realize v xs
mpr₁ : φ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mpr₂ : ψ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mpr₃ : φ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mpr₄ : ψ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mpr₅ : φ.Realize v xs → (∼φ).Realize v xs → ψ.Realize v xs
⊢ (∼φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs
have mpr₆ : ψ.Realize v xs → (∼φ).Realize v xs → ψ.Realize v xs
Tactic: tauto
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih :
  Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ ∈ l, φ.Realize v xs
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ (φ :: l)) v xs ↔
    ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
have cons : (φ ⊔ List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
Tactic: simp_rw [List.foldr_cons, realize_sup, ih, List.mem_cons, or_and_right, exists_or,
      exists_eq_left]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih :
  Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ ∈ l, φ.Realize v xs
cons :
  (φ ⊔ List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ (φ :: l)) v xs ↔
    ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
have cons₁ : φ.Realize v xs ∨ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
  ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
Tactic: simp_rw [List.foldr_cons, realize_sup, ih, List.mem_cons, or_and_right, exists_or,
      exists_eq_left]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih :
  Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ ∈ l, φ.Realize v xs
cons :
  (φ ⊔ List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
cons₁ :
  φ.Realize v xs ∨ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ (φ :: l)) v xs ↔
    ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
have cons₂ : (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
Tactic: simp_rw [List.foldr_cons, realize_sup, ih, List.mem_cons, or_and_right, exists_or,
      exists_eq_left]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih :
  Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ ∈ l, φ.Realize v xs
cons :
  (φ ⊔ List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
cons₁ :
  φ.Realize v xs ∨ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
cons₂ : (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ (φ :: l)) v xs ↔
    ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
have cons₃ : (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔ ∃ (φ_1 : L.BoundedFormula α n), (φ_1 = φ ∨ φ_1 ∈ l) ∧ φ_1.Realize v xs
Tactic: simp_rw [List.foldr_cons, realize_sup, ih, List.mem_cons, or_and_right, exists_or,
      exists_eq_left]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih :
  Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ ∈ l, φ.Realize v xs
cons :
  (φ ⊔ List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
cons₁ :
  φ.Realize v xs ∨ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
cons₂ : (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
cons₃ :
  (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔ ∃ (φ_1 : L.BoundedFormula α n), (φ_1 = φ ∨ φ_1 ∈ l) ∧ φ_1.Realize v xs
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ (φ :: l)) v xs ↔
    ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
have cons₄ : (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔
  ∃ (φ_1 : L.BoundedFormula α n), φ_1 = φ ∧ φ_1.Realize v xs ∨ φ_1 ∈ l ∧ φ_1.Realize v xs
Tactic: simp_rw [List.foldr_cons, realize_sup, ih, List.mem_cons, or_and_right, exists_or,
      exists_eq_left]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih :
  Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ ∈ l, φ.Realize v xs
cons :
  (φ ⊔ List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
cons₁ :
  φ.Realize v xs ∨ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
cons₂ : (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
cons₃ :
  (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔ ∃ (φ_1 : L.BoundedFormula α n), (φ_1 = φ ∨ φ_1 ∈ l) ∧ φ_1.Realize v xs
cons₄ :
  (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔
    ∃ (φ_1 : L.BoundedFormula α n), φ_1 = φ ∧ φ_1.Realize v xs ∨ φ_1 ∈ l ∧ φ_1.Realize v xs
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ (φ :: l)) v xs ↔
    ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
have cons₅ : (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔
  (∃ (x : L.BoundedFormula α n), x = φ ∧ x.Realize v xs) ∨ ∃ x ∈ l, x.Realize v xs
Tactic: simp_rw [List.foldr_cons, realize_sup, ih, List.mem_cons, or_and_right, exists_or,
      exists_eq_left]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
l : List (L.BoundedFormula α n)
v : α → M
xs : Fin n → M
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ ∈ l, φ.Realize v xs
have nil : Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ []) v xs ↔
  ∃ (φ : L.BoundedFormula α n), Membership.mem (γ := List (L.BoundedFormula α n)) [] φ ∧ φ.Realize v xs
Tactic: induction l with
  | nil => simp
  | cons φ l ih =>
    simp_rw [List.foldr_cons, realize_sup, ih, List.mem_cons, or_and_right, exists_or,
      exists_eq_left]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
l : List (L.BoundedFormula α n)
v : α → M
xs : Fin n → M
nil :
  Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ []) v xs ↔
    ∃ (φ : L.BoundedFormula α n), Membership.mem (γ := List (L.BoundedFormula α n)) [] φ ∧ φ.Realize v xs
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ ∈ l, φ.Realize v xs
have cons : ∀ (φ : L.BoundedFormula α n) (l : List (L.BoundedFormula α n))
  (ih :
    Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
      ∃ φ ∈ l, φ.Realize v xs),
  Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ (φ :: l)) v xs ↔
    ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
Tactic: induction l with
  | nil => simp
  | cons φ l ih =>
    simp_rw [List.foldr_cons, realize_sup, ih, List.mem_cons, or_and_right, exists_or,
      exists_eq_left]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
⊢ (∃' θ).Realize v xs ↔ ∃ (a : M), θ.Realize v (snoc (α := fun (a : Fin l.succ) ↦ M) xs a)
have rw : (∃ (x : M), ¬(∼θ).Realize v (snoc (α := fun (a : Fin l.succ) ↦ M) xs x)) ↔
  ∃ (a : M), θ.Realize v (snoc (α := fun (a : Fin l.succ) ↦ M) xs a)
Tactic: rw [BoundedFormula.ex, realize_not, realize_all, not_forall]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
m n : ℕ
h : m = n
h' : m ≤ n
φ : L.BoundedFormula α m
v : α → M
xs : Fin n → M
⊢ (castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h)
have subst : ∀ {h' : m ≤ m} {xs : Fin m → M}, (castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast sorry)
Tactic: subst h
Cleared hypotheses: n, h, h', xs