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

State before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
a b : valType
⊢ valAdd a b = valAdd b a
Tactic:
cases a
State after:
case mk
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
b : valType
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ valAdd { val := val✝, property := property✝ } b = valAdd b { val := val✝, property := property✝ }

State before:
case mk
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
b : valType
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ valAdd { val := val✝, property := property✝ } b = valAdd b { val := val✝, property := property✝ }
Tactic:
cases b
State after:
case mk.mk
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
val✝¹ : Nat
property✝¹ : Nat.lt 0 val✝¹
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ valAdd { val := val✝¹, property := property✝¹ } { val := val✝, property := property✝ } =
    valAdd { val := val✝, property := property✝ } { val := val✝¹, property := property✝¹ }

State before:
case mk.mk
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
val✝¹ : Nat
property✝¹ : Nat.lt 0 val✝¹
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ valAdd { val := val✝¹, property := property✝¹ } { val := val✝, property := property✝ } =
    valAdd { val := val✝, property := property✝ } { val := val✝¹, property := property✝¹ }
Tactic:
apply Subtype.eq
State after:
case mk.mk.a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
val✝¹ : Nat
property✝¹ : Nat.lt 0 val✝¹
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ (valAdd { val := val✝¹, property := property✝¹ } { val := val✝, property := property✝ }).val =
    (valAdd { val := val✝, property := property✝ } { val := val✝¹, property := property✝¹ }).val

State before:
case mk.mk.a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
val✝¹ : Nat
property✝¹ : Nat.lt 0 val✝¹
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ (valAdd { val := val✝¹, property := property✝¹ } { val := val✝, property := property✝ }).val =
    (valAdd { val := val✝, property := property✝ } { val := val✝¹, property := property✝¹ }).val
Tactic:
dsimp [valAdd]
State after:
case mk.mk.a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
val✝¹ : Nat
property✝¹ : Nat.lt 0 val✝¹
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ val✝¹ + val✝ = val✝ + val✝¹

State before:
case mk.mk.a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
val✝¹ : Nat
property✝¹ : Nat.lt 0 val✝¹
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ val✝¹ + val✝ = val✝ + val✝¹
Tactic:
rw [Nat.add_comm]
State after:
no goals