-- Mathlib/Data/Nat/MaxPowDiv.lean
theorem pow_dvd (p n : ℕ) : p ^ (p.maxPowDiv n) ∣ n

Proof state:
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ n / p < n

Tactic:
apply Nat.div_lt_self <;> aesop

Result:
no goals

Proof state:
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ p.maxPowDiv (n / p) * c
⊢ n / p * p = p ^ go 0 p (n / p) * p * c

Tactic:
nth_rw 1 [hc]

Result:
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ p.maxPowDiv (n / p) * c
⊢ p ^ p.maxPowDiv (n / p) * c * p = p ^ go 0 p (n / p) * p * c

Proof state:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ p.maxPowDiv (n / p) * c
⊢ p ^ go 0 p (n / p) * p ∣ n % p + n / p * p

Tactic:
rw [h.right.right, zero_add]

Result:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ p.maxPowDiv (n / p) * c
⊢ p ^ go 0 p (n / p) * p ∣ n / p * p

Proof state:
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ p.maxPowDiv (n / p) * c
⊢ p ^ p.maxPowDiv (n / p) * c * p = p ^ go 0 p (n / p) * p * c

Tactic:
ac_rfl

Result:
no goals

Proof state:
case neg
p n : ℕ
h : ¬(1 < p ∧ 0 < n ∧ n % p = 0)
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n

Tactic:
rw [if_neg h]

Result:
case neg
p n : ℕ
h : ¬(1 < p ∧ 0 < n ∧ n % p = 0)
⊢ p ^ 0 ∣ n

Proof state:
p n : ℕ
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n

Tactic:
by_cases h : (1 < p ∧ 0 < n ∧ n % p = 0)

Result:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n

case neg
p n : ℕ
h : ¬(1 < p ∧ 0 < n ∧ n % p = 0)
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n

Proof state:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ p.maxPowDiv (n / p) * c
⊢ p ^ go (0 + 1) p (n / p) ∣ n

Tactic:
rw [go_succ, pow_succ]

Result:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ p.maxPowDiv (n / p) * c
⊢ p ^ go 0 p (n / p) * p ∣ n

Proof state:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
⊢ p ^ go (0 + 1) p (n / p) ∣ n

Tactic:
have ⟨c,hc⟩ := pow_dvd p (n / p)

Result:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ p.maxPowDiv (n / p) * c
⊢ p ^ go (0 + 1) p (n / p) ∣ n

Proof state:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n

Tactic:
rw [if_pos h]

Result:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
⊢ p ^ go (0 + 1) p (n / p) ∣ n

Proof state:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ p.maxPowDiv (n / p) * c
⊢ p ^ go 0 p (n / p) * p ∣ n / p * p

Tactic:
exact ⟨c,by nth_rw 1 [hc]; ac_rfl⟩

Result:
no goals

Proof state:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ p.maxPowDiv (n / p) * c
⊢ p ^ go 0 p (n / p) * p ∣ n

Tactic:
nth_rw 2 [← mod_add_div' n p]

Result:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ p.maxPowDiv (n / p) * c
⊢ p ^ go 0 p (n / p) * p ∣ n % p + n / p * p

Proof state:
p n : ℕ
⊢ p ^ go 0 p n ∣ n

Tactic:
rw [go]

Result:
p n : ℕ
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n

Proof state:
p n : ℕ
⊢ p ^ p.maxPowDiv n ∣ n

Tactic:
dsimp [maxPowDiv]

Result:
p n : ℕ
⊢ p ^ go 0 p n ∣ n

Proof state:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n

Tactic:
have : n / p < n := by apply Nat.div_lt_self <;> aesop

Result:
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n

Proof state:
case neg
p n : ℕ
h : ¬(1 < p ∧ 0 < n ∧ n % p = 0)
⊢ p ^ 0 ∣ n

Tactic:
simp

Result:
no goals