Theorem: FormalSum.coords_well_defined (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
⊢ s₁ ≃ s₂ → coords s₁ x = coords s₂ x
Tactic:
intro hyp
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
⊢ coords s₁ x = coords s₂ x

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
⊢ coords s₁ x = coords s₂ x
Tactic:
have l : FreeModuleAux.coeff x (sum s₂) = s₂.coords x := by
  simp [coeff_factors, hyp]
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
l : FreeModuleAux.coeff x (sum s₂) = coords s₂ x
⊢ coords s₁ x = coords s₂ x

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
l : FreeModuleAux.coeff x (sum s₂) = coords s₂ x
⊢ coords s₁ x = coords s₂ x
Tactic:
rw [← l]
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
l : FreeModuleAux.coeff x (sum s₂) = coords s₂ x
⊢ coords s₁ x = FreeModuleAux.coeff x (sum s₂)

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
l : FreeModuleAux.coeff x (sum s₂) = coords s₂ x
⊢ coords s₁ x = FreeModuleAux.coeff x (sum s₂)
Tactic:
rw [← coeff_factors]
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
l : FreeModuleAux.coeff x (sum s₂) = coords s₂ x
⊢ FreeModuleAux.coeff x (sum s₁) = FreeModuleAux.coeff x (sum s₂)

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
l : FreeModuleAux.coeff x (sum s₂) = coords s₂ x
⊢ FreeModuleAux.coeff x (sum s₁) = FreeModuleAux.coeff x (sum s₂)
Tactic:
rw [hyp]
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
⊢ FreeModuleAux.coeff x (sum s₂) = coords s₂ x
Tactic:
simp [coeff_factors, hyp]
State after:
no goals