-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
falsum :
  ∀ {n : ℕ},
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (L := L) (α := α)
        (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t) (fun (x : ℕ) ↦ id)
        (fun (x : ℕ) ↦ castLE ⋯) BoundedFormula.falsum)
      (castLE ⋯ BoundedFormula.falsum)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (BoundedFormula.equal t₁ t₂))
      (castLE ⋯ (BoundedFormula.equal t₁ t₂))
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (BoundedFormula.rel R ts))
      (castLE ⋯ (BoundedFormula.rel R ts))
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 :
      Eq (α := L.BoundedFormula α (0 + n))
        (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f₁)
        (castLE ⋯ f₁))
    (ih2 :
      Eq (α := L.BoundedFormula α (0 + n))
        (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f₂)
        (castLE ⋯ f₂)),
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (f₁.imp f₂))
      (castLE ⋯ (f₁.imp f₂))
all :
  ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
    (ih3 :
      Eq (α := L.BoundedFormula α (0 + (n + 1)))
        (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        (castLE ⋯ f)),
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f.all)
      (castLE ⋯ f.all)
⊢ Eq (α := L.BoundedFormula α (0 + n))
    (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
      (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) φ)
    (castLE ⋯ φ)

Tactic:
induction φ with
  | falsum => rfl
  | equal => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]
  | rel => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]; rfl
  | imp _ _ ih1 ih2 => simp_all [mapTermRel]
  | all _ ih3 => simp_all [mapTermRel]

Premises used: FirstOrder.Language.BoundedFormula.imp, FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.equal, FirstOrder.Language.BoundedFormula.falsum, Fin.castLE_of_eq, Fin.natAdd_zero, FirstOrder.Language.BoundedFormula.all, FirstOrder.Language.BoundedFormula.rel