case intro
α : Type u_1
β : Type ?u.29194
γ : Type ?u.29197
δ : Type ?u.29200
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b c : α
hc : p * b = a * c
⊢ p ∣ a ∨ a ∣ b
α : Type u_1
β : Type ?u.29194
γ : Type ?u.29197
δ : Type ?u.29200
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
⊢ a ∣ p * b → p ∣ a ∨ a ∣ b
rintro ⟨c, hc⟩
case intro.inl
α : Type u_1
β : Type ?u.29194
γ : Type ?u.29197
δ : Type ?u.29200
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b c : α
hc : p * b = a * c
h : p ∣ a
⊢ p ∣ a ∨ a ∣ b

case intro.inr.intro
α : Type u_1
β : Type ?u.29194
γ : Type ?u.29197
δ : Type ?u.29200
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b x : α
hc : p * b = a * (p * x)
⊢ p ∣ a ∨ a ∣ b
case intro
α : Type u_1
β : Type ?u.29194
γ : Type ?u.29197
δ : Type ?u.29200
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b c : α
hc : p * b = a * c
⊢ p ∣ a ∨ a ∣ b
rcases hp.2.2 a c (hc ▸ dvd_mul_right _ _) with (h | ⟨x, rfl⟩)
no goals
case intro.inl
α : Type u_1
β : Type ?u.29194
γ : Type ?u.29197
δ : Type ?u.29200
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b c : α
hc : p * b = a * c
h : p ∣ a
⊢ p ∣ a ∨ a ∣ b
exact Or.inl h
case intro.inr.intro
α : Type u_1
β : Type ?u.29194
γ : Type ?u.29197
δ : Type ?u.29200
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b x : α
hc : b = a * x
⊢ p ∣ a ∨ a ∣ b
case intro.inr.intro
α : Type u_1
β : Type ?u.29194
γ : Type ?u.29197
δ : Type ?u.29200
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b x : α
hc : p * b = a * (p * x)
⊢ p ∣ a ∨ a ∣ b
rw [mul_left_comm, mul_right_inj' hp.ne_zero] at hc
no goals
case intro.inr.intro
α : Type u_1
β : Type ?u.29194
γ : Type ?u.29197
δ : Type ?u.29200
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b x : α
hc : b = a * x
⊢ p ∣ a ∨ a ∣ b
exact Or.inr (hc.symm ▸ dvd_mul_right _ _)