Theorem: LO.FirstOrder.Rew.operator (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₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ ω (o.operator v) = o.operator fun i => ω (v i)
Tactic:
simp [Semiterm.Operator.operator, ←comp_app]
State after:
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₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ (ω.comp ((substs v).comp emb)) o.term = ((substs fun i => ω (v i)).comp emb) o.term

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₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ (ω.comp ((substs v).comp emb)) o.term = ((substs fun i => ω (v i)).comp emb) o.term
Tactic:
congr 1
State after:
case e_a
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₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ ω.comp ((substs v).comp emb) = (substs fun i => ω (v i)).comp emb

State before:
case e_a
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₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ ω.comp ((substs v).comp emb) = (substs fun i => ω (v i)).comp emb
Tactic:
ext <;> simp [comp_app]
State after:
case e_a.hf
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₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
x✝ : Empty
⊢ ω ((substs v) (emb &x✝)) = (substs fun i => ω (v i)) (emb &x✝)

State before:
case e_a.hf
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₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
x✝ : Empty
⊢ ω ((substs v) (emb &x✝)) = (substs fun i => ω (v i)) (emb &x✝)
Tactic:
try contradiction
State after:
no goals

State before:
case e_a.hf
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₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
x✝ : Empty
⊢ ω ((substs v) (emb &x✝)) = (substs fun i => ω (v i)) (emb &x✝)
Tactic:
contradiction
State after:
no goals