awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.LeastGreatest (goal)
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ (z : ℤ), P z
⊢ ∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
have let : ∀ (b : ℤ) (Hb : ∀ (z : ℤ), P z → b ≤ z), ∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
Tactic: classical
  let ⟨b, Hb⟩ := Hbdd
  let ⟨lb, H⟩ := leastOfBdd b Hb Hinh
  exact ⟨lb, H⟩
-- Lean 4 proof step from Mathlib.Data.Int.LeastGreatest (goal)
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ (z : ℤ), P z
let let₁ let₂ : ∀ (b : ℤ) (Hb : ∀ (z : ℤ), P z → b ≤ z), ∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
⊢ ∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
have let₃ : ∀ (b : ℤ) (Hb : ∀ (z : ℤ), P z → b ≤ z) (lb : ℤ) (H : P lb ∧ ∀ (z : ℤ), P z → lb ≤ z),
  ∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
Tactic: classical
  let ⟨b, Hb⟩ := Hbdd
  let ⟨lb, H⟩ := leastOfBdd b Hb Hinh
  exact ⟨lb, H⟩
-- Lean 4 proof step from Mathlib.Data.Int.LeastGreatest (goal)
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ (z : ℤ), P z
⊢ ∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
have let : ∀ (b : ℤ) (Hb : ∀ (z : ℤ), P z → z ≤ b), ∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
Tactic: let ⟨b, Hb⟩ := Hbdd
-- Lean 4 proof step from Mathlib.Data.Int.LeastGreatest (goal)
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ (z : ℤ), P z
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
⊢ ∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
have let : ∀ (lb : ℤ) (H : P lb ∧ ∀ (z : ℤ), P z → z ≤ lb), ∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
Tactic: let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh
-- Lean 4 proof step from Mathlib.Data.Int.LeastGreatest (goal)
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ (z : ℤ), P z
⊢ ∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
have let : ∀ (b : ℤ) (Hb : ∀ (z : ℤ), P z → z ≤ b), ∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
Tactic: classical
  let ⟨b, Hb⟩ := Hbdd
  let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh
  exact ⟨lb, H⟩
-- Lean 4 proof step from Mathlib.Data.Int.LeastGreatest (goal)
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ (z : ℤ), P z
let let₁ let₂ : ∀ (b : ℤ) (Hb : ∀ (z : ℤ), P z → z ≤ b), ∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
⊢ ∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
have let₃ : ∀ (b : ℤ) (Hb : ∀ (z : ℤ), P z → z ≤ b) (lb : ℤ) (H : P lb ∧ ∀ (z : ℤ), P z → z ≤ lb),
  ∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
Tactic: classical
  let ⟨b, Hb⟩ := Hbdd
  let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh
  exact ⟨lb, 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
hr : r ≤ 1
⊢ log b r = -(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)
have inl : ∀ (hr : LE.le.{u_1} (α := R) 1 1), log.{u_1} (R := R) b 1 = -(↑(Nat.clog b (Nat.ceil.{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), log.{u_1} (R := R) b 1 = -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ)
⊢ log b r = -(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)
have inr : ∀ (hr : r < 1), log b r = -(↑(Nat.clog 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
⊢ log.{u_1} (R := R) b 1 = -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl : Eq (α := ℤ)
  (if LE.le.{u_1} (α := R) 1 1 then (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ)
  else -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
  (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
Tactic: rw [log, 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.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ)
    else -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
    (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
⊢ log.{u_1} (R := R) b 1 = -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₁ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
Tactic: rw [log, 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.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ)
    else -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
    (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₁ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
⊢ log.{u_1} (R := R) b 1 = -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₂ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ))
Tactic: rw [log, 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.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ)
    else -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
    (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₁ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₂ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ))
⊢ log.{u_1} (R := R) b 1 = -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₃ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b 1) : ℤ))
Tactic: rw [log, 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.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ)
    else -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
    (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₁ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₂ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ))
inl₃ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b 1) : ℤ))
⊢ log.{u_1} (R := R) b 1 = -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₄ : Eq (α := ℤ) (↑(Nat.log b 1) : ℤ) (-(↑(Nat.clog b 1) : ℤ))
Tactic: rw [log, 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.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ)
    else -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
    (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₁ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₂ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ))
inl₃ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b 1) : ℤ))
inl₄ : Eq (α := ℤ) (↑(Nat.log b 1) : ℤ) (-(↑(Nat.clog b 1) : ℤ))
⊢ log.{u_1} (R := R) b 1 = -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₅ : Eq (α := ℤ) (↑0 : ℤ) (-(↑(Nat.clog b 1) : ℤ))
Tactic: rw [log, 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.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ)
    else -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
    (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₁ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₂ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ))
inl₃ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b 1) : ℤ))
inl₄ : Eq (α := ℤ) (↑(Nat.log b 1) : ℤ) (-(↑(Nat.clog b 1) : ℤ))
inl₅ : Eq (α := ℤ) (↑0 : ℤ) (-(↑(Nat.clog b 1) : ℤ))
⊢ log.{u_1} (R := R) b 1 = -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₆ : Eq (α := ℤ) (↑0 : ℤ) (-(↑0 : ℤ))
Tactic: rw [log, 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.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ)
    else -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
    (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₁ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₂ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ))
inl₃ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b 1) : ℤ))
inl₄ : Eq (α := ℤ) (↑(Nat.log b 1) : ℤ) (-(↑(Nat.clog b 1) : ℤ))
inl₅ : Eq (α := ℤ) (↑0 : ℤ) (-(↑(Nat.clog b 1) : ℤ))
inl₆ : Eq (α := ℤ) (↑0 : ℤ) (-(↑0 : ℤ))
⊢ log.{u_1} (R := R) b 1 = -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₇ : Eq (α := ℤ) 0 (-0)
Tactic: rw [log, 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.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ)
    else -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
    (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₁ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ))
inl₂ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1)) : ℤ))
inl₃ : Eq (α := ℤ) (↑(Nat.log b (Nat.floor.{u_1} (α := R) 1)) : ℤ) (-(↑(Nat.clog b 1) : ℤ))
inl₄ : Eq (α := ℤ) (↑(Nat.log b 1) : ℤ) (-(↑(Nat.clog b 1) : ℤ))
inl₅ : Eq (α := ℤ) (↑0 : ℤ) (-(↑(Nat.clog b 1) : ℤ))
inl₆ : Eq (α := ℤ) (↑0 : ℤ) (-(↑0 : ℤ))
inl₇ : Eq (α := ℤ) 0 (-0)
⊢ log.{u_1} (R := R) b 1 = -(↑(Nat.clog b (Nat.ceil.{u_1} (α := R) 1⁻¹)) : ℤ)
have inl₈ : Eq (α := ℤ) 0 0
Tactic: rw [log, 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 n : ℕ
⊢ log.{u_1} (R := R) b (↑n : R) = (↑(Nat.log b n) : ℤ)
have zero : log.{u_1} (R := R) b (↑0 : R) = (↑(Nat.log b 0) : ℤ)
Tactic: cases 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 : log.{u_1} (R := R) b (↑0 : R) = (↑(Nat.log b 0) : ℤ)
⊢ log.{u_1} (R := R) b (↑n : R) = (↑(Nat.log b n) : ℤ)
have succ : ∀ (n : ℕ), log.{u_1} (R := R) b (↑(n + 1) : R) = (↑(Nat.log b (n + 1)) : ℤ)
Tactic: cases 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 : ℕ
⊢ log.{u_1} (R := R) b (↑(n + 1) : R) = (↑(Nat.log b (n + 1)) : ℤ)
have succ : LE.le.{u_1} (α := R) 1 (↑(n + 1) : R)
Tactic: rw [log_of_one_le_right, Nat.floor_natCast]
-- 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
⊢ log b r = 0
have inl : ∀ (h : 1 ≤ r), log b r = 0
Tactic: rcases le_total 1 r 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 : ℕ
hb : b ≤ 1
r : R
inl : ∀ (h : 1 ≤ r), log b r = 0
⊢ log b r = 0
have inr : ∀ (h : r ≤ 1), log b r = 0
Tactic: rcases le_total 1 r 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 : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
⊢ log b r = 0
have inl : Eq (α := ℤ) (↑(Nat.log b ⌊r⌋₊) : ℤ) 0
Tactic: rw [log_of_one_le_right _ h, Nat.log_of_left_le_one hb, 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 : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
inl : Eq (α := ℤ) (↑(Nat.log b ⌊r⌋₊) : ℤ) 0
⊢ log b r = 0
have inl₁ : Eq (α := ℤ) (↑0 : ℤ) 0
Tactic: rw [log_of_one_le_right _ h, Nat.log_of_left_le_one hb, 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 : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
inl : Eq (α := ℤ) (↑(Nat.log b ⌊r⌋₊) : ℤ) 0
inl₁ : Eq (α := ℤ) (↑0 : ℤ) 0
⊢ log b r = 0
have inl₂ : Eq (α := ℤ) 0 0
Tactic: rw [log_of_one_le_right _ h, Nat.log_of_left_le_one hb, 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 : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
⊢ log b r = 0
have inr : Eq (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 0
Tactic: rw [log_of_right_le_one _ h, Nat.clog_of_left_le_one hb, 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 : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
inr : Eq (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 0
⊢ log b r = 0
have inr₁ : Eq (α := ℤ) (-(↑0 : ℤ)) 0
Tactic: rw [log_of_right_le_one _ h, Nat.clog_of_left_le_one hb, 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 : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
inr : Eq (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 0
inr₁ : Eq (α := ℤ) (-(↑0 : ℤ)) 0
⊢ log b r = 0
have inr₂ : Eq (α := ℤ) (-0) 0
Tactic: rw [log_of_right_le_one _ h, Nat.clog_of_left_le_one hb, 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 : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
inr : Eq (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 0
inr₁ : Eq (α := ℤ) (-(↑0 : ℤ)) 0
inr₂ : Eq (α := ℤ) (-0) 0
⊢ log b r = 0
have inr₃ : Eq (α := ℤ) 0 0
Tactic: rw [log_of_right_le_one _ h, Nat.clog_of_left_le_one hb, 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
⊢ log b r = 0
have rw : Eq (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 0
Tactic: rw [log_of_right_le_one _ (hr.trans zero_le_one),
    Nat.clog_of_right_le_one ((Nat.ceil_eq_zero.mpr <| inv_nonpos.2 hr).trans_le zero_le_one),
    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
rw : Eq (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 0
⊢ log b r = 0
have rw₁ : Eq (α := ℤ) (-(↑0 : ℤ)) 0
Tactic: rw [log_of_right_le_one _ (hr.trans zero_le_one),
    Nat.clog_of_right_le_one ((Nat.ceil_eq_zero.mpr <| inv_nonpos.2 hr).trans_le zero_le_one),
    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
rw : Eq (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 0
rw₁ : Eq (α := ℤ) (-(↑0 : ℤ)) 0
⊢ log b r = 0
have rw₂ : Eq (α := ℤ) (-0) 0
Tactic: rw [log_of_right_le_one _ (hr.trans zero_le_one),
    Nat.clog_of_right_le_one ((Nat.ceil_eq_zero.mpr <| inv_nonpos.2 hr).trans_le zero_le_one),
    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
rw : Eq (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 0
rw₁ : Eq (α := ℤ) (-(↑0 : ℤ)) 0
rw₂ : Eq (α := ℤ) (-0) 0
⊢ log b r = 0
have rw₃ : Eq (α := ℤ) 0 0
Tactic: rw [log_of_right_le_one _ (hr.trans zero_le_one),
    Nat.clog_of_right_le_one ((Nat.ceil_eq_zero.mpr <| inv_nonpos.2 hr).trans_le zero_le_one),
    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
hb : 1 < b
hr : 0 < r
⊢ HPow.hPow (α := R) (↑b : R) (log b r) ≤ r
have inl : ∀ (hr1 : 1 ≤ r), HPow.hPow (α := R) (↑b : R) (log b r) ≤ r
Tactic: rcases le_total 1 r with hr1 | hr1
-- 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
inl : ∀ (hr1 : 1 ≤ r), HPow.hPow (α := R) (↑b : R) (log b r) ≤ r
⊢ HPow.hPow (α := R) (↑b : R) (log b r) ≤ r
have inr : ∀ (hr1 : r ≤ 1), HPow.hPow (α := R) (↑b : R) (log b r) ≤ r
Tactic: rcases le_total 1 r with hr1 | hr1
-- 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
hr1 : 1 ≤ r
⊢ HPow.hPow (α := R) (↑b : R) (log b r) ≤ r
have inl : HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑(Nat.log b ⌊r⌋₊) : ℤ) ≤ r
Tactic: rw [log_of_one_le_right _ hr1]
-- 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
hr1 : 1 ≤ r
⊢ HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑(Nat.log b ⌊r⌋₊) : ℤ) ≤ r
have inl : b ^ Nat.log b ⌊r⌋₊ ≤ ⌊r⌋₊
Tactic: rw [zpow_natCast, ← Nat.cast_pow, ← Nat.le_floor_iff hr.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
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ HPow.hPow (α := R) (↑b : R) (log b r) ≤ r
have inr : (HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ))⁻¹ ≤ r
Tactic: rw [log_of_right_le_one _ hr1, zpow_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
r : R
⊢ r < HPow.hPow (α := R) (↑b : R) (log b r + 1)
have inl : ∀ (hr : r ≤ 0), r < HPow.hPow (α := R) (↑b : R) (log b r + 1)
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) (log b r + 1)
⊢ r < HPow.hPow (α := R) (↑b : R) (log b r + 1)
have inr : ∀ (hr : 0 < r), r < HPow.hPow (α := R) (↑b : R) (log b r + 1)
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) (log b r + 1)
have inl : r < (↑b : R)
Tactic: rw [log_of_right_le_zero _ hr, zero_add, zpow_one]
-- 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) (log b r + 1)
have inr : ∀ (hr1 : 1 ≤ r), r < HPow.hPow (α := R) (↑b : R) (log b r + 1)
Tactic: rcases le_or_gt 1 r with hr1 | hr1
-- 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 : ∀ (hr1 : 1 ≤ r), r < HPow.hPow (α := R) (↑b : R) (log b r + 1)
⊢ r < HPow.hPow (α := R) (↑b : R) (log b r + 1)
have inr₁ : ∀ (hr1 : r < 1), r < HPow.hPow (α := R) (↑b : R) (log b r + 1)
Tactic: rcases le_or_gt 1 r with hr1 | hr1
-- 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 : 1 ≤ r
⊢ r < HPow.hPow (α := R) (↑b : R) (log b r + 1)
have inr : r < HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑(Nat.log b ⌊r⌋₊).succ : ℤ)
Tactic: rw [log_of_one_le_right _ hr1, Int.ofNat_add_one_out]
-- 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
⊢ r < HPow.hPow (α := R) (↑b : R) (log b r + 1)
have inr : r < HPow.hPow (α := R) (↑b : R) (HAdd.hAdd (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 1)
Tactic: rw [log_of_right_le_one _ hr1.le]
-- 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 : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
⊢ r < HPow.hPow (α := R) (↑b : R) (HAdd.hAdd (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 1)
have hcri : 1 < r⁻¹
Tactic: have hcri : 1 < r⁻¹ := (one_lt_inv₀ hr).2 hr1
-- 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 : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
⊢ r < HPow.hPow (α := R) (↑b : R) (HAdd.hAdd (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 1)
have this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
Tactic: have : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊ :=
      Nat.succ_le_of_lt (Nat.clog_pos hb <| Nat.one_lt_cast.1 <| hcri.trans_le (Nat.le_ceil _))