-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
ft : (n : ℕ) → Term.{u, v, u'} L (α ⊕ Fin n) → Term.{u_4, u_5, v'} L' (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
ft' : (n : ℕ) → Term.{u_4, u_5, v'} L' (β ⊕ Fin n) → Term.{u_2, u_3, u_1} L'' (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n : ℕ
φ : L.BoundedFormula α n
falsum :
  ∀ {n : ℕ},
    Eq (α := L''.BoundedFormula γ n)
      (mapTermRel ft' fr' fun (x : ℕ) ↦ id (n := n) (mapTermRel ft fr fun (x : ℕ) ↦ id (n := n) BoundedFormula.falsum) :
        L''.BoundedFormula γ n)
      (mapTermRel.{u, v, u', u_1, u_2, u_3} (L := L) (L' := L'') (α := α) (β := γ) (g := fun (x : ℕ) ↦ x)
          (fun (x : ℕ) ↦ ft' x ∘ ft x) (fun (x : ℕ) ↦ fr' x ∘ fr x) fun (x : ℕ) ↦ id (n := n) BoundedFormula.falsum :
        L''.BoundedFormula γ n)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) (BoundedFormula.equal t₁ t₂)) =
      mapTermRel.{u, v, u', u_1, u_2, u_3} (L' := L'') (β := γ) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ ft' x ∘ ft x)
        (fun (x : ℕ) ↦ fr' x ∘ fr x) (fun (x : ℕ) ↦ id) (BoundedFormula.equal t₁ t₂)
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) (BoundedFormula.rel R ts)) =
      mapTermRel.{u, v, u', u_1, u_2, u_3} (L' := L'') (β := γ) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ ft' x ∘ ft x)
        (fun (x : ℕ) ↦ fr' x ∘ fr x) (fun (x : ℕ) ↦ id) (BoundedFormula.rel R ts)
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 :
      mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) f₁) =
        mapTermRel.{u, v, u', u_1, u_2, u_3} (L' := L'') (β := γ) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ ft' x ∘ ft x)
          (fun (x : ℕ) ↦ fr' x ∘ fr x) (fun (x : ℕ) ↦ id) f₁)
    (ih2 :
      mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) f₂) =
        mapTermRel.{u, v, u', u_1, u_2, u_3} (L' := L'') (β := γ) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ ft' x ∘ ft x)
          (fun (x : ℕ) ↦ fr' x ∘ fr x) (fun (x : ℕ) ↦ id) f₂),
    mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) (f₁.imp f₂)) =
      mapTermRel.{u, v, u', u_1, u_2, u_3} (L' := L'') (β := γ) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ ft' x ∘ ft x)
        (fun (x : ℕ) ↦ fr' x ∘ fr x) (fun (x : ℕ) ↦ id) (f₁.imp f₂)
⊢ mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) φ) =
    mapTermRel.{u, v, u', u_1, u_2, u_3} (L' := L'') (β := γ) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ ft' x ∘ ft x)
      (fun (x : ℕ) ↦ fr' x ∘ fr x) (fun (x : ℕ) ↦ id) φ
have all : ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
  (ih3 :
    mapTermRel.{u_4, u_5, v', u_1, u_2, u_3} (α := β) ft' fr' (fun (x : ℕ) ↦ id)
        (mapTermRel.{u, v, u', v', u_4, u_5} (α := α) ft fr (fun (x : ℕ) ↦ id) f) =
      mapTermRel.{u, v, u', u_1, u_2, u_3} (L := L) (α := α) (fun (x : ℕ) ↦ ft' x ∘ ft x) (fun (x : ℕ) ↦ fr' x ∘ fr x)
        (fun (x : ℕ) ↦ id) f),
  mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) f.all) =
    mapTermRel.{u, v, u', u_1, u_2, u_3} (L' := L'') (β := γ) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ ft' x ∘ ft x)
      (fun (x : ℕ) ↦ fr' x ∘ fr x) (fun (x : ℕ) ↦ id) f.all
Tactic: induction φ with
  | falsum => rfl
  | equal => simp [mapTermRel]
  | rel => simp [mapTermRel]
  | imp _ _ ih1 ih2 => simp [mapTermRel, ih1, ih2]
  | all _ ih3 => simp [mapTermRel, ih3]
Cleared hypotheses: φ