awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n_1 : ℕ
t₁ t₂ : Term.{u, v, u_3} L (β ⊕ Fin n_1)
v : Fin n_1 → (a : α) → M a
h2 :
  ∀ (a : α),
    Eq (α := β ⊕ Fin n_1 → M a) (Sum.elim (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) fun (i : β ⊕ Fin n_1) ↦
      Sum.elim x v i a
⊢ ((BoundedFormula.equal t₁ t₂).Realize (M := Quotient ((↑u : Filter α).productSetoid M))
      (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n_1) ↦ Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) (BoundedFormula.equal t₁ t₂) (fun (i : β) ↦ x i a)
        fun (i : Fin n_1) ↦ v i a
have equal : Eq (α := Quotient ((↑u : Filter α).productSetoid M))
    (Term.realize (Sum.elim (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n_1) ↦ Quotient.mk' (v i)) t₁)
    (Term.realize (Sum.elim (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n_1) ↦ Quotient.mk' (v i)) t₂) ↔
  ∀ᶠ (a : α) in (↑u : Filter α),
    Eq.{u_2 + 1} (α := M a) (Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) t₁)
      (Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) t₂)
Tactic: simp only [BoundedFormula.Realize, h2]
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n_1 : ℕ
t₁ t₂ : Term.{u, v, u_3} L (β ⊕ Fin n_1)
v : Fin n_1 → (a : α) → M a
h2 :
  ∀ (a : α),
    Eq (α := β ⊕ Fin n_1 → M a) (Sum.elim (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) fun (i : β ⊕ Fin n_1) ↦
      Sum.elim x v i a
⊢ Eq (α := Quotient ((↑u : Filter α).productSetoid M))
      (Term.realize (Sum.elim (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n_1) ↦ Quotient.mk' (v i)) t₁)
      (Term.realize (Sum.elim (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n_1) ↦ Quotient.mk' (v i)) t₂) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      Eq.{u_2 + 1} (α := M a) (Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) t₁)
        (Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) t₂)
have equal : Eq (α := Quotient ((↑u : Filter α).productSetoid M))
    (Quotient.mk' fun (a : α) ↦ Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) t₁)
    (Quotient.mk' fun (a : α) ↦ Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) t₂) ↔
  ∀ᶠ (a : α) in (↑u : Filter α),
    Eq.{u_2 + 1} (α := M a) (Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) t₁)
      (Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) t₂)
Tactic: erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm,
      term_realize_cast, term_realize_cast]
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (hypothesis)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u_3} L (β ⊕ Fin n_1)
v : Fin n_1 → (a : α) → M a
⊢ ((BoundedFormula.rel R ts).Realize (M := Quotient ((↑u : Filter α).productSetoid M))
      (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n_1) ↦ Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) (BoundedFormula.rel R ts) (fun (i : β) ↦ x i a)
        fun (i : Fin n_1) ↦ v i a
have h2 : ∀ (a : α),
  Eq (α := β ⊕ Fin n_1 → M a) (Sum.elim (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) fun (i : β ⊕ Fin n_1) ↦
    Sum.elim x v i a
Tactic: have h2 : ∀ a : α, (Sum.elim (fun i : β => x i a) fun i => v i a) = fun i => Sum.elim x v i a :=
      fun a => funext fun i => Sum.casesOn i (fun i => rfl) fun i => rfl
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u_3} L (β ⊕ Fin n_1)
v : Fin n_1 → (a : α) → M a
h2 :
  ∀ (a : α),
    Eq (α := β ⊕ Fin n_1 → M a) (Sum.elim (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) fun (i : β ⊕ Fin n_1) ↦
      Sum.elim x v i a
⊢ ((BoundedFormula.rel R ts).Realize (M := Quotient ((↑u : Filter α).productSetoid M))
      (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n_1) ↦ Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) (BoundedFormula.rel R ts) (fun (i : β) ↦ x i a)
        fun (i : Fin n_1) ↦ v i a
have rel : (RelMap (M := Quotient ((↑u : Filter α).productSetoid M)) R fun (i : Fin l) ↦
    Term.realize (Sum.elim (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n_1) ↦ Quotient.mk' (v i)) (ts i)) ↔
  ∀ᶠ (a : α) in (↑u : Filter α),
    RelMap.{u, v, u_2} (M := M a) R fun (i : Fin l) ↦ Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) (ts i)
Tactic: simp only [BoundedFormula.Realize, h2]
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u_3} L (β ⊕ Fin n_1)
v : Fin n_1 → (a : α) → M a
h2 :
  ∀ (a : α),
    Eq (α := β ⊕ Fin n_1 → M a) (Sum.elim (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) fun (i : β ⊕ Fin n_1) ↦
      Sum.elim x v i a
⊢ (RelMap (M := Quotient ((↑u : Filter α).productSetoid M)) R fun (i : Fin l) ↦
      Term.realize (Sum.elim (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n_1) ↦ Quotient.mk' (v i)) (ts i)) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      RelMap.{u, v, u_2} (M := M a) R fun (i : Fin l) ↦ Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) (ts i)
have rel : (RelMap (M := Quotient ((↑u : Filter α).productSetoid M)) R fun (i : Fin l) ↦
    Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts i)) ↔
  ∀ᶠ (a : α) in (↑u : Filter α),
    RelMap.{u, v, u_2} (M := M a) R fun (i : Fin l) ↦ Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) (ts i)
Tactic: erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm]
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u_3} L (β ⊕ Fin n_1)
v : Fin n_1 → (a : α) → M a
h2 :
  ∀ (a : α),
    Eq (α := β ⊕ Fin n_1 → M a) (Sum.elim (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) fun (i : β ⊕ Fin n_1) ↦
      Sum.elim x v i a
| RelMap (M := Quotient ((↑u : Filter α).productSetoid M)) R fun (i : Fin l) ↦
    Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts i)
have h : ∀ (i : Fin l), Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts i)
Tactic: enter [2, i]
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u_3} L (β ⊕ Fin n_1)
v : Fin n_1 → (a : α) → M a
h2 :
  ∀ (a : α),
    Eq (α := β ⊕ Fin n_1 → M a) (Sum.elim (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) fun (i : β ⊕ Fin n_1) ↦
      Sum.elim x v i a
i : Fin l
| Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts i)
have h : Quotient.mk' fun (a : α) ↦ Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) (ts i)
Tactic: erw [term_realize_cast]
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u_3} L (β ⊕ Fin n_1)
v : Fin n_1 → (a : α) → M a
h2 :
  ∀ (a : α),
    Eq (α := β ⊕ Fin n_1 → M a) (Sum.elim (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) fun (i : β ⊕ Fin n_1) ↦
      Sum.elim x v i a
| RelMap (M := Quotient ((↑u : Filter α).productSetoid M)) R fun (i : Fin l) ↦
    Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts i)
have h : ∀ (i : Fin l), Quotient.mk' fun (a : α) ↦ Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) (ts i)
Tactic: enter [2, i]; erw [term_realize_cast]
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u_3} L (β ⊕ Fin n_1)
v : Fin n_1 → (a : α) → M a
h2 :
  ∀ (a : α),
    Eq (α := β ⊕ Fin n_1 → M a) (Sum.elim (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) fun (i : β ⊕ Fin n_1) ↦
      Sum.elim x v i a
⊢ (RelMap (M := Quotient ((↑u : Filter α).productSetoid M)) R fun (i : Fin l) ↦
      Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts i)) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      RelMap.{u, v, u_2} (M := M a) R fun (i : Fin l) ↦ Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) (ts i)
have rel : (RelMap (M := Quotient ((↑u : Filter α).productSetoid M)) R fun (i : Fin l) ↦
    Quotient.mk' fun (a : α) ↦ Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) (ts i)) ↔
  ∀ᶠ (a : α) in (↑u : Filter α),
    RelMap.{u, v, u_2} (M := M a) R fun (i : Fin l) ↦ Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) (ts i)
Tactic: conv_lhs => enter [2, i]; erw [term_realize_cast]
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n_1 : ℕ
f₁ f₂ : L.BoundedFormula β n_1
ih :
  ∀ (v : Fin n_1 → (a : α) → M a),
    (f₁.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n_1) ↦
        Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) f₁ (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a
ih' :
  ∀ (v : Fin n_1 → (a : α) → M a),
    (f₂.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n_1) ↦
        Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) f₂ (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a
v : Fin n_1 → (a : α) → M a
⊢ ((f₁ ⟹ f₂).Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
      fun (i : Fin n_1) ↦ Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) (f₁ ⟹ f₂) (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a
have imp : ((∀ᶠ (a : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) f₁ (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) →
    ∀ᶠ (a : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) f₂ (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) ↔
  ∀ᶠ (a : α) in (↑u : Filter α),
    (BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) f₁ (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) →
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) f₂ (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a
Tactic: simp only [BoundedFormula.Realize, ih v, ih' v]
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n_1 : ℕ
f₁ f₂ : L.BoundedFormula β n_1
ih :
  ∀ (v : Fin n_1 → (a : α) → M a),
    (f₁.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n_1) ↦
        Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) f₁ (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a
ih' :
  ∀ (v : Fin n_1 → (a : α) → M a),
    (f₂.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n_1) ↦
        Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) f₂ (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a
v : Fin n_1 → (a : α) → M a
⊢ ((∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) f₁ (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) →
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) f₂ (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      (BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) f₁ (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) →
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) f₂ (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a
have imp : ((∀ᶠ (a : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) f₁ (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) →
    ∀ᶠ (a : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) f₂ (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) ↔
  (∀ᶠ (x_1 : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M x_1) f₁ (fun (i : β) ↦ x i x_1) fun (i : Fin n_1) ↦ v i x_1) →
    ∀ᶠ (x_1 : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M x_1) f₂ (fun (i : β) ↦ x i x_1) fun (i : Fin n_1) ↦ v i x_1
Tactic: rw [Ultrafilter.eventually_imp]
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        fun (i : Fin (k + 1)) ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a) fun (i : Fin (k + 1)) ↦ v i a
v : Fin k → (a : α) → M a
⊢ (∀ (x_1 : Quotient ((↑u : Filter α).productSetoid M)),
      φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ Quotient ((↑u : Filter α).productSetoid M))
          (fun (i : Fin k) ↦ Quotient.mk' (v i)) x_1)) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      ∀ (x_1 : M a),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1)
have all : (∀ (x_1 : Quotient ((↑u : Filter α).productSetoid M)),
    φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
      (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ Quotient ((↑u : Filter α).productSetoid M))
        (fun (i : Fin k) ↦ Quotient.mk' (v i)) x_1)) ↔
  ∀ (m : (a : α) → M a),
    φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
      (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ Quotient ((↑u : Filter α).productSetoid M)) (Quotient.mk' ∘ v)
        (Quotient.mk' m))
Tactic: apply Iff.trans (b := ∀ m : ∀ a : α, M a,
      φ.Realize (fun i : β => (x i : (u : Filter α).Product M))
        (Fin.snoc (((↑) : (∀ a, M a) → (u : Filter α).Product M) ∘ v)
          (m : (u : Filter α).Product M)))
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        fun (i : Fin (k + 1)) ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a) fun (i : Fin (k + 1)) ↦ v i a
v : Fin k → (a : α) → M a
all :
  (∀ (x_1 : Quotient ((↑u : Filter α).productSetoid M)),
      φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ Quotient ((↑u : Filter α).productSetoid M))
          (fun (i : Fin k) ↦ Quotient.mk' (v i)) x_1)) ↔
    ∀ (m : (a : α) → M a),
      φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ Quotient ((↑u : Filter α).productSetoid M)) (Quotient.mk' ∘ v)
          (Quotient.mk' m))
⊢ (∀ (x_1 : Quotient ((↑u : Filter α).productSetoid M)),
      φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ Quotient ((↑u : Filter α).productSetoid M))
          (fun (i : Fin k) ↦ Quotient.mk' (v i)) x_1)) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      ∀ (x_1 : M a),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1)
have all₁ : (∀ (m : (a : α) → M a),
    φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
      (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ Quotient ((↑u : Filter α).productSetoid M)) (Quotient.mk' ∘ v)
        (Quotient.mk' m))) ↔
  ∀ᶠ (a : α) in (↑u : Filter α),
    ∀ (x_1 : M a),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
        (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1)
Tactic: apply Iff.trans (b := ∀ m : ∀ a : α, M a,
      φ.Realize (fun i : β => (x i : (u : Filter α).Product M))
        (Fin.snoc (((↑) : (∀ a, M a) → (u : Filter α).Product M) ∘ v)
          (m : (u : Filter α).Product M)))
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        fun (i : Fin (k + 1)) ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a) fun (i : Fin (k + 1)) ↦ v i a
v : Fin k → (a : α) → M a
⊢ ∀ (m : (a : α) → M a) (a : α),
    Eq.{u_2 + 1} (α := (i : Fin (k + 1)) → M a)
      (fun (i : Fin (k + 1)) ↦ Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m i a)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))
have refine_1 : ∀ (m : (a : α) → M a) (a : α),
  Eq.{u_2 + 1} (α := M a) (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m (Fin.last k) a : M a)
    (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a) (Fin.last k) : M a)
Tactic: refine fun m a => funext (Fin.reverseInduction ?_ fun i _ => ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        fun (i : Fin (k + 1)) ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a) fun (i : Fin (k + 1)) ↦ v i a
v : Fin k → (a : α) → M a
refine_1 :
  ∀ (m : (a : α) → M a) (a : α),
    Eq.{u_2 + 1} (α := M a) (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m (Fin.last k) a : M a)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a) (Fin.last k) : M a)
⊢ ∀ (m : (a : α) → M a) (a : α),
    Eq.{u_2 + 1} (α := (i : Fin (k + 1)) → M a)
      (fun (i : Fin (k + 1)) ↦ Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m i a)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))
have refine_2 : ∀ (m : (a : α) → M a) (a : α) (i : Fin k),
  Eq.{u_2 + 1} (α := M a) (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m i.succ a : M a)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a) i.succ : M a) →
    Eq.{u_2 + 1} (α := M a) (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m i.castSucc a : M a)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a) i.castSucc : M a)
Tactic: refine fun m a => funext (Fin.reverseInduction ?_ fun i _ => ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (hypothesis)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        fun (i : Fin (k + 1)) ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a) fun (i : Fin (k + 1)) ↦ v i a
v : Fin k → (a : α) → M a
⊢ (∀ (m : (a : α) → M a),
      φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ Quotient ((↑u : Filter α).productSetoid M)) (Quotient.mk' ∘ v)
          (Quotient.mk' m))) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      ∀ (x_1 : M a),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1)
have h' : ∀ (m : (a : α) → M a) (a : α),
  Eq.{u_2 + 1} (α := (i : Fin (k + 1)) → M a)
    (fun (i : Fin (k + 1)) ↦ Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m i a)
    (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))
Tactic: have h' :
      ∀ (m : ∀ a, M a) (a : α),
        (fun i : Fin (k + 1) => (Fin.snoc v m : _ → ∀ a, M a) i a) =
          Fin.snoc (fun i : Fin k => v i a) (m a) := by
      refine fun m a => funext (Fin.reverseInduction ?_ fun i _ => ?_)
      · simp only [Fin.snoc_last]
      · simp only [Fin.snoc_castSucc]