awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hfu : LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) (1 : ℝ≥0)
n : ℕ
hn : HPow.hPow (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) n < r
h₁ : (f : (a : Γ₀) → ℝ≥0) (↑(u ^ n) : Γ₀) < r
⊢ ∃ (d : Γ₀ˣ), (f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀) < r

Tactic:
use u ^ n
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hfu : LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) (1 : ℝ≥0)
n : ℕ
hn : HPow.hPow (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) n < r
h₁ : (f : (a : Γ₀) → ℝ≥0) ((↑u : Γ₀) ^ n) < r
h₂ h₃ h₄ h₅ : HPow.hPow (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) n < r
⊢ (f : (a : Γ₀) → ℝ≥0) (↑(u ^ n) : Γ₀) < r

Tactic:
rwa [Units.val_pow_eq_pow_val, map_pow]

Premises used: map_pow, Units.val_pow_eq_pow_val
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ
hr : 0 < r
s : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) r ⋯
⊢ 0 < s

Tactic:
have hs : 0 < s := hr
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ
hr : 0 < r
s : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) r ⋯
hs : 0 < s
⊢ ∃ (d : Γ₀ˣ), (↑((f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀)) : ℝ) < r

Tactic:
NNReal.exists_lt_of_strictMono hf hs

Premises used: NNReal.exists_lt_of_strictMono, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ
hr : 0 < r
s : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) r ⋯
hs : 0 < s
⊢ ∃ (d : Γ₀ˣ), (↑((f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀)) : ℝ) < r

Tactic:
exact NNReal.exists_lt_of_strictMono hf hs

Premises used: NNReal.exists_lt_of_strictMono
-- Module: Mathlib.Data.NNReal.Star
Goal:
⊢ ∀ (r : ℝ≥0) (a : ℝ), star (r • a) = star r • star a

Tactic:
simp only [star_trivial, forall_const]

Premises used: TrivialStar.star_trivial, forall_const
-- Module: Mathlib.Data.Nat.Basic
Goal:
a b c d m n k : ℕ
p : ℕ → Prop
⊢ Nontrivial ℕ

Tactic:
⟨⟨0, 1, Nat.zero_ne_one⟩⟩

Premises used: Nat.zero_ne_one, Nontrivial.mk, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Basic
Goal:
⊢ Injective succ

Tactic:
@succ.inj

Premises used: Nat.succ.inj, Function.Injective
-- Module: Mathlib.Data.Nat.Basic
Goal:
a b c : ℕ
rw : a / (b * c) = a / c / b
rw₁ : a / (c * b) = a / c / b
rw₂ rw₃ : a / c / b = a / c / b
⊢ a / b / c = a / c / b

Tactic:
rw [Nat.div_div_eq_div_mul, Nat.mul_comm, ← Nat.div_div_eq_div_mul]

Premises used: Nat.mul_comm, Nat.div_div_eq_div_mul
-- Module: Mathlib.Data.Nat.Basic
Goal:
n : ℕ
hn : n ≠ 0
⊢ Injective (β := ℕ) fun (a : ℕ) ↦ a ^ n

Tactic:
simp [Injective, le_antisymm_iff, Nat.pow_le_pow_iff_left hn]

Premises used: Nat.pow_le_pow_iff_left, le_antisymm_iff, Function.Injective
-- Module: Mathlib.Data.Nat.Basic
Goal:
a : ℕ
ha : 2 ≤ a
⊢ Injective (β := ℕ) fun (x : ℕ) ↦ a ^ x

Tactic:
simp [Injective, le_antisymm_iff, Nat.pow_le_pow_iff_right ha]

Premises used: le_antisymm_iff, Nat.pow_le_pow_iff_right, Function.Injective
-- Module: Mathlib.Data.Nat.Basic
Goal:
x a : ℕ
hx : x ≠ 0
ha : a ≠ 0
rw : x ^ a / HPow.hPow (β := ℕ) x 1 = x ^ a / x
rw₁ rw₂ : x ^ a / x = x ^ a / x
⊢ x ^ (a - 1) = x ^ a / x

Tactic:
rw [← Nat.pow_div (one_le_iff_ne_zero.mpr ha) (Nat.pos_iff_ne_zero.mpr hx), Nat.pow_one]

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, Nat.pow_one, Nat.one_le_iff_ne_zero, Nat.pow_div
-- Module: Mathlib.Data.Nat.Basic
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective (α := C n) next
x y : C n
H : leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) x = leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) y
refl : ∀ (H : x = leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) y), x = y
refl₁ refl₂ refl₃ refl₄ : ∀ (H : x = y), x = y
⊢ x = y

Tactic:
rwa [leRecOn_self, leRecOn_self] at H

Premises used: Nat.leRecOn_self
-- Module: Mathlib.Data.Nat.Basic
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective (α := C n) next
m_1 : ℕ
hnm : n.le m_1
ih : Injective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
x y : C n
H : leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) x = leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) y
⊢ next (leRecOn (C := fun (x : ℕ) ↦ C x) hnm (fun {k : ℕ} ↦ next) x) =
    next (leRecOn (C := fun (x : ℕ) ↦ C x) hnm (fun {k : ℕ} ↦ next) y)

Tactic:
rw [leRecOn_succ hnm, leRecOn_succ hnm] at H

Premises used: Nat.leRecOn_succ
-- Module: Mathlib.Data.Nat.Basic
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective (α := C n) next
m_1 : ℕ
hnm : n.le m_1
ih : Injective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
x y : C n
H :
  next (leRecOn (C := fun (x : ℕ) ↦ C x) hnm (fun {k : ℕ} ↦ next) x) =
    next (leRecOn (C := fun (x : ℕ) ↦ C x) hnm (fun {k : ℕ} ↦ next) y)
⊢ x = y

Tactic:
ih (Hnext _ H)
-- Module: Mathlib.Data.Nat.Basic
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective (α := C n) next
m_1 : ℕ
hnm : n.le m_1
ih : Injective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
x y : C n
H :
  next (leRecOn (C := fun (x : ℕ) ↦ C x) hnm (fun {k : ℕ} ↦ next) x) =
    next (leRecOn (C := fun (x : ℕ) ↦ C x) hnm (fun {k : ℕ} ↦ next) y)
⊢ x = y

Tactic:
exact ih (Hnext _ H)
-- Module: Mathlib.Data.Nat.Basic
Goal:
C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective (α := C n) next
refl : Injective.{u_1, u_1} (α := C n) (leRecOn (C := C) ⋯ fun {k : ℕ} ↦ next)
step :
  ∀ {m : ℕ} (hnm : n.le m) (ih : Injective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)),
    Injective.{u_1, u_1} (α := C n) (leRecOn (C := C) ⋯ fun {k : ℕ} ↦ next)
⊢ Injective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)

Tactic:
induction hnm with
  | refl =>
    intro x y H
    rwa [leRecOn_self, leRecOn_self] at H
  | step hnm ih =>
    intro x y H
    rw [leRecOn_succ hnm, leRecOn_succ hnm] at H
    exact ih (Hnext _ H)

Premises used: Nat.leRecOn_succ, Nat.leRecOn_self, refl
-- Module: Mathlib.Data.Nat.Basic
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
x : C n
⊢ ∃ (a : C n), leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) a = x

Tactic:
⟨x, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Nat.Basic
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
x : C n
refl : leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) x = x
⊢ ∃ (a : C n), leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) a = x

Tactic:
refine ⟨x, ?_⟩
-- Module: Mathlib.Data.Nat.Basic
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
x : C n
refl refl₁ : x = x
⊢ leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) x = x

Tactic:
rw [leRecOn_self]

Premises used: Nat.leRecOn_self
-- Module: Mathlib.Data.Nat.Basic
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
m_1 : ℕ
hnm : n.le m_1
ih : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
x : C m_1.succ
step : ∀ (w : C m_1), ∃ (a : C n), leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) a = next w
⊢ ∃ (a : C n), leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) a = x

Tactic:
obtain ⟨w, rfl⟩ := Hnext _ x

Premises used: rfl
-- Module: Mathlib.Data.Nat.Basic
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
m_1 : ℕ
hnm : n.le m_1
ih : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
w : C m_1
step :
  ∀ (x : C n),
    ∃ (a : C n), leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) a = next (leRecOn (C := C) hnm (fun {k : ℕ} ↦ next) x)
⊢ ∃ (a : C n), leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) a = next w

Tactic:
obtain ⟨x, rfl⟩ := ih w

Premises used: rfl
-- Module: Mathlib.Data.Nat.Basic
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
m_1 : ℕ
hnm : n.le m_1
ih : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
x : C n
⊢ ∃ (a : C n), leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) a = next (leRecOn (C := C) hnm (fun {k : ℕ} ↦ next) x)

Tactic:
⟨x, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Nat.Basic
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
m_1 : ℕ
hnm : n.le m_1
ih : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
x : C n
step : leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) x = next (leRecOn (C := C) hnm (fun {k : ℕ} ↦ next) x)
⊢ ∃ (a : C n), leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) a = next (leRecOn (C := C) hnm (fun {k : ℕ} ↦ next) x)

Tactic:
refine ⟨x, ?_⟩
-- Module: Mathlib.Data.Nat.Basic
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
m_1 : ℕ
hnm : n.le m_1
ih : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)
x : C n
step :
  next (leRecOn (C := fun (x : ℕ) ↦ C x) hnm (fun {k : ℕ} ↦ next) x) =
    next (leRecOn (C := C) hnm (fun {k : ℕ} ↦ next) x)
step₁ : n ≤ m_1
step₂ :
  next (leRecOn (C := fun (x : ℕ) ↦ C x) hnm (fun {k : ℕ} ↦ next) x) =
    next (leRecOn (C := C) hnm (fun {k : ℕ} ↦ next) x)
step₃ : n ≤ m_1
⊢ leRecOn (C := C) ⋯ (fun {k : ℕ} ↦ next) x = next (leRecOn (C := C) hnm (fun {k : ℕ} ↦ next) x)

Tactic:
rw [leRecOn_succ]

Premises used: Nat.leRecOn_succ
-- Module: Mathlib.Data.Nat.Basic
Goal:
C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective (α := C n) next
refl : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) ⋯ fun {k : ℕ} ↦ next)
step :
  ∀ {m : ℕ} (hnm : n.le m) (ih : Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)),
    Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) ⋯ fun {k : ℕ} ↦ next)
⊢ Surjective.{u_1, u_1} (α := C n) (leRecOn (C := C) hnm fun {k : ℕ} ↦ next)

Tactic:
induction hnm with
  | refl =>
    intro x
    refine ⟨x, ?_⟩
    rw [leRecOn_self]
  | step hnm ih =>
    intro x
    obtain ⟨w, rfl⟩ := Hnext _ x
    obtain ⟨x, rfl⟩ := ih w
    refine ⟨x, ?_⟩
    rw [leRecOn_succ]

Premises used: Nat.leRecOn_succ, Nat.leRecOn_self, refl, rfl
-- Module: Mathlib.Data.Nat.Basic
Goal:
n k : ℕ
S : Set ℕ
hk : k ∈ S
h_ind : ∀ (k : ℕ), k ∈ S → k + 1 ∈ S
hnk : k ≤ n
⊢ n ∈ S

Tactic:
@leRecOn (fun n => n ∈ S) k n hnk @h_ind hk

Premises used: Nat.leRecOn
-- Module: Mathlib.Data.Nat.Basic
Goal:
S : Set ℕ
hb : 0 ∈ S
h_ind : ∀ (k : ℕ), k ∈ S → k + 1 ∈ S
n : ℕ
⊢ n ∈ S

Tactic:
set_induction_bounded hb h_ind (zero_le n)

Premises used: Nat.zero_le, Nat.set_induction_bounded
-- Module: Mathlib.Data.Nat.Basic
Goal:
⊢ Injective (β := ℕ → Prop) fun (x1 x2 : ℕ) ↦ x1 ∣ x2

Tactic:
fun _ _ h =>
  dvd_right_iff_eq.mp fun a => iff_of_eq (congr_fun h a)

Premises used: Nat.dvd_right_iff_eq, Iff.mp, Function.Injective, congr_fun, iff_of_eq
-- Module: Mathlib.Data.Nat.Basic
Goal:
n m : ℕ
inl : ∀ (h : n ≤ m), n ∣ n - m ↔ m = 0 ∨ n ≤ m
inr : ∀ (h : m < n), n ∣ n - m ↔ m = 0 ∨ n ≤ m
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
rcases le_or_gt n m with h | h

Premises used: le_or_gt
-- Module: Mathlib.Data.Nat.Basic
Goal:
n m : ℕ
h : n ≤ m
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
simp [h]
-- Module: Mathlib.Data.Nat.Basic
Goal:
n m : ℕ
h : m < n
inr : ∀ (h : 0 < n), n ∣ n - 0 ↔ Eq (α := ℕ) 0 0 ∨ n ≤ 0
inr₁ : ∀ (hm : m ≠ 0), n ∣ n - m ↔ m = 0 ∨ n ≤ m
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
rcases eq_or_ne m 0 with rfl | hm

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Basic
Goal:
n : ℕ
h : 0 < n
⊢ n ∣ n - 0 ↔ Eq (α := ℕ) 0 0 ∨ n ≤ 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Basic
Goal:
n m : ℕ
h : m < n
hm : m ≠ 0
inr : ¬n ∣ n - m
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
simp only [hm, h.not_ge, or_self, iff_false]

Premises used: iff_false, or_self, LT.lt.not_ge
-- Module: Mathlib.Data.Nat.Basic
Goal:
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ ¬n ∣ n - m

Tactic:
not_dvd_of_pos_of_lt ?_ ?_

Premises used: Nat.not_dvd_of_pos_of_lt
-- Module: Mathlib.Data.Nat.Basic
Goal:
n m : ℕ
h : m < n
hm : m ≠ 0
inr : 0 < n - m
inr₁ : n - m < n
⊢ ¬n ∣ n - m

Tactic:
refine not_dvd_of_pos_of_lt ?_ ?_

Premises used: Nat.not_dvd_of_pos_of_lt
-- Module: Mathlib.Data.Nat.Basic
Goal:
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ 0 < n - m

Tactic:
grind
-- Module: Mathlib.Data.Nat.Basic
Goal:
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ n - m < n

Tactic:
grind
-- Module: Mathlib.Data.Nat.Basic
Goal:
n m : ℕ
inl : ∀ (h : m ≤ n), n ∣ m - n ↔ n ∣ m ∨ m ≤ n
inr : ∀ (h : n < m), n ∣ m - n ↔ n ∣ m ∨ m ≤ n
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n

Tactic:
rcases le_or_gt m n with h | h

Premises used: le_or_gt
-- Module: Mathlib.Data.Nat.Basic
Goal:
n m : ℕ
h : m ≤ n
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n

Tactic:
simp [h]
-- Module: Mathlib.Data.Nat.Basic
Goal:
n m : ℕ
h : n < m
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n

Tactic:
simp [dvd_sub_iff_left (le_of_lt h) (Nat.dvd_refl _), h.not_ge]

Premises used: Nat.dvd_sub_iff_left, le_of_lt, Nat.dvd_refl, LT.lt.not_ge
-- Module: Mathlib.Data.Nat.Basic
Goal:
a : ℕ
ha : a ≠ 1
⊢ a * 0 ≤ HPow.hPow (β := ℕ) a 0

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Basic
Goal:
a : ℕ
ha : a ≠ 1
⊢ a * 0 ≤ HPow.hPow (β := ℕ) a 0

Tactic:
exact Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Basic
Goal:
a : ℕ
ha : a ≠ 1
b : ℕ
⊢ a = 0 ∨ a > 0

Tactic:
a.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.Data.Nat.Basic
Goal:
a : ℕ
ha : a ≠ 1
b : ℕ
succ : ∀ (ha : Ne (α := ℕ) 0 1), 0 * (b + 1) ≤ HPow.hPow (α := ℕ) 0 (b + 1)
succ₁ : ∀ (ha0 : a > 0), a * (b + 1) ≤ a ^ (b + 1)
⊢ a * (b + 1) ≤ a ^ (b + 1)

Tactic:
obtain rfl | ha0 : a = 0 ∨ a > 0 := a.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Basic
Goal:
b : ℕ
ha : Ne (α := ℕ) 0 1
succ : 0 ≤ HPow.hPow (α := ℕ) 0 (b + 1)
⊢ 0 * (b + 1) ≤ HPow.hPow (α := ℕ) 0 (b + 1)

Tactic:
rw [Nat.zero_mul]

Premises used: Nat.zero_mul
-- Module: Mathlib.Data.Nat.Basic
Goal:
b : ℕ
ha : Ne (α := ℕ) 0 1
⊢ 0 ≤ HPow.hPow (α := ℕ) 0 (b + 1)

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Basic
Goal:
b : ℕ
ha : Ne (α := ℕ) 0 1
⊢ 0 ≤ HPow.hPow (α := ℕ) 0 (b + 1)

Tactic:
exact Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Basic
Goal:
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
⊢ a > 1

Tactic:
have ha1 : a > 1 := Nat.lt_of_le_of_ne ha0 ha.symm
-- Module: Mathlib.Data.Nat.Basic
Goal:
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
ha1 : a > 1
succ : a * (b + 1) ≤ a * a ^ b
⊢ a * (b + 1) ≤ a ^ (b + 1)

Tactic:
rw [Nat.pow_succ']

Premises used: Nat.pow_succ'
-- Module: Mathlib.Data.Nat.Basic
Goal:
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
ha1 : a > 1
⊢ a * (b + 1) ≤ a * a ^ b

Tactic:
Nat.mul_le_mul_left a (Nat.lt_pow_self ha1)

Premises used: Nat.lt_pow_self, Nat.mul_le_mul_left
-- Module: Mathlib.Data.Nat.Basic
Goal:
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
ha1 : a > 1
⊢ a * (b + 1) ≤ a * a ^ b

Tactic:
exact Nat.mul_le_mul_left a (Nat.lt_pow_self ha1)

Premises used: Nat.lt_pow_self, Nat.mul_le_mul_left
-- Module: Mathlib.Data.Nat.Basic
Goal:
a : ℕ
ha : a ≠ 1
b : ℕ
zero : a * 0 ≤ HPow.hPow (β := ℕ) a 0
succ : ∀ (b : ℕ), a * (b + 1) ≤ a ^ (b + 1)
⊢ a * b ≤ a ^ b

Tactic:
cases b with
  | zero => exact Nat.zero_le _
  | succ b =>
      obtain rfl | ha0 : a = 0 ∨ a > 0 := a.eq_zero_or_pos
      · rw [Nat.zero_mul]; exact Nat.zero_le _
      · have ha1 : a > 1 := Nat.lt_of_le_of_ne ha0 ha.symm
        rw [Nat.pow_succ']; exact Nat.mul_le_mul_left a (Nat.lt_pow_self ha1)

Premises used: Nat.pow_succ', Nat.zero_le, Nat.zero_mul, Nat.zero, Nat.succ, Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Basic
Goal:
k : ℕ
⊢ k = 0 ∨ k > 0

Tactic:
k.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.Data.Nat.Basic
Goal:
k : ℕ
inl : 2 * HPow.hPow (α := ℕ) (β := ℕ) 0 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (HMul.hMul (α := ℕ) 2 0)
inr : ∀ (hk : k > 0), 2 * HPow.hPow (β := ℕ) k 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (2 * k)
⊢ 2 * HPow.hPow (β := ℕ) k 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (2 * k)

Tactic:
obtain rfl | hk : k = 0 ∨ k > 0 := k.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Basic
Goal:
⊢ 2 * HPow.hPow (α := ℕ) (β := ℕ) 0 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (HMul.hMul (α := ℕ) 2 0)

Tactic:
decide
-- Module: Mathlib.Data.Nat.Basic
Goal:
k : ℕ
hk : k > 0
⊢ 0 < 2 * HPow.hPow (β := ℕ) k 2

Tactic:
have hk0 : 0 < 2 * k ^ 2 := Nat.mul_pos Nat.two_pos (Nat.pow_pos hk)
-- Module: Mathlib.Data.Nat.Basic
Goal:
k : ℕ
hk : k > 0
hk0 : 0 < 2 * HPow.hPow (β := ℕ) k 2
⊢ 2 * HPow.hPow (β := ℕ) k 2 < 2 * HPow.hPow (β := ℕ) k 2 + 2 * HPow.hPow (β := ℕ) k 2

Tactic:
Nat.lt_add_of_pos_left hk0

Premises used: Nat.lt_add_of_pos_left
-- Module: Mathlib.Data.Nat.Basic
Goal:
k : ℕ
hk : k > 0
hk0 : 0 < 2 * HPow.hPow (β := ℕ) k 2
rw : 2 * HPow.hPow (β := ℕ) k 2 + 2 * HPow.hPow (β := ℕ) k 2 = HPow.hPow (α := ℕ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) k 2
rw₁ rw₂ : HAdd.hAdd (α := ℕ) 2 2 * HPow.hPow (β := ℕ) k 2 = HPow.hPow (α := ℕ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) k 2
⊢ 2 * HPow.hPow (β := ℕ) k 2 + 2 * HPow.hPow (β := ℕ) k 2 = HPow.hPow (β := ℕ) (2 * k) 2

Tactic:
rw [Nat.mul_pow, ← Nat.add_mul]

Premises used: Nat.mul_pow, Nat.add_mul
-- Module: Mathlib.Data.Nat.Basic
Goal:
k : ℕ
hk : k > 0
hk0 : 0 < 2 * HPow.hPow (β := ℕ) k 2
⊢ Ne (α := ℕ) 2 1

Tactic:
decide
-- Module: Mathlib.Data.Nat.Basic
Goal:
k : ℕ
hk : k > 0
hk0 : 0 < 2 * HPow.hPow (β := ℕ) k 2
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 k) 2 = HPow.hPow (α := ℕ) 2 (2 * k)

Tactic:
(Nat.pow_mul' _ _ _).symm

Premises used: Nat.pow_mul', Eq.symm
-- Module: Mathlib.Data.Nat.Basic
Goal:
k : ℕ
hk : k > 0
hk0 : 0 < 2 * HPow.hPow (β := ℕ) k 2
calc : 2 * HPow.hPow (β := ℕ) k 2 + 2 * HPow.hPow (β := ℕ) k 2 = HPow.hPow (β := ℕ) (2 * k) 2
⊢ 2 * HPow.hPow (β := ℕ) k 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (2 * k)

Tactic:
calc 2 * k ^ 2
      _ < 2 * k ^ 2 + 2 * k ^ 2 := Nat.lt_add_of_pos_left hk0
      _ = (2 * k) ^ 2 := by rw [Nat.mul_pow, ← Nat.add_mul]
      _ ≤ (2 ^ k) ^ 2 := Nat.pow_le_pow_left (Nat.mul_le_pow (by decide : 2 ≠ 1) _) 2
      _ = 2 ^ (2 * k) := (Nat.pow_mul' _ _ _).symm

Premises used: HMul.hMul, Nat.lt_add_of_pos_left, Nat.mul_le_pow, HPow.hPow, Nat.pow_mul', OfNat.ofNat, Eq.symm, Nat.pow_le_pow_left
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
⊢ HShiftRight.hShiftRight (β := Nat) n 1 = n / 2

Tactic:
rfl

Premises used: Nat.shiftRight, rfl
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
simp : (bif decide (n % 2 = 1) then 2 * (n / 2) + 1 else 2 * (n / 2)) = n
⊢ bit (decide (n % 2 = 1)) (HShiftRight.hShiftRight (β := Nat) n 1) = n

Tactic:
simp only [bit, shiftRight_one]

Premises used: Nat.bit, Nat.shiftRight_one
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
h : n % 2 = 0
⊢ (bif decide (n % 2 = 1) then 2 * (n / 2) + 1 else 2 * (n / 2)) = n

Tactic:
simpa [h] using Nat.div_add_mod n 2

Premises used: Nat.div_add_mod, OfNat.ofNat
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
h : n % 2 = 1
⊢ (bif decide (n % 2 = 1) then 2 * (n / 2) + 1 else 2 * (n / 2)) = n

Tactic:
simpa [h] using Nat.div_add_mod n 2

Premises used: Nat.div_add_mod, OfNat.ofNat
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
⊢ n % 2 = 0 ∨ n % 2 = 1

Tactic:
cases mod_two_eq_zero_or_one n with | _ h => simpa [h] using Nat.div_add_mod n 2

Premises used: Nat.div_add_mod, Nat.mod_two_eq_zero_or_one, OfNat.ofNat
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
⊢ bit (n.testBit 0) (HShiftRight.hShiftRight (β := Nat) n 1) = n

Tactic:
simp
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
⊢ bit false = fun (x : Nat) ↦ 2 * x

Tactic:
rfl

Premises used: cond, Nat.bit, rfl
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
⊢ bit true = fun (x : Nat) ↦ 2 * x + 1

Tactic:
rfl

Premises used: cond, Nat.bit, rfl
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
⊢ bit false n = 2 * n

Tactic:
rfl

Premises used: cond, Nat.bit, rfl
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
⊢ bit true n = 2 * n + 1

Tactic:
rfl

Premises used: cond, Nat.bit, rfl
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
b : Bool
zero : bit b 0 = 0 ↔ Eq (α := Nat) 0 0 ∧ b = false
succ : ∀ (n : Nat), bit b (n + 1) = 0 ↔ n + 1 = 0 ∧ b = false
⊢ bit b n = 0 ↔ n = 0 ∧ b = false

Tactic:
cases n
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
b : Bool
zero : bit false 0 = 0 ↔ Eq (α := Nat) 0 0 ∧ false = false
zero₁ : bit true 0 = 0 ↔ Eq (α := Nat) 0 0 ∧ true = false
⊢ bit b 0 = 0 ↔ Eq (α := Nat) 0 0 ∧ b = false

Tactic:
cases b
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
b : Bool
n : Nat
succ : bit false (n + 1) = 0 ↔ n + 1 = 0 ∧ false = false
succ₁ : bit true (n + 1) = 0 ↔ n + 1 = 0 ∧ true = false
⊢ bit b (n + 1) = 0 ↔ n + 1 = 0 ∧ b = false

Tactic:
cases b
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
⊢ bit false 0 = 0 ↔ Eq (α := Nat) 0 0 ∧ false = false

Tactic:
simp [bit, Nat.two_mul, ← Nat.add_assoc]

Premises used: Nat.bit, Nat.add_assoc, Nat.two_mul
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
⊢ bit true 0 = 0 ↔ Eq (α := Nat) 0 0 ∧ true = false

Tactic:
simp [bit, Nat.two_mul, ← Nat.add_assoc]

Premises used: Nat.bit, Nat.add_assoc, Nat.two_mul
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
⊢ bit false (n + 1) = 0 ↔ n + 1 = 0 ∧ false = false

Tactic:
simp [bit, Nat.two_mul, ← Nat.add_assoc]

Premises used: Nat.bit, Nat.add_assoc, Nat.two_mul
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
⊢ bit true (n + 1) = 0 ↔ n + 1 = 0 ∧ true = false

Tactic:
simp [bit, Nat.two_mul, ← Nat.add_assoc]

Premises used: Nat.bit, Nat.add_assoc, Nat.two_mul
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
b : Bool
⊢ bit b n ≠ 0 ↔ n = 0 → b = true

Tactic:
simp
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
b : Bool
x n : Nat
false : bit Bool.false x < HPow.hPow (α := Nat) 2 (n + 1) ↔ x < HPow.hPow (α := Nat) 2 n
true : bit Bool.true x < HPow.hPow (α := Nat) 2 (n + 1) ↔ x < HPow.hPow (α := Nat) 2 n
⊢ bit b x < HPow.hPow (α := Nat) 2 (n + 1) ↔ x < HPow.hPow (α := Nat) 2 n

Tactic:
cases b
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
x n : Nat
⊢ 2 * x < HPow.hPow (α := Nat) 2 (n + 1) ↔ x < HPow.hPow (α := Nat) 2 n

Tactic:
lia
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
x n : Nat
⊢ 2 * x + 1 < HPow.hPow (α := Nat) 2 (n + 1) ↔ x < HPow.hPow (α := Nat) 2 n

Tactic:
lia
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
hn : HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 ≠ 0
⊢ False

Tactic:
hn rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
hn : HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 ≠ 0
⊢ False

Tactic:
exact hn rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
hn : HShiftRight.hShiftRight (β := Nat) n 1 ≠ 0
⊢ LT.lt (α := Nat) 0 2

Tactic:
decide
-- Module: Mathlib.Data.Nat.BinaryRec
Goal:
n : Nat
n0 : ¬n = 0
zero :
  ∀ (n0 : ¬Eq (α := Nat) 0 0),
    (if HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1 = 0 then 0
      else (HShiftRight.hShiftRight (α := Nat) (β := Nat) 0 1).log2.succ) <
      if Eq (α := Nat) 0 0 then 0 else (log2 0).succ
succ :
  ∀ (n : Nat) (n0 : ¬n + 1 = 0),
    (if HShiftRight.hShiftRight (β := Nat) (n + 1) 1 = 0 then 0
      else (HShiftRight.hShiftRight (β := Nat) (n + 1) 1).log2.succ) <
      if n + 1 = 0 then 0 else (n + 1).log2.succ
⊢ (if HShiftRight.hShiftRight (β := Nat) n 1 = 0 then 0 else (HShiftRight.hShiftRight (β := Nat) n 1).log2.succ) <
    if n = 0 then 0 else n.log2.succ

Tactic:
obtain _ | n := n