-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + n') → M
hmn : m + n' ≤ n + 1
falsum :
  ∀ {n : ℕ} {xs : Fin (n + n') → M} (hmn : m + n' ≤ n + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) BoundedFormula.falsum)
        v xs ↔
      Realize.{u, v, w, u'} (L := L) (l := n) BoundedFormula.falsum v
        (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin (n + n') → M} (hmn : m + n' ≤ n + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (BoundedFormula.equal t₁ t₂))
        v xs ↔
      (BoundedFormula.equal t₁ t₂).Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin (n + n') → M}
    (hmn : m + n' ≤ n + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (BoundedFormula.rel R ts))
        v xs ↔
      (BoundedFormula.rel R ts).Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 :
      ∀ {xs : Fin (n + n') → M} (hmn : m + n' ≤ n + 1),
        Realize.{u, v, w, u'} (L := L)
            (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
              (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f₁)
            v xs ↔
          f₁.Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n'))
    (ih2 :
      ∀ {xs : Fin (n + n') → M} (hmn : m + n' ≤ n + 1),
        Realize.{u, v, w, u'} (L := L)
            (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
              (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f₂)
            v xs ↔
          f₂.Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n'))
    {xs : Fin (n + n') → M} (hmn : m + n' ≤ n + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (f₁ ⟹ f₂))
        v xs ↔
      (f₁ ⟹ f₂).Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
all :
  ∀ {k : ℕ} (f : L.BoundedFormula α (k + 1))
    (ih3 :
      ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
        Realize.{u, v, w, u'} (L := L)
            (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
              (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
            v xs ↔
          f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n'))
    {xs : Fin (k + n') → M} (hmn : m + n' ≤ k + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (∀' f))
        v xs ↔
      (∀' f).Realize v (xs ∘ fun (i : Fin k) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
⊢ Realize.{u, v, w, u'} (L := L)
      (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) φ)
      v xs ↔
    φ.Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')

Tactic:
induction φ with
  | falsum => simp [mapTermRel, Realize]
  | equal => simp [mapTermRel, Realize, Sum.elim_comp_map]
  | rel => simp [mapTermRel, Realize, Sum.elim_comp_map]
  | imp _ _ ih1 ih2 => simp only [mapTermRel, Realize, ih1 hmn, ih2 hmn]
  | @all k _ ih3 =>
    have h : k + 1 + n' = k + n' + 1 := by rw [add_assoc, add_comm 1 n', ← add_assoc]
    simp only [mapTermRel, Realize, realize_castLE_of_eq h, ih3 (hmn.trans k.succ.le_succ)]
    refine forall_congr' fun x => iff_eq_eq.mpr (congr rfl (funext (Fin.lastCases ?_ fun i => ?_)))
    · simp only [Function.comp_apply, val_last, snoc_last]
      refine (congr rfl (Fin.ext ?_)).trans (snoc_last _ _)
      split_ifs <;> dsimp; lia
    · simp only [Function.comp_apply, Fin.snoc_castSucc]
      refine (congr rfl (Fin.ext ?_)).trans (snoc_castSucc _ _ _)
      simp only [val_castSucc, val_cast]
      split_ifs <;> simp

Premises used: FirstOrder.Language.BoundedFormula.imp, Eq.mpr, FirstOrder.Language.BoundedFormula.mapTermRel, Fin.snoc_castSucc, Fin.lastCases, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.BoundedFormula.equal, Fin.ext, FirstOrder.Language.BoundedFormula.falsum, funext, Sum.elim_comp_map, congr, forall_congr', iff_eq_eq, Fin.val_cast, Function.comp_apply, FirstOrder.Language.BoundedFormula.all, FirstOrder.Language.BoundedFormula.rel, Fin.val_last, Fin.snoc_last, Fin.val_castSucc, rfl, Eq.trans