Theorem: LO.FirstOrder.Semiterm.Operator.operator_comp (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Operator L l
v : Fin l → Semiterm L ξ n
⊢ (o.comp w).operator v = o.operator fun x => (w x).operator v
Tactic:
simp [operator, comp, ←Rew.comp_app]
State after:
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Operator L l
v : Fin l → Semiterm L ξ n
⊢ ((Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term))) o.term =
    ((Rew.substs fun x => ((Rew.substs v).comp Rew.emb) (w x).term).comp Rew.emb) o.term

State before:
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Operator L l
v : Fin l → Semiterm L ξ n
⊢ ((Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term))) o.term =
    ((Rew.substs fun x => ((Rew.substs v).comp Rew.emb) (w x).term).comp Rew.emb) o.term
Tactic:
congr 1
State after:
case e_a
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Operator L l
v : Fin l → Semiterm L ξ n
⊢ (Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term)) =
    (Rew.substs fun x => ((Rew.substs v).comp Rew.emb) (w x).term).comp Rew.emb

State before:
case e_a
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Operator L l
v : Fin l → Semiterm L ξ n
⊢ (Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term)) =
    (Rew.substs fun x => ((Rew.substs v).comp Rew.emb) (w x).term).comp Rew.emb
Tactic:
ext <;> simp [Rew.comp_app]
State after:
case e_a.hf
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Operator L l
v : Fin l → Semiterm L ξ n
x✝ : Empty
⊢ (Rew.substs v) (Rew.emb &x✝) = (Rew.substs fun x => (Rew.substs v) (Rew.emb (w x).term)) (Rew.emb &x✝)

State before:
case e_a.hf
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Operator L l
v : Fin l → Semiterm L ξ n
x✝ : Empty
⊢ (Rew.substs v) (Rew.emb &x✝) = (Rew.substs fun x => (Rew.substs v) (Rew.emb (w x).term)) (Rew.emb &x✝)
Tactic:
contradiction
State after:
no goals