-- Mathlib/ModelTheory/Ultraproducts.lean
theorem boundedFormula_realize_cast {β : Type*} {n : ℕ} (φ : L.BoundedFormula β n)
    (x : β → ∀ a, M a) (v : Fin n → ∀ a, M a) :
    (φ.Realize (fun i : β => (x i : (u : Filter α).Product M))
        (fun i => (v i : (u : Filter α).Product M))) ↔
      ∀ᶠ a : α in u, φ.Realize (fun i : β => x i a) fun i => v i a

Proof state:
case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
this : Setoid ((a : α) → M a) := (↑u).productSetoid M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
⊢ ((BoundedFormula.equal t₁✝ t₂✝).Realize (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, (BoundedFormula.equal t₁✝ t₂✝).Realize (fun i => x i a) fun i => 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

Result:
case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
this : Setoid ((a : α) → M a) := (↑u).productSetoid M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
⊢ ((BoundedFormula.equal t₁✝ t₂✝).Realize (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, (BoundedFormula.equal t₁✝ t₂✝).Realize (fun i => x i a) fun i => v i a

Proof state:
case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
this : Setoid ((a : α) → M a) := (↑u).productSetoid M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
⊢ Term.realize (Sum.elim (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) t₁✝ =
      Term.realize (Sum.elim (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) t₂✝ ↔
    ∀ᶠ (a : α) in ↑u, Term.realize (fun i => Sum.elim x v i a) t₁✝ = Term.realize (fun i => 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]

Result:
case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
this : Setoid ((a : α) → M a) := (↑u).productSetoid M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
⊢ ((Quotient.mk' fun a => Term.realize (fun i => Sum.elim x v i a) t₁✝) =
      Quotient.mk' fun a => Term.realize (fun i => Sum.elim x v i a) t₂✝) ↔
    ∀ᶠ (a : α) in ↑u, Term.realize (fun i => Sum.elim x v i a) t₁✝ = Term.realize (fun i => Sum.elim x v i a) t₂✝

Proof state:
case rel
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
this : Setoid ((a : α) → M a) := (↑u).productSetoid M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
⊢ ((BoundedFormula.rel R✝ ts✝).Realize (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, (BoundedFormula.rel R✝ ts✝).Realize (fun i => x i a) fun i => v i a

Tactic:
simp only [BoundedFormula.Realize, h2]

Result:
case rel
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
this : Setoid ((a : α) → M a) := (↑u).productSetoid M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
⊢ (RelMap R✝ fun i => Term.realize (Sum.elim (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) (ts✝ i)) ↔
    ∀ᶠ (a : α) in ↑u, RelMap R✝ fun i => Term.realize (fun i => Sum.elim x v i a) (ts✝ i)

Proof state:
case rel
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
this : Setoid ((a : α) → M a) := (↑u).productSetoid M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
⊢ (RelMap R✝ fun i => Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)) ↔
    ∀ᶠ (a : α) in ↑u, RelMap R✝ fun i => Term.realize (fun i => Sum.elim x v i a) (ts✝ i)

Tactic:
conv_lhs => enter [2, i]; erw [term_realize_cast]

Result:
case rel
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
this : Setoid ((a : α) → M a) := (↑u).productSetoid M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
⊢ (RelMap R✝ fun i => Quotient.mk' fun a => Term.realize (fun i => Sum.elim x v i a) (ts✝ i)) ↔
    ∀ᶠ (a : α) in ↑u, RelMap R✝ fun i => Term.realize (fun i => Sum.elim x v i a) (ts✝ i)

Proof state:
case all.h₂.refine_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
this : Setoid ((a : α) → M a) := (↑u).productSetoid M
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i => Fin.snoc v m i a) = Fin.snoc (fun i => v i a) (m a)
h : ∀ᶠ (x_1 : α) in ↑u, ∃ x_2, ¬φ.Realize (fun i => x i x_1) (Fin.snoc (fun i => v i x_1) x_2)
⊢ ¬∀ᶠ (a : α) in ↑u,
      φ.Realize (fun i => x i a)
        (Fin.snoc (fun i => v i a)
          ((fun a => Classical.epsilon fun m => ¬φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) m)) a))

Tactic:
rw [← Ultrafilter.eventually_not]

Result:
case all.h₂.refine_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
this : Setoid ((a : α) → M a) := (↑u).productSetoid M
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i => Fin.snoc v m i a) = Fin.snoc (fun i => v i a) (m a)
h : ∀ᶠ (x_1 : α) in ↑u, ∃ x_2, ¬φ.Realize (fun i => x i x_1) (Fin.snoc (fun i => v i x_1) x_2)
⊢ ∀ᶠ (x_1 : α) in ↑u,
    ¬φ.Realize (fun i => x i x_1)
        (Fin.snoc (fun i => v i x_1)
          ((fun a => Classical.epsilon fun m => ¬φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) m)) x_1))