-- Mathlib/ModelTheory/Semantics.lean
theorem realize_liftAt {n n' m : ℕ} {φ : L.BoundedFormula α n} {v : α → M} {xs : Fin (n + n') → M}
    (hmn : m + n' ≤ n + 1) :
    (φ.liftAt n' m).Realize v xs ↔
      φ.Realize v (xs ∘ fun i => if ↑i < m then Fin.castAdd n' i else Fin.addNat i n')

Proof state:
case all.refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m + n' ≤ k + 1 + 1 →
      ((mapTermRel (fun x t => Term.liftAt n' m t) (fun x => id) (fun x => castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
⊢ ((snoc xs x ∘ Fin.cast h) ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n') (last k) =
    snoc (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n') x (last k)

Tactic:
simp only [Function.comp_apply, val_last, snoc_last]

Result:
case all.refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m + n' ≤ k + 1 + 1 →
      ((mapTermRel (fun x t => Term.liftAt n' m t) (fun x => id) (fun x => castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
⊢ snoc xs x (Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) = x

Proof state:
case all.refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m + n' ≤ k + 1 + 1 →
      ((mapTermRel (fun x t => Term.liftAt n' m t) (fun x => id) (fun x => castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
⊢ snoc xs x (Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) = x

Tactic:
refine (congr rfl (Fin.ext ?_)).trans (snoc_last _ _)

Result:
case all.refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m + n' ≤ k + 1 + 1 →
      ((mapTermRel (fun x t => Term.liftAt n' m t) (fun x => id) (fun x => castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
⊢ ↑(Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) = ↑(last (k + n'))

Proof state:
case falsum
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
n✝ : ℕ
xs : Fin (n✝ + n') → M
hmn : m + n' ≤ n✝ + 1
⊢ (mapTermRel (fun x t => Term.liftAt n' m t) (fun x => id) (fun x => castLE ⋯) falsum).Realize v xs ↔
    falsum.Realize v (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n')

Tactic:
simp [mapTermRel, Realize]

Result:
no goals

Proof state:
case all.refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m + n' ≤ k + 1 + 1 →
      ((mapTermRel (fun x t => Term.liftAt n' m t) (fun x => id) (fun x => castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
⊢ ↑(Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) = ↑(last (k + n'))

Tactic:
split_ifs <;> dsimp

Result:
case pos
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m + n' ≤ k + 1 + 1 →
      ((mapTermRel (fun x t => Term.liftAt n' m t) (fun x => id) (fun x => castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
h✝ : k < m
⊢ k = k + n'