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

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