case h
α : Type u
β : Type v
inst✝ : Ring α
I : Ideal α
a b x x✝ : α
⊢ x✝ ∈ span {-x} ↔ x✝ ∈ span {x}
α : Type u
β : Type v
inst✝ : Ring α
I : Ideal α
a b x : α
⊢ span {-x} = span {x}
ext
case h
α : Type u
β : Type v
inst✝ : Ring α
I : Ideal α
a b x x✝ : α
⊢ (∃ a, a * -x = x✝) ↔ ∃ a, a * x = x✝
case h
α : Type u
β : Type v
inst✝ : Ring α
I : Ideal α
a b x x✝ : α
⊢ x✝ ∈ span {-x} ↔ x✝ ∈ span {x}
simp only [mem_span_singleton']
no goals
case h
α : Type u
β : Type v
inst✝ : Ring α
I : Ideal α
a b x x✝ : α
⊢ (∃ a, a * -x = x✝) ↔ ∃ a, a * x = x✝
exact ⟨fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_comm y x⟩, fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_neg y x⟩⟩