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

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
s₁ s₂ : FormalSum R X
h : ElementaryMove R X s₁ s₂
⊢ coords s₁ x₀ = coords s₂ x₀
Tactic:
induction h with
| zeroCoeff tail x a hyp =>
  simp [coords, hyp, monom_coords_at_zero]
| addCoeffs a b x tail =>
  simp [coords, monom_coords_at_zero, ← add_assoc, monom_coords_hom]
| cons a x s₁ s₂ _ step =>
  simp [coords, step]
| swap a₁ a₂ x₁ x₂ tail =>
  simp [coords, ← add_assoc, add_comm]
State after:
no goals

State before:
case zeroCoeff
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
s₁ s₂ tail : FormalSum R X
x : X
a : R
hyp : a = 0
⊢ coords ((a, x) :: tail) x₀ = coords tail x₀
Tactic:
simp [coords, hyp, monom_coords_at_zero]
State after:
no goals

State before:
case addCoeffs
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
s₁ s₂ : FormalSum R X
a b : R
x : X
tail : FormalSum R X
⊢ coords ((a, x) :: (b, x) :: tail) x₀ = coords ((a + b, x) :: tail) x₀
Tactic:
simp [coords, monom_coords_at_zero, ← add_assoc, monom_coords_hom]
State after:
no goals

State before:
case cons
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
s₁✝ s₂✝ : FormalSum R X
a : R
x : X
s₁ s₂ : FormalSum R X
a✝ : ElementaryMove R X s₁ s₂
step : coords s₁ x₀ = coords s₂ x₀
⊢ coords ((a, x) :: s₁) x₀ = coords ((a, x) :: s₂) x₀
Tactic:
simp [coords, step]
State after:
no goals

State before:
case swap
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
s₁ s₂ : FormalSum R X
a₁ a₂ : R
x₁ x₂ : X
tail : FormalSum R X
⊢ coords ((a₁, x₁) :: (a₂, x₂) :: tail) x₀ = coords ((a₂, x₂) :: (a₁, x₁) :: tail) x₀
Tactic:
simp [coords, ← add_assoc, add_comm]
State after:
no goals