-- 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 : ℕ
φ : L.BoundedFormula β n
x : β → (a : α) → M a
v : Fin n → (a : α) → M a
falsum :
  ∀ {n : ℕ} (v : Fin n → (a : α) → M a),
    (BoundedFormula.Realize (L := L) (M := Quotient ((↑u : Filter α).productSetoid M)) (l := n) BoundedFormula.falsum
        (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n) ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (L := L) (M := M a) (l := n) BoundedFormula.falsum (fun (i : β) ↦ x i a)
          fun (i : Fin n) ↦ v i a
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u_3} L (β ⊕ Fin n)) (v : Fin n → (a : α) → M a),
    ((BoundedFormula.equal t₁ t₂).Realize (M := Quotient ((↑u : Filter α).productSetoid M))
        (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n) ↦ 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) ↦ v i a
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u_3} L (β ⊕ Fin n)) (v : Fin n → (a : α) → M a),
    ((BoundedFormula.rel R ts).Realize (M := Quotient ((↑u : Filter α).productSetoid M))
        (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n) ↦ 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) ↦ v i a
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula β n)
    (ih :
      ∀ (v : Fin n → (a : α) → M a),
        (f₁.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
            fun (i : Fin n) ↦ 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) ↦ v i a)
    (ih' :
      ∀ (v : Fin n → (a : α) → M a),
        (f₂.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
            fun (i : Fin n) ↦ 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) ↦ v i a)
    (v : Fin n → (a : α) → M a),
    ((f₁ ⟹ f₂).Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        fun (i : Fin n) ↦ 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) ↦ v i a
all :
  ∀ {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),
    ((∀' φ).Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        fun (i : Fin k) ↦ 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) ↦ v i a
⊢ (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n) ↦
      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 n) ↦ v i a

Tactic:
induction φ with
  | falsum => simp only [BoundedFormula.Realize, eventually_const]
  | equal =>
    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
    simp only [BoundedFormula.Realize, h2]
    erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm,
      term_realize_cast, term_realize_cast]
    exact Quotient.eq''
  | rel =>
    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
    simp only [BoundedFormula.Realize, h2]
    erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm]
    conv_lhs => enter [2, i]; erw [term_realize_cast]
    apply relMap_quotient_mk'
  | imp _ _ ih ih' =>
    simp only [BoundedFormula.Realize, ih v, ih' v]
    rw [Ultrafilter.eventually_imp]
  | @all k φ ih =>
    simp only [BoundedFormula.Realize]
    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)))
    · exact Quotient.forall
    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]
    simp only [← Fin.comp_snoc]
    simp only [Function.comp_def, ih, h']
    refine ⟨fun h => ?_, fun h m => ?_⟩
    · contrapose! h
      refine
        ⟨fun a : α =>
          Classical.epsilon fun m : M a =>
            ¬φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) m),
          ?_⟩
      exact Filter.mem_of_superset h fun a ha => Classical.epsilon_spec ha
    · rw [Filter.eventually_iff] at *
      exact Filter.mem_of_superset h fun a ha => ha (m a)

Premises used: Fin.comp_snoc, FirstOrder.Language.relMap_quotient_mk', Quotient.forall, Filter.eventually_iff, Quotient.eq'', FirstOrder.Language.BoundedFormula.Realize, Function.comp_def, Quotient.mk', Filter.eventually_const, Iff.trans, Sum.comp_elim, FirstOrder.Language.Ultraproduct.term_realize_cast, Eq.symm, Ultrafilter.eventually_imp