Theorem: FormalSum.action (UnitConjecture/FreeModule.lean)

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a b : R
s : FormalSum R X
⊢ scmul a (scmul b s) = scmul (a * b) s
Tactic:
induction s with
| nil =>
  simp [scmul]
| cons h t ih =>
  simp [scmul, ih, mul_assoc]
State after:
no goals

State before:
case nil
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a b : R
⊢ scmul a (scmul b []) = scmul (a * b) []
Tactic:
simp [scmul]
State after:
no goals

State before:
case cons
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a (scmul b t) = scmul (a * b) t
⊢ scmul a (scmul b (h :: t)) = scmul (a * b) (h :: t)
Tactic:
simp [scmul, ih, mul_assoc]
State after:
no goals