awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
h : Ne (α := ℕ) 0 0
⊢ nthRoot 0 0 = 0

Tactic:
grind [nthRoot, nthRoot.go]

Premises used: Nat.nthRoot, Nat.nthRoot.go
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
h : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
⊢ (HAdd.hAdd (α := ℕ) 0 1).nthRoot 0 = 0

Tactic:
grind [nthRoot, nthRoot.go]

Premises used: Nat.nthRoot, Nat.nthRoot.go
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n : ℕ
h : n + 1 + 1 ≠ 0
⊢ (n + 1 + 1).nthRoot 0 = 0

Tactic:
grind [nthRoot, nthRoot.go]

Premises used: Nat.nthRoot, Nat.nthRoot.go
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n : ℕ
zero : nthRoot 0 1 = 1
succ : (HAdd.hAdd (α := ℕ) 0 1).nthRoot 1 = 1
succ₁ : ∀ (n : ℕ), (n + 1 + 1).nthRoot 1 = 1
⊢ n.nthRoot 1 = 1

Tactic:
rcases n with _ | _ | _
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
⊢ nthRoot 0 1 = 1

Tactic:
simp [nthRoot, nthRoot.go, Nat.add_comm 1]

Premises used: Nat.nthRoot, Nat.nthRoot.go, OfNat.ofNat, Nat.add_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
⊢ (HAdd.hAdd (α := ℕ) 0 1).nthRoot 1 = 1

Tactic:
simp [nthRoot, nthRoot.go, Nat.add_comm 1]

Premises used: Nat.nthRoot, Nat.nthRoot.go, OfNat.ofNat, Nat.add_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n : ℕ
⊢ (n + 1 + 1).nthRoot 1 = 1

Tactic:
simp [nthRoot, nthRoot.go, Nat.add_comm 1]

Premises used: Nat.nthRoot, Nat.nthRoot.go, OfNat.ofNat, Nat.add_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a guess : ℕ
hle : guess ≤ 0
⊢ guess = 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a guess : ℕ
hle : guess ≤ 0
zero : ∀ (hle : LE.le (α := ℕ) 0 0), go n a 0 0 ^ (n + 2) ≤ a
⊢ go n a 0 guess ^ (n + 2) ≤ a

Tactic:
obtain rfl : guess = 0 := by grind

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a : ℕ
hle : LE.le (α := ℕ) 0 0
⊢ go n a 0 0 ^ (n + 2) ≤ a

Tactic:
simp [go]

Premises used: Nat.nthRoot.go
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hle : guess ≤ fuel), go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
split_ifs :
  ∀ (h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess),
    go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) ^ (n + 2) ≤ a
split_ifs₁ : ∀ (h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess), guess ^ (n + 2) ≤ a
⊢ (if (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess then
        go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2))
      else guess) ^
      (n + 2) ≤
    a

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hle : guess ≤ fuel), go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) ^ (n + 2) ≤ a

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hle : guess ≤ fuel), go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) ^ (n + 2) ≤ a

Tactic:
case pos =>
      grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hle : guess ≤ fuel), go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
linarith :
  a / guess ^ (n + 1) < guess →
    -1 + ((↑a : ℤ) / HPow.hPow (α := ℤ) (↑guess : ℤ) (n + 1) + 1 - (↑guess : ℤ)) +
        ((↑guess : ℤ) * HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 -
          ((↑a : ℤ) / HPow.hPow (α := ℤ) (↑guess : ℤ) (n + 1) + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑guess : ℤ))) =
      0
⊢ guess ≤ a / guess ^ (n + 1)

Tactic:
linarith only [Nat.mul_le_of_le_div _ _ _ (not_lt.1 h)]

Premises used: not_lt, Iff.mp, Nat.mul_le_of_le_div
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hle : guess ≤ fuel), go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ guess ≤ a / guess ^ (n + 1)

Tactic:
have : guess ≤ a / guess ^ (n + 1) := by
        linarith only [Nat.mul_le_of_le_div _ _ _ (not_lt.1 h)]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hle : guess ≤ fuel), go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
this : guess ≤ a / guess ^ (n + 1)
⊢ guess * guess ^ (n + 1) ≤ a

Tactic:
replace := Nat.mul_le_of_le_div _ _ _ this
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hle : guess ≤ fuel), go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
this : guess * guess ^ (n + 1) ≤ a
⊢ guess ^ (n + 2) ≤ a

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hle : guess ≤ fuel), go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
case : guess ≤ a / guess ^ (n + 1)
case₁ : ∀ (this : guess ≤ a / guess ^ (n + 1)), guess ^ (n + 2) ≤ a
case₂ : guess ≤ a / guess ^ (n + 1)
case₃ case₄ : ∀ (this : guess ≤ a / guess ^ (n + 1)), guess ^ (n + 2) ≤ a
case₅ : ∀ (this : guess * guess ^ (n + 1) ≤ a), guess ^ (n + 2) ≤ a
⊢ guess ^ (n + 2) ≤ a

Tactic:
case neg =>
      have : guess ≤ a / guess ^ (n + 1) := by
        linarith only [Nat.mul_le_of_le_div _ _ _ (not_lt.1 h)]
      replace := Nat.mul_le_of_le_div _ _ _ this
      grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
guess fuel : ℕ
hle : guess ≤ fuel
n a : ℕ
zero : ∀ {guess : ℕ} (hle : guess ≤ 0), go n a 0 guess ^ (n + 2) ≤ a
succ :
  ∀ (fuel : ℕ) (ih : ∀ {guess : ℕ} (hle : guess ≤ fuel), go n a fuel guess ^ (n + 2) ≤ a) {guess : ℕ}
    (hle : guess ≤ fuel + 1), go n a (fuel + 1) guess ^ (n + 2) ≤ a
⊢ go n a fuel guess ^ (n + 2) ≤ a

Tactic:
induction fuel generalizing guess with
  | zero =>
    obtain rfl : guess = 0 := by grind
    simp [go]
  | succ fuel ih =>
    rw [go]
    split_ifs with h
    case pos =>
      grind
    case neg =>
      have : guess ≤ a / guess ^ (n + 1) := by
        linarith only [Nat.mul_le_of_le_div _ _ _ (not_lt.1 h)]
      replace := Nat.mul_le_of_le_div _ _ _ this
      grind

Premises used: Nat.nthRoot.go, Nat.zero, Nat.succ, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a : ℕ
zero : HPow.hPow (β := ℕ) (nthRoot 0 a) 0 ≤ a ↔ Ne (α := ℕ) 0 0 ∨ a ≠ 0
succ : (HAdd.hAdd (α := ℕ) 0 1).nthRoot a ^ HAdd.hAdd (α := ℕ) 0 1 ≤ a ↔ HAdd.hAdd (α := ℕ) 0 1 ≠ 0 ∨ a ≠ 0
succ₁ : ∀ (n : ℕ), (n + 1 + 1).nthRoot a ^ (n + 1 + 1) ≤ a ↔ n + 1 + 1 ≠ 0 ∨ a ≠ 0
⊢ n.nthRoot a ^ n ≤ a ↔ n ≠ 0 ∨ a ≠ 0

Tactic:
rcases n with _ | _ | _
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
a : ℕ
⊢ HPow.hPow (β := ℕ) (nthRoot 0 a) 0 ≤ a ↔ Ne (α := ℕ) 0 0 ∨ a ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
a : ℕ
⊢ HPow.hPow (β := ℕ) (nthRoot 0 a) 0 ≤ a ↔ Ne (α := ℕ) 0 0 ∨ a ≠ 0

Tactic:
first | grind | simp [nthRoot, nthRoot.pow_go_le]

Premises used: Nat.nthRoot, _private.0.Nat.nthRoot.pow_go_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
a : ℕ
⊢ (HAdd.hAdd (α := ℕ) 0 1).nthRoot a ^ HAdd.hAdd (α := ℕ) 0 1 ≤ a ↔ HAdd.hAdd (α := ℕ) 0 1 ≠ 0 ∨ a ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
a : ℕ
⊢ (HAdd.hAdd (α := ℕ) 0 1).nthRoot a ^ HAdd.hAdd (α := ℕ) 0 1 ≤ a ↔ HAdd.hAdd (α := ℕ) 0 1 ≠ 0 ∨ a ≠ 0

Tactic:
simp [nthRoot, nthRoot.pow_go_le]

Premises used: Nat.nthRoot, _private.0.Nat.nthRoot.pow_go_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
a : ℕ
⊢ (HAdd.hAdd (α := ℕ) 0 1).nthRoot a ^ HAdd.hAdd (α := ℕ) 0 1 ≤ a ↔ HAdd.hAdd (α := ℕ) 0 1 ≠ 0 ∨ a ≠ 0

Tactic:
first | grind | simp [nthRoot, nthRoot.pow_go_le]

Premises used: Nat.nthRoot, _private.0.Nat.nthRoot.pow_go_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
a n : ℕ
⊢ (n + 1 + 1).nthRoot a ^ (n + 1 + 1) ≤ a ↔ n + 1 + 1 ≠ 0 ∨ a ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
a n : ℕ
⊢ (n + 1 + 1).nthRoot a ^ (n + 1 + 1) ≤ a ↔ n + 1 + 1 ≠ 0 ∨ a ≠ 0

Tactic:
simp [nthRoot, nthRoot.pow_go_le]

Premises used: Nat.nthRoot, _private.0.Nat.nthRoot.pow_go_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
a n : ℕ
⊢ (n + 1 + 1).nthRoot a ^ (n + 1 + 1) ≤ a ↔ n + 1 + 1 ≠ 0 ∨ a ≠ 0

Tactic:
first | grind | simp [nthRoot, nthRoot.pow_go_le]

Premises used: Nat.nthRoot, _private.0.Nat.nthRoot.pow_go_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hb : b ≠ 0
⊢ 0 < n + 1

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hb : b ≠ 0
⊢ 0 < b ^ n

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hb : b ≠ 0
rw : (n + 1) * a * b ^ n ≤ a ^ (n + 1) + n * b * b ^ n
⊢ a ≤ (a ^ (n + 1) / b ^ n + n * b) / (n + 1)

Tactic:
rw [Nat.le_div_iff_mul_le (by positivity), Nat.mul_comm,
    ← Nat.add_mul_div_right _ _ (by positivity),
    Nat.le_div_iff_mul_le (by positivity)]

Premises used: Nat.mul_comm, Nat.add_mul_div_right, Nat.le_div_iff_mul_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hb : b ≠ 0
⊢ LE.le (α := ℤ) 0 (↑b : ℤ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hb : b ≠ 0
⊢ 0 ≤ HMul.hMul (α := ℤ) 2 (↑b : ℤ) + HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hb : b ≠ 0
⊢ HPow.hPow (α := ℤ) (↑b : ℤ) (n + 1) +
      (↑(n + 1) : ℤ) * HPow.hPow (α := ℤ) (↑b : ℤ) (n + 1 - 1) * HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ) ≤
    ((↑b : ℤ) + HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)) ^ (n + 1)

Tactic:
have := (Commute.all (b : ℤ) (a - b)).pow_add_mul_le_add_pow_of_sq_nonneg
    (by positivity) (sq_nonneg _) (sq_nonneg _) (by grind) (n + 1)
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hb : b ≠ 0
this :
  HPow.hPow (α := ℤ) (↑b : ℤ) (n + 1) +
      (↑(n + 1) : ℤ) * HPow.hPow (α := ℤ) (↑b : ℤ) (n + 1 - 1) * HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ) ≤
    ((↑b : ℤ) + HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)) ^ (n + 1)
⊢ (n + 1) * a * b ^ n ≤ a ^ (n + 1) + n * b * b ^ n

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a : ℕ
⊢ n + 1 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a : ℕ
⊢ ∃ (c : ℕ), a < (c + 1) ^ (n + 1)

Tactic:
have H : ∃ c, a < (c + 1) ^ (n + 1) := ⟨a, Nat.le_self_pow (by positivity) (a + 1)⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a : ℕ
H : ∃ (c : ℕ), a < (c + 1) ^ (n + 1)
let :
  ∀ (c : ℕ) (hc : c = Nat.find (p := fun (n_1 : ℕ) ↦ a < (n_1 + 1) ^ (n + 1)) H),
    ∃ (c : ℕ), c ^ (n + 1) ≤ a ∧ a < (c + 1) ^ (n + 1)
⊢ ∃ (c : ℕ), c ^ (n + 1) ≤ a ∧ a < (c + 1) ^ (n + 1)

Tactic:
let +nondep (eq := hc) c := Nat.find H
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a : ℕ
H : ∃ (c : ℕ), a < (c + 1) ^ (n + 1)
c : ℕ
hc : c = Nat.find (p := fun (n_1 : ℕ) ↦ a < (n_1 + 1) ^ (n + 1)) H
⊢ ∃ (c : ℕ), c ^ (n + 1) ≤ a ∧ a < (c + 1) ^ (n + 1)

Tactic:
⟨c, ?_, hc ▸ Nat.find_spec H⟩

Premises used: Eq.rec, And.intro, Exists.intro, Eq.symm, Nat.find_spec
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a : ℕ
H : ∃ (c : ℕ), a < (c + 1) ^ (n + 1)
c : ℕ
hc : c = Nat.find (p := fun (n_1 : ℕ) ↦ a < (n_1 + 1) ^ (n + 1)) H
refine : c ^ (n + 1) ≤ a
⊢ ∃ (c : ℕ), c ^ (n + 1) ≤ a ∧ a < (c + 1) ^ (n + 1)

Tactic:
refine ⟨c, ?_, hc ▸ Nat.find_spec H⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a : ℕ
H : ∃ (c : ℕ), a < (c + 1) ^ (n + 1)
hc : 0 = Nat.find (p := fun (n_1 : ℕ) ↦ a < (n_1 + 1) ^ (n + 1)) H
⊢ HPow.hPow (α := ℕ) 0 (n + 1) ≤ a

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a : ℕ
H : ∃ (c : ℕ), a < (c + 1) ^ (n + 1)
k : ℕ
hc : k + 1 = Nat.find (p := fun (n_1 : ℕ) ↦ a < (n_1 + 1) ^ (n + 1)) H
⊢ (k + 1) ^ (n + 1) ≤ a

Tactic:
simpa using Nat.find_min H hc.le

Premises used: Eq.le, Nat.find_min
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a : ℕ
H : ∃ (c : ℕ), a < (c + 1) ^ (n + 1)
c : ℕ
hc : c = Nat.find (p := fun (n_1 : ℕ) ↦ a < (n_1 + 1) ^ (n + 1)) H
zero : ∀ (hc : 0 = Nat.find (p := fun (n_1 : ℕ) ↦ a < (n_1 + 1) ^ (n + 1)) H), HPow.hPow (α := ℕ) 0 (n + 1) ≤ a
succ : ∀ (k : ℕ) (hc : k + 1 = Nat.find (p := fun (n_1 : ℕ) ↦ a < (n_1 + 1) ^ (n + 1)) H), (k + 1) ^ (n + 1) ≤ a
⊢ c ^ (n + 1) ≤ a

Tactic:
cases c with
  | zero => simp
  | succ k => simpa using Nat.find_min H hc.le

Premises used: Nat.find_min, Nat.zero, Nat.succ
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hb : b ≠ 0
have :
  ∀ (c : ℕ) (hc1 : c ^ (n + 1) ≤ a) (hc2 : a < (c + 1) ^ (n + 1)), a < ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)
⊢ a < ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)

Tactic:
have ⟨c, hc1, hc2⟩ := nthRoot.always_exists n a
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hb : b ≠ 0
c : ℕ
hc1 : c ^ (n + 1) ≤ a
hc2 : a < (c + 1) ^ (n + 1)
⊢ a < (c + 1) ^ (n + 1)

Tactic:
hc2
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hb : b ≠ 0
c : ℕ
hc1 : c ^ (n + 1) ≤ a
hc2 : a < (c + 1) ^ (n + 1)
hab : c ≤ (c ^ (n + 1) / b ^ n + n * b) / (n + 1)
⊢ (c + 1) ^ (n + 1) ≤ ((c ^ (n + 1) / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hb : b ≠ 0
c : ℕ
hc1 : c ^ (n + 1) ≤ a
hc2 : a < (c + 1) ^ (n + 1)
⊢ c ≤ (c ^ (n + 1) / b ^ n + n * b) / (n + 1)

Tactic:
nthRoot.lt_pow_go_succ_aux0 hb

Premises used: _private.0.Nat.nthRoot.lt_pow_go_succ_aux0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hb : b ≠ 0
c : ℕ
hc1 : c ^ (n + 1) ≤ a
hc2 : a < (c + 1) ^ (n + 1)
⊢ c ≤ (c ^ (n + 1) / b ^ n + n * b) / (n + 1)

Tactic:
exact nthRoot.lt_pow_go_succ_aux0 hb

Premises used: _private.0.Nat.nthRoot.lt_pow_go_succ_aux0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hb : b ≠ 0
c : ℕ
hc1 : c ^ (n + 1) ≤ a
hc2 : a < (c + 1) ^ (n + 1)
⊢ ((c ^ (n + 1) / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) ≤ ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hb : b ≠ 0
c : ℕ
hc1 : c ^ (n + 1) ≤ a
hc2 : a < (c + 1) ^ (n + 1)
calc : (c + 1) ^ (n + 1) ≤ ((c ^ (n + 1) / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)
calc₁ : ((c ^ (n + 1) / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) ≤ ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)
⊢ a < ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)

Tactic:
calc a < (c + 1) ^ (n + 1) := hc2
    _ ≤ ((c ^ (n + 1) / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) := by
      gcongr
      exact nthRoot.lt_pow_go_succ_aux0 hb
    _ ≤ ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) := by
      gcongr

Premises used: HMul.hMul, HDiv.hDiv, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
⊢ a < (go n a 0 guess + 1) ^ (n + 2)

Tactic:
simpa [go]

Premises used: Nat.nthRoot.go
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
split_ifs :
  ∀ (h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess),
    a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)
split_ifs₁ : ∀ (h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess), a < (guess + 1) ^ (n + 2)
⊢ a <
    ((if (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess then
          go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2))
        else guess) +
        1) ^
      (n + 2)

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
inl :
  ∀ (hlt : a < HAdd.hAdd (α := ℕ) 0 1 ^ (n + 2)) (h : (a / HPow.hPow (α := ℕ) 0 (n + 1) + (n + 1) * 0) / (n + 2) < 0),
    a < (go n a fuel ((a / HPow.hPow (α := ℕ) 0 (n + 1) + (n + 1) * 0) / (n + 2)) + 1) ^ (n + 2)
inr : ∀ (hguess : guess ≠ 0), a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)
⊢ a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)

Tactic:
rcases eq_or_ne guess 0 with rfl | hguess

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a fuel guess + 1) ^ (n + 2)
hlt : a < HAdd.hAdd (α := ℕ) 0 1 ^ (n + 2)
h : (a / HPow.hPow (α := ℕ) 0 (n + 1) + (n + 1) * 0) / (n + 2) < 0
⊢ a < (go n a fuel ((a / HPow.hPow (α := ℕ) 0 (n + 1) + (n + 1) * 0) / (n + 2)) + 1) ^ (n + 2)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
hguess : guess ≠ 0
⊢ a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)

Tactic:
ih <| Nat.nthRoot.lt_pow_go_succ_aux hguess

Premises used: Nat.nthRoot.lt_pow_go_succ_aux
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
hguess : guess ≠ 0
⊢ a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)

Tactic:
exact ih <| Nat.nthRoot.lt_pow_go_succ_aux hguess

Premises used: Nat.nthRoot.lt_pow_go_succ_aux
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)

Tactic:
case pos =>
      rcases eq_or_ne guess 0 with rfl | hguess
      · grind
      · exact ih <| Nat.nthRoot.lt_pow_go_succ_aux hguess

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ a < (guess + 1) ^ (n + 2)

Tactic:
assumption
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ a < (guess + 1) ^ (n + 2)

Tactic:
case neg =>
      assumption
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a guess fuel : ℕ
hlt : a < (guess + 1) ^ (n + 2)
zero : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a 0 guess + 1) ^ (n + 2)
succ :
  ∀ (fuel : ℕ) (ih : ∀ {guess : ℕ} (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a fuel guess + 1) ^ (n + 2)) {guess : ℕ}
    (hlt : a < (guess + 1) ^ (n + 2)), a < (go n a (fuel + 1) guess + 1) ^ (n + 2)
⊢ a < (go n a fuel guess + 1) ^ (n + 2)

Tactic:
induction fuel generalizing guess with
  | zero => simpa [go]
  | succ fuel ih =>
    rw [go]
    split_ifs with h
    case pos =>
      rcases eq_or_ne guess 0 with rfl | hguess
      · grind
      · exact ih <| Nat.nthRoot.lt_pow_go_succ_aux hguess
    case neg =>
      assumption

Premises used: Nat.nthRoot.go, eq_or_ne, Nat.zero, OfNat.ofNat, Nat.succ, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
h : Ne (α := ℕ) 1 0
⊢ a < HPow.hPow (β := ℕ) (nthRoot 1 a + 1) 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n_1 : ℕ
hn_1 : n_1 ≠ 0
a n : ℕ
hn : n + 2 ≠ 0
hlt : a < (a + 1) ^ (n + 2)
⊢ a < (nthRoot.go n a a a + 1) ^ (n + 2)

Tactic:
apply nthRoot.lt_pow_go_succ

Premises used: _private.0.Nat.nthRoot.lt_pow_go_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n_1 : ℕ
hn_1 : n_1 ≠ 0
a n : ℕ
hn : n + 2 ≠ 0
⊢ a < (a + 1) ^ (n + 2)

Tactic:
a.lt_succ_self.trans_le (Nat.le_self_pow hn _)

Premises used: Nat.le_self_pow, Nat.lt_succ_self, LT.lt.trans_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n_1 : ℕ
hn_1 : n_1 ≠ 0
a n : ℕ
hn : n + 2 ≠ 0
⊢ a < (a + 1) ^ (n + 2)

Tactic:
exact a.lt_succ_self.trans_le (Nat.le_self_pow hn _)

Premises used: Nat.le_self_pow, Nat.lt_succ_self, LT.lt.trans_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ a < (n.nthRoot a + 1) ^ n

Tactic:
match n, hn with
  | 1, _ => simp
  | n + 2, hn =>
    simp only [nthRoot]
    apply nthRoot.lt_pow_go_succ
    exact a.lt_succ_self.trans_le (Nat.le_self_pow hn _)
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hn : n ≠ 0
hle : a ≤ n.nthRoot b
inl : a ^ n ≤ b
⊢ a ≤ n.nthRoot b ↔ a ^ n ≤ b

Tactic:
simp only [hle, true_iff]

Premises used: true_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hn : n ≠ 0
hle : a ≤ n.nthRoot b
⊢ a ^ n ≤ b

Tactic:
le_trans ?_ (pow_nthRoot_le (.inl hn))

Premises used: Or.inl, Nat.pow_nthRoot_le, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hn : n ≠ 0
hle : a ≤ n.nthRoot b
inl : a ^ n ≤ n.nthRoot b ^ n
⊢ a ^ n ≤ b

Tactic:
refine le_trans ?_ (pow_nthRoot_le (.inl hn))

Premises used: Or.inl, Nat.pow_nthRoot_le, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hn : n ≠ 0
hle : a ≤ n.nthRoot b
⊢ a ^ n ≤ n.nthRoot b ^ n

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hn : n ≠ 0
hlt : n.nthRoot b < a
inr : b < a ^ n
⊢ a ≤ n.nthRoot b ↔ a ^ n ≤ b

Tactic:
simp only [hlt.not_ge, false_iff, not_le]

Premises used: not_le, false_iff, LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hn : n ≠ 0
hlt : n.nthRoot b < a
⊢ b < a ^ n

Tactic:
(lt_pow_nthRoot_add_one hn b).trans_le ?_

Premises used: Nat.lt_pow_nthRoot_add_one, LT.lt.trans_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hn : n ≠ 0
hlt : n.nthRoot b < a
inr : (n.nthRoot b + 1) ^ n ≤ a ^ n
⊢ b < a ^ n

Tactic:
refine (lt_pow_nthRoot_add_one hn b).trans_le ?_

Premises used: Nat.lt_pow_nthRoot_add_one, LT.lt.trans_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hn : n ≠ 0
hlt : n.nthRoot b < a
inr : n.nthRoot b + 1 ≤ a
⊢ (n.nthRoot b + 1) ^ n ≤ a ^ n

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hn : n ≠ 0
hlt : n.nthRoot b < a
⊢ n.nthRoot b + 1 ≤ a

Tactic:
assumption