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

State before:
α : Type u
inst✝ : LT α
x y : FreeCMonoid α
xvar yvar : KVChain LT.lt fun x => valType
h : { vars := xvar }.vars = { vars := yvar }.vars
⊢ { vars := xvar } = { vars := yvar }
Tactic:
simp at h
State after:
α : Type u
inst✝ : LT α
x y : FreeCMonoid α
xvar yvar : KVChain LT.lt fun x => valType
h : xvar = yvar
⊢ { vars := xvar } = { vars := yvar }

State before:
α : Type u
inst✝ : LT α
x y : FreeCMonoid α
xvar yvar : KVChain LT.lt fun x => valType
h : xvar = yvar
⊢ { vars := xvar } = { vars := yvar }
Tactic:
cases h
State after:
case refl
α : Type u
inst✝ : LT α
x y : FreeCMonoid α
xvar : KVChain LT.lt fun x => valType
⊢ { vars := xvar } = { vars := xvar }

State before:
case refl
α : Type u
inst✝ : LT α
x y : FreeCMonoid α
xvar : KVChain LT.lt fun x => valType
⊢ { vars := xvar } = { vars := xvar }
Tactic:
rfl
State after:
no goals