-- 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₂
α : 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)
⊢ (∀ (m : (a : α) → M a), φ.Realize (fun i => Quotient.mk' (x i)) (Fin.snoc (Quotient.mk' ∘ v) (Quotient.mk' m))) ↔
    ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) x_1)

Tactic:
simp only [← Fin.comp_snoc]

Result:
case all.h₂
α : 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)
⊢ (∀ (m : (a : α) → M a), φ.Realize (fun i => Quotient.mk' (x i)) (Quotient.mk' ∘ Fin.snoc v m)) ↔
    ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) x_1)

Proof state:
case 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
m : (a : α) → M a
a : α
⊢ Fin.snoc v m (Fin.last k) a = Fin.snoc (fun i => v i a) (m a) (Fin.last k)

Tactic:
simp only [Fin.snoc_last]

Result:
no goals

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
⊢ ((f₁✝ ⟹ f₂✝).Realize (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, (f₁✝ ⟹ f₂✝).Realize (fun i => x i a) fun i => v i a

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

Result:
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

Proof state:
case all.h₂
α : 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)
⊢ (∀ (m : (a : α) → M a), ∀ᶠ (a : α) in ↑u, φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) (m a))) ↔
    ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) x_1)

Tactic:
refine ⟨fun h => ?_, fun h 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 : ∀ (m : (a : α) → M a), ∀ᶠ (a : α) in ↑u, φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) (m a))
⊢ ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) x_1)

case all.h₂.refine_2
α : 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 : ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) x_1)
m : (a : α) → M a
⊢ ∀ᶠ (a : α) in ↑u, φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) (m a))