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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : RelMap r x
a : α
ha1 :
  Membership.mem (γ := Set α) {x_1 : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a) x_1} a
ha2 : Membership.mem (γ := Set α) (⋂ (i : Fin n), {x_1 : α | (fun (a : α) ↦ x i a = y i a) x_1}) a
refine_1 : ∀ (ha2 : ∀ (i : Fin n), x i a = y i a), RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a
⊢ Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a) x} a

Tactic:
simp only [Set.mem_iInter, Set.mem_setOf_eq] at *

Premises used: Set.mem_setOf_eq, Set.mem_iInter
-- 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : ∀ᶠ (a : α) in (↑u : Filter α), RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a
a : α
ha1 : RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a
ha2 : ∀ (i : Fin n), x i a = y i a
refine_1 : RelMap.{u, v, u_2} (M := M a) r fun (x_1 : Fin n) ↦ x x_1 a
⊢ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a

Tactic:
rw [← funext ha2]

Premises used: 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : ∀ᶠ (a : α) in (↑u : Filter α), RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a
a : α
ha1 : RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap.{u, v, u_2} (M := M a) r fun (x_1 : Fin n) ↦ x x_1 a

Tactic:
ha1
-- 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : ∀ᶠ (a : α) in (↑u : Filter α), RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a
a : α
ha1 : RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap.{u, v, u_2} (M := M a) r fun (x_1 : Fin n) ↦ x x_1 a

Tactic:
exact ha1
-- 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : RelMap r y
⊢ RelMap r x

Tactic:
mem_of_superset (inter_mem hy (iInter_mem.2 xy)) ?_

Premises used: Iff.mpr, Filter.Eventually, Filter.inter_mem, Filter.iInter_mem, Filter.mem_of_superset
-- 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : RelMap r y
refine_2 :
  Subset.{u_1} (α := Set α)
    ({x : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a) x} ∩
      ⋂ (i : Fin n), {x_1 : α | (fun (a : α) ↦ x i a = y i a) x_1})
    {x_1 : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a) x_1}
⊢ RelMap r x

Tactic:
refine mem_of_superset (inter_mem hy (iInter_mem.2 xy)) ?_

Premises used: Iff.mpr, Filter.inter_mem, Filter.iInter_mem, Filter.mem_of_superset
-- 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : RelMap r y
a : α
ha1 : Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a) x} a
ha2 : Membership.mem (γ := Set α) (⋂ (i : Fin n), {x_1 : α | (fun (a : α) ↦ x i a = y i a) x_1}) a
refine_2 : ∀ (ha2 : ∀ (i : Fin n), x i a = y i a), RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a
⊢ Membership.mem (γ := Set α) {x_1 : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a) x_1} a

Tactic:
simp only [Set.mem_iInter, Set.mem_setOf_eq] at *

Premises used: Set.mem_setOf_eq, Set.mem_iInter
-- 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : ∀ᶠ (a : α) in (↑u : Filter α), RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a
a : α
ha1 : RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a
ha2 : ∀ (i : Fin n), x i a = y i a
refine_2 : RelMap.{u, v, u_2} (M := M a) r fun (x : Fin n) ↦ y x a
⊢ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a

Tactic:
rw [funext ha2]

Premises used: 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : ∀ᶠ (a : α) in (↑u : Filter α), RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a
a : α
ha1 : RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap.{u, v, u_2} (M := M a) r fun (x : Fin n) ↦ y x a

Tactic:
ha1
-- 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : ∀ᶠ (a : α) in (↑u : Filter α), RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a
a : α
ha1 : RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap.{u, v, u_2} (M := M a) r fun (x : Fin n) ↦ y x a

Tactic:
exact ha1
-- 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)
n : ℕ
f : L.Functions n
x : Fin n → (a : α) → M a
⊢ Eq (α := Quotient ((↑u : Filter α).productSetoid M)) (funMap f fun (i : Fin n) ↦ Quotient.mk' (x i))
    (Quotient.mk' fun (a : α) ↦ funMap f fun (i : Fin n) ↦ x i a)

Tactic:
apply funMap_quotient_mk'

Premises used: FirstOrder.Language.funMap_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)
β : Type u_3
x : β → (a : α) → M a
t : L.Term β
⊢ Term.realize (fun (i : β) ↦ ⟦x i⟧) t = ⟦Term.realize x t⟧

Tactic:
@Term.realize_quotient_mk' L _ ((u : Filter α).productSetoid M)
      (Ultraproduct.setoidPrestructure M u) _ t x

Premises used: FirstOrder.Language.Term.realize_quotient_mk', Filter.productSetoid, Ultrafilter.toFilter
-- 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)
β : Type u_3
x : β → (a : α) → M a
t : L.Term β
h : (fun (a : α) ↦ Term.realize (fun (i : β) ↦ x i a) t) = Term.realize x t
⊢ Eq (α := Quotient ((↑u : Filter α).productSetoid M)) (Term.realize (fun (i : β) ↦ Quotient.mk' (x i)) t)
    (Quotient.mk' fun (a : α) ↦ Term.realize (fun (i : β) ↦ x i a) t)

Tactic:
convert!
    @Term.realize_quotient_mk' L _ ((u : Filter α).productSetoid M)
      (Ultraproduct.setoidPrestructure M u) _ t x using 2

Premises used: FirstOrder.Language.Term.realize_quotient_mk', Filter.productSetoid, Ultrafilter.toFilter
-- 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)
β : Type u_3
x : β → (a : α) → M a
t : L.Term β
h : ∀ (a : α), Term.realize (fun (i : β) ↦ x i a) t = Term.realize x t a
⊢ (fun (a : α) ↦ Term.realize (fun (i : β) ↦ x i a) t) = Term.realize x t

Tactic:
ext a
-- 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)
β : Type u_3
x : β → (a : α) → M a
a : α
a_1 : β
⊢ Term.realize.{u, v, u_2, u_3} (L := L) (fun (i : β) ↦ x i a) (var a_1) = Term.realize (L := L) x (var a_1) a

Tactic:
rfl
-- 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)
β : Type u_3
x : β → (a : α) → M a
a : α
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term β
t_ih : ∀ (a_1 : Fin l), Term.realize (fun (i : β) ↦ x i a) (_ts a_1) = Term.realize x (_ts a_1) a
h :
  Eq.{u_2 + 1} (α := M a) (funMap _f fun (i : Fin l) ↦ Term.realize x (_ts i) a)
    (funMap _f (fun (i : Fin l) ↦ Term.realize x (_ts i)) a)
⊢ Term.realize (fun (i : β) ↦ x i a) (func _f _ts) = Term.realize x (func _f _ts) a

Tactic:
simp only [Term.realize, t_ih]

Premises used: FirstOrder.Language.Term.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)
β : Type u_3
x : β → (a : α) → M a
a : α
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term β
t_ih : ∀ (a_1 : Fin l), Term.realize (fun (i : β) ↦ x i a) (_ts a_1) = Term.realize x (_ts a_1) a
⊢ Eq.{u_2 + 1} (α := M a) (funMap _f fun (i : Fin l) ↦ Term.realize x (_ts i) a)
    (funMap _f (fun (i : Fin l) ↦ Term.realize x (_ts i)) a)

Tactic:
rfl
-- 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)
β : Type u_3
x : β → (a : α) → M a
t : L.Term β
a : α
h :
  ∀ (a_1 : β),
    Term.realize.{u, v, u_2, u_3} (L := L) (fun (i : β) ↦ x i a) (var a_1) = Term.realize (L := L) x (var a_1) a
h₁ :
  ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term β)
    (t_ih : ∀ (a_1 : Fin l), Term.realize (fun (i : β) ↦ x i a) (_ts a_1) = Term.realize x (_ts a_1) a),
    Term.realize (fun (i : β) ↦ x i a) (func _f _ts) = Term.realize x (func _f _ts) a
⊢ Term.realize (fun (i : β) ↦ x i a) t = Term.realize x t a

Tactic:
induction t with
  | var => rfl
  | func _ _ t_ih => simp only [Term.realize, t_ih]; rfl

Premises used: FirstOrder.Language.Term.func, FirstOrder.Language.Term.var, FirstOrder.Language.Term.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 : ℕ
v : Fin n_1 → (a : α) → M a
⊢ (BoundedFormula.Realize (L := L) (M := Quotient ((↑u : Filter α).productSetoid M)) (l := n_1) BoundedFormula.falsum
      (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} (L := L) (M := M a) (l := n_1) BoundedFormula.falsum (fun (i : β) ↦ x i a)
        fun (i : Fin n_1) ↦ v i a

Tactic:
simp only [BoundedFormula.Realize, eventually_const]

Premises used: FirstOrder.Language.BoundedFormula.Realize, Filter.eventually_const
-- 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 : ℕ
t₁ t₂ : Term.{u, v, u_3} L (β ⊕ Fin n_1)
v : Fin n_1 → (a : α) → M a
⊢ ∀ (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
-- 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 : ℕ
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
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₂)
⊢ ((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

Tactic:
simp only [BoundedFormula.Realize, h2]

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 : ℕ
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
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₂)
⊢ 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:
erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm,
      term_realize_cast, term_realize_cast]

Premises used: Quotient.mk', Sum.comp_elim, FirstOrder.Language.Ultraproduct.term_realize_cast, Eq.symm
-- 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 : ℕ
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))
      (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:
Quotient.eq''

Premises used: Quotient.eq'', 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 : ℕ
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))
      (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:
exact Quotient.eq''

Premises used: Quotient.eq''
-- 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
⊢ ∀ (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
-- 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
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)
⊢ ((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

Tactic:
simp only [BoundedFormula.Realize, h2]

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 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
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)
⊢ (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:
erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm]

Premises used: Quotient.mk', Sum.comp_elim, Eq.symm
-- 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
h : ∀ (i : Fin l), Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts i)
| RelMap (M := Quotient ((↑u : Filter α).productSetoid M)) R fun (i : Fin l) ↦
    Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts i)

Tactic:
enter [2, i]
-- 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
i : Fin l
h : Quotient.mk' fun (a : α) ↦ Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) (ts i)
| Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts i)

Tactic:
erw [term_realize_cast]

Premises used: FirstOrder.Language.Ultraproduct.term_realize_cast
-- 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
h : ∀ (i : Fin l), Quotient.mk' fun (a : α) ↦ Term.realize (fun (i : β ⊕ Fin n_1) ↦ Sum.elim x v i a) (ts i)
| RelMap (M := Quotient ((↑u : Filter α).productSetoid M)) R fun (i : Fin l) ↦
    Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts i)

Tactic:
enter [2, i]; erw [term_realize_cast]

Premises used: FirstOrder.Language.Ultraproduct.term_realize_cast
-- 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
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)
⊢ (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:
conv_lhs => enter [2, i]; erw [term_realize_cast]

Premises used: FirstOrder.Language.Ultraproduct.term_realize_cast