[GOAL]
p✝ n✝ k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ n / p < n
[PROOFSTEP]
apply Nat.div_lt_self
[GOAL]
case hLtN
p✝ n✝ k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ 0 < n
[PROOFSTEP]
aesop
[GOAL]
case hLtK
p✝ n✝ k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ 1 < p
[PROOFSTEP]
aesop
[GOAL]
k p n : ℕ
⊢ go k p n = if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k
[PROOFSTEP]
dsimp [go, go._unary]
[GOAL]
k p n : ℕ
⊢ WellFounded.fix go._unary.proof_1
      (fun _x a =>
        if h : 1 < _x.snd.fst ∧ 0 < _x.snd.snd ∧ _x.snd.snd % _x.snd.fst = 0 then
          a { fst := _x.fst + 1, snd := { fst := _x.snd.fst, snd := _x.snd.snd / _x.snd.fst } }
            (_ : _x.snd.snd / _x.snd.fst < _x.snd.snd)
        else _x.fst)
      { fst := k, snd := { fst := p, snd := n } } =
    if 1 < p ∧ 0 < n ∧ n % p = 0 then
      WellFounded.fix go._unary.proof_1
        (fun _x a =>
          if h : 1 < _x.snd.fst ∧ 0 < _x.snd.snd ∧ _x.snd.snd % _x.snd.fst = 0 then
            a { fst := _x.fst + 1, snd := { fst := _x.snd.fst, snd := _x.snd.snd / _x.snd.fst } }
              (_ : _x.snd.snd / _x.snd.fst < _x.snd.snd)
          else _x.fst)
        { fst := k + 1, snd := { fst := p, snd := n / p } }
    else k
[PROOFSTEP]
rw [WellFounded.fix_eq]
[GOAL]
k p n : ℕ
⊢ (if h :
        1 < { fst := k, snd := { fst := p, snd := n } }.snd.fst ∧
          0 < { fst := k, snd := { fst := p, snd := n } }.snd.snd ∧
            { fst := k, snd := { fst := p, snd := n } }.snd.snd % { fst := k, snd := { fst := p, snd := n } }.snd.fst =
              0 then
      (fun y x =>
          WellFounded.fix go._unary.proof_1
            (fun _x a =>
              if h : 1 < _x.snd.fst ∧ 0 < _x.snd.snd ∧ _x.snd.snd % _x.snd.fst = 0 then
                a { fst := _x.fst + 1, snd := { fst := _x.snd.fst, snd := _x.snd.snd / _x.snd.fst } }
                  (_ : _x.snd.snd / _x.snd.fst < _x.snd.snd)
              else _x.fst)
            y)
        { fst := { fst := k, snd := { fst := p, snd := n } }.fst + 1,
          snd :=
            { fst := { fst := k, snd := { fst := p, snd := n } }.snd.fst,
              snd :=
                { fst := k, snd := { fst := p, snd := n } }.snd.snd /
                  { fst := k, snd := { fst := p, snd := n } }.snd.fst } }
        (_ :
          { fst := k, snd := { fst := p, snd := n } }.snd.snd / { fst := k, snd := { fst := p, snd := n } }.snd.fst <
            { fst := k, snd := { fst := p, snd := n } }.snd.snd)
    else { fst := k, snd := { fst := p, snd := n } }.fst) =
    if 1 < p ∧ 0 < n ∧ n % p = 0 then
      WellFounded.fix go._unary.proof_1
        (fun _x a =>
          if h : 1 < _x.snd.fst ∧ 0 < _x.snd.snd ∧ _x.snd.snd % _x.snd.fst = 0 then
            a { fst := _x.fst + 1, snd := { fst := _x.snd.fst, snd := _x.snd.snd / _x.snd.fst } }
              (_ : _x.snd.snd / _x.snd.fst < _x.snd.snd)
          else _x.fst)
        { fst := k + 1, snd := { fst := p, snd := n / p } }
    else k
[PROOFSTEP]
simp
[GOAL]
k p n : ℕ
⊢ go (k + 1) p n = go k p n + 1
[PROOFSTEP]
rw [go_eq]
[GOAL]
k p n : ℕ
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) = go k p n + 1
[PROOFSTEP]
conv_rhs => rw [go_eq]
[GOAL]
k p n : ℕ
| go k p n + 1
[PROOFSTEP]
rw [go_eq]
[GOAL]
k p n : ℕ
| go k p n + 1
[PROOFSTEP]
rw [go_eq]
[GOAL]
k p n : ℕ
| go k p n + 1
[PROOFSTEP]
rw [go_eq]
[GOAL]
k p n : ℕ
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) =
    (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k) + 1
[PROOFSTEP]
by_cases (1 < p ∧ 0 < n ∧ n % p = 0)
[GOAL]
k p n : ℕ
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) =
    (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k) + 1
[PROOFSTEP]
by_cases (1 < p ∧ 0 < n ∧ n % p = 0)
[GOAL]
case pos
k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) =
    (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k) + 1
case neg
k p n : ℕ
h : ¬(1 < p ∧ 0 < n ∧ n % p = 0)
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) =
    (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k) + 1
[PROOFSTEP]
swap
[GOAL]
case neg
k p n : ℕ
h : ¬(1 < p ∧ 0 < n ∧ n % p = 0)
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) =
    (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k) + 1
[PROOFSTEP]
simp only [if_neg h]
[GOAL]
case pos
k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) =
    (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k) + 1
[PROOFSTEP]
have : n / p < n := by apply Nat.div_lt_self <;> aesop
[GOAL]
k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ n / p < n
[PROOFSTEP]
apply Nat.div_lt_self
[GOAL]
case hLtN
k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ 0 < n
[PROOFSTEP]
aesop
[GOAL]
case hLtK
k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ 1 < p
[PROOFSTEP]
aesop
[GOAL]
case pos
k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
⊢ (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1 + 1) p (n / p) else k + 1) =
    (if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k) + 1
[PROOFSTEP]
simp only [if_pos h]
[GOAL]
case pos
k p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
⊢ go (k + 1 + 1) p (n / p) = go (k + 1) p (n / p) + 1
[PROOFSTEP]
apply go_succ
[GOAL]
n : ℕ
⊢ maxPowDiv 0 n = 0
[PROOFSTEP]
dsimp [maxPowDiv]
[GOAL]
n : ℕ
⊢ go 0 0 n = 0
[PROOFSTEP]
rw [maxPowDiv.go_eq]
[GOAL]
n : ℕ
⊢ (if 1 < 0 ∧ 0 < n ∧ n % 0 = 0 then go (0 + 1) 0 (n / 0) else 0) = 0
[PROOFSTEP]
simp
[GOAL]
p : ℕ
⊢ maxPowDiv p 0 = 0
[PROOFSTEP]
dsimp [maxPowDiv]
[GOAL]
p : ℕ
⊢ go 0 p 0 = 0
[PROOFSTEP]
rw [maxPowDiv.go_eq]
[GOAL]
p : ℕ
⊢ (if 1 < p ∧ 0 < 0 ∧ 0 % p = 0 then go (0 + 1) p (0 / p) else 0) = 0
[PROOFSTEP]
simp
[GOAL]
p n : ℕ
hp : 1 < p
hn : 0 < n
⊢ maxPowDiv p (p * n) = maxPowDiv p n + 1
[PROOFSTEP]
have : 0 < p := lt_trans (b := 1) (by simp) hp
[GOAL]
p n : ℕ
hp : 1 < p
hn : 0 < n
⊢ 0 < 1
[PROOFSTEP]
simp
[GOAL]
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ maxPowDiv p (p * n) = maxPowDiv p n + 1
[PROOFSTEP]
dsimp [maxPowDiv]
[GOAL]
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ go 0 p (p * n) = go 0 p n + 1
[PROOFSTEP]
rw [maxPowDiv.go_eq, if_pos, mul_div_right _ this]
[GOAL]
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ go (0 + 1) p n = go 0 p n + 1
[PROOFSTEP]
apply go_succ
[GOAL]
case hc
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ 1 < p ∧ 0 < p * n ∧ p * n % p = 0
[PROOFSTEP]
refine ⟨hp, ?_, by simp⟩
[GOAL]
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ p * n % p = 0
[PROOFSTEP]
simp
[GOAL]
case hc
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ 0 < p * n
[PROOFSTEP]
apply Nat.mul_pos this hn
[GOAL]
p n exp : ℕ
hp : 1 < p
hn : 0 < n
⊢ maxPowDiv p (p ^ exp * n) = maxPowDiv p n + exp
[PROOFSTEP]
match exp with
| 0 => simp
| e + 1 =>
  rw [pow_succ, mul_assoc, mul_comm, mul_assoc, base_mul_eq_succ hp, mul_comm, base_pow_mul hp hn]
  · ac_rfl
  · apply Nat.mul_pos hn <| pow_pos (pos_of_gt hp) e
[GOAL]
p n exp : ℕ
hp : 1 < p
hn : 0 < n
⊢ maxPowDiv p (p ^ 0 * n) = maxPowDiv p n + 0
[PROOFSTEP]
simp
[GOAL]
p n exp : ℕ
hp : 1 < p
hn : 0 < n
e : ℕ
⊢ maxPowDiv p (p ^ (e + 1) * n) = maxPowDiv p n + (e + 1)
[PROOFSTEP]
rw [pow_succ, mul_assoc, mul_comm, mul_assoc, base_mul_eq_succ hp, mul_comm, base_pow_mul hp hn]
[GOAL]
p n exp : ℕ
hp : 1 < p
hn : 0 < n
e : ℕ
⊢ maxPowDiv p n + e + 1 = maxPowDiv p n + (e + 1)
[PROOFSTEP]
ac_rfl
[GOAL]
p n exp : ℕ
hp : 1 < p
hn : 0 < n
e : ℕ
⊢ 0 < n * p ^ e
[PROOFSTEP]
apply Nat.mul_pos hn <| pow_pos (pos_of_gt hp) e
[GOAL]
p n : ℕ
⊢ p ^ maxPowDiv p n ∣ n
[PROOFSTEP]
dsimp [maxPowDiv]
[GOAL]
p n : ℕ
⊢ p ^ go 0 p n ∣ n
[PROOFSTEP]
rw [go_eq]
[GOAL]
p n : ℕ
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n
[PROOFSTEP]
by_cases (1 < p ∧ 0 < n ∧ n % p = 0)
[GOAL]
p n : ℕ
⊢ (p ^ if 1 < p ∧ 0 < n ∧ n % p = 0 then go (0 + 1) p (n / p) else 0) ∣ n
[PROOFSTEP]
by_cases (1 < p ∧ 0 < n ∧ n % p = 0)
[GOAL]
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
[PROOFSTEP]
have : n / p < n := by apply Nat.div_lt_self <;> aesop
[GOAL]
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ n / p < n
[PROOFSTEP]
apply Nat.div_lt_self
[GOAL]
case hLtN
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ 0 < n
[PROOFSTEP]
aesop
[GOAL]
case hLtK
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
⊢ 1 < p
[PROOFSTEP]
aesop
[GOAL]
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
[PROOFSTEP]
rw [if_pos h]
[GOAL]
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
⊢ p ^ go (0 + 1) p (n / p) ∣ n
[PROOFSTEP]
have ⟨c, hc⟩ := pow_dvd p (n / p)
[GOAL]
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ maxPowDiv p (n / p) * c
⊢ p ^ go (0 + 1) p (n / p) ∣ n
[PROOFSTEP]
rw [go_succ, pow_succ]
[GOAL]
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ maxPowDiv p (n / p) * c
⊢ p ^ go 0 p (n / p) * p ∣ n
[PROOFSTEP]
nth_rw 2 [← mod_add_div' n p]
[GOAL]
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ maxPowDiv p (n / p) * c
⊢ p ^ go 0 p (n / p) * p ∣ n % p + n / p * p
[PROOFSTEP]
rw [h.right.right, zero_add]
[GOAL]
case pos
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ maxPowDiv p (n / p) * c
⊢ p ^ go 0 p (n / p) * p ∣ n / p * p
[PROOFSTEP]
exact ⟨c, by nth_rw 1 [hc]; ac_rfl⟩
[GOAL]
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ maxPowDiv p (n / p) * c
⊢ n / p * p = p ^ go 0 p (n / p) * p * c
[PROOFSTEP]
nth_rw 1 [hc]
[GOAL]
p n : ℕ
h : 1 < p ∧ 0 < n ∧ n % p = 0
this : n / p < n
c : ℕ
hc : n / p = p ^ maxPowDiv p (n / p) * c
⊢ p ^ maxPowDiv p (n / p) * c * p = p ^ go 0 p (n / p) * p * c
[PROOFSTEP]
ac_rfl
[GOAL]
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
[PROOFSTEP]
rw [if_neg h]
[GOAL]
case neg
p n : ℕ
h : ¬(1 < p ∧ 0 < n ∧ n % p = 0)
⊢ p ^ 0 ∣ n
[PROOFSTEP]
simp
[GOAL]
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
⊢ pow ≤ maxPowDiv p n
[PROOFSTEP]
have ⟨c, hc⟩ := h
[GOAL]
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
⊢ pow ≤ maxPowDiv p n
[PROOFSTEP]
have : 0 < c := by
  apply Nat.pos_of_ne_zero
  intro h'
  rw [h', mul_zero] at hc 
  exact not_eq_zero_of_lt hn hc
[GOAL]
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
⊢ 0 < c
[PROOFSTEP]
apply Nat.pos_of_ne_zero
[GOAL]
case a
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
⊢ c ≠ 0
[PROOFSTEP]
intro h'
[GOAL]
case a
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
h' : c = 0
⊢ False
[PROOFSTEP]
rw [h', mul_zero] at hc 
[GOAL]
case a
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = 0
h' : c = 0
⊢ False
[PROOFSTEP]
exact not_eq_zero_of_lt hn hc
[GOAL]
p n pow : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ pow ∣ n
c : ℕ
hc : n = p ^ pow * c
this : 0 < c
⊢ pow ≤ maxPowDiv p n
[PROOFSTEP]
simp [hc, base_pow_mul hp this]
