no goals
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
⊢ multiplicity m n = ↑(card (Ico 1 (Part.get (multiplicity m n) (_ : multiplicity.Finite m n) + 1)))
simp
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
i : ℕ
⊢ 1 ≤ i ∧ m ^ i ∣ n ↔ (1 ≤ i ∧ m ^ i ∣ n) ∧ i < b
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
i : ℕ
⊢ i ∈ Ico 1 (Part.get (multiplicity m n) (_ : multiplicity.Finite m n) + 1) ↔ i ∈ filter (fun i => m ^ i ∣ n) (Ico 1 b)
rw [mem_filter, mem_Ico, mem_Ico, lt_succ_iff, ← @PartENat.coe_le_coe i,
  PartENat.natCast_get, ← pow_dvd_iff_le_multiplicity, and_right_comm]
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
i : ℕ
h : 1 ≤ i ∧ m ^ i ∣ n
⊢ i ≤ log m n
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
i : ℕ
⊢ 1 ≤ i ∧ m ^ i ∣ n ↔ (1 ≤ i ∧ m ^ i ∣ n) ∧ i < b
refine' (and_iff_left_of_imp fun h => lt_of_le_of_lt _ hb).symm
case zero
n b : ℕ
hn : 0 < n
i : ℕ
hm : zero ≠ 1
hb : log zero n < b
h : 1 ≤ i ∧ zero ^ i ∣ n
⊢ i ≤ log zero n

case succ
n b : ℕ
hn : 0 < n
i m : ℕ
hm : succ m ≠ 1
hb : log (succ m) n < b
h : 1 ≤ i ∧ succ m ^ i ∣ n
⊢ i ≤ log (succ m) n
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
i : ℕ
h : 1 ≤ i ∧ m ^ i ∣ n
⊢ i ≤ log m n
cases' m with m
no goals
case succ
n b : ℕ
hn : 0 < n
i m : ℕ
hm : succ m ≠ 1
hb : log (succ m) n < b
h : 1 ≤ i ∧ succ m ^ i ∣ n
⊢ i ≤ log (succ m) n
exact le_log_of_pow_le (one_lt_iff_ne_zero_and_ne_one.2 ⟨m.succ_ne_zero, hm⟩)
    (le_of_dvd hn h.2)
case zero
n b : ℕ
hn : 0 < n
i : ℕ
hm : zero ≠ 1
hb : log zero n < b
h : 1 ≤ i ∧ n = 0
⊢ i ≤ log zero n

case zero
n b : ℕ
hn : 0 < n
i : ℕ
hm : zero ≠ 1
hb : log zero n < b
h : 1 ≤ i ∧ 0 ^ i ∣ n
⊢ 0 < i
case zero
n b : ℕ
hn : 0 < n
i : ℕ
hm : zero ≠ 1
hb : log zero n < b
h : 1 ≤ i ∧ zero ^ i ∣ n
⊢ i ≤ log zero n
rw [zero_eq, zero_pow, zero_dvd_iff] at h
no goals
case zero
n b : ℕ
hn : 0 < n
i : ℕ
hm : zero ≠ 1
hb : log zero n < b
h : 1 ≤ i ∧ n = 0
⊢ i ≤ log zero n

case zero
n b : ℕ
hn : 0 < n
i : ℕ
hm : zero ≠ 1
hb : log zero n < b
h : 1 ≤ i ∧ 0 ^ i ∣ n
⊢ 0 < i
exacts [(hn.ne' h.2).elim, h.1]