-- Mathlib/ModelTheory/Syntax.lean
theorem castLE_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) (φ : L.BoundedFormula α k) :
    (φ.castLE km).castLE mn = φ.castLE (km.trans mn)

Proof state:
case all
L : Language
α : Type u'
k n✝¹ : ℕ
f✝ : L.BoundedFormula α (n✝¹ + 1)
ih3 : ∀ {m n : ℕ} (km : n✝¹ + 1 ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝) = castLE ⋯ f✝
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ f✝.all) = castLE ⋯ f✝.all

Tactic:
simp only [castLE, ih3]

Result:
no goals

Proof state:
case equal
L : Language
α : Type u'
k n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km (equal t₁✝ t₂✝)) = castLE ⋯ (equal t₁✝ t₂✝)

Tactic:
simp

Result:
no goals

Proof state:
L : Language
α : Type u'
k m n : ℕ
km : k ≤ m
mn : m ≤ n
φ : L.BoundedFormula α k
⊢ castLE mn (castLE km φ) = castLE ⋯ φ

Tactic:
revert m n

Result:
L : Language
α : Type u'
k : ℕ
φ : L.BoundedFormula α k
⊢ ∀ {m n : ℕ} (km : k ≤ m) (mn : m ≤ n), castLE mn (castLE km φ) = castLE ⋯ φ

Proof state:
case rel
L : Language
α : Type u'
k n✝¹ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝¹)
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ (rel R✝ ts✝)) = castLE ⋯ (rel R✝ ts✝)

Tactic:
simp only [castLE, eq_self_iff_true, heq_iff_eq]

Result:
case rel
L : Language
α : Type u'
k n✝¹ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝¹)
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ rel R✝ (Term.relabel (Sum.map id (Fin.castLE mn✝)) ∘ Term.relabel (Sum.map id (Fin.castLE km✝)) ∘ ts✝) =
    rel R✝ (Term.relabel (Sum.map id (Fin.castLE ⋯)) ∘ ts✝)

Proof state:
case all
L : Language
α : Type u'
k n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {m n : ℕ} (km : n✝ + 1 ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝) = castLE ⋯ f✝
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝.all) = castLE ⋯ f✝.all

Tactic:
intros

Result:
case all
L : Language
α : Type u'
k n✝¹ : ℕ
f✝ : L.BoundedFormula α (n✝¹ + 1)
ih3 : ∀ {m n : ℕ} (km : n✝¹ + 1 ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝) = castLE ⋯ f✝
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ f✝.all) = castLE ⋯ f✝.all

Proof state:
case rel
L : Language
α : Type u'
k n✝¹ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝¹)
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ rel R✝ (Term.relabel (Sum.map id (Fin.castLE mn✝) ∘ Sum.map id (Fin.castLE km✝)) ∘ ts✝) =
    rel R✝ (Term.relabel (Sum.map id (Fin.castLE ⋯)) ∘ ts✝)

Tactic:
simp

Result:
no goals

Proof state:
case falsum
L : Language
α : Type u'
k n✝¹ m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ falsum) = castLE ⋯ falsum

Tactic:
rfl

Result:
no goals

Proof state:
case rel
L : Language
α : Type u'
k n✝¹ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝¹)
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ rel R✝ (Term.relabel (Sum.map id (Fin.castLE mn✝)) ∘ Term.relabel (Sum.map id (Fin.castLE km✝)) ∘ ts✝) =
    rel R✝ (Term.relabel (Sum.map id (Fin.castLE ⋯)) ∘ ts✝)

Tactic:
rw [← Function.comp_assoc, Term.relabel_comp_relabel]

Result:
case rel
L : Language
α : Type u'
k n✝¹ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝¹)
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ rel R✝ (Term.relabel (Sum.map id (Fin.castLE mn✝) ∘ Sum.map id (Fin.castLE km✝)) ∘ ts✝) =
    rel R✝ (Term.relabel (Sum.map id (Fin.castLE ⋯)) ∘ ts✝)

Proof state:
case falsum
L : Language
α : Type u'
k n✝ : ℕ
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km falsum) = castLE ⋯ falsum

Tactic:
intros

Result:
case falsum
L : Language
α : Type u'
k n✝¹ m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ falsum) = castLE ⋯ falsum

Proof state:
case rel
L : Language
α : Type u'
k n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km (rel R✝ ts✝)) = castLE ⋯ (rel R✝ ts✝)

Tactic:
intros

Result:
case rel
L : Language
α : Type u'
k n✝¹ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝¹)
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ (rel R✝ ts✝)) = castLE ⋯ (rel R✝ ts✝)

Proof state:
case imp
L : Language
α : Type u'
k n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km f₁✝) = castLE ⋯ f₁✝
ih2 : ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km f₂✝) = castLE ⋯ f₂✝
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km (f₁✝.imp f₂✝)) = castLE ⋯ (f₁✝.imp f₂✝)

Tactic:
simp [ih1, ih2]

Result:
no goals

Proof state:
L : Language
α : Type u'
k : ℕ
φ : L.BoundedFormula α k
⊢ ∀ {m n : ℕ} (km : k ≤ m) (mn : m ≤ n), castLE mn (castLE km φ) = castLE ⋯ φ

Tactic:
induction φ with
| falsum => intros; rfl
| equal => simp
| rel =>
  intros
  simp only [castLE, eq_self_iff_true, heq_iff_eq]
  rw [← Function.comp_assoc, Term.relabel_comp_relabel]
  simp
| imp _ _ ih1 ih2 => simp [ih1, ih2]
| all _ ih3 => intros; simp only [castLE, ih3]

Result:
no goals