awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
pos :
  ∀ (hr : 0 < r),
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
      (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
have neg : ∀ (hr : r ≤ 0),
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
Tactic: by_cases! hr : 0 < r
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hr : 0 < r
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
have pos : -1 < HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α
Tactic: rw [intervalIntegral.integrableOn_Ioo_rpow_iff hr]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hr : 0 < r
⊢ -1 < HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α
have linarith : HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α ≤ -1 →
  α - (↑(Module.finrank ℝ E) : ℝ) + (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α - -1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (hypothesis)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α))) (Ioo 0 r) volume
have h_rpow : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
  (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
Tactic: have h_rpow : IntegrableOn (fun y ↦ y ^ ((Module.finrank ℝ E : ℝ) - 1 - α)) (Ioo 0 r) := by
      by_cases! hr : 0 < r
      · rw [intervalIntegral.integrableOn_Ioo_rpow_iff hr]
        linarith
      · simp [hr]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α))) (Ioo 0 r) volume
have apply : EqOn (β := ℝ) (fun (x : ℝ) ↦ C * x ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α))
  (fun (y : ℝ) ↦ y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α))) (Ioo 0 r)
Tactic: apply IntegrableOn.congr_fun (h_rpow.const_mul C) ?_ measurableSet_Ioo
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
y : ℝ
⊢ y ∈ Ioo 0 r →
    Eq (α := ℝ) ((fun (x : ℝ) ↦ C * x ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) y)
      ((fun (y : ℝ) ↦ y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α))) y)
have this₁ : ∀ (hy : 0 < y),
  y < r →
    Eq (α := ℝ) ((fun (x : ℝ) ↦ C * x ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) y)
      ((fun (y : ℝ) ↦ y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α))) y)
Tactic: ⟨hy, _⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right : y < r
⊢ C * y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α) = y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α))
have move_mul : y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α) * C = y ^ (Module.finrank ℝ E - 1) * y ^ (-α) * C
Tactic: move_mul [C]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right : y < r
⊢ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α) * C = y ^ (Module.finrank ℝ E - 1) * y ^ (-α) * C
have rw : y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α) * C = y ^ ((↑(Module.finrank ℝ E - 1) : ℝ) + -α) * C
Tactic: rw [← Real.rpow_natCast y (Module.finrank ℝ E - 1), ← Real.rpow_add hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right : y < r
⊢ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α) * C = y ^ ((↑(Module.finrank ℝ E - 1) : ℝ) + -α) * C
have e_a : HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 = (↑(Module.finrank ℝ E - 1) : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right : y < r
⊢ HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 = (↑(Module.finrank ℝ E - 1) : ℝ)
have e_a : Module.finrank ℝ E - 1 = Module.finrank ℝ E - 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (hypothesis)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
⊢ IntegrableOn f (ball 0 r) μ
have hint : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
  (fun (y : ℝ) ↦ y ^ (Module.finrank ℝ E - 1) • (C * y ^ (-α))) (Ioo 0 r) volume
Tactic: have hint : IntegrableOn (fun y ↦ y ^ (Module.finrank ℝ E - 1) • (C * y ^ (-α))) (Ioo 0 r) := by
    simp only [smul_eq_mul]
    have h_rpow : IntegrableOn (fun y ↦ y ^ ((Module.finrank ℝ E : ℝ) - 1 - α)) (Ioo 0 r) := by
      by_cases! hr : 0 < r
      · rw [intervalIntegral.integrableOn_Ioo_rpow_iff hr]
        linarith
      · simp [hr]
    apply IntegrableOn.congr_fun (h_rpow.const_mul C) ?_ measurableSet_Ioo
    intro y ⟨hy, _⟩
    simp only
    move_mul [C]
    rw [← Real.rpow_natCast y (Module.finrank ℝ E - 1), ← Real.rpow_add hy]
    congr
    norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (hypothesis)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hint :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (Module.finrank ℝ E - 1) • (C * y ^ (-α))) (Ioo 0 r) volume
⊢ IntegrableOn f (ball 0 r) μ
have hint₁ : IntegrableOn (ε := ℝ) (fun (x : E) ↦ C * ‖x‖ ^ (-α)) (ball 0 r) μ
Tactic: rw [← integrableOn_fun_norm_addHaar μ] at hint
Cleared hypotheses: hint
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hdim : 1 ≤ Module.finrank ℝ E
f : E → F
C α : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ, ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
⊢ LocallyIntegrable f μ
have rw : ∀ (k : Set E), IsCompact k → IntegrableOn f k μ
Tactic: rw [locallyIntegrable_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hdim : 1 ≤ Module.finrank ℝ E
f : E → F
C α : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ, ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
K : Set E
hK : IsCompact K
⊢ IntegrableOn f K μ
have obtain : ∀ (R : ℝ) (hR_pos : R > 0) (hR : ∀ x ∈ K, ‖x‖ < R), IntegrableOn f K μ
Tactic: obtain ⟨R, hR_pos, hR⟩ := hK.isBounded.exists_pos_norm_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n : ℕ
h : n ≠ 0
⊢ n.nthRoot 0 = 0
have zero : ∀ (h : Ne (α := ℕ) 0 0), nthRoot 0 0 = 0
Tactic: rcases n with _ | _ | _
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n : ℕ
h : n ≠ 0
zero : ∀ (h : Ne (α := ℕ) 0 0), nthRoot 0 0 = 0
⊢ n.nthRoot 0 = 0
have succ : ∀ (h : HAdd.hAdd (α := ℕ) 0 1 ≠ 0), (HAdd.hAdd (α := ℕ) 0 1).nthRoot 0 = 0
Tactic: rcases n with _ | _ | _
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n : ℕ
h : n ≠ 0
zero : ∀ (h : Ne (α := ℕ) 0 0), nthRoot 0 0 = 0
succ : ∀ (h : HAdd.hAdd (α := ℕ) 0 1 ≠ 0), (HAdd.hAdd (α := ℕ) 0 1).nthRoot 0 = 0
⊢ n.nthRoot 0 = 0
have succ₁ : ∀ (n : ℕ) (h : n + 1 + 1 ≠ 0), (n + 1 + 1).nthRoot 0 = 0
Tactic: rcases n with _ | _ | _
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n : ℕ
⊢ n.nthRoot 1 = 1
have zero : nthRoot 0 1 = 1
Tactic: rcases n with _ | _ | _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n : ℕ
zero : nthRoot 0 1 = 1
⊢ n.nthRoot 1 = 1
have succ : (HAdd.hAdd (α := ℕ) 0 1).nthRoot 1 = 1
Tactic: rcases n with _ | _ | _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n : ℕ
zero : nthRoot 0 1 = 1
succ : (HAdd.hAdd (α := ℕ) 0 1).nthRoot 1 = 1
⊢ n.nthRoot 1 = 1
have succ₁ : ∀ (n : ℕ), (n + 1 + 1).nthRoot 1 = 1
Tactic: rcases n with _ | _ | _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a guess : ℕ
hle : guess ≤ 0
⊢ go n a 0 guess ^ (n + 2) ≤ a
have zero : ∀ (hle : LE.le (α := ℕ) 0 0), go n a 0 0 ^ (n + 2) ≤ a
Tactic: obtain rfl : guess = 0 := by grind
Cleared hypotheses: guess, hle
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a fuel : ℕ
ih : ∀ {guess : ℕ} (hle : guess ≤ fuel), go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
⊢ (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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
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
⊢ (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
have split_ifs₁ : ∀ (h : ¬(a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess), guess ^ (n + 2) ≤ a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
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)
have 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
Tactic: linarith only [Nat.mul_le_of_le_div _ _ _ (not_lt.1 h)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (hypothesis)
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 ^ (n + 2) ≤ a
have this : 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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (hypothesis)
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 ^ (n + 2) ≤ a
have this₁ : guess * guess ^ (n + 1) ≤ a
Tactic: replace := Nat.mul_le_of_le_div _ _ _ this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
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 ^ (n + 2) ≤ a
have case : guess ≤ a / guess ^ (n + 1)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
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)
⊢ guess ^ (n + 2) ≤ a
have case₁ : ∀ (this : guess ≤ a / guess ^ (n + 1)), 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
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
⊢ guess ^ (n + 2) ≤ a
have case₅ : ∀ (this : guess * guess ^ (n + 1) ≤ 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
guess fuel : ℕ
hle : guess ≤ fuel
n a : ℕ
⊢ go n a fuel guess ^ (n + 2) ≤ a
have zero : ∀ {guess : ℕ} (hle : guess ≤ 0), go n a 0 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
Cleared hypotheses: guess, fuel, hle
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
guess fuel : ℕ
hle : guess ≤ fuel
n a : ℕ
zero : ∀ {guess : ℕ} (hle : guess ≤ 0), go n a 0 guess ^ (n + 2) ≤ a
⊢ go n a fuel guess ^ (n + 2) ≤ a
have 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
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
Cleared hypotheses: guess, fuel, hle
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a : ℕ
⊢ n.nthRoot a ^ n ≤ a ↔ n ≠ 0 ∨ a ≠ 0
have zero : HPow.hPow (β := ℕ) (nthRoot 0 a) 0 ≤ a ↔ Ne (α := ℕ) 0 0 ∨ a ≠ 0
Tactic: rcases n with _ | _ | _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a : ℕ
zero : HPow.hPow (β := ℕ) (nthRoot 0 a) 0 ≤ a ↔ Ne (α := ℕ) 0 0 ∨ a ≠ 0
⊢ n.nthRoot a ^ n ≤ a ↔ n ≠ 0 ∨ a ≠ 0
have succ : (HAdd.hAdd (α := ℕ) 0 1).nthRoot a ^ HAdd.hAdd (α := ℕ) 0 1 ≤ a ↔ HAdd.hAdd (α := ℕ) 0 1 ≠ 0 ∨ a ≠ 0
Tactic: rcases n with _ | _ | _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
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
⊢ n.nthRoot a ^ n ≤ a ↔ n ≠ 0 ∨ a ≠ 0
have succ₁ : ∀ (n : ℕ), (n + 1 + 1).nthRoot a ^ (n + 1 + 1) ≤ a ↔ n + 1 + 1 ≠ 0 ∨ a ≠ 0
Tactic: rcases n with _ | _ | _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a b : ℕ
hb : b ≠ 0
⊢ a ≤ (a ^ (n + 1) / b ^ n + n * b) / (n + 1)
have rw : (n + 1) * a * b ^ n ≤ a ^ (n + 1) + n * b * b ^ n
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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (hypothesis)
Goal:
n a b : ℕ
hb : b ≠ 0
⊢ (n + 1) * a * b ^ n ≤ a ^ (n + 1) + n * b * b ^ n
have 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)
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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (hypothesis)
Goal:
n a : ℕ
⊢ ∃ (c : ℕ), c ^ (n + 1) ≤ a ∧ a < (c + 1) ^ (n + 1)
have H : ∃ (c : ℕ), a < (c + 1) ^ (n + 1)
Tactic: have H : ∃ c, a < (c + 1) ^ (n + 1) := ⟨a, Nat.le_self_pow (by positivity) (a + 1)⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
Goal:
n a : ℕ
H : ∃ (c : ℕ), a < (c + 1) ^ (n + 1)
⊢ ∃ (c : ℕ), c ^ (n + 1) ≤ a ∧ a < (c + 1) ^ (n + 1)
have 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)
Tactic: let +nondep (eq := hc) c := Nat.find H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas (goal)
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)
have refine : c ^ (n + 1) ≤ a
Tactic: refine ⟨c, ?_, hc ▸ Nat.find_spec H⟩