awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ r < HPow.hPow (α := R) (↑b : R) (HAdd.hAdd (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 1)
have inr : (↑(b ^ (Nat.clog b ⌈r⁻¹⌉₊ - 1)) : R) < r⁻¹
Tactic: rw [neg_add_eq_sub, ← neg_sub, ← Int.ofNat_one, ← Int.ofNat_sub this, zpow_neg, zpow_natCast,
      lt_inv_comm₀ hr (pow_pos (Nat.cast_pos.mpr <| zero_lt_one.trans hb) _), ← Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ (↑(b ^ (Nat.clog b ⌈r⁻¹⌉₊ - 1)) : R) < r⁻¹
have inr : b ^ (Nat.clog b ⌈r⁻¹⌉₊ - 1) < ⌈r⁻¹⌉₊
Tactic: refine Nat.lt_ceil.1 ?_
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
⊢ log.{u_1} (R := R) b 1 = 0
have rw : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) 0
Tactic: rw [log_of_one_le_right _ le_rfl, Nat.floor_one, Nat.log_one_right, Int.ofNat_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
rw : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) 0
⊢ log.{u_1} (R := R) b 1 = 0
have rw₁ : Eq (α := ℤ) (↑(Nat.log b 1) : ℤ) 0
Tactic: rw [log_of_one_le_right _ le_rfl, Nat.floor_one, Nat.log_one_right, Int.ofNat_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
rw : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) 0
rw₁ : Eq (α := ℤ) (↑(Nat.log b 1) : ℤ) 0
⊢ log.{u_1} (R := R) b 1 = 0
have rw₂ : Eq (α := ℤ) (↑0 : ℤ) 0
Tactic: rw [log_of_one_le_right _ le_rfl, Nat.floor_one, Nat.log_one_right, Int.ofNat_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
rw : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) 0
rw₁ : Eq (α := ℤ) (↑(Nat.log b 1) : ℤ) 0
rw₂ : Eq (α := ℤ) (↑0 : ℤ) 0
⊢ log.{u_1} (R := R) b 1 = 0
have rw₃ : Eq (α := ℤ) 0 0
Tactic: rw [log_of_one_le_right _ le_rfl, Nat.floor_one, Nat.log_one_right, Int.ofNat_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
r : R
⊢ log 1 r = 0
have pos : ∀ (hr : 1 ≤ r), log 1 r = 0
Tactic: by_cases hr : 1 ≤ r
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
r : R
pos : ∀ (hr : 1 ≤ r), log 1 r = 0
⊢ log 1 r = 0
have neg : ∀ (hr : ¬1 ≤ r), log 1 r = 0
Tactic: by_cases hr : 1 ≤ r
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ log b (HPow.hPow (α := R) (↑b : R) z) = z
have inl : ∀ (n : ℕ), log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)) = (↑n : ℤ)
Tactic: obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
inl : ∀ (n : ℕ), log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)) = (↑n : ℤ)
⊢ log b (HPow.hPow (α := R) (↑b : R) z) = z
have inr : ∀ (n : ℕ), log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ))) = -(↑n : ℤ)
Tactic: obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)) = (↑n : ℤ)
have inl : Eq (α := ℤ) (↑(Nat.log b ⌊HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)⌋₊) : ℤ) (↑n : ℤ)
Tactic: rw [log_of_one_le_right _ (one_le_zpow₀ (mod_cast hb.le) <| Int.natCast_nonneg _), zpow_natCast,
      ← Nat.cast_pow, Nat.floor_natCast, Nat.log_pow hb]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
inl : Eq (α := ℤ) (↑(Nat.log b ⌊HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)⌋₊) : ℤ) (↑n : ℤ)
⊢ log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)) = (↑n : ℤ)
have inl₁ : Eq (α := ℤ) (↑(Nat.log b ⌊HPow.hPow (α := R) (↑b : R) n⌋₊) : ℤ) (↑n : ℤ)
Tactic: rw [log_of_one_le_right _ (one_le_zpow₀ (mod_cast hb.le) <| Int.natCast_nonneg _), zpow_natCast,
      ← Nat.cast_pow, Nat.floor_natCast, Nat.log_pow hb]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
inl : Eq (α := ℤ) (↑(Nat.log b ⌊HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)⌋₊) : ℤ) (↑n : ℤ)
inl₁ : Eq (α := ℤ) (↑(Nat.log b ⌊HPow.hPow (α := R) (↑b : R) n⌋₊) : ℤ) (↑n : ℤ)
⊢ log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)) = (↑n : ℤ)
have inl₂ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) (↑(b ^ n) : R))) : ℤ) (↑n : ℤ)
Tactic: rw [log_of_one_le_right _ (one_le_zpow₀ (mod_cast hb.le) <| Int.natCast_nonneg _), zpow_natCast,
      ← Nat.cast_pow, Nat.floor_natCast, Nat.log_pow hb]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
inl : Eq (α := ℤ) (↑(Nat.log b ⌊HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)⌋₊) : ℤ) (↑n : ℤ)
inl₁ : Eq (α := ℤ) (↑(Nat.log b ⌊HPow.hPow (α := R) (↑b : R) n⌋₊) : ℤ) (↑n : ℤ)
inl₂ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) (↑(b ^ n) : R))) : ℤ) (↑n : ℤ)
⊢ log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)) = (↑n : ℤ)
have inl₃ : Eq (α := ℤ) (↑(Nat.log b (b ^ n)) : ℤ) (↑n : ℤ)
Tactic: rw [log_of_one_le_right _ (one_le_zpow₀ (mod_cast hb.le) <| Int.natCast_nonneg _), zpow_natCast,
      ← Nat.cast_pow, Nat.floor_natCast, Nat.log_pow hb]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
inl : Eq (α := ℤ) (↑(Nat.log b ⌊HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)⌋₊) : ℤ) (↑n : ℤ)
inl₁ : Eq (α := ℤ) (↑(Nat.log b ⌊HPow.hPow (α := R) (↑b : R) n⌋₊) : ℤ) (↑n : ℤ)
inl₂ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) (↑(b ^ n) : R))) : ℤ) (↑n : ℤ)
inl₃ : Eq (α := ℤ) (↑(Nat.log b (b ^ n)) : ℤ) (↑n : ℤ)
⊢ log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)) = (↑n : ℤ)
have inl₄ : Eq (α := ℤ) (↑n : ℤ) (↑n : ℤ)
Tactic: rw [log_of_one_le_right _ (one_le_zpow₀ (mod_cast hb.le) <| Int.natCast_nonneg _), zpow_natCast,
      ← Nat.cast_pow, Nat.floor_natCast, Nat.log_pow hb]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ))) = -(↑n : ℤ)
have inr : Eq (α := ℤ) (-(↑(Nat.clog b ⌈(HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ)))⁻¹⌉₊) : ℤ)) (-(↑n : ℤ))
Tactic: rw [log_of_right_le_one _ (zpow_le_one_of_nonpos₀ (mod_cast hb.le) <|
      neg_nonpos.2 (Int.natCast_nonneg _)),
      zpow_neg, inv_inv, zpow_natCast, ← Nat.cast_pow, Nat.ceil_natCast, Nat.clog_pow _ _ hb]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
inr : Eq (α := ℤ) (-(↑(Nat.clog b ⌈(HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ)))⁻¹⌉₊) : ℤ)) (-(↑n : ℤ))
⊢ log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ))) = -(↑n : ℤ)
have inr₁ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈(HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ))⁻¹⁻¹⌉₊) : ℤ)) (-(↑n : ℤ))
Tactic: rw [log_of_right_le_one _ (zpow_le_one_of_nonpos₀ (mod_cast hb.le) <|
      neg_nonpos.2 (Int.natCast_nonneg _)),
      zpow_neg, inv_inv, zpow_natCast, ← Nat.cast_pow, Nat.ceil_natCast, Nat.clog_pow _ _ hb]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
inr : Eq (α := ℤ) (-(↑(Nat.clog b ⌈(HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ)))⁻¹⌉₊) : ℤ)) (-(↑n : ℤ))
inr₁ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈(HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ))⁻¹⁻¹⌉₊) : ℤ)) (-(↑n : ℤ))
⊢ log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ))) = -(↑n : ℤ)
have inr₂ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)⌉₊) : ℤ)) (-(↑n : ℤ))
Tactic: rw [log_of_right_le_one _ (zpow_le_one_of_nonpos₀ (mod_cast hb.le) <|
      neg_nonpos.2 (Int.natCast_nonneg _)),
      zpow_neg, inv_inv, zpow_natCast, ← Nat.cast_pow, Nat.ceil_natCast, Nat.clog_pow _ _ hb]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
inr : Eq (α := ℤ) (-(↑(Nat.clog b ⌈(HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ)))⁻¹⌉₊) : ℤ)) (-(↑n : ℤ))
inr₁ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈(HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ))⁻¹⁻¹⌉₊) : ℤ)) (-(↑n : ℤ))
inr₂ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)⌉₊) : ℤ)) (-(↑n : ℤ))
⊢ log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ))) = -(↑n : ℤ)
have inr₃ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈HPow.hPow (α := R) (↑b : R) n⌉₊) : ℤ)) (-(↑n : ℤ))
Tactic: rw [log_of_right_le_one _ (zpow_le_one_of_nonpos₀ (mod_cast hb.le) <|
      neg_nonpos.2 (Int.natCast_nonneg _)),
      zpow_neg, inv_inv, zpow_natCast, ← Nat.cast_pow, Nat.ceil_natCast, Nat.clog_pow _ _ hb]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
inr : Eq (α := ℤ) (-(↑(Nat.clog b ⌈(HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ)))⁻¹⌉₊) : ℤ)) (-(↑n : ℤ))
inr₁ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈(HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ))⁻¹⁻¹⌉₊) : ℤ)) (-(↑n : ℤ))
inr₂ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)⌉₊) : ℤ)) (-(↑n : ℤ))
inr₃ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈HPow.hPow (α := R) (↑b : R) n⌉₊) : ℤ)) (-(↑n : ℤ))
⊢ log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ))) = -(↑n : ℤ)
have inr₄ : Eq (α := ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) (↑(b ^ n) : R))) : ℤ)) (-(↑n : ℤ))
Tactic: rw [log_of_right_le_one _ (zpow_le_one_of_nonpos₀ (mod_cast hb.le) <|
      neg_nonpos.2 (Int.natCast_nonneg _)),
      zpow_neg, inv_inv, zpow_natCast, ← Nat.cast_pow, Nat.ceil_natCast, Nat.clog_pow _ _ hb]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
inr : Eq (α := ℤ) (-(↑(Nat.clog b ⌈(HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ)))⁻¹⌉₊) : ℤ)) (-(↑n : ℤ))
inr₁ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈(HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ))⁻¹⁻¹⌉₊) : ℤ)) (-(↑n : ℤ))
inr₂ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)⌉₊) : ℤ)) (-(↑n : ℤ))
inr₃ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈HPow.hPow (α := R) (↑b : R) n⌉₊) : ℤ)) (-(↑n : ℤ))
inr₄ : Eq (α := ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) (↑(b ^ n) : R))) : ℤ)) (-(↑n : ℤ))
⊢ log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ))) = -(↑n : ℤ)
have inr₅ : Eq (α := ℤ) (-(↑(Nat.clog b (b ^ n)) : ℤ)) (-(↑n : ℤ))
Tactic: rw [log_of_right_le_one _ (zpow_le_one_of_nonpos₀ (mod_cast hb.le) <|
      neg_nonpos.2 (Int.natCast_nonneg _)),
      zpow_neg, inv_inv, zpow_natCast, ← Nat.cast_pow, Nat.ceil_natCast, Nat.clog_pow _ _ hb]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
inr : Eq (α := ℤ) (-(↑(Nat.clog b ⌈(HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ)))⁻¹⌉₊) : ℤ)) (-(↑n : ℤ))
inr₁ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈(HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ))⁻¹⁻¹⌉₊) : ℤ)) (-(↑n : ℤ))
inr₂ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑n : ℤ)⌉₊) : ℤ)) (-(↑n : ℤ))
inr₃ : Eq (α := ℤ) (-(↑(Nat.clog b ⌈HPow.hPow (α := R) (↑b : R) n⌉₊) : ℤ)) (-(↑n : ℤ))
inr₄ : Eq (α := ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) (↑(b ^ n) : R))) : ℤ)) (-(↑n : ℤ))
inr₅ : Eq (α := ℤ) (-(↑(Nat.clog b (b ^ n)) : ℤ)) (-(↑n : ℤ))
⊢ log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ))) = -(↑n : ℤ)
have inr₆ : Eq (α := ℤ) (-(↑n : ℤ)) (-(↑n : ℤ))
Tactic: rw [log_of_right_le_one _ (zpow_le_one_of_nonpos₀ (mod_cast hb.le) <|
      neg_nonpos.2 (Int.natCast_nonneg _)),
      zpow_neg, inv_inv, zpow_natCast, ← Nat.cast_pow, Nat.ceil_natCast, Nat.clog_pow _ _ hb]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
⊢ log b r₁ ≤ log b r₂
have inl : ∀ (h₁ : r₁ ≤ 1), log b r₁ ≤ log b r₂
Tactic: rcases le_total r₁ 1 with h₁ | h₁
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
inl : ∀ (h₁ : r₁ ≤ 1), log b r₁ ≤ log b r₂
⊢ log b r₁ ≤ log b r₂
have inr : ∀ (h₁ : 1 ≤ r₁), log b r₁ ≤ log b r₂
Tactic: rcases le_total r₁ 1 with h₁ | h₁
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
⊢ log b r₁ ≤ log b r₂
have inl : ∀ (h₂ : r₂ ≤ 1), log b r₁ ≤ log b r₂
Tactic: rcases le_total r₂ 1 with h₂ | h₂
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
inl : ∀ (h₂ : r₂ ≤ 1), log b r₁ ≤ log b r₂
⊢ log b r₁ ≤ log b r₂
have inl₁ : ∀ (h₂ : 1 ≤ r₂), log b r₁ ≤ log b r₂
Tactic: rcases le_total r₂ 1 with h₂ | h₂
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
⊢ log b r₁ ≤ log b r₂
have inr : ∀ (h₂ : r₂ ≤ 1), log b r₁ ≤ log b r₂
Tactic: rcases le_total r₂ 1 with h₂ | h₂
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
inr : ∀ (h₂ : r₂ ≤ 1), log b r₁ ≤ log b r₂
⊢ log b r₁ ≤ log b r₂
have inr₁ : ∀ (h₂ : 1 ≤ r₂), log b r₁ ≤ log b r₂
Tactic: rcases le_total r₂ 1 with h₂ | h₂
-- Lean 4 proof step from Mathlib.Data.Int.Log (hypothesis)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
⊢ log b r₁ ≤ log b r₂
have h₀' : 0 < r₂
Tactic: have h₀' : 0 < r₂ := lt_of_lt_of_le h₀ h
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
h₀' : 0 < r₂
⊢ log b r₁ ≤ log b r₂
have inl : Nat.clog b ⌈r₂⁻¹⌉₊ ≤ Nat.clog b ⌈r₁⁻¹⌉₊
Tactic: rw [log_of_right_le_one _ h₁, log_of_right_le_one _ h₂, neg_le_neg_iff, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂
have inl : LE.le (α := ℤ) (-(↑(Nat.clog b ⌈r₁⁻¹⌉₊) : ℤ)) (↑(Nat.log b ⌊r₂⌋₊) : ℤ)
Tactic: rw [log_of_right_le_one _ h₁, log_of_one_le_right _ h₂]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : r₂ ≤ 1
⊢ log b r₁ ≤ log b r₂
have inr : ∀ (h : r₁ ≤ r₁) (h₂ : r₁ ≤ 1), log b r₁ ≤ log b r₁
Tactic: obtain rfl := le_antisymm h (h₂.trans h₁)
Cleared hypotheses: r₂, h, h₂
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂
have inr : Nat.log b ⌊r₁⌋₊ ≤ Nat.log b ⌊r₂⌋₊
Tactic: rw [log_of_one_le_right _ h₁, log_of_one_le_right _ h₂, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 1
⊢ clog b r = -(↑(Nat.log b ⌊r⁻¹⌋₊) : ℤ)
have inl : ∀ (hr : LE.le.{u_1} (α := R) 1 1), clog.{u_1} (R := R) b 1 = -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ)
Tactic: obtain rfl | hr := hr.eq_or_lt
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 1
inl : ∀ (hr : LE.le.{u_1} (α := R) 1 1), clog.{u_1} (R := R) b 1 = -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ)
⊢ clog b r = -(↑(Nat.log b ⌊r⁻¹⌋₊) : ℤ)
have inr : ∀ (hr : r < 1), clog b r = -(↑(Nat.log b ⌊r⁻¹⌋₊) : ℤ)
Tactic: obtain rfl | hr := hr.eq_or_lt
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hr : LE.le.{u_1} (α := R) 1 1
⊢ clog.{u_1} (R := R) b 1 = -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl : Eq (α := ℤ)
  (if LE.le.{u_1} (α := R) 1 1 then (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ)
  else -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
  (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
Tactic: rw [clog, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right,
      Nat.clog_one_right, Int.ofNat_zero, neg_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hr : LE.le.{u_1} (α := R) 1 1
inl :
  Eq (α := ℤ)
    (if LE.le.{u_1} (α := R) 1 1 then (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ)
    else -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
    (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
⊢ clog.{u_1} (R := R) b 1 = -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₁ : Eq (α := ℤ) (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
Tactic: rw [clog, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right,
      Nat.clog_one_right, Int.ofNat_zero, neg_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hr : LE.le.{u_1} (α := R) 1 1
inl :
  Eq (α := ℤ)
    (if LE.le.{u_1} (α := R) 1 1 then (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ)
    else -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
    (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₁ : Eq (α := ℤ) (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
⊢ clog.{u_1} (R := R) b 1 = -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₂ : Eq (α := ℤ) (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ))
Tactic: rw [clog, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right,
      Nat.clog_one_right, Int.ofNat_zero, neg_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hr : LE.le.{u_1} (α := R) 1 1
inl :
  Eq (α := ℤ)
    (if LE.le.{u_1} (α := R) 1 1 then (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ)
    else -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
    (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₁ : Eq (α := ℤ) (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₂ : Eq (α := ℤ) (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ))
⊢ clog.{u_1} (R := R) b 1 = -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₃ : Eq (α := ℤ) (↑(Nat.clog b 1) : ℤ) (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ))
Tactic: rw [clog, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right,
      Nat.clog_one_right, Int.ofNat_zero, neg_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hr : LE.le.{u_1} (α := R) 1 1
inl :
  Eq (α := ℤ)
    (if LE.le.{u_1} (α := R) 1 1 then (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ)
    else -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
    (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₁ : Eq (α := ℤ) (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₂ : Eq (α := ℤ) (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ))
inl₃ : Eq (α := ℤ) (↑(Nat.clog b 1) : ℤ) (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ))
⊢ clog.{u_1} (R := R) b 1 = -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₄ : Eq (α := ℤ) (↑(Nat.clog b 1) : ℤ) (-(↑(Nat.log b 1) : ℤ))
Tactic: rw [clog, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right,
      Nat.clog_one_right, Int.ofNat_zero, neg_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Log (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hr : LE.le.{u_1} (α := R) 1 1
inl :
  Eq (α := ℤ)
    (if LE.le.{u_1} (α := R) 1 1 then (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ)
    else -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
    (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₁ : Eq (α := ℤ) (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₂ : Eq (α := ℤ) (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ))
inl₃ : Eq (α := ℤ) (↑(Nat.clog b 1) : ℤ) (-(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ))
inl₄ : Eq (α := ℤ) (↑(Nat.clog b 1) : ℤ) (-(↑(Nat.log b 1) : ℤ))
⊢ clog.{u_1} (R := R) b 1 = -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₅ : Eq (α := ℤ) (↑(Nat.clog b 1) : ℤ) (-(↑0 : ℤ))
Tactic: rw [clog, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right,
      Nat.clog_one_right, Int.ofNat_zero, neg_zero]