awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.Log
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⁻¹⌉₊

Tactic:
exact Nat.pow_pred_clog_lt_self hb <| Nat.one_lt_cast.1 <| hcri.trans_le <| Nat.le_ceil _

Premises used: Nat.pow_pred_clog_lt_self, LT.lt.trans_le, Nat.one_lt_cast, Iff.mp, Nat.le_ceil
-- Module: Mathlib.Data.Int.Log
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 0 = 0

Tactic:
log_of_right_le_zero b le_rfl

Premises used: le_rfl, Int.log_of_right_le_zero
-- Module: Mathlib.Data.Int.Log
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
rw₃ rw₄ : Eq (α := ℤ) 0 0
⊢ log.{u_1} (R := R) b 1 = 0

Tactic:
rw [log_of_one_le_right _ le_rfl, Nat.floor_one, Nat.log_one_right, Int.ofNat_zero]

Premises used: Nat.log_one_right, le_rfl, Int.ofNat_zero, Int.log_of_one_le_right, Nat.floor_one
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
r : R
⊢ log 0 r = 0

Tactic:
simp only [log, Nat.log_zero_left, Nat.cast_zero, Nat.clog_zero_left, neg_zero, ite_self]

Premises used: Nat.log_zero_left, ite_self, Nat.clog_zero_left, Nat.cast_zero, neg_zero, Int.log
-- Module: Mathlib.Data.Int.Log
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
neg : ∀ (hr : ¬1 ≤ r), log 1 r = 0
⊢ log 1 r = 0

Tactic:
by_cases hr : 1 ≤ r
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
r : R
hr : 1 ≤ r
⊢ log 1 r = 0

Tactic:
simp_all only [log, ↓reduceIte, Nat.log_one_left, Nat.cast_zero]

Premises used: reduceIte, Nat.cast_zero, Nat.log_one_left, Int.log
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
r : R
hr : ¬1 ≤ r
⊢ log 1 r = 0

Tactic:
simp only [log, Nat.log_one_left, Nat.cast_zero, Nat.clog_one_left, neg_zero, ite_self]

Premises used: ite_self, Nat.clog_one_left, Nat.cast_zero, neg_zero, Nat.log_one_left, Int.log
-- Module: Mathlib.Data.Int.Log
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 : ℤ)
inr : ∀ (n : ℕ), log b (HPow.hPow (α := R) (β := ℤ) (↑b : R) (-(↑n : ℤ))) = -(↑n : ℤ)
⊢ log b (HPow.hPow (α := R) (↑b : R) z) = z

Tactic:
obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg z

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Data.Int.Log
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 : ℤ)
inl₄ inl₅ : Eq (α := ℤ) (↑n : ℤ) (↑n : ℤ)
⊢ 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]

Premises used: zpow_natCast, Nat.floor_natCast, Int.log_of_one_le_right, Nat.log_pow, Nat.cast_pow
-- Module: Mathlib.Data.Int.Log
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 : ℤ))
inr₆ inr₇ : Eq (α := ℤ) (-(↑n : ℤ)) (-(↑n : ℤ))
⊢ log 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]

Premises used: zpow_natCast, Nat.clog_pow, inv_inv, zpow_neg, Nat.ceil_natCast, Nat.cast_pow, Int.log_of_right_le_one
-- Module: Mathlib.Data.Int.Log
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₂
inr : ∀ (h₁ : 1 ≤ r₁), log b r₁ ≤ log b r₂
⊢ log b r₁ ≤ log b r₂

Tactic:
rcases le_total r₁ 1 with h₁ | h₁

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Data.Int.Log
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₂
inl₁ : ∀ (h₂ : 1 ≤ r₂), log b r₁ ≤ log b r₂
⊢ log b r₁ ≤ log b r₂

Tactic:
rcases le_total r₂ 1 with h₂ | h₂

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Data.Int.Log
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₂
inr₁ : ∀ (h₂ : 1 ≤ r₂), log b r₁ ≤ log b r₂
⊢ log b r₁ ≤ log b r₂

Tactic:
rcases le_total r₂ 1 with h₂ | h₂

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Data.Int.Log
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
⊢ 0 < r₂

Tactic:
have h₀' : 0 < r₂ := lt_of_lt_of_le h₀ h
-- Module: Mathlib.Data.Int.Log
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₂
inl : Nat.clog b ⌈r₂⁻¹⌉₊ ≤ Nat.clog b ⌈r₁⁻¹⌉₊
⊢ log b r₁ ≤ log b r₂

Tactic:
rw [log_of_right_le_one _ h₁, log_of_right_le_one _ h₂, neg_le_neg_iff, Nat.cast_le]

Premises used: Nat.cast_le, Int.log_of_right_le_one, neg_le_neg_iff
-- Module: Mathlib.Data.Int.Log
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₂
⊢ Nat.clog b ⌈r₂⁻¹⌉₊ ≤ Nat.clog b ⌈r₁⁻¹⌉₊

Tactic:
Nat.clog_mono_right b <| Nat.ceil_mono <| (inv_le_inv₀ h₀' h₀).2 h

Premises used: Iff.mpr, Nat.ceil_mono, Nat.clog_mono_right, inv_le_inv₀
-- Module: Mathlib.Data.Int.Log
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₂
⊢ Nat.clog b ⌈r₂⁻¹⌉₊ ≤ Nat.clog b ⌈r₁⁻¹⌉₊

Tactic:
exact Nat.clog_mono_right b <| Nat.ceil_mono <| (inv_le_inv₀ h₀' h₀).2 h

Premises used: Iff.mpr, Nat.ceil_mono, Nat.clog_mono_right, inv_le_inv₀
-- Module: Mathlib.Data.Int.Log
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₂
inl : LE.le (α := ℤ) (-(↑(Nat.clog b ⌈r₁⁻¹⌉₊) : ℤ)) (↑(Nat.log b ⌊r₂⌋₊) : ℤ)
⊢ log b r₁ ≤ log b r₂

Tactic:
rw [log_of_right_le_one _ h₁, log_of_one_le_right _ h₂]

Premises used: Int.log_of_one_le_right, Int.log_of_right_le_one
-- Module: Mathlib.Data.Int.Log
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₂
⊢ LE.le (α := ℤ) (-(↑(Nat.clog b ⌈r₁⁻¹⌉₊) : ℤ)) (↑(Nat.log b ⌊r₂⌋₊) : ℤ)

Tactic:
(neg_nonpos.mpr (Int.natCast_nonneg _)).trans (Int.natCast_nonneg _)

Premises used: Iff.mpr, neg_nonpos, LE.le.trans, Int.natCast_nonneg
-- Module: Mathlib.Data.Int.Log
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₂
⊢ LE.le (α := ℤ) (-(↑(Nat.clog b ⌈r₁⁻¹⌉₊) : ℤ)) (↑(Nat.log b ⌊r₂⌋₊) : ℤ)

Tactic:
exact (neg_nonpos.mpr (Int.natCast_nonneg _)).trans (Int.natCast_nonneg _)

Premises used: Iff.mpr, neg_nonpos, LE.le.trans, Int.natCast_nonneg
-- Module: Mathlib.Data.Int.Log
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
inr : ∀ (h : r₁ ≤ r₁) (h₂ : r₁ ≤ 1), log b r₁ ≤ log b r₁
⊢ log b r₁ ≤ log b r₂

Tactic:
obtain rfl := le_antisymm h (h₂.trans h₁)

Premises used: le_antisymm, LE.le.trans, rfl
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r₁ : R
h₀ : 0 < r₁
h₁ : 1 ≤ r₁
h : r₁ ≤ r₁
h₂ : r₁ ≤ 1
⊢ log b r₁ ≤ log b r₁

Tactic:
rfl
-- Module: Mathlib.Data.Int.Log
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₂
inr : Nat.log b ⌊r₁⌋₊ ≤ Nat.log b ⌊r₂⌋₊
⊢ log b r₁ ≤ log b r₂

Tactic:
rw [log_of_one_le_right _ h₁, log_of_one_le_right _ h₂, Nat.cast_le]

Premises used: Int.log_of_one_le_right, Nat.cast_le
-- Module: Mathlib.Data.Int.Log
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₂
⊢ Nat.log b ⌊r₁⌋₊ ≤ Nat.log b ⌊r₂⌋₊

Tactic:
Nat.log_mono_right (Nat.floor_mono h)

Premises used: Nat.floor_mono, Nat.log_mono_right
-- Module: Mathlib.Data.Int.Log
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₂
⊢ Nat.log b ⌊r₁⌋₊ ≤ Nat.log b ⌊r₂⌋₊

Tactic:
exact Nat.log_mono_right (Nat.floor_mono h)

Premises used: Nat.floor_mono, Nat.log_mono_right
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
x : ℤ
r : R
hr : 0 < r
⊢ r < HPow.hPow (α := R) (↑b : R) x ↔ log b r < x

Tactic:
@GaloisConnection.lt_iff_lt _ _ _ _ _ _ (zpowLogGi R hb).gc x ⟨r, hr⟩

Premises used: Int.zpowLogGi, GaloisCoinsertion.gc, GaloisConnection.lt_iff_lt
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : 1 < b
x : ℤ
r : R
hr : 0 < r
⊢ HPow.hPow (α := R) (↑b : R) x ≤ r ↔ x ≤ log b r

Tactic:
@GaloisConnection.le_iff_le _ _ _ _ _ _ (zpowLogGi R hb).gc x ⟨r, hr⟩

Premises used: Int.zpowLogGi, GaloisConnection.le_iff_le, GaloisCoinsertion.gc
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
b : ℕ
r : R
hr : 1 ≤ r
⊢ clog b r = (↑(Nat.clog b ⌈r⌉₊) : ℤ)

Tactic:
if_pos hr

Premises used: if_pos, Int.clog
-- Module: Mathlib.Data.Int.Log
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⁻¹)) : ℤ)
inr : ∀ (hr : r < 1), clog b r = -(↑(Nat.log b ⌊r⁻¹⌋₊) : ℤ)
⊢ clog b r = -(↑(Nat.log b ⌊r⁻¹⌋₊) : ℤ)

Tactic:
obtain rfl | hr := hr.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Data.Int.Log
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) : ℤ))
inl₅ : Eq (α := ℤ) (↑(Nat.clog b 1) : ℤ) (-(↑0 : ℤ))
inl₆ : Eq (α := ℤ) (↑0 : ℤ) (-(↑0 : ℤ))
inl₇ : Eq (α := ℤ) 0 (-0)
inl₈ inl₉ : Eq (α := ℤ) 0 0
⊢ clog.{u_1} (R := R) 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]

Premises used: Nat.log_one_right, inv_one, if_pos, Nat.ceil_one, Int.ofNat_zero, Nat.clog_one_right, Int.clog, Nat.floor_one, neg_zero
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
hr_1 : r ≤ 1
hr : r < 1
⊢ clog b r = -(↑(Nat.log b ⌊r⁻¹⌋₊) : ℤ)

Tactic:
if_neg hr.not_ge

Premises used: Int.clog, LT.lt.not_ge, if_neg
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
hr_1 : r ≤ 1
hr : r < 1
⊢ clog b r = -(↑(Nat.log b ⌊r⁻¹⌋₊) : ℤ)

Tactic:
exact if_neg hr.not_ge

Premises used: LT.lt.not_ge, if_neg
-- Module: Mathlib.Data.Int.Log
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 ≤ 0
rw : ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
⊢ clog b r = 0

Tactic:
rw [clog, if_neg (hr.trans_lt zero_lt_one).not_ge, neg_eq_zero, Int.natCast_eq_zero,
    Nat.log_eq_zero_iff]

Premises used: Nat.log_eq_zero_iff, neg_eq_zero, Int.natCast_eq_zero, zero_lt_one, Int.clog, LT.lt.not_ge, LE.le.trans_lt, if_neg
-- Module: Mathlib.Data.Int.Log
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 ≤ 0
inl : ∀ (hb : b ≤ 1), ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
inr : ∀ (hb : 1 < b), ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

Tactic:
rcases le_or_gt b 1 with hb | hb

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Data.Int.Log
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 ≤ 0
hb : b ≤ 1
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

Tactic:
Or.inr hb

Premises used: Or.inr
-- Module: Mathlib.Data.Int.Log
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 ≤ 0
hb : b ≤ 1
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

Tactic:
exact Or.inr hb

Premises used: Or.inr
-- Module: Mathlib.Data.Int.Log
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 ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

Tactic:
Or.inl (lt_of_le_of_lt ?_ hb)

Premises used: lt_of_le_of_lt, Or.inl
-- Module: Mathlib.Data.Int.Log
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 ≤ 0
hb : 1 < b
inr : ⌊r⁻¹⌋₊ ≤ 1
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

Tactic:
refine Or.inl (lt_of_le_of_lt ?_ hb)

Premises used: lt_of_le_of_lt, Or.inl
-- Module: Mathlib.Data.Int.Log
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 ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ ≤ 1

Tactic:
Nat.floor_le_one_of_le_one ((inv_nonpos.2 hr).trans zero_le_one)

Premises used: Iff.mpr, Nat.floor_le_one_of_le_one, zero_le_one, inv_nonpos, LE.le.trans
-- Module: Mathlib.Data.Int.Log
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 ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ ≤ 1

Tactic:
exact Nat.floor_le_one_of_le_one ((inv_nonpos.2 hr).trans zero_le_one)

Premises used: Iff.mpr, Nat.floor_le_one_of_le_one, zero_le_one, inv_nonpos, LE.le.trans
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
inl : ∀ (hrp : 0 < r), clog b r⁻¹ = -log b r
inr : ∀ (hrp : r ≤ 0), clog b r⁻¹ = -log b r
⊢ clog b r⁻¹ = -log b r

Tactic:
rcases lt_or_ge 0 r with hrp | hrp

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
inl : ∀ (hr : 1 ≤ r), clog b r⁻¹ = -log b r
inl₁ : ∀ (hr : r ≤ 1), clog b r⁻¹ = -log b r
⊢ clog b r⁻¹ = -log b r

Tactic:
obtain hr | hr := le_total 1 r

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : 1 ≤ r
inl : -(↑(Nat.log b ⌊r⁻¹⁻¹⌋₊) : ℤ) = -log b r
inl₁ : Eq (α := ℤ) (-(↑(Nat.log b ⌊r⁻¹⁻¹⌋₊) : ℤ)) (-(↑(Nat.log b ⌊r⌋₊) : ℤ))
inl₂ inl₃ : Eq (α := ℤ) (-(↑(Nat.log b ⌊r⌋₊) : ℤ)) (-(↑(Nat.log b ⌊r⌋₊) : ℤ))
⊢ clog b r⁻¹ = -log b r

Tactic:
rw [clog_of_right_le_one _ (inv_le_one_of_one_le₀ hr), log_of_one_le_right _ hr, inv_inv]

Premises used: Int.clog_of_right_le_one, Int.log_of_one_le_right, inv_inv, inv_le_one_of_one_le₀
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : r ≤ 1
inl : (↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ) = -log b r
inl₁ : Eq (α := ℤ) (↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ) (- -(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ))
inl₂ inl₃ : Eq (α := ℤ) (↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ) (↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)
⊢ clog b r⁻¹ = -log b r

Tactic:
rw [clog_of_one_le_right _ ((one_le_inv₀ hrp).2 hr), log_of_right_le_one _ hr, neg_neg]

Premises used: Iff.mpr, one_le_inv₀, neg_neg, Int.clog_of_one_le_right, Int.log_of_right_le_one
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
hrp : r ≤ 0
inr : 0 = -log b r
inr₁ : Eq (α := ℤ) 0 (-0)
inr₂ inr₃ : Eq (α := ℤ) 0 0
⊢ clog b r⁻¹ = -log b r

Tactic:
rw [clog_of_right_le_zero _ (inv_nonpos.mpr hrp), log_of_right_le_zero _ hrp, neg_zero]

Premises used: Iff.mpr, Int.log_of_right_le_zero, Int.clog_of_right_le_zero, inv_nonpos, neg_zero
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
rw : log b r⁻¹⁻¹⁻¹ = -clog b r⁻¹⁻¹
rw₁ : log b r⁻¹⁻¹⁻¹ = - -log b r⁻¹
rw₂ : log b r⁻¹⁻¹⁻¹ = log b r⁻¹
rw₃ rw₄ : log b r⁻¹ = log b r⁻¹
⊢ log b r⁻¹ = -clog b r

Tactic:
rw [← inv_inv r, clog_inv, neg_neg, inv_inv]

Premises used: neg_neg, inv_inv, Int.clog_inv
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
rw : - -clog b r = clog b r
rw₁ rw₂ : clog b r = clog b r
⊢ -log b r⁻¹ = clog b r

Tactic:
rw [log_inv, neg_neg]

Premises used: Int.log_inv, neg_neg
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
r : R
rw : - -log b r = log b r
rw₁ rw₂ : log b r = log b r
⊢ -clog b r⁻¹ = log b r

Tactic:
rw [clog_inv, neg_neg]

Premises used: neg_neg, Int.clog_inv
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b n : ℕ
zero : clog.{u_1} (R := R) b (↑0 : R) = (↑(Nat.clog b 0) : ℤ)
succ : ∀ (n : ℕ), clog.{u_1} (R := R) b (↑(n + 1) : R) = (↑(Nat.clog b (n + 1)) : ℤ)
⊢ clog.{u_1} (R := R) b (↑n : R) = (↑(Nat.clog b n) : ℤ)

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
⊢ clog.{u_1} (R := R) b (↑0 : R) = (↑(Nat.clog b 0) : ℤ)

Tactic:
simp [clog_of_right_le_one]

Premises used: Int.clog_of_right_le_one
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b n : ℕ
succ : LT.lt.{u_1} (α := R) (↑(n.succ - 1) : R) (↑(n + 1) : R) ∧ LE.le.{u_1} (α := R) (↑(n + 1) : R) (↑n.succ : R)
succ₁ : LE.le.{u_1} (α := R) 1 (↑(n + 1) : R)
⊢ clog.{u_1} (R := R) b (↑(n + 1) : R) = (↑(Nat.clog b (n + 1)) : ℤ)

Tactic:
rw [clog_of_one_le_right, (Nat.ceil_eq_iff (Nat.succ_ne_zero n)).mpr]

Premises used: Iff.mpr, Int.clog_of_one_le_right, Nat.succ_ne_zero, Nat.ceil_eq_iff
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b n : ℕ
⊢ LT.lt.{u_1} (α := R) (↑(n.succ - 1) : R) (↑(n + 1) : R) ∧ LE.le.{u_1} (α := R) (↑(n + 1) : R) (↑n.succ : R)

Tactic:
simp
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b n : ℕ
inst_4 : n.AtLeastTwo
⊢ clog.{u_1} (R := R) b (OfNat.ofNat n) = (↑(Nat.clog b (OfNat.ofNat n)) : ℤ)

Tactic:
clog_natCast b n

Premises used: Int.clog_natCast
-- Module: Mathlib.Data.Int.Log
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
rw : -log b r⁻¹ = 0
rw₁ : Eq (α := ℤ) (-0) 0
rw₂ rw₃ : Eq (α := ℤ) 0 0
⊢ clog b r = 0

Tactic:
rw [← neg_log_inv_eq_clog, log_of_left_le_one hb, neg_zero]

Premises used: Int.log_of_left_le_one, neg_zero, Int.neg_log_inv_eq_clog
-- Module: Mathlib.Data.Int.Log
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
inl : ∀ (hr : r ≤ 0), r ≤ HPow.hPow (α := R) (↑b : R) (clog b r)
inr : ∀ (hr : 0 < r), r ≤ HPow.hPow (α := R) (↑b : R) (clog b r)
⊢ r ≤ HPow.hPow (α := R) (↑b : R) (clog b r)

Tactic:
rcases le_or_gt r 0 with hr | hr

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Data.Int.Log
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 : r ≤ 0
inl : r ≤ 1
⊢ r ≤ HPow.hPow (α := R) (↑b : R) (clog b r)

Tactic:
rw [clog_of_right_le_zero _ hr, zpow_zero]

Premises used: zpow_zero, Int.clog_of_right_le_zero
-- Module: Mathlib.Data.Int.Log
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 : r ≤ 0
⊢ r ≤ 1

Tactic:
hr.trans zero_le_one

Premises used: zero_le_one, LE.le.trans
-- Module: Mathlib.Data.Int.Log
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 : r ≤ 0
⊢ r ≤ 1

Tactic:
exact hr.trans zero_le_one

Premises used: zero_le_one, LE.le.trans
-- Module: Mathlib.Data.Int.Log
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
inr : HPow.hPow (α := R) (↑b : R) (log b r⁻¹) ≤ r⁻¹
rw : LT.lt.{u_1} (α := R) 0 (↑b : R)
⊢ r ≤ HPow.hPow (α := R) (↑b : R) (clog b r)

Tactic:
rw [← neg_log_inv_eq_clog, zpow_neg, le_inv_comm₀ hr (zpow_pos ..)]

Premises used: le_inv_comm₀, zpow_pos, zpow_neg, Int.neg_log_inv_eq_clog