apply eqg
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
⊢ z⁻¹ = g
case a
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
⊢ FreeModule.coordinates z⁻¹ α ≠ 0