awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Ultraproducts
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) ↦
      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:
apply relMap_quotient_mk'

Premises used: FirstOrder.Language.relMap_quotient_mk'
-- Module: Mathlib.ModelTheory.Ultraproducts
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
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
⊢ ((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

Tactic:
simp only [BoundedFormula.Realize, ih v, ih' v]

Premises used: FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Ultraproducts
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
imp 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
⊢ ((∀ᶠ (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:
rw [Ultrafilter.eventually_imp]

Premises used: Ultrafilter.eventually_imp
-- Module: Mathlib.ModelTheory.Ultraproducts
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))
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)
⊢ (∀ (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)

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)))

Premises used: Iff.trans
-- Module: Mathlib.ModelTheory.Ultraproducts
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)) ↔
    ∀ (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:
Quotient.forall

Premises used: Quotient.forall, Quotient.mk'
-- Module: Mathlib.ModelTheory.Ultraproducts
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)) ↔
    ∀ (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:
exact Quotient.forall

Premises used: Quotient.forall
-- Module: Mathlib.ModelTheory.Ultraproducts
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))

Tactic:
fun m a => funext (Fin.reverseInduction ?_ fun i _ => ?_)

Premises used: Fin.reverseInduction, funext
-- Module: Mathlib.ModelTheory.Ultraproducts
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)
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)
⊢ ∀ (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:
refine fun m a => funext (Fin.reverseInduction ?_ fun i _ => ?_)

Premises used: Fin.reverseInduction, funext
-- Module: Mathlib.ModelTheory.Ultraproducts
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} (α := 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:
simp only [Fin.snoc_last]

Premises used: Fin.snoc_last
-- Module: Mathlib.ModelTheory.Ultraproducts
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 : α
i : Fin k
h :
  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:
simp only [Fin.snoc_castSucc]

Premises used: Fin.snoc_castSucc
-- Module: Mathlib.ModelTheory.Ultraproducts
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))

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]
-- Module: Mathlib.ModelTheory.Ultraproducts
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
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))
all :
  (∀ (m : (a : α) → M a),
      φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        (Quotient.mk' ∘ Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v 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)
⊢ (∀ (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:
simp only [← Fin.comp_snoc]

Premises used: Fin.comp_snoc
-- Module: Mathlib.ModelTheory.Ultraproducts
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
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))
all :
  (∀ (m : (a : α) → M a),
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))) ↔
    ∀ᶠ (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)
⊢ (∀ (m : (a : α) → M a),
      φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        (Quotient.mk' ∘ Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v 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:
simp only [Function.comp_def, ih, h']

Premises used: Function.comp_def
-- Module: Mathlib.ModelTheory.Ultraproducts
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
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))
⊢ (∀ (m : (a : α) → M a),
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))) ↔
    ∀ᶠ (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:
⟨fun h => ?_, fun h m => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.ModelTheory.Ultraproducts
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
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))
all :
  ∀
    (h :
      ∀ (m : (a : α) → M a),
        ∀ᶠ (a : α) in (↑u : Filter α),
          BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
            (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))),
    ∀ᶠ (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)
all₁ :
  ∀
    (h :
      ∀ᶠ (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))
    (m : (a : α) → M a),
    ∀ᶠ (a : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
        (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))
⊢ (∀ (m : (a : α) → M a),
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))) ↔
    ∀ᶠ (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:
refine ⟨fun h => ?_, fun h m => ?_⟩