case zero
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n : ℕ
h✝ : p ∣ a ^ n
h : p ∣ a ^ Nat.zero
⊢ p ∣ a

case succ
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n✝ : ℕ
h✝ : p ∣ a ^ n✝
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a ^ Nat.succ n
⊢ p ∣ a
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n : ℕ
h : p ∣ a ^ n
⊢ p ∣ a
induction' n with n ih
case succ
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n✝ : ℕ
h✝ : p ∣ a ^ n✝
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
⊢ p ∣ a
case succ
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n✝ : ℕ
h✝ : p ∣ a ^ n✝
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a ^ Nat.succ n
⊢ p ∣ a
rw [pow_succ] at h
case succ.inl
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n✝ : ℕ
h✝ : p ∣ a ^ n✝
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_a : p ∣ a
⊢ p ∣ a

case succ.inr
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n✝ : ℕ
h✝ : p ∣ a ^ n✝
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_pow : p ∣ a ^ n
⊢ p ∣ a
case succ
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n✝ : ℕ
h✝ : p ∣ a ^ n✝
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
⊢ p ∣ a
cases' dvd_or_dvd hp h with dvd_a dvd_pow
no goals
case succ.inr
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n✝ : ℕ
h✝ : p ∣ a ^ n✝
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_pow : p ∣ a ^ n
⊢ p ∣ a
exact ih dvd_pow
case zero
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n : ℕ
h✝ : p ∣ a ^ n
h : p ∣ 1
⊢ p ∣ a
case zero
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n : ℕ
h✝ : p ∣ a ^ n
h : p ∣ a ^ Nat.zero
⊢ p ∣ a
rw [pow_zero] at h
case zero
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n : ℕ
h✝ : p ∣ a ^ n
h : p ∣ 1
this : IsUnit p
⊢ p ∣ a
case zero
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n : ℕ
h✝ : p ∣ a ^ n
h : p ∣ 1
⊢ p ∣ a
have := isUnit_of_dvd_one h
case zero
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n : ℕ
h✝ : p ∣ a ^ n
h : p ∣ 1
this✝ : IsUnit p
this : ¬IsUnit p
⊢ p ∣ a
case zero
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n : ℕ
h✝ : p ∣ a ^ n
h : p ∣ 1
this : IsUnit p
⊢ p ∣ a
have := not_unit hp
no goals
case zero
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n : ℕ
h✝ : p ∣ a ^ n
h : p ∣ 1
this✝ : IsUnit p
this : ¬IsUnit p
⊢ p ∣ a
contradiction
no goals
case succ.inl
α : Type u_1
β : Type ?u.3519
γ : Type ?u.3522
δ : Type ?u.3525
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n✝ : ℕ
h✝ : p ∣ a ^ n✝
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_a : p ∣ a
⊢ p ∣ a
assumption