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

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

State before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars : KVChain LT.lt fun x => valType
⊢ { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xvars KVChain.nil } = { vars := xvars }
Tactic:
rw [KVChain.mergeWith_nil]
State after:
no goals