case zero
p m n : ℕ
pp : Prime p
h✝ : p ∣ m ^ n
h : p ∣ m ^ zero
⊢ p ∣ m

case succ
p m n✝ : ℕ
pp : Prime p
h✝ : p ∣ m ^ n✝
n : ℕ
IH : p ∣ m ^ n → p ∣ m
h : p ∣ m ^ succ n
⊢ p ∣ m
p m n : ℕ
pp : Prime p
h : p ∣ m ^ n
⊢ p ∣ m
induction' n with n IH
no goals
case zero
p m n : ℕ
pp : Prime p
h✝ : p ∣ m ^ n
h : p ∣ m ^ zero
⊢ p ∣ m
exact pp.not_dvd_one.elim h
case succ
p m n✝ : ℕ
pp : Prime p
h✝ : p ∣ m ^ n✝
n : ℕ
IH : p ∣ m ^ n → p ∣ m
h : p ∣ m ^ n * m
⊢ p ∣ m
case succ
p m n✝ : ℕ
pp : Prime p
h✝ : p ∣ m ^ n✝
n : ℕ
IH : p ∣ m ^ n → p ∣ m
h : p ∣ m ^ succ n
⊢ p ∣ m
rw [pow_succ] at h
no goals
case succ
p m n✝ : ℕ
pp : Prime p
h✝ : p ∣ m ^ n✝
n : ℕ
IH : p ∣ m ^ n → p ∣ m
h : p ∣ m ^ n * m
⊢ p ∣ m
exact (pp.dvd_mul.1 h).elim IH id