α : Type u_1
β : Type ?u.355226
γ : Type ?u.355229
δ : Type ?u.355232
inst✝ : CancelCommMonoidWithZero α
p q : α
h : DvdNotUnit p q
hcontra : p = q
⊢ False
α : Type u_1
β : Type ?u.355226
γ : Type ?u.355229
δ : Type ?u.355232
inst✝ : CancelCommMonoidWithZero α
p q : α
h : DvdNotUnit p q
⊢ p ≠ q
by_contra hcontra
case intro.intro.intro
α : Type u_1
β : Type ?u.355226
γ : Type ?u.355229
δ : Type ?u.355232
inst✝ : CancelCommMonoidWithZero α
p q : α
hcontra : p = q
hp : p ≠ 0
x : α
hx' : ¬IsUnit x
hx'' : q = p * x
⊢ False
α : Type u_1
β : Type ?u.355226
γ : Type ?u.355229
δ : Type ?u.355232
inst✝ : CancelCommMonoidWithZero α
p q : α
h : DvdNotUnit p q
hcontra : p = q
⊢ False
obtain ⟨hp, x, hx', hx''⟩ := h
case intro.intro.intro
α : Type u_1
β : Type ?u.355226
γ : Type ?u.355229
δ : Type ?u.355232
inst✝ : CancelCommMonoidWithZero α
p q : α
hcontra : p = q
hp : p ≠ 0
x : α
hx' : ¬IsUnit x
hx'' : p * 1 = p * x
⊢ False
case intro.intro.intro
α : Type u_1
β : Type ?u.355226
γ : Type ?u.355229
δ : Type ?u.355232
inst✝ : CancelCommMonoidWithZero α
p q : α
hcontra : p = q
hp : p ≠ 0
x : α
hx' : ¬IsUnit x
hx'' : q = p * x
⊢ False
conv_lhs at hx'' => rw [← hcontra, ← mul_one p]
case intro.intro.intro
α : Type u_1
β : Type ?u.355226
γ : Type ?u.355229
δ : Type ?u.355232
inst✝ : CancelCommMonoidWithZero α
p q : α
hcontra : p = q
hp : p ≠ 0
x : α
hx' : ¬IsUnit 1
hx'' : p * 1 = p * x
⊢ False
case intro.intro.intro
α : Type u_1
β : Type ?u.355226
γ : Type ?u.355229
δ : Type ?u.355232
inst✝ : CancelCommMonoidWithZero α
p q : α
hcontra : p = q
hp : p ≠ 0
x : α
hx' : ¬IsUnit x
hx'' : p * 1 = p * x
⊢ False
rw [(mul_left_cancel₀ hp hx'').symm] at hx'
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.355226
γ : Type ?u.355229
δ : Type ?u.355232
inst✝ : CancelCommMonoidWithZero α
p q : α
hcontra : p = q
hp : p ≠ 0
x : α
hx' : ¬IsUnit 1
hx'' : p * 1 = p * x
⊢ False
exact hx' isUnit_one