Theorem: FreeCMonoid.mul_comm (Algdata/Algebra/Monoid/FreeCMonoid.lean)

State before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ x * y = y * x
Tactic:
dsimp [HMul.hMul, Mul.mul]
State after:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) x.vars y.vars } =
    { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars }

State before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) x.vars y.vars } =
    { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars }
Tactic:
apply FreeCMonoid.eq
State after:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) x.vars y.vars }.vars =
    { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars }.vars

State before:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) x.vars y.vars }.vars =
    { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars }.vars
Tactic:
dsimp
State after:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ KVChain.mergeWith (fun x a b => some (valAdd a b)) x.vars y.vars =
    KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars

State before:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ KVChain.mergeWith (fun x a b => some (valAdd a b)) x.vars y.vars =
    KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars
Tactic:
rw [KVChain.mergeWith_flip]
State after:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ KVChain.mergeWith (fun a => flip fun a b => some (valAdd a b)) y.vars x.vars =
    KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars

State before:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ KVChain.mergeWith (fun a => flip fun a b => some (valAdd a b)) y.vars x.vars =
    KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars
Tactic:
dsimp [flip]
State after:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ KVChain.mergeWith (fun a b a => some (valAdd a b)) y.vars x.vars =
    KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars

State before:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ KVChain.mergeWith (fun a b a => some (valAdd a b)) y.vars x.vars =
    KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars
Tactic:
apply KVChain.mergeWith_congrFun
State after:
case a.hfg
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ α → ∀ (b₁ b₂ : valType), some (valAdd b₂ b₁) = some (valAdd b₁ b₂)

State before:
case a.hfg
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ α → ∀ (b₁ b₂ : valType), some (valAdd b₂ b₁) = some (valAdd b₁ b₂)
Tactic:
intros
State after:
case a.hfg
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
a✝ : α
b₁✝ b₂✝ : valType
⊢ some (valAdd b₂✝ b₁✝) = some (valAdd b₁✝ b₂✝)

State before:
case a.hfg
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
a✝ : α
b₁✝ b₂✝ : valType
⊢ some (valAdd b₂✝ b₁✝) = some (valAdd b₁✝ b₂✝)
Tactic:
rw [valAdd_comm]
State after:
no goals