-- Mathlib/ModelTheory/Syntax.lean
theorem comp_onBoundedFormula {L'' : Language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :
    ((φ.comp ψ).onBoundedFormula : L.BoundedFormula α n → L''.BoundedFormula α n) =
      φ.onBoundedFormula ∘ ψ.onBoundedFormula

Proof state:
case h.rel
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ (φ.comp ψ).onBoundedFormula (rel R✝ ts✝) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (rel R✝ ts✝)

Tactic:
simp only [onBoundedFormula, comp_onRelation, comp_onTerm, Function.comp_apply]

Result:
case h.rel
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ (φ.onRelation (ψ.onRelation R✝)).boundedFormula ((φ.onTerm ∘ ψ.onTerm) ∘ ts✝) =
    φ.onBoundedFormula ((ψ.onRelation R✝).boundedFormula (ψ.onTerm ∘ ts✝))

Proof state:
case h.rel
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ (φ.onRelation (ψ.onRelation R✝)).boundedFormula ((φ.onTerm ∘ ψ.onTerm) ∘ ts✝) =
    φ.onBoundedFormula ((ψ.onRelation R✝).boundedFormula (ψ.onTerm ∘ ts✝))

Tactic:
rfl

Result:
no goals

Proof state:
case h.imp
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : (φ.comp ψ).onBoundedFormula f₁✝ = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f₁✝
ih2 : (φ.comp ψ).onBoundedFormula f₂✝ = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f₂✝
⊢ (φ.comp ψ).onBoundedFormula (f₁✝.imp f₂✝) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (f₁✝.imp f₂✝)

Tactic:
simp only [onBoundedFormula, Function.comp_apply, ih1, ih2, eq_self_iff_true, and_self_iff]

Result:
no goals

Proof state:
case h.falsum
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ : ℕ
⊢ (φ.comp ψ).onBoundedFormula falsum = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) falsum

Tactic:
rfl

Result:
no goals

Proof state:
case h.equal
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ (φ.comp ψ).onBoundedFormula (equal t₁✝ t₂✝) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (equal t₁✝ t₂✝)

Tactic:
simp [Term.bdEqual]

Result:
no goals

Proof state:
case h.all
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : (φ.comp ψ).onBoundedFormula f✝ = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f✝
⊢ (φ.comp ψ).onBoundedFormula f✝.all = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f✝.all

Tactic:
simp only [ih3, onBoundedFormula, Function.comp_apply]

Result:
no goals

Proof state:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
⊢ (φ.comp ψ).onBoundedFormula = φ.onBoundedFormula ∘ ψ.onBoundedFormula

Tactic:
ext f

Result:
case h
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
f : L.BoundedFormula α n
⊢ (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f

Proof state:
case h
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
f : L.BoundedFormula α n
⊢ (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f

Tactic:
induction f with
| falsum => rfl
| equal => simp [Term.bdEqual]
| rel => simp only [onBoundedFormula, comp_onRelation, comp_onTerm, Function.comp_apply]; rfl
| imp _ _ ih1 ih2 =>
  simp only [onBoundedFormula, Function.comp_apply, ih1, ih2, eq_self_iff_true, and_self_iff]
| all _ ih3 => simp only [ih3, onBoundedFormula, Function.comp_apply]

Result:
no goals