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

State before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars : KVChain LT.lt fun x => valType
⊢ 1 * { vars := xvars } = { 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)) KVChain.nil xvars } = { 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)) KVChain.nil xvars } = { vars := xvars }
Tactic:
rw [KVChain.nil_mergeWith]
State after:
no goals