-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
φ : L.BoundedFormula α n
f : ↥φ.freeVarFinset → β
v : β → M
xs : Fin n → M
v' : α → M
hv' : ∀ (a : ↥φ.freeVarFinset), v (f a) = v' (↑a : α)
falsum :
  ∀ {n : ℕ} {f : ↥(freeVarFinset.{u, v, u'} (L := L) (n := n) BoundedFormula.falsum) → β} {xs : Fin n → M}
    (hv' : ∀ (a : ↥(freeVarFinset.{u, v, u'} (L := L) (n := n) BoundedFormula.falsum)), v (f a) = v' (↑a : α)),
    (restrictFreeVar BoundedFormula.falsum f).Realize v xs ↔ Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum v' xs
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {f : ↥(BoundedFormula.equal t₁ t₂).freeVarFinset → β}
    {xs : Fin n → M} (hv' : ∀ (a : ↥(BoundedFormula.equal t₁ t₂).freeVarFinset), v (f a) = v' (↑a : α)),
    ((BoundedFormula.equal t₁ t₂).restrictFreeVar f).Realize v xs ↔ (BoundedFormula.equal t₁ t₂).Realize v' xs
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n))
    {f : ↥(BoundedFormula.rel R ts).freeVarFinset → β} {xs : Fin n → M}
    (hv' : ∀ (a : ↥(BoundedFormula.rel R ts).freeVarFinset), v (f a) = v' (↑a : α)),
    ((BoundedFormula.rel R ts).restrictFreeVar f).Realize v xs ↔ (BoundedFormula.rel R ts).Realize v' xs
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 :
      ∀ {f : ↥f₁.freeVarFinset → β} {xs : Fin n → M} (hv' : ∀ (a : ↥f₁.freeVarFinset), v (f a) = v' (↑a : α)),
        (f₁.restrictFreeVar f).Realize v xs ↔ f₁.Realize v' xs)
    (ih2 :
      ∀ {f : ↥f₂.freeVarFinset → β} {xs : Fin n → M} (hv' : ∀ (a : ↥f₂.freeVarFinset), v (f a) = v' (↑a : α)),
        (f₂.restrictFreeVar f).Realize v xs ↔ f₂.Realize v' xs)
    {f : ↥(f₁ ⟹ f₂).freeVarFinset → β} {xs : Fin n → M} (hv' : ∀ (a : ↥(f₁ ⟹ f₂).freeVarFinset), v (f a) = v' (↑a : α)),
    ((f₁ ⟹ f₂).restrictFreeVar f).Realize v xs ↔ (f₁ ⟹ f₂).Realize v' xs
all :
  ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
    (ih3 :
      ∀ {f_1 : ↥f.freeVarFinset → β} {xs : Fin (n + 1) → M} (hv' : ∀ (a : ↥f.freeVarFinset), v (f_1 a) = v' (↑a : α)),
        (f.restrictFreeVar f_1).Realize v xs ↔ f.Realize v' xs)
    {f_1 : ↥(∀' f).freeVarFinset → β} {xs : Fin n → M} (hv' : ∀ (a : ↥(∀' f).freeVarFinset), v (f_1 a) = v' (↑a : α)),
    ((∀' f).restrictFreeVar f_1).Realize v xs ↔ (∀' f).Realize v' xs
⊢ (φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs

Tactic:
induction φ with
  | falsum => rfl
  | equal =>
    simp only [Realize, restrictFreeVar, freeVarFinset.eq_2]
    rw [realize_restrictVarLeft v' (by simp [hv']), realize_restrictVarLeft v' (by simp [hv'])]
    simp
  | rel =>
    simp only [Realize, freeVarFinset.eq_3, restrictFreeVar]
    congr!
    rw [realize_restrictVarLeft v' (by simp [hv'])]
    simp
  | imp _ _ ih1 ih2 =>
    simp only [Realize, restrictFreeVar, freeVarFinset.eq_4]
    rw [ih1, ih2] <;> simp [hv']
  | all _ ih3 =>
    simp only [restrictFreeVar, Realize]
    refine forall_congr' (fun _ => ?_)
    rw [ih3]; simp [hv']

Premises used: FirstOrder.Language.BoundedFormula.imp, FirstOrder.Language.BoundedFormula.freeVarFinset.eq_3, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.BoundedFormula.equal, FirstOrder.Language.BoundedFormula.restrictFreeVar, FirstOrder.Language.BoundedFormula.falsum, FirstOrder.Language.BoundedFormula.freeVarFinset.eq_4, forall_congr', FirstOrder.Language.BoundedFormula.freeVarFinset.eq_2, FirstOrder.Language.Term.realize_restrictVarLeft, FirstOrder.Language.BoundedFormula.all, FirstOrder.Language.BoundedFormula.rel