-- Mathlib/Data/Nat/Log.lean
private lemma logC_step {m pw q e : ℕ} (hpw : 1 < pw) (hqe : logC.step m pw hpw = (q, e)) :
    pw ^ e * q ≤ m ∧ q < pw ∧ (m < pw ^ e * (q + 1)) ∧ (0 < m → 0 < q)

Proof state:
case case1.refl
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : m < pw
⊢ pw ^ 0 * m ≤ m ∧ m < pw ∧ m < pw ^ 0 * (m + 1) ∧ (0 < m → 0 < m)

Tactic:
simpa

Result:
no goals

Proof state:
case case2.refl
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
⊢ pw ^ (2 * e') * q' ≤ m ∧ q' < pw ∧ m < pw ^ (2 * e') * (q' + 1) ∧ (0 < m → 0 < q')

Tactic:
rw [Nat.pow_mul, Nat.pow_two]

Result:
case case2.refl
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
⊢ (pw * pw) ^ e' * q' ≤ m ∧ q' < pw ∧ m < (pw * pw) ^ e' * (q' + 1) ∧ (0 < m → 0 < q')

Proof state:
case case3.refl
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : ¬q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
⊢ (pw * pw) ^ e' * (pw * (q' / pw)) ≤ m ∧
    q' / pw < pw ∧ m < (pw * pw) ^ e' * (pw * (q' / pw + 1)) ∧ (0 < m → 0 < q' / pw)

Tactic:
refine ⟨(ih hqe').1.trans' (Nat.mul_le_mul_left _ (Nat.mul_div_le _ _)),
  Nat.div_lt_of_lt_mul (ih hqe').2.1, (ih hqe').2.2.1.trans_le ?_,
  fun _ => Nat.div_pos (le_of_not_lt hqpw) (by omega)⟩

Result:
case case3.refl
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : ¬q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
⊢ (pw * pw) ^ e' * (q' + 1) ≤ (pw * pw) ^ e' * (pw * (q' / pw + 1))

Proof state:
m pw q e : ℕ
hpw : 1 < pw
hqe : logC.step m pw hpw = (q, e)
⊢ pw ^ e * q ≤ m ∧ q < pw ∧ m < pw ^ e * (q + 1) ∧ (0 < m → 0 < q)

Tactic:
induction pw, hpw using logC.step.induct m generalizing q e with
| case1 pw hpw hmpw =>
    rw [logC.step, dif_pos hmpw] at hqe
    cases hqe
    simpa
| case2 pw hpw hmpw q' e' hqe' hqpw ih =>
    simp only [logC.step, dif_neg hmpw, hqe', if_pos hqpw] at hqe
    cases hqe
    rw [Nat.pow_mul, Nat.pow_two]
    exact ⟨(ih hqe').1, hqpw, (ih hqe').2.2⟩
| case3 pw hpw hmpw q' e' hqe' hqpw ih =>
    simp only [Nat.logC.step, dif_neg hmpw, hqe', if_neg hqpw] at hqe
    cases hqe
    rw [Nat.pow_succ, Nat.mul_assoc, Nat.pow_mul, Nat.pow_two, Nat.mul_assoc]
    refine ⟨(ih hqe').1.trans' (Nat.mul_le_mul_left _ (Nat.mul_div_le _ _)),
      Nat.div_lt_of_lt_mul (ih hqe').2.1, (ih hqe').2.2.1.trans_le ?_,
      fun _ => Nat.div_pos (le_of_not_lt hqpw) (by omega)⟩
    exact Nat.mul_le_mul_left _ (Nat.lt_mul_div_succ _ (zero_lt_of_lt hpw))

Result:
no goals

Proof state:
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : ¬q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
x✝ : 0 < m
⊢ 0 < pw

Tactic:
omega

Result:
no goals

Proof state:
case case3
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : ¬q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
q e : ℕ
hqe : logC.step m pw hpw = (q, e)
⊢ pw ^ e * q ≤ m ∧ q < pw ∧ m < pw ^ e * (q + 1) ∧ (0 < m → 0 < q)

Tactic:
simp only [Nat.logC.step, dif_neg hmpw, hqe', if_neg hqpw] at hqe

Result:
case case3
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : ¬q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
q e : ℕ
hqe : (q' / pw, 2 * e' + 1) = (q, e)
⊢ pw ^ e * q ≤ m ∧ q < pw ∧ m < pw ^ e * (q + 1) ∧ (0 < m → 0 < q)

Proof state:
case case3.refl
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : ¬q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
⊢ (pw * pw) ^ e' * (q' + 1) ≤ (pw * pw) ^ e' * (pw * (q' / pw + 1))

Tactic:
exact Nat.mul_le_mul_left _ (Nat.lt_mul_div_succ _ (zero_lt_of_lt hpw))

Result:
no goals

Proof state:
case case3.refl
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : ¬q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
⊢ pw ^ (2 * e' + 1) * (q' / pw) ≤ m ∧ q' / pw < pw ∧ m < pw ^ (2 * e' + 1) * (q' / pw + 1) ∧ (0 < m → 0 < q' / pw)

Tactic:
rw [Nat.pow_succ, Nat.mul_assoc, Nat.pow_mul, Nat.pow_two, Nat.mul_assoc]

Result:
case case3.refl
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : ¬q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
⊢ (pw * pw) ^ e' * (pw * (q' / pw)) ≤ m ∧
    q' / pw < pw ∧ m < (pw * pw) ^ e' * (pw * (q' / pw + 1)) ∧ (0 < m → 0 < q' / pw)

Proof state:
case case1
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : m < pw
q e : ℕ
hqe : logC.step m pw hpw = (q, e)
⊢ pw ^ e * q ≤ m ∧ q < pw ∧ m < pw ^ e * (q + 1) ∧ (0 < m → 0 < q)

Tactic:
rw [logC.step, dif_pos hmpw] at hqe

Result:
case case1
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : m < pw
q e : ℕ
hqe : (m, 0) = (q, e)
⊢ pw ^ e * q ≤ m ∧ q < pw ∧ m < pw ^ e * (q + 1) ∧ (0 < m → 0 < q)

Proof state:
case case2.refl
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
⊢ (pw * pw) ^ e' * q' ≤ m ∧ q' < pw ∧ m < (pw * pw) ^ e' * (q' + 1) ∧ (0 < m → 0 < q')

Tactic:
exact ⟨(ih hqe').1, hqpw, (ih hqe').2.2⟩

Result:
no goals

Proof state:
case case2
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
q e : ℕ
hqe : (q', 2 * e') = (q, e)
⊢ pw ^ e * q ≤ m ∧ q < pw ∧ m < pw ^ e * (q + 1) ∧ (0 < m → 0 < q)

Tactic:
cases hqe

Result:
case case2.refl
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
⊢ pw ^ (2 * e') * q' ≤ m ∧ q' < pw ∧ m < pw ^ (2 * e') * (q' + 1) ∧ (0 < m → 0 < q')