-- 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
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)

Tactic:
refine forall_congr' fun x => iff_eq_eq.mpr (congr rfl (funext (Fin.lastCases ?_ fun i => ?_)))

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) ∘ 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)

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) ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n') i.castSucc =
    snoc (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n') x i.castSucc

Proof state:
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'

Tactic:
omega

Result:
no goals

Proof state:
case imp
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {xs : Fin (n✝ + n') → M},
    m + n' ≤ 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'))
ih2 :
  ∀ {xs : Fin (n✝ + n') → M},
    m + n' ≤ 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'))
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 ⋯) (f₁✝ ⟹ f₂✝)).Realize v xs ↔
    (f₁✝ ⟹ f₂✝).Realize v (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n')

Tactic:
simp only [mapTermRel, Realize, ih1 hmn, ih2 hmn]

Result:
no goals

Proof state:
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
⊢ k + 1 + n' = k + n' + 1

Tactic:
rw [add_assoc, add_comm 1 n', ← add_assoc]

Result:
no goals

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) ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n') i.castSucc =
    snoc (xs ∘ fun i => if ↑i < m then castAdd n' i else i.addNat n') x i.castSucc

Tactic:
simp only [Function.comp_apply, Fin.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
⊢ 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')

Proof state:
case equal
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
n✝ : ℕ
t₁✝ t₂✝ : 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 ⋯) (equal t₁✝ t₂✝)).Realize v xs ↔
    (equal t₁✝ t₂✝).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.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')

Tactic:
split_ifs <;> simp

Result:
no goals