awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.Interval
Goal:
m n : ℕ
a : ℤ
h :
  -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 ≤ a ∧ a < HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
    a = -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 ∨ a = (↑n : ℤ) ∨ -(↑m : ℤ) ≤ a ∧ a < (↑n : ℤ)
⊢ a ∈ Ico (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ↔
    Membership.mem (γ := Finset ℤ) (Ico (-(↑m : ℤ)) (↑n : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1, (↑n : ℤ)}) a

Tactic:
simp only [mem_Ico, union_insert, union_singleton, mem_insert]

Premises used: Finset.mem_insert, Finset.union_insert, Finset.union_singleton, Finset.mem_Ico
-- Module: Mathlib.Data.Int.Interval
Goal:
m n : ℕ
a : ℤ
⊢ -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 ≤ a ∧ a < HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
    a = -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 ∨ a = (↑n : ℤ) ∨ -(↑m : ℤ) ≤ a ∧ a < (↑n : ℤ)

Tactic:
omega
-- Module: Mathlib.Data.Int.Interval
Goal:
m n : ℕ
h :
  ∀ (a : ℤ),
    a ∈ Ioc (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ↔
      Membership.mem (γ := Finset ℤ) (Ioc (-(↑m : ℤ)) (↑n : ℤ) ∪ {-(↑m : ℤ), HAdd.hAdd (α := ℤ) (↑n : ℤ) 1}) a
⊢ Ioc (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    Ioc (-(↑m : ℤ)) (↑n : ℤ) ∪ {-(↑m : ℤ), HAdd.hAdd (α := ℤ) (↑n : ℤ) 1}

Tactic:
ext
-- Module: Mathlib.Data.Int.Interval
Goal:
m n : ℕ
a : ℤ
h :
  -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 < a ∧ a ≤ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
    a = -(↑m : ℤ) ∨ a = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ∨ -(↑m : ℤ) < a ∧ a ≤ (↑n : ℤ)
⊢ a ∈ Ioc (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ↔
    Membership.mem (γ := Finset ℤ) (Ioc (-(↑m : ℤ)) (↑n : ℤ) ∪ {-(↑m : ℤ), HAdd.hAdd (α := ℤ) (↑n : ℤ) 1}) a

Tactic:
simp only [mem_Ioc, union_insert, union_singleton, mem_insert]

Premises used: Finset.mem_insert, Finset.union_insert, Finset.mem_Ioc, Finset.union_singleton
-- Module: Mathlib.Data.Int.Interval
Goal:
m n : ℕ
a : ℤ
⊢ -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 < a ∧ a ≤ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
    a = -(↑m : ℤ) ∨ a = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ∨ -(↑m : ℤ) < a ∧ a ≤ (↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Int.Interval
Goal:
m n : ℕ
h :
  ∀ (a : ℤ),
    a ∈ Ioo (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ↔
      Membership.mem (γ := Finset ℤ) (Ioo (-(↑m : ℤ)) (↑n : ℤ) ∪ {-(↑m : ℤ), (↑n : ℤ)}) a
⊢ Ioo (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    Ioo (-(↑m : ℤ)) (↑n : ℤ) ∪ {-(↑m : ℤ), (↑n : ℤ)}

Tactic:
ext
-- Module: Mathlib.Data.Int.Interval
Goal:
m n : ℕ
a : ℤ
h :
  -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 < a ∧ a < HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
    a = -(↑m : ℤ) ∨ a = (↑n : ℤ) ∨ -(↑m : ℤ) < a ∧ a < (↑n : ℤ)
⊢ a ∈ Ioo (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ↔
    Membership.mem (γ := Finset ℤ) (Ioo (-(↑m : ℤ)) (↑n : ℤ) ∪ {-(↑m : ℤ), (↑n : ℤ)}) a

Tactic:
simp only [mem_Ioo, union_insert, union_singleton, mem_insert]

Premises used: Finset.mem_insert, Finset.union_insert, Finset.mem_Ioo, Finset.union_singleton
-- Module: Mathlib.Data.Int.Interval
Goal:
m n : ℕ
a : ℤ
⊢ -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 < a ∧ a < HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
    a = -(↑m : ℤ) ∨ a = (↑n : ℤ) ∨ -(↑m : ℤ) < a ∧ a < (↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
inst : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ (z : ℤ), P z
EX : ∃ (n : ℕ), P (b + (↑n : ℤ))
z : ℤ
h : P z
obtain : ∀ (n : ℕ) (h : P (b + (↑n : ℤ))), b + (↑(Nat.find (p := fun (n : ℕ) ↦ P (b + (↑n : ℤ))) EX) : ℤ) ≤ b + (↑n : ℤ)
⊢ b + (↑(Nat.find (p := fun (n : ℕ) ↦ P (b + (↑n : ℤ))) EX) : ℤ) ≤ z

Tactic:
obtain ⟨n, rfl⟩ := le.dest (Hb _ h)

Premises used: Int.le.dest, rfl
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
inst : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ (z : ℤ), P z
EX : ∃ (n : ℕ), P (b + (↑n : ℤ))
n : ℕ
h : P (b + (↑n : ℤ))
grw grw₁ : b + (↑n : ℤ) ≤ b + (↑n : ℤ)
⊢ b + (↑(Nat.find (p := fun (n : ℕ) ↦ P (b + (↑n : ℤ))) EX) : ℤ) ≤ b + (↑n : ℤ)

Tactic:
grw [Nat.find_min' EX h]

Premises used: Nat.find_min'
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
inst : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ (z : ℤ), P z
⊢ IsLeast {z : ℤ | P z} (↑(b.leastOfBdd (P := P) Hb Hinh) : ℤ)

Tactic:
(leastOfBdd b Hb Hinh).2

Premises used: lowerBounds, Set.Mem, setOf, IsLeast, Int.leastOfBdd, Subtype.property
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ (z : ℤ), P z
let : ∀ (b : ℤ) (Hb : ∀ (z : ℤ), P z → b ≤ z), ∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
⊢ ∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z

Tactic:
let ⟨b, Hb⟩ := Hbdd
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ (z : ℤ), P z
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
let : ∀ (lb : ℤ) (H : P lb ∧ ∀ (z : ℤ), P z → lb ≤ z), ∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
⊢ ∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z

Tactic:
let ⟨lb, H⟩ := leastOfBdd b Hb Hinh
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ (z : ℤ), P z
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:
⟨lb, H⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ (z : ℤ), P z
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:
exact ⟨lb, H⟩
-- Module: Mathlib.Data.Int.LeastGreatest
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
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
⊢ ∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z

Tactic:
classical
  let ⟨b, Hb⟩ := Hbdd
  let ⟨lb, H⟩ := leastOfBdd b Hb Hinh
  exact ⟨lb, H⟩
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
inst : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ (z : ℤ), P z
⊢ (↑(b.leastOfBdd (P := P) Hb Hinh) : ℤ) = (↑(b'.leastOfBdd (P := P) Hb' Hinh) : ℤ)

Tactic:
grind
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
inst : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ (z : ℤ), P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
elt : ℤ
Helt rw : P elt
⊢ P (- -elt)

Tactic:
rw [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
inst : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ (z : ℤ), P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
elt : ℤ
Helt : P elt
⊢ P elt

Tactic:
Helt
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
inst : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ (z : ℤ), P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
elt : ℤ
Helt : P elt
⊢ P elt

Tactic:
exact Helt
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
inst : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ (z : ℤ), P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
Hinh' : ∃ (z : ℤ), P (-z)
lb : ℤ
Plb : P (-lb)
al : ∀ (z : ℤ), P (-z) → lb ≤ z
z : ℤ
h rwa rwa₁ rwa₂ rwa₃ : P z
⊢ P (- -z)

Tactic:
rwa [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
inst : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ (z : ℤ), P z
⊢ IsGreatest {z : ℤ | P z} (↑(b.greatestOfBdd (P := P) Hb Hinh) : ℤ)

Tactic:
(greatestOfBdd b Hb Hinh).2

Premises used: Set.Mem, setOf, upperBounds, IsGreatest, Int.greatestOfBdd, Subtype.property
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ (z : ℤ), P z
let : ∀ (b : ℤ) (Hb : ∀ (z : ℤ), P z → z ≤ b), ∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
⊢ ∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

Tactic:
let ⟨b, Hb⟩ := Hbdd
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ (z : ℤ), P z
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
let : ∀ (lb : ℤ) (H : P lb ∧ ∀ (z : ℤ), P z → z ≤ lb), ∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
⊢ ∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

Tactic:
let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ (z : ℤ), P z
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:
⟨lb, H⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ (z : ℤ), P z
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:
exact ⟨lb, H⟩
-- Module: Mathlib.Data.Int.LeastGreatest
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
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
⊢ ∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

Tactic:
classical
  let ⟨b, Hb⟩ := Hbdd
  let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh
  exact ⟨lb, H⟩
-- Module: Mathlib.Data.Int.LeastGreatest
Goal:
P : ℤ → Prop
inst : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ (z : ℤ), P z
⊢ (↑(b.greatestOfBdd (P := P) Hb Hinh) : ℤ) = (↑(b'.greatestOfBdd (P := P) Hb' Hinh) : ℤ)

Tactic:
grind
-- 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
⊢ log b r = (↑(Nat.log b ⌊r⌋₊) : ℤ)

Tactic:
if_pos hr

Premises used: if_pos, 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 : ℕ
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⁻¹)) : ℤ)
inr : ∀ (hr : r < 1), log b r = -(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)
⊢ log b r = -(↑(Nat.clog 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.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)
inl₈ inl₉ : Eq (α := ℤ) 0 0
⊢ log.{u_1} (R := R) b 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]

Premises used: Nat.log_one_right, inv_one, if_pos, Nat.ceil_one, Int.ofNat_zero, Nat.clog_one_right, Nat.floor_one, neg_zero, 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 : ℕ
r : R
hr_1 : r ≤ 1
hr : r < 1
⊢ log b r = -(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)

Tactic:
if_neg hr.not_ge

Premises used: LT.lt.not_ge, if_neg, 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 : ℕ
r : R
hr_1 : r ≤ 1
hr : r < 1
⊢ log b r = -(↑(Nat.clog 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 n : ℕ
zero : log.{u_1} (R := R) b (↑0 : R) = (↑(Nat.log b 0) : ℤ)
succ : ∀ (n : ℕ), log.{u_1} (R := R) b (↑(n + 1) : R) = (↑(Nat.log b (n + 1)) : ℤ)
⊢ log.{u_1} (R := R) b (↑n : R) = (↑(Nat.log b n) : ℤ)

Tactic:
cases 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 : ℕ
⊢ log.{u_1} (R := R) b (↑0 : R) = (↑(Nat.log b 0) : ℤ)

Tactic:
simp [log_of_right_le_one]

Premises used: 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 n : ℕ
succ : LE.le.{u_1} (α := R) 1 (↑(n + 1) : R)
⊢ log.{u_1} (R := R) b (↑(n + 1) : R) = (↑(Nat.log b (n + 1)) : ℤ)

Tactic:
rw [log_of_one_le_right, Nat.floor_natCast]

Premises used: Nat.floor_natCast, Int.log_of_one_le_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 n : ℕ
⊢ LE.le.{u_1} (α := R) 1 (↑(n + 1) : 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
⊢ log.{u_1} (R := R) b (OfNat.ofNat n) = (↑(Nat.log b (OfNat.ofNat n)) : ℤ)

Tactic:
log_natCast b n

Premises used: Int.log_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
inl : ∀ (h : 1 ≤ r), log b r = 0
inr : ∀ (h : r ≤ 1), log b r = 0
⊢ log b r = 0

Tactic:
rcases le_total 1 r 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 : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
inl : Eq (α := ℤ) (↑(Nat.log b ⌊r⌋₊) : ℤ) 0
inl₁ : Eq (α := ℤ) (↑0 : ℤ) 0
inl₂ inl₃ : Eq (α := ℤ) 0 0
⊢ log b r = 0

Tactic:
rw [log_of_one_le_right _ h, Nat.log_of_left_le_one hb, Int.ofNat_zero]

Premises used: Int.ofNat_zero, Int.log_of_one_le_right, Nat.log_of_left_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 : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
inr : Eq (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 0
inr₁ : Eq (α := ℤ) (-(↑0 : ℤ)) 0
inr₂ : Eq (α := ℤ) (-0) 0
inr₃ inr₄ : Eq (α := ℤ) 0 0
⊢ log b r = 0

Tactic:
rw [log_of_right_le_one _ h, Nat.clog_of_left_le_one hb, Int.ofNat_zero, neg_zero]

Premises used: Int.ofNat_zero, Nat.clog_of_left_le_one, Int.log_of_right_le_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 : r ≤ 0
rw : Eq (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 0
rw₁ : Eq (α := ℤ) (-(↑0 : ℤ)) 0
rw₂ : Eq (α := ℤ) (-0) 0
rw₃ rw₄ : Eq (α := ℤ) 0 0
⊢ log 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]

Premises used: Iff.mpr, Nat.clog_of_right_le_one, Nat.ceil_eq_zero, Eq.trans_le, Int.ofNat_zero, zero_le_one, inv_nonpos, LE.le.trans, Int.log_of_right_le_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
hb : 1 < b
hr : 0 < r
inl : ∀ (hr1 : 1 ≤ r), HPow.hPow (α := R) (↑b : R) (log b r) ≤ r
inr : ∀ (hr1 : r ≤ 1), HPow.hPow (α := R) (↑b : R) (log b r) ≤ r
⊢ HPow.hPow (α := R) (↑b : R) (log b r) ≤ r

Tactic:
rcases le_total 1 r with hr1 | hr1

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
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
inl : HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑(Nat.log b ⌊r⌋₊) : ℤ) ≤ r
⊢ HPow.hPow (α := R) (↑b : R) (log b r) ≤ r

Tactic:
rw [log_of_one_le_right _ hr1]

Premises used: Int.log_of_one_le_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
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
inl : b ^ Nat.log b ⌊r⌋₊ ≤ ⌊r⌋₊
⊢ HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑(Nat.log b ⌊r⌋₊) : ℤ) ≤ r

Tactic:
rw [zpow_natCast, ← Nat.cast_pow, ← Nat.le_floor_iff hr.le]

Premises used: zpow_natCast, LT.lt.le, Nat.le_floor_iff, 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 : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ b ^ Nat.log b ⌊r⌋₊ ≤ ⌊r⌋₊

Tactic:
Nat.pow_log_le_self b (Nat.floor_pos.mpr hr1).ne'

Premises used: Iff.mpr, LT.lt.ne', Nat.pow_log_le_self, Nat.floor_pos
-- 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
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ b ^ Nat.log b ⌊r⌋₊ ≤ ⌊r⌋₊

Tactic:
exact Nat.pow_log_le_self b (Nat.floor_pos.mpr hr1).ne'

Premises used: Iff.mpr, LT.lt.ne', Nat.pow_log_le_self, Nat.floor_pos
-- 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
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
inr : (HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ))⁻¹ ≤ r
⊢ HPow.hPow (α := R) (↑b : R) (log b r) ≤ r

Tactic:
rw [log_of_right_le_one _ hr1, zpow_neg]

Premises used: zpow_neg, 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
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ (HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ))⁻¹ ≤ r

Tactic:
exact_mod_cast inv_le_of_inv_le₀ hr (Nat.ceil_le.1 <| Nat.le_pow_clog hb _)

Premises used: Nat.le_pow_clog, Iff.mp, inv_le_of_inv_le₀, Nat.ceil_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 : ℕ
hb : 1 < b
r : R
inl : ∀ (hr : r ≤ 0), r < HPow.hPow (α := R) (↑b : R) (log b r + 1)
inr : ∀ (hr : 0 < r), r < HPow.hPow (α := R) (↑b : R) (log b r + 1)
⊢ r < HPow.hPow (α := R) (↑b : R) (log b r + 1)

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 < (↑b : R)
⊢ r < HPow.hPow (α := R) (↑b : R) (log b r + 1)

Tactic:
rw [log_of_right_le_zero _ hr, zero_add, zpow_one]

Premises used: zpow_one, Int.log_of_right_le_zero, zero_add
-- 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 < (↑b : R)

Tactic:
hr.trans_lt (zero_lt_one.trans_le <| mod_cast hb.le)

Premises used: zero_lt_one, LT.lt.trans_le, LE.le.trans_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
r : R
hr : r ≤ 0
⊢ r < (↑b : R)

Tactic:
exact hr.trans_lt (zero_lt_one.trans_le <| mod_cast hb.le)

Premises used: zero_lt_one, LT.lt.trans_le, LE.le.trans_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
r : R
hr : 0 < r
inr : ∀ (hr1 : 1 ≤ r), r < HPow.hPow (α := R) (↑b : R) (log b r + 1)
inr₁ : ∀ (hr1 : r < 1), r < HPow.hPow (α := R) (↑b : R) (log b r + 1)
⊢ r < HPow.hPow (α := R) (↑b : R) (log b r + 1)

Tactic:
rcases le_or_gt 1 r with hr1 | hr1

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 : 0 < r
hr1 : 1 ≤ r
inr : r < HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑(Nat.log b ⌊r⌋₊).succ : ℤ)
⊢ r < HPow.hPow (α := R) (↑b : R) (log b r + 1)

Tactic:
rw [log_of_one_le_right _ hr1, Int.ofNat_add_one_out]

Premises used: Int.ofNat_add_one_out, Int.log_of_one_le_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
r : R
hr : 0 < r
hr1 : 1 ≤ r
⊢ r < HPow.hPow (α := R) (β := ℤ) (↑b : R) (↑(Nat.log b ⌊r⌋₊).succ : ℤ)

Tactic:
exact_mod_cast Nat.lt_of_floor_lt <| Nat.lt_pow_succ_log_self hb _

Premises used: Nat.lt_of_floor_lt, Nat.lt_pow_succ_log_self
-- 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
inr : r < HPow.hPow (α := R) (↑b : R) (HAdd.hAdd (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 1)
⊢ r < HPow.hPow (α := R) (↑b : R) (log b r + 1)

Tactic:
rw [log_of_right_le_one _ hr1.le]

Premises used: LT.lt.le, 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 : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
⊢ 1 < r⁻¹

Tactic:
have hcri : 1 < r⁻¹ := (one_lt_inv₀ hr).2 hr1
-- 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⁻¹
⊢ 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 _))
-- 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⁻¹⌉₊
inr : (↑(b ^ (Nat.clog b ⌈r⁻¹⌉₊ - 1)) : R) < r⁻¹
⊢ r < HPow.hPow (α := R) (↑b : R) (HAdd.hAdd (α := ℤ) (-(↑(Nat.clog b ⌈r⁻¹⌉₊) : ℤ)) 1)

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]

Premises used: zpow_natCast, pow_pos, neg_sub, Int.ofNat_sub, neg_add_eq_sub, lt_inv_comm₀, Int.ofNat_one, zpow_neg, 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
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⁻¹

Tactic:
Nat.lt_ceil.1 ?_

Premises used: Iff.mp, Nat.lt_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 : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
inr : b ^ (Nat.clog b ⌈r⁻¹⌉₊ - 1) < ⌈r⁻¹⌉₊
⊢ (↑(b ^ (Nat.clog b ⌈r⁻¹⌉₊ - 1)) : R) < r⁻¹

Tactic:
refine Nat.lt_ceil.1 ?_

Premises used: Iff.mp, Nat.lt_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 : ℕ
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:
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, Nat.clog, Nat.pred