-- 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:
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
⊢ (liftAt n' m φ).Realize v xs ↔ φ.Realize v (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n')

Tactic:
rw [liftAt]

Result:
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
⊢ (mapTermRel (fun x t => Term.liftAt n' m t) (fun x => id) (fun x => castLE ⋯) φ).Realize v xs ↔
    φ.Realize v (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n')

Proof state:
case all.refine_2
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
i : Fin k
⊢ snoc xs x (Fin.cast h (if ↑i.castSucc < m then castAdd n' i.castSucc else i.castSucc.addNat n')) =
    xs (if ↑i < m then castAdd n' i else i.addNat n')

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

Result:
case all.refine_2
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
i : Fin k
⊢ ↑(Fin.cast h (if ↑i.castSucc < m then castAdd n' i.castSucc else i.castSucc.addNat n')) =
    ↑(if ↑i < m then castAdd n' i else i.addNat n').castSucc

Proof state:
case all
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
⊢ (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')

Tactic:
simp only [mapTermRel, Realize, realize_castLE_of_eq h, ih3 (hmn.trans k.succ.le_succ)]

Result:
case all
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), f✝.Realize v ((snoc xs x ∘ Fin.cast h) ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n')) ↔
    ∀ (x : M), f✝.Realize v (snoc (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n') x)

Proof state:
case all.refine_2
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
i : Fin k
⊢ ↑(Fin.cast h (if ↑i.castSucc < m then castAdd n' i.castSucc else i.castSucc.addNat n')) =
    ↑(if ↑i < m then castAdd n' i else i.addNat n').castSucc

Tactic:
simp only [coe_castSucc, coe_cast]

Result:
case all.refine_2
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
i : Fin k
⊢ ↑(if ↑i < m then castAdd n' i.castSucc else i.castSucc.addNat n') = ↑(if ↑i < m then castAdd n' i else i.addNat n')

Proof state:
case rel
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin 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 ⋯) (rel R✝ ts✝)).Realize v xs ↔
    (rel R✝ ts✝).Realize v (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n')

Tactic:
simp [mapTermRel, Realize, realize_rel, realize_liftAt, Sum.elim_comp_map]

Result:
no goals

Proof state:
case all
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
⊢ (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')

Tactic:
have h : k + 1 + n' = k + n' + 1 := by rw [add_assoc, add_comm 1 n', ← add_assoc]

Result:
case all
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
⊢ (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')