case h
L : Language
L' : Language
M : Type w
N : Type ?u.28526
P : Type ?u.28529
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28557
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
t : Term L α
⊢ onTerm (comp φ ψ) t = (onTerm φ ∘ onTerm ψ) t
L : Language
L' : Language
M : Type w
N : Type ?u.28526
P : Type ?u.28529
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28557
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
⊢ onTerm (comp φ ψ) = onTerm φ ∘ onTerm ψ
ext t
case h.var
L : Language
L' : Language
M : Type w
N : Type ?u.28526
P : Type ?u.28529
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28557
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
_a✝ : α
⊢ onTerm (comp φ ψ) (var _a✝) = (onTerm φ ∘ onTerm ψ) (var _a✝)

case h.func
L : Language
L' : Language
M : Type w
N : Type ?u.28526
P : Type ?u.28529
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28557
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), onTerm (comp φ ψ) (_ts✝ a) = (onTerm φ ∘ onTerm ψ) (_ts✝ a)
⊢ onTerm (comp φ ψ) (func _f✝ _ts✝) = (onTerm φ ∘ onTerm ψ) (func _f✝ _ts✝)
case h
L : Language
L' : Language
M : Type w
N : Type ?u.28526
P : Type ?u.28529
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28557
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
t : Term L α
⊢ onTerm (comp φ ψ) t = (onTerm φ ∘ onTerm ψ) t
induction' t with _ _ _ _ ih
no goals
case h.var
L : Language
L' : Language
M : Type w
N : Type ?u.28526
P : Type ?u.28529
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28557
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
_a✝ : α
⊢ onTerm (comp φ ψ) (var _a✝) = (onTerm φ ∘ onTerm ψ) (var _a✝)
rfl
case h.func
L : Language
L' : Language
M : Type w
N : Type ?u.28526
P : Type ?u.28529
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28557
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), onTerm (comp φ ψ) (_ts✝ a) = (onTerm φ ∘ onTerm ψ) (_ts✝ a)
⊢ (func (onFunction (comp φ ψ) _f✝) fun i => (onTerm φ ∘ onTerm ψ) (_ts✝ i)) = (onTerm φ ∘ onTerm ψ) (func _f✝ _ts✝)
case h.func
L : Language
L' : Language
M : Type w
N : Type ?u.28526
P : Type ?u.28529
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28557
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), onTerm (comp φ ψ) (_ts✝ a) = (onTerm φ ∘ onTerm ψ) (_ts✝ a)
⊢ onTerm (comp φ ψ) (func _f✝ _ts✝) = (onTerm φ ∘ onTerm ψ) (func _f✝ _ts✝)
simp_rw [onTerm, ih]
no goals
case h.func
L : Language
L' : Language
M : Type w
N : Type ?u.28526
P : Type ?u.28529
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.28557
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), onTerm (comp φ ψ) (_ts✝ a) = (onTerm φ ∘ onTerm ψ) (_ts✝ a)
⊢ (func (onFunction (comp φ ψ) _f✝) fun i => (onTerm φ ∘ onTerm ψ) (_ts✝ i)) = (onTerm φ ∘ onTerm ψ) (func _f✝ _ts✝)
rfl