α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
⊢ m = 1 ∨ m = p
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
⊢ m = 1 ∨ m = p
have dvd_rfl' : p ∣ m * d := by rw[r]
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
⊢ m = 1 ∨ m = m * d
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
⊢ m = 1 ∨ m = p
rw [r]
no goals
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
⊢ m = 1 ∨ m = m * d
match h m d dvd_rfl' with
| Or.inl h' =>
  by_cases h : m = 0
  case pos =>
    simp [h, zero_mul]
  case neg =>
    rw [r] at h'
    have : m * d ≤ m * 1 := by simpa using h'
    have : d ≤ 1 := Associates.le_of_mul_le_mul_left m d 1 ‹m ≠ 0› this
    have : d = 1 := bot_unique this
    simp [this]
| Or.inr h' =>
    by_cases h : d = 0
    case pos =>
      rw [r] at hp0
      have : m * d = 0 := by rw [h]; simp
      contradiction
    case neg =>
      rw [r] at h'
      have : d * m ≤ d * 1 := by simpa [mul_comm] using h'
      exact Or.inl <| bot_unique <| Associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this
no goals
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
⊢ p ∣ m * d
rw[r]
case pos
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : m = 0
⊢ m = 1 ∨ m = m * d

case neg
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : ¬m = 0
⊢ m = 1 ∨ m = m * d
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
⊢ m = 1 ∨ m = m * d
by_cases h : m = 0
case neg
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : ¬m = 0
⊢ m = 1 ∨ m = m * d
case pos
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : m = 0
⊢ m = 1 ∨ m = m * d

case neg
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : ¬m = 0
⊢ m = 1 ∨ m = m * d
case pos =>
  simp [h, zero_mul]
no goals
case neg
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : ¬m = 0
⊢ m = 1 ∨ m = m * d
case neg =>
  rw [r] at h'
  have : m * d ≤ m * 1 := by simpa using h'
  have : d ≤ 1 := Associates.le_of_mul_le_mul_left m d 1 ‹m ≠ 0› this
  have : d = 1 := bot_unique this
  simp [this]
no goals
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : m = 0
⊢ m = 1 ∨ m = m * d
simp [h, zero_mul]
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ m
h : ¬m = 0
⊢ m = 1 ∨ m = m * d
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : ¬m = 0
⊢ m = 1 ∨ m = m * d
rw [r] at h'
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ m
h : ¬m = 0
this : m * d ≤ m * 1
⊢ m = 1 ∨ m = m * d
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ m
h : ¬m = 0
⊢ m = 1 ∨ m = m * d
have : m * d ≤ m * 1 := by simpa using h'
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ m
h : ¬m = 0
this✝ : m * d ≤ m * 1
this : d ≤ 1
⊢ m = 1 ∨ m = m * d
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ m
h : ¬m = 0
this : m * d ≤ m * 1
⊢ m = 1 ∨ m = m * d
have : d ≤ 1 := Associates.le_of_mul_le_mul_left m d 1 ‹m ≠ 0› this
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ m
h : ¬m = 0
this✝¹ : m * d ≤ m * 1
this✝ : d ≤ 1
this : d = 1
⊢ m = 1 ∨ m = m * d
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ m
h : ¬m = 0
this✝ : m * d ≤ m * 1
this : d ≤ 1
⊢ m = 1 ∨ m = m * d
have : d = 1 := bot_unique this
no goals
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ m
h : ¬m = 0
this✝¹ : m * d ≤ m * 1
this✝ : d ≤ 1
this : d = 1
⊢ m = 1 ∨ m = m * d
simp [this]
no goals
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ m
h : ¬m = 0
⊢ m * d ≤ m * 1
simpa using h'
case pos
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
⊢ m = 1 ∨ m = m * d

case neg
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : ¬d = 0
⊢ m = 1 ∨ m = m * d
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
⊢ m = 1 ∨ m = m * d
by_cases h : d = 0
case neg
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : ¬d = 0
⊢ m = 1 ∨ m = m * d
case pos
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
⊢ m = 1 ∨ m = m * d

case neg
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : ¬d = 0
⊢ m = 1 ∨ m = m * d
case pos =>
  rw [r] at hp0
  have : m * d = 0 := by rw [h]; simp
  contradiction
no goals
case neg
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : ¬d = 0
⊢ m = 1 ∨ m = m * d
case neg =>
  rw [r] at h'
  have : d * m ≤ d * 1 := by simpa [mul_comm] using h'
  exact Or.inl <| bot_unique <| Associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
hp0 : m * d ≠ 0
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
⊢ m = 1 ∨ m = m * d
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
⊢ m = 1 ∨ m = m * d
rw [r] at hp0
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
hp0 : m * d ≠ 0
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
this : m * d = 0
⊢ m = 1 ∨ m = m * d
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
hp0 : m * d ≠ 0
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
⊢ m = 1 ∨ m = m * d
have : m * d = 0 := by rw [h]; simp
no goals
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
hp0 : m * d ≠ 0
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
this : m * d = 0
⊢ m = 1 ∨ m = m * d
contradiction
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
hp0 : m * d ≠ 0
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
⊢ m * 0 = 0
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
hp0 : m * d ≠ 0
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
⊢ m * d = 0
rw [h]
no goals
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
hp0 : m * d ≠ 0
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
⊢ m * 0 = 0
simp
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ d
h : ¬d = 0
⊢ m = 1 ∨ m = m * d
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : ¬d = 0
⊢ m = 1 ∨ m = m * d
rw [r] at h'
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ d
h : ¬d = 0
this : d * m ≤ d * 1
⊢ m = 1 ∨ m = m * d
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ d
h : ¬d = 0
⊢ m = 1 ∨ m = m * d
have : d * m ≤ d * 1 := by simpa [mul_comm] using h'
no goals
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ d
h : ¬d = 0
this : d * m ≤ d * 1
⊢ m = 1 ∨ m = m * d
exact Or.inl <| bot_unique <| Associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this
no goals
α : Type u_1
β : Type ?u.335369
γ : Type ?u.335372
δ : Type ?u.335375
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ d
h : ¬d = 0
⊢ d * m ≤ d * 1
simpa [mul_comm] using h'