apply equiv_of_equal_coeffs
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
⊢ sum s₁ = sum s₂
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
⊢ ∀ (x : X), coords s₁ x = coords s₂ x