case intro
α : Type u_1
β : Type ?u.348972
γ : Type ?u.348975
δ : Type ?u.348978
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
p r : α
u : αˣ
h : DvdNotUnit p (r * ↑u)
h' : r * ↑u ~ᵤ r
⊢ DvdNotUnit p r
α : Type u_1
β : Type ?u.348972
γ : Type ?u.348975
δ : Type ?u.348978
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
p q r : α
h : DvdNotUnit p q
h' : q ~ᵤ r
⊢ DvdNotUnit p r
obtain ⟨u, rfl⟩ := Associated.symm h'
case intro.intro.intro
α : Type u_1
β : Type ?u.348972
γ : Type ?u.348975
δ : Type ?u.348978
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
p r : α
u : αˣ
h' : r * ↑u ~ᵤ r
hp : p ≠ 0
x : α
hx : ¬IsUnit x ∧ r * ↑u = p * x
⊢ DvdNotUnit p r
case intro
α : Type u_1
β : Type ?u.348972
γ : Type ?u.348975
δ : Type ?u.348978
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
p r : α
u : αˣ
h : DvdNotUnit p (r * ↑u)
h' : r * ↑u ~ᵤ r
⊢ DvdNotUnit p r
obtain ⟨hp, x, hx⟩ := h
case intro.intro.intro
α : Type u_1
β : Type ?u.348972
γ : Type ?u.348975
δ : Type ?u.348978
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
p r : α
u : αˣ
h' : r * ↑u ~ᵤ r
hp : p ≠ 0
x : α
hx : ¬IsUnit x ∧ r * ↑u = p * x
⊢ r = p * (x * ↑u⁻¹)
case intro.intro.intro
α : Type u_1
β : Type ?u.348972
γ : Type ?u.348975
δ : Type ?u.348978
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
p r : α
u : αˣ
h' : r * ↑u ~ᵤ r
hp : p ≠ 0
x : α
hx : ¬IsUnit x ∧ r * ↑u = p * x
⊢ DvdNotUnit p r
refine' ⟨hp, x * ↑u⁻¹, DvdNotUnit.not_unit ⟨u⁻¹.ne_zero, x, hx.left, mul_comm _ _⟩, _⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.348972
γ : Type ?u.348975
δ : Type ?u.348978
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
p r : α
u : αˣ
h' : r * ↑u ~ᵤ r
hp : p ≠ 0
x : α
hx : ¬IsUnit x ∧ r * ↑u = p * x
⊢ r = p * (x * ↑u⁻¹)
rw [← mul_assoc, ← hx.right, mul_assoc, Units.mul_inv, mul_one]