case zero
α : Type u_1
β : Type ?u.30722
γ : Type ?u.30725
δ : Type ?u.30728
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n : ℕ
h : ¬p ∣ a
h'✝ : p ^ n ∣ a * b
h' : p ^ Nat.zero ∣ a * b
⊢ p ^ Nat.zero ∣ b

case succ
α : Type u_1
β : Type ?u.30722
γ : Type ?u.30725
δ : Type ?u.30728
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n✝ : ℕ
h : ¬p ∣ a
h'✝ : p ^ n✝ ∣ a * b
n : ℕ
ih : p ^ n ∣ a * b → p ^ n ∣ b
h' : p ^ Nat.succ n ∣ a * b
⊢ p ^ Nat.succ n ∣ b
α : Type u_1
β : Type ?u.30722
γ : Type ?u.30725
δ : Type ?u.30728
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n : ℕ
h : ¬p ∣ a
h' : p ^ n ∣ a * b
⊢ p ^ n ∣ b
induction' n with n ih
case zero
α : Type u_1
β : Type ?u.30722
γ : Type ?u.30725
δ : Type ?u.30728
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n : ℕ
h : ¬p ∣ a
h'✝ : p ^ n ∣ a * b
h' : p ^ Nat.zero ∣ a * b
⊢ 1 ∣ b
case zero
α : Type u_1
β : Type ?u.30722
γ : Type ?u.30725
δ : Type ?u.30728
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n : ℕ
h : ¬p ∣ a
h'✝ : p ^ n ∣ a * b
h' : p ^ Nat.zero ∣ a * b
⊢ p ^ Nat.zero ∣ b
rw [pow_zero]
no goals
case zero
α : Type u_1
β : Type ?u.30722
γ : Type ?u.30725
δ : Type ?u.30728
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n : ℕ
h : ¬p ∣ a
h'✝ : p ^ n ∣ a * b
h' : p ^ Nat.zero ∣ a * b
⊢ 1 ∣ b
exact one_dvd b
case succ.intro
α : Type u_1
β : Type ?u.30722
γ : Type ?u.30725
δ : Type ?u.30728
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
n✝ : ℕ
h : ¬p ∣ a
n : ℕ
c : α
h'✝ : p ^ n✝ ∣ a * (p ^ n * c)
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ Nat.succ n ∣ a * (p ^ n * c)
⊢ p ^ Nat.succ n ∣ p ^ n * c
case succ
α : Type u_1
β : Type ?u.30722
γ : Type ?u.30725
δ : Type ?u.30728
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n✝ : ℕ
h : ¬p ∣ a
h'✝ : p ^ n✝ ∣ a * b
n : ℕ
ih : p ^ n ∣ a * b → p ^ n ∣ b
h' : p ^ Nat.succ n ∣ a * b
⊢ p ^ Nat.succ n ∣ b
obtain ⟨c, rfl⟩ := ih (dvd_trans (pow_dvd_pow p n.le_succ) h')
case succ.intro
α : Type u_1
β : Type ?u.30722
γ : Type ?u.30725
δ : Type ?u.30728
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
n✝ : ℕ
h : ¬p ∣ a
n : ℕ
c : α
h'✝ : p ^ n✝ ∣ a * (p ^ n * c)
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ Nat.succ n ∣ a * (p ^ n * c)
⊢ p ^ n * p ∣ p ^ n * c
case succ.intro
α : Type u_1
β : Type ?u.30722
γ : Type ?u.30725
δ : Type ?u.30728
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
n✝ : ℕ
h : ¬p ∣ a
n : ℕ
c : α
h'✝ : p ^ n✝ ∣ a * (p ^ n * c)
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ Nat.succ n ∣ a * (p ^ n * c)
⊢ p ^ Nat.succ n ∣ p ^ n * c
rw [pow_succ']
α : Type u_1
β : Type ?u.30722
γ : Type ?u.30725
δ : Type ?u.30728
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
n✝ : ℕ
h : ¬p ∣ a
n : ℕ
c : α
h'✝ : p ^ n✝ ∣ a * (p ^ n * c)
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ Nat.succ n ∣ a * (p ^ n * c)
⊢ p ∣ a * c
case succ.intro
α : Type u_1
β : Type ?u.30722
γ : Type ?u.30725
δ : Type ?u.30728
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
n✝ : ℕ
h : ¬p ∣ a
n : ℕ
c : α
h'✝ : p ^ n✝ ∣ a * (p ^ n * c)
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ Nat.succ n ∣ a * (p ^ n * c)
⊢ p ^ n * p ∣ p ^ n * c
apply mul_dvd_mul_left _ ((hp.dvd_or_dvd _).resolve_left h)
no goals
α : Type u_1
β : Type ?u.30722
γ : Type ?u.30725
δ : Type ?u.30728
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
n✝ : ℕ
h : ¬p ∣ a
n : ℕ
c : α
h'✝ : p ^ n✝ ∣ a * (p ^ n * c)
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ Nat.succ n ∣ a * (p ^ n * c)
⊢ p ∣ a * c
rwa [← mul_dvd_mul_iff_left (pow_ne_zero n hp.ne_zero), ← pow_succ', mul_left_comm]