no goals
α : Type u
β : Type v
a b : α
inst✝² : CommSemiring α
I : Ideal α
inst✝¹ : CommRing β
inst✝ : IsDomain β
b₁ b₂ : β
h₁ : b₁ ≠ 0
h₂ : ¬IsUnit b₂
h : span {b₁} ≤ span {b₁ * b₂}
⊢ b₁ * b₂ ∣ b₁ * 1
rwa [mul_one, ← Ideal.span_singleton_le_span_singleton]