case a
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a✝ b a : α
h2 : IsUnit a
x : α
⊢ ∃ a_1, a_1 * x = a * x

case a
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a✝ b a : α
h2 : IsUnit a
x : α
⊢ ∃ a_1, a_1 * (a * x) = x
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a✝ b a : α
h2 : IsUnit a
x : α
⊢ span {a * x} = span {x}
apply le_antisymm <;> rw [span_singleton_le_iff_mem, mem_span_singleton']
no goals
case a
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a✝ b a : α
h2 : IsUnit a
x : α
⊢ ∃ a_1, a_1 * x = a * x

case a
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a✝ b a : α
h2 : IsUnit a
x : α
⊢ ∃ a_1, a_1 * (a * x) = x
exacts [⟨a, rfl⟩, ⟨_, h2.unit.inv_mul_cancel_left x⟩]