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 : ℕ
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 : ℤ))
⊢ clog.{u_1} (R := R) b 1 = -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₆ : Eq (α := ℤ) (↑0 : ℤ) (-(↑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]
-- 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) : ℤ))
inl₅ : Eq (α := ℤ) (↑(Nat.clog b 1) : ℤ) (-(↑0 : ℤ))
inl₆ : Eq (α := ℤ) (↑0 : ℤ) (-(↑0 : ℤ))
⊢ clog.{u_1} (R := R) b 1 = -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₇ : Eq (α := ℤ) 0 (-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]
-- 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) : ℤ))
inl₅ : Eq (α := ℤ) (↑(Nat.clog b 1) : ℤ) (-(↑0 : ℤ))
inl₆ : Eq (α := ℤ) (↑0 : ℤ) (-(↑0 : ℤ))
inl₇ : Eq (α := ℤ) 0 (-0)
⊢ clog.{u_1} (R := R) b 1 = -(↑(Nat.log b (Nat.floor.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₈ : Eq (α := ℤ) 0 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]
-- 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 ≤ 0
⊢ clog b r = 0
have rw : ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
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]
-- 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 ≤ 0
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
have inl : ∀ (hb : b ≤ 1), ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
Tactic: rcases le_or_gt b 1 with hb | 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
hr : r ≤ 0
inl : ∀ (hb : b ≤ 1), ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
have inr : ∀ (hb : 1 < b), ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
Tactic: rcases le_or_gt b 1 with hb | 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
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
have inr : ⌊r⁻¹⌋₊ ≤ 1
Tactic: refine Or.inl (lt_of_le_of_lt ?_ 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
⊢ clog b r⁻¹ = -log b r
have inl : ∀ (hrp : 0 < r), clog b r⁻¹ = -log b r
Tactic: rcases lt_or_ge 0 r with hrp | hrp
-- 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
inl : ∀ (hrp : 0 < r), clog b r⁻¹ = -log b r
⊢ clog b r⁻¹ = -log b r
have inr : ∀ (hrp : r ≤ 0), clog b r⁻¹ = -log b r
Tactic: rcases lt_or_ge 0 r with hrp | hrp
-- 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
hrp : 0 < r
⊢ clog b r⁻¹ = -log b r
have inl : ∀ (hr : 1 ≤ r), clog b r⁻¹ = -log b r
Tactic: obtain hr | hr := le_total 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 : ℕ
r : R
hrp : 0 < r
inl : ∀ (hr : 1 ≤ r), clog b r⁻¹ = -log b r
⊢ clog b r⁻¹ = -log b r
have inl₁ : ∀ (hr : r ≤ 1), clog b r⁻¹ = -log b r
Tactic: obtain hr | hr := le_total 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 : ℕ
r : R
hrp : 0 < r
hr : 1 ≤ r
⊢ clog b r⁻¹ = -log b r
have inl : -(↑(Nat.log 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]
-- 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
hrp : 0 < r
hr : 1 ≤ r
inl : -(↑(Nat.log b ⌊r⁻¹⁻¹⌋₊) : ℤ) = -log b r
⊢ clog b r⁻¹ = -log b r
have inl₁ : Eq (α := ℤ) (-(↑(Nat.log b ⌊r⁻¹⁻¹⌋₊) : ℤ)) (-(↑(Nat.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]
-- 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
hrp : 0 < r
hr : 1 ≤ r
inl : -(↑(Nat.log b ⌊r⁻¹⁻¹⌋₊) : ℤ) = -log b r
inl₁ : Eq (α := ℤ) (-(↑(Nat.log b ⌊r⁻¹⁻¹⌋₊) : ℤ)) (-(↑(Nat.log b ⌊r⌋₊) : ℤ))
⊢ clog b r⁻¹ = -log b r
have inl₂ : Eq (α := ℤ) (-(↑(Nat.log b ⌊r⌋₊) : ℤ)) (-(↑(Nat.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]
-- 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
hrp : 0 < r
hr : r ≤ 1
⊢ clog b r⁻¹ = -log b r
have inl : (↑(Nat.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]
-- 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
hrp : 0 < r
hr : r ≤ 1
inl : (↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ) = -log b r
⊢ clog b r⁻¹ = -log b r
have inl₁ : Eq (α := ℤ) (↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ) (- -(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ))
Tactic: rw [clog_of_one_le_right _ ((one_le_inv₀ hrp).2 hr), log_of_right_le_one _ hr, neg_neg]
-- 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
hrp : 0 < r
hr : r ≤ 1
inl : (↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ) = -log b r
inl₁ : Eq (α := ℤ) (↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ) (- -(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ))
⊢ clog b r⁻¹ = -log b r
have inl₂ : Eq (α := ℤ) (↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ) (↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)
Tactic: rw [clog_of_one_le_right _ ((one_le_inv₀ hrp).2 hr), log_of_right_le_one _ hr, neg_neg]
-- 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
hrp : r ≤ 0
⊢ clog b r⁻¹ = -log b r
have inr : 0 = -log b r
Tactic: rw [clog_of_right_le_zero _ (inv_nonpos.mpr hrp), log_of_right_le_zero _ hrp, 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 : ℕ
r : R
hrp : r ≤ 0
inr : 0 = -log b r
⊢ clog b r⁻¹ = -log b r
have inr₁ : Eq (α := ℤ) 0 (-0)
Tactic: rw [clog_of_right_le_zero _ (inv_nonpos.mpr hrp), log_of_right_le_zero _ hrp, 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 : ℕ
r : R
hrp : r ≤ 0
inr : 0 = -log b r
inr₁ : Eq (α := ℤ) 0 (-0)
⊢ clog b r⁻¹ = -log b r
have inr₂ : Eq (α := ℤ) 0 0
Tactic: rw [clog_of_right_le_zero _ (inv_nonpos.mpr hrp), log_of_right_le_zero _ hrp, 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 : ℕ
r : R
⊢ log b r⁻¹ = -clog b r
have rw : log b r⁻¹⁻¹⁻¹ = -clog b r⁻¹⁻¹
Tactic: rw [← inv_inv r, clog_inv, neg_neg, inv_inv]
-- 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
rw : log b r⁻¹⁻¹⁻¹ = -clog b r⁻¹⁻¹
⊢ log b r⁻¹ = -clog b r
have rw₁ : log b r⁻¹⁻¹⁻¹ = - -log b r⁻¹
Tactic: rw [← inv_inv r, clog_inv, neg_neg, inv_inv]
-- 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
rw : log b r⁻¹⁻¹⁻¹ = -clog b r⁻¹⁻¹
rw₁ : log b r⁻¹⁻¹⁻¹ = - -log b r⁻¹
⊢ log b r⁻¹ = -clog b r
have rw₂ : log b r⁻¹⁻¹⁻¹ = log b r⁻¹
Tactic: rw [← inv_inv r, clog_inv, neg_neg, inv_inv]
-- 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
rw : log b r⁻¹⁻¹⁻¹ = -clog b r⁻¹⁻¹
rw₁ : log b r⁻¹⁻¹⁻¹ = - -log b r⁻¹
rw₂ : log b r⁻¹⁻¹⁻¹ = log b r⁻¹
⊢ log b r⁻¹ = -clog b r
have rw₃ : log b r⁻¹ = log b r⁻¹
Tactic: rw [← inv_inv r, clog_inv, neg_neg, inv_inv]
-- 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
⊢ -log b r⁻¹ = clog b r
have rw : - -clog b r = clog b r
Tactic: rw [log_inv, neg_neg]
-- 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
rw : - -clog b r = clog b r
⊢ -log b r⁻¹ = clog b r
have rw₁ : clog b r = clog b r
Tactic: rw [log_inv, neg_neg]
-- 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
⊢ -clog b r⁻¹ = log b r
have rw : - -log b r = log b r
Tactic: rw [clog_inv, neg_neg]
-- 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
rw : - -log b r = log b r
⊢ -clog b r⁻¹ = log b r
have rw₁ : log b r = log b r
Tactic: rw [clog_inv, neg_neg]
-- 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 n : ℕ
⊢ clog.{u_1} (R := R) b (↑n : R) = (↑(Nat.clog b n) : ℤ)
have zero : clog.{u_1} (R := R) b (↑0 : R) = (↑(Nat.clog b 0) : ℤ)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- 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 n : ℕ
zero : clog.{u_1} (R := R) b (↑0 : R) = (↑(Nat.clog b 0) : ℤ)
⊢ clog.{u_1} (R := R) b (↑n : R) = (↑(Nat.clog b n) : ℤ)
have succ : ∀ (n : ℕ), clog.{u_1} (R := R) b (↑(n + 1) : R) = (↑(Nat.clog b (n + 1)) : ℤ)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- 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 n : ℕ
⊢ clog.{u_1} (R := R) b (↑(n + 1) : R) = (↑(Nat.clog b (n + 1)) : ℤ)
have succ : LT.lt.{u_1} (α := R) (↑(n.succ - 1) : R) (↑(n + 1) : R) ∧ LE.le.{u_1} (α := R) (↑(n + 1) : R) (↑n.succ : R)
Tactic: rw [clog_of_one_le_right, (Nat.ceil_eq_iff (Nat.succ_ne_zero n)).mpr]
-- 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 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)
⊢ clog.{u_1} (R := R) b (↑(n + 1) : R) = (↑(Nat.clog b (n + 1)) : ℤ)
have succ₁ : LE.le.{u_1} (α := R) 1 (↑(n + 1) : R)
Tactic: rw [clog_of_one_le_right, (Nat.ceil_eq_iff (Nat.succ_ne_zero n)).mpr]
-- 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 : b ≤ 1
r : R
⊢ clog b r = 0
have rw : -log b r⁻¹ = 0
Tactic: rw [← neg_log_inv_eq_clog, log_of_left_le_one hb, 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 : ℕ
hb : b ≤ 1
r : R
rw : -log b r⁻¹ = 0
⊢ clog b r = 0
have rw₁ : Eq (α := ℤ) (-0) 0
Tactic: rw [← neg_log_inv_eq_clog, log_of_left_le_one hb, 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 : ℕ
hb : b ≤ 1
r : R
rw : -log b r⁻¹ = 0
rw₁ : Eq (α := ℤ) (-0) 0
⊢ clog b r = 0
have rw₂ : Eq (α := ℤ) 0 0
Tactic: rw [← neg_log_inv_eq_clog, log_of_left_le_one hb, 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 : ℕ
hb : 1 < b
r : R
⊢ r ≤ HPow.hPow (α := R) (↑b : R) (clog b r)
have inl : ∀ (hr : r ≤ 0), r ≤ HPow.hPow (α := R) (↑b : R) (clog b r)
Tactic: rcases le_or_gt r 0 with hr | 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 : ℕ
hb : 1 < b
r : R
inl : ∀ (hr : r ≤ 0), r ≤ HPow.hPow (α := R) (↑b : R) (clog b r)
⊢ r ≤ HPow.hPow (α := R) (↑b : R) (clog b r)
have inr : ∀ (hr : 0 < r), r ≤ HPow.hPow (α := R) (↑b : R) (clog b r)
Tactic: rcases le_or_gt r 0 with hr | 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 : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ HPow.hPow (α := R) (↑b : R) (clog b r)
have inl : r ≤ 1
Tactic: rw [clog_of_right_le_zero _ hr, zpow_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 : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ r ≤ HPow.hPow (α := R) (↑b : R) (clog b r)
have inr : HPow.hPow (α := R) (↑b : R) (log b r⁻¹) ≤ r⁻¹
Tactic: rw [← neg_log_inv_eq_clog, zpow_neg, le_inv_comm₀ hr (zpow_pos ..)]
-- 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
inr : HPow.hPow (α := R) (↑b : R) (log b r⁻¹) ≤ r⁻¹
⊢ r ≤ HPow.hPow (α := R) (↑b : R) (clog b r)
have rw : LT.lt.{u_1} (α := R) 0 (↑b : R)
Tactic: rw [← neg_log_inv_eq_clog, zpow_neg, le_inv_comm₀ hr (zpow_pos ..)]
-- 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
hb : 1 < b
hr : 0 < r
⊢ HPow.hPow (α := R) (↑b : R) (clog b r - 1) < r
have rw : r⁻¹ < HPow.hPow (α := R) (↑b : R) (log b r⁻¹ + 1)
Tactic: rw [← neg_log_inv_eq_clog, ← neg_add', zpow_neg, inv_lt_comm₀ _ 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
hb : 1 < b
hr : 0 < r
rw : r⁻¹ < HPow.hPow (α := R) (↑b : R) (log b r⁻¹ + 1)
⊢ HPow.hPow (α := R) (↑b : R) (clog b r - 1) < r
have rw₁ : 0 < HPow.hPow (α := R) (↑b : R) (log b r⁻¹ + 1)
Tactic: rw [← neg_log_inv_eq_clog, ← neg_add', zpow_neg, inv_lt_comm₀ _ 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 : ℕ
⊢ clog.{u_1} (R := R) b 1 = 0
have rw : Eq (α := ℤ) (↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ) 0
Tactic: rw [clog_of_one_le_right _ le_rfl, Nat.ceil_one, Nat.clog_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.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ) 0
⊢ clog.{u_1} (R := R) b 1 = 0
have rw₁ : Eq (α := ℤ) (↑(Nat.clog b 1) : ℤ) 0
Tactic: rw [clog_of_one_le_right _ le_rfl, Nat.ceil_one, Nat.clog_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.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ) 0
rw₁ : Eq (α := ℤ) (↑(Nat.clog b 1) : ℤ) 0
⊢ clog.{u_1} (R := R) b 1 = 0
have rw₂ : Eq (α := ℤ) (↑0 : ℤ) 0
Tactic: rw [clog_of_one_le_right _ le_rfl, Nat.ceil_one, Nat.clog_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.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ) 0
rw₁ : Eq (α := ℤ) (↑(Nat.clog b 1) : ℤ) 0
rw₂ : Eq (α := ℤ) (↑0 : ℤ) 0
⊢ clog.{u_1} (R := R) b 1 = 0
have rw₃ : Eq (α := ℤ) 0 0
Tactic: rw [clog_of_one_le_right _ le_rfl, Nat.ceil_one, Nat.clog_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
⊢ clog 0 r = 0
have pos : ∀ (hr : 1 ≤ r), clog 0 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), clog 0 r = 0
⊢ clog 0 r = 0
have neg : ∀ (hr : ¬1 ≤ r), clog 0 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 : ℤ
⊢ clog b (HPow.hPow (α := R) (↑b : R) z) = z
have rw : -log b (HPow.hPow (α := R) (↑b : R) z)⁻¹ = z
Tactic: rw [← neg_log_inv_eq_clog, ← zpow_neg, log_zpow hb, neg_neg]
-- 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 : ℤ
rw : -log b (HPow.hPow (α := R) (↑b : R) z)⁻¹ = z
⊢ clog b (HPow.hPow (α := R) (↑b : R) z) = z
have rw₁ : -log b (HPow.hPow (α := R) (↑b : R) (-z)) = z
Tactic: rw [← neg_log_inv_eq_clog, ← zpow_neg, log_zpow hb, neg_neg]
-- 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 : ℤ
rw : -log b (HPow.hPow (α := R) (↑b : R) z)⁻¹ = z
rw₁ : -log b (HPow.hPow (α := R) (↑b : R) (-z)) = z
⊢ clog b (HPow.hPow (α := R) (↑b : R) z) = z
have rw₂ : - -z = z
Tactic: rw [← neg_log_inv_eq_clog, ← zpow_neg, log_zpow hb, neg_neg]
-- 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 : ℤ
rw : -log b (HPow.hPow (α := R) (↑b : R) z)⁻¹ = z
rw₁ : -log b (HPow.hPow (α := R) (↑b : R) (-z)) = z
rw₂ : - -z = z
⊢ clog b (HPow.hPow (α := R) (↑b : R) z) = z
have rw₃ : z = z
Tactic: rw [← neg_log_inv_eq_clog, ← zpow_neg, log_zpow hb, neg_neg]
-- 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₂
⊢ clog b r₁ ≤ clog 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₀' : 0 < r₂
⊢ clog b r₁ ≤ clog b r₂
have rw : log b r₂⁻¹ ≤ log b r₁⁻¹
Tactic: rw [← neg_log_inv_eq_clog, ← neg_log_inv_eq_clog, neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
a b z : ℤ
⊢ a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z]
have rw : b ≡ a [PMOD z] ↔ a ≡ b [ZMOD z]
Tactic: rw [modEq_comm]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
a b n : ℕ
⊢ HMod.hMod (α := ℤ) (↑a : ℤ) (↑n : ℤ) = HMod.hMod (α := ℤ) (↑b : ℤ) (↑n : ℤ) ↔ a % n = b % n
have rw : HMod.hMod (α := ℤ) (↑a : ℤ) (↑n : ℤ) = HMod.hMod (α := ℤ) (↑b : ℤ) (↑n : ℤ) ↔ Eq (α := ℤ) (↑(a % n) : ℤ) (↑(b % n) : ℤ)
Tactic: rw [← Int.ofNat_inj]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a : ℤ
⊢ a ≡ 0 [ZMOD n] ↔ n ∣ a
have rw : a % n = 0 % n ↔ n ∣ a
Tactic: rw [ModEq, zero_emod, dvd_iff_emod_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a : ℤ
rw : a % n = 0 % n ↔ n ∣ a
⊢ a ≡ 0 [ZMOD n] ↔ n ∣ a
have rw₁ : a % n = 0 ↔ n ∣ a
Tactic: rw [ModEq, zero_emod, dvd_iff_emod_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a : ℤ
rw : a % n = 0 % n ↔ n ∣ a
rw₁ : a % n = 0 ↔ n ∣ a
⊢ a ≡ 0 [ZMOD n] ↔ n ∣ a
have rw₂ : a % n = 0 ↔ a % n = 0
Tactic: rw [ModEq, zero_emod, dvd_iff_emod_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b : ℤ
⊢ a ≡ b [ZMOD n] ↔ n ∣ b - a
have rw : b % n = a % n ↔ n ∣ b - a
Tactic: rw [ModEq, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
a b n : ℤ
⊢ a ≡ b [ZMOD n] ↔ ∃ (t : ℤ), b = a + n * t
have rw : n ∣ b - a ↔ ∃ (t : ℤ), b = a + n * t
Tactic: rw [modEq_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD c * n]
have inl : ∀ (hc : c < 0), c * a ≡ c * b [ZMOD c * n]
Tactic: obtain hc | rfl | hc := lt_trichotomy c 0
-- Lean 4 proof step from Mathlib.Data.Int.ModEq (goal)
Goal:
n a b c : ℤ
h : a ≡ b [ZMOD n]
inl : ∀ (hc : c < 0), c * a ≡ c * b [ZMOD c * n]
⊢ c * a ≡ c * b [ZMOD c * n]
have inr : 0 * a ≡ 0 * b [ZMOD 0 * n]
Tactic: obtain hc | rfl | hc := lt_trichotomy c 0
Cleared hypotheses: c