-- 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 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)
⊢ ∃ m, ¬∀ᶠ (a : α) in ↑u, φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) (m a))

Tactic:
refine
  ⟨fun a : α =>
    Classical.epsilon fun m : M a =>
      ¬φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) m),
    ?_⟩

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)
⊢ ¬∀ᶠ (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))

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
⊢ ((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:
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 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

Proof state:
α : 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 : ℕ
φ : L.BoundedFormula β n
x : β → (a : α) → M a
v : Fin n → (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

Tactic:
letI := (u : Filter α).productSetoid M

Result:
α : 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 : ℕ
φ : L.BoundedFormula β n
x : β → (a : α) → M a
v : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := (↑u).productSetoid M
⊢ (φ.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

Proof state:
case imp
α : 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✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula β n✝
ih :
  ∀ (v : Fin n✝ → (a : α) → M a),
    (f₁✝.Realize (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, f₁✝.Realize (fun i => x i a) fun i => v i a
ih' :
  ∀ (v : Fin n✝ → (a : α) → M a),
    (f₂✝.Realize (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, f₂✝.Realize (fun i => x i a) fun i => v i a
v : Fin n✝ → (a : α) → M a
⊢ ((∀ᶠ (a : α) in ↑u, f₁✝.Realize (fun i => x i a) fun i => v i a) →
      ∀ᶠ (a : α) in ↑u, f₂✝.Realize (fun i => x i a) fun i => v i a) ↔
    ∀ᶠ (a : α) in ↑u, (f₁✝.Realize (fun i => x i a) fun i => v i a) → f₂✝.Realize (fun i => x i a) fun i => v i a

Tactic:
rw [Ultrafilter.eventually_imp]

Result:
no goals

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
⊢ ((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:
simp only [BoundedFormula.Realize, h2, 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
⊢ 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₂✝