Theorem: LO.FirstOrder.Semiformula.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 → Semiterm.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.hom_comp_app]
State after:
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
⊢ ((Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term))).hom o.sentence =
    ((Rew.substs fun x => (w x).operator v).comp Rew.emb).hom o.sentence

State before:
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
⊢ ((Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term))).hom o.sentence =
    ((Rew.substs fun x => (w x).operator v).comp Rew.emb).hom o.sentence
Tactic:
congr 2
State after:
case e_a.e_ω
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.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 => (w x).operator v).comp Rew.emb

State before:
case e_a.e_ω
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.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 => (w x).operator v).comp Rew.emb
Tactic:
ext <;> simp [Rew.comp_app]
State after:
case e_a.e_ω.hb
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
x✝ : Fin k
⊢ (Rew.substs v) (Rew.emb (w x✝).term) = (w x✝).operator v

case e_a.e_ω.hf
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
x✝ : Empty
⊢ (Rew.substs v) (Rew.emb &x✝) = (Rew.substs fun x => (w x).operator v) (Rew.emb &x✝)

State before:
case e_a.e_ω.hb
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
x✝ : Fin k
⊢ (Rew.substs v) (Rew.emb (w x✝).term) = (w x✝).operator v
Tactic:
congr
State after:
no goals

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