Theorem: LO.FirstOrder.Rew.hom_finitary3 (Logic/FirstOrder/Basic/Operator.lean)

State before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
o : Semiformula.Operator L 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
⊢ ω.hom (o.operator ![t₁, t₂, t₃]) = o.operator ![ω t₁, ω t₂, ω t₃]
Tactic:
simp [ω.hom_operator']
State after:
no goals