-- Mathlib/Data/Nat/Log.lean
theorem log_eq_iff {b m n : ℕ} (h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0) :
    log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Proof state:
case inl.intro
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
rw [le_antisymm_iff, ← Nat.lt_succ_iff, ← pow_le_iff_le_log, ← lt_pow_iff_log_lt,
  and_comm] <;> assumption

Result:
no goals

Proof state:
case inr.inl.inr
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 1 ∧ n ≠ 0
hb : 1 ≤ 1
⊢ log 1 n = m ↔ 1 ^ m ≤ n ∧ n < 1 ^ (m + 1)

Tactic:
simp only [ne_eq, zero_eq, reduceSucc, lt_self_iff_false,  not_lt_zero, false_and, or_false]
  at h

Result:
case inr.inl.inr
m n : ℕ
hm : m ≠ 0
hb : 1 ≤ 1
h : ¬m = 0
⊢ log 1 n = m ↔ 1 ^ m ≤ n ∧ n < 1 ^ (m + 1)

Proof state:
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : b ≤ 1 ∨ n = 0
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
rcases hbn with (hb | rfl)

Result:
case inr.inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hm : m ≠ 0
hb : b ≤ 1
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

case inr.inr
b m : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < b ∧ 0 ≠ 0
⊢ log b 0 = m ↔ b ^ m ≤ 0 ∧ 0 < b ^ (m + 1)

Proof state:
case inr.inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hm : m ≠ 0
hb : b ≤ 1
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
obtain rfl | rfl := le_one_iff_eq_zero_or_eq_one.1 hb

Result:
case inr.inl.inl
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 0 ∧ n ≠ 0
hb : 0 ≤ 1
⊢ log 0 n = m ↔ 0 ^ m ≤ n ∧ n < 0 ^ (m + 1)

case inr.inl.inr
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 1 ∧ n ≠ 0
hb : 1 ≤ 1
⊢ log 1 n = m ↔ 1 ^ m ≤ n ∧ n < 1 ^ (m + 1)

Proof state:
case inr.inr
b m : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < b ∧ 0 ≠ 0
⊢ log b 0 = m ↔ b ^ m ≤ 0 ∧ 0 < b ^ (m + 1)

Tactic:
simp [@eq_comm _ 0, hm]

Result:
no goals

Proof state:
case inr.inl.inr
m n : ℕ
hm : m ≠ 0
hb : 1 ≤ 1
h : ¬m = 0
⊢ log 1 n = m ↔ 1 ^ m ≤ n ∧ n < 1 ^ (m + 1)

Tactic:
simp [h, eq_comm (a := 0), Nat.zero_pow (Nat.pos_iff_ne_zero.2 _)] <;> omega

Result:
no goals

Proof state:
case inr.inl.inl
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 0 ∧ n ≠ 0
hb : 0 ≤ 1
⊢ log 0 n = m ↔ 0 ^ m ≤ n ∧ n < 0 ^ (m + 1)

case inr.inl.inr
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 1 ∧ n ≠ 0
hb : 1 ≤ 1
⊢ log 1 n = m ↔ 1 ^ m ≤ n ∧ n < 1 ^ (m + 1)

Tactic:
any_goals
  simp only [ne_eq, zero_eq, reduceSucc, lt_self_iff_false,  not_lt_zero, false_and, or_false]
    at h
  simp [h, eq_comm (a := 0), Nat.zero_pow (Nat.pos_iff_ne_zero.2 _)] <;> omega

Result:
no goals

Proof state:
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬(1 < b ∧ n ≠ 0)
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
have hm : m ≠ 0 := h.resolve_right hbn

Result:
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬(1 < b ∧ n ≠ 0)
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Proof state:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
rcases em (1 < b ∧ n ≠ 0) with (⟨hb, hn⟩ | hbn)

Result:
case inl.intro
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬(1 < b ∧ n ≠ 0)
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Proof state:
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬(1 < b ∧ n ≠ 0)
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
rw [not_and_or, not_lt, Ne, not_not] at hbn

Result:
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : b ≤ 1 ∨ n = 0
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)