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

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
r : R
s : FormalSum R X
x₀ : X
⊢ r * coords s x₀ = coords (scmul r s) x₀
Tactic:
induction s with
| nil =>
  simp [coords]
| cons h t ih =>
  simp [scmul, coords, monom_coords_mul, left_distrib, ih]
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
r : R
x₀ : X
⊢ r * coords [] x₀ = coords (scmul r []) x₀
Tactic:
simp [coords]
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
r : R
x₀ : X
h : R × X
t : List (R × X)
ih : r * coords t x₀ = coords (scmul r t) x₀
⊢ r * coords (h :: t) x₀ = coords (scmul r (h :: t)) x₀
Tactic:
simp [scmul, coords, monom_coords_mul, left_distrib, ih]
State after:
no goals