awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi t) volume ↔ s.re < -1

Tactic:
⟨fun h ↦ (integrableOn_Ioi_norm_cpow_iff ht).mp h.norm, fun h ↦ integrableOn_Ioi_cpow_of_lt h ht⟩

Premises used: integrableOn_Ioi_norm_cpow_iff, integrableOn_Ioi_cpow_of_lt, Iff.intro, Iff.mp, MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s * (↑x : ℂ) ^ (s - 1)) (Ioi t) volume

Tactic:
(integrableOn_Ioi_cpow_of_lt ?_ ht).const_mul _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.IntegrableOn, integrableOn_Ioi_cpow_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
refine : (s - 1).re < -1
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s * (↑x : ℂ) ^ (s - 1)) (Ioi t) volume

Tactic:
refine (integrableOn_Ioi_cpow_of_lt ?_ ht).const_mul _

Premises used: MeasureTheory.Integrable.const_mul, integrableOn_Ioi_cpow_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
rwa : s.re - Complex.re 1 < -1
rwa₁ : s.re - 1 < -1
rwa₂ : s.re < HAdd.hAdd (α := ℝ) (-1) 1
rwa₃ rwa₄ rwa₅ rwa₆ : s.re < 0
⊢ (s - 1).re < -1

Tactic:
rwa [Complex.sub_re, Complex.one_re, sub_lt_iff_lt_add, neg_add_cancel]

Premises used: Complex.sub_re, neg_add_cancel, sub_lt_iff_lt_add, Complex.one_re
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s * (↑x : ℂ) ^ (s - 1)) (Ioi t) volume

Tactic:
have h : IntegrableOn (fun x : ℝ ↦ s * x ^ (s - 1)) (Set.Ioi t) := by
    refine (integrableOn_Ioi_cpow_of_lt ?_ ht).const_mul _
    rwa [Complex.sub_re, Complex.one_re, sub_lt_iff_lt_add, neg_add_cancel]
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s * (↑x : ℂ) ^ (s - 1)) (Ioi t) volume
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi t) volume

Tactic:
h.congr_fun (fun x hx ↦ ?_) measurableSet_Ioi

Premises used: measurableSet_Ioi, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s * (↑x : ℂ) ^ (s - 1)) (Ioi t) volume
refine : ∀ (x : ℝ) (hx : x ∈ Ioi t), s * (↑x : ℂ) ^ (s - 1) = deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) x
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi t) volume

Tactic:
refine h.congr_fun (fun x hx ↦ ?_) measurableSet_Ioi

Premises used: measurableSet_Ioi, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s * (↑x : ℂ) ^ (s - 1)) (Ioi t) volume
x : ℝ
hx : x ∈ Ioi t
rw rw₁ : s * (↑x : ℂ) ^ (s - 1) = s * (↑x : ℂ) ^ (s - 1)
⊢ s * (↑x : ℂ) ^ (s - 1) = deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) x

Tactic:
rw [Complex.deriv_ofReal_cpow_const (ht.trans hx).ne' (fun h ↦ (Complex.zero_re ▸ h ▸ hs).false)]

Premises used: Complex.deriv_ofReal_cpow_const, LT.lt.ne', LT.lt.trans
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re ≤ 0
x : ℝ
hx : x ∈ Ioi t
rw rw₁ : s.re * x ^ (s.re - 1) = s.re * x ^ (s.re - 1)
⊢ deriv (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ s‖) x = s.re * x ^ (s.re - 1)

Tactic:
rw [deriv_norm_ofReal_cpow _ (ht.trans hx)]

Premises used: deriv_norm_ofReal_cpow, LT.lt.trans
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re ≤ 0
rw : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (deriv fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ s‖) (Ioi t) volume

Tactic:
rw [integrableOn_congr_fun (fun x hx ↦ by
    rw [deriv_norm_ofReal_cpow _ (ht.trans hx)]) measurableSet_Ioi]

Premises used: MeasureTheory.integrableOn_congr_fun, measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re ≤ 0
inl :
  ∀ (hs : s.re = 0),
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume
inr :
  ∀ (hs : s.re < 0),
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume

Tactic:
obtain hs | hs := eq_or_lt_of_le hs

Premises used: eq_or_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs_1 : s.re ≤ 0
hs : s.re = 0
inl : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ 0) (Ioi t) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume

Tactic:
simp_rw [hs, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs_1 : s.re ≤ 0
hs : s.re = 0
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ 0) (Ioi t) volume

Tactic:
integrableOn_zero

Premises used: MeasureTheory.integrableOn_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs_1 : s.re ≤ 0
hs : s.re = 0
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ 0) (Ioi t) volume

Tactic:
exact integrableOn_zero

Premises used: MeasureTheory.integrableOn_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs_1 : s.re ≤ 0
hs : s.re < 0
rwa : s.re < HAdd.hAdd (α := ℝ) (-1) 1
rwa₁ rwa₂ rwa₃ rwa₄ : s.re < 0
⊢ s.re - 1 < -1

Tactic:
rwa [sub_lt_iff_lt_add, neg_add_cancel]

Premises used: neg_add_cancel, sub_lt_iff_lt_add
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs_1 : s.re ≤ 0
hs : s.re < 0
⊢ s.re - 1 < -1

Tactic:
replace hs : s.re - 1 < -1 := by rwa [sub_lt_iff_lt_add, neg_add_cancel]
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs_1 : s.re ≤ 0
hs : s.re - 1 < -1
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume

Tactic:
(integrableOn_Ioi_rpow_of_lt hs ht).const_mul s.re

Premises used: integrableOn_Ioi_rpow_of_lt, MeasureTheory.Integrable.const_mul, MeasureTheory.IntegrableOn, Complex.re
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs_1 : s.re ≤ 0
hs : s.re - 1 < -1
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume

Tactic:
exact (integrableOn_Ioi_rpow_of_lt hs ht).const_mul s.re

Premises used: integrableOn_Ioi_rpow_of_lt, MeasureTheory.Integrable.const_mul, Complex.re
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
inl : ∀ (hs : s.re ≤ -1), False
inr : ∀ (hs : -1 < s.re), False
⊢ False

Tactic:
rcases le_or_gt s.re (-1) with hs | hs

Premises used: Complex.re, le_or_gt, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
hs : s.re ≤ -1
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 1) volume

Tactic:
have : IntegrableOn (fun x : ℝ ↦ (x : ℂ) ^ s) (Ioo (0 : ℝ) 1) :=
      h.mono Ioo_subset_Ioi_self le_rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
hs : s.re ≤ -1
this : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 1) volume
⊢ -1 < s.re

Tactic:
rw [integrableOn_Ioo_cpow_iff zero_lt_one] at this

Premises used: intervalIntegral.integrableOn_Ioo_cpow_iff, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
hs : s.re ≤ -1
this : -1 < s.re
⊢ False

Tactic:
hs.not_gt this

Premises used: LE.le.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
hs : s.re ≤ -1
this : -1 < s.re
⊢ False

Tactic:
exact hs.not_gt this

Premises used: LE.le.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
hs : -1 < s.re
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 1) volume

Tactic:
have : IntegrableOn (fun x : ℝ ↦ (x : ℂ) ^ s) (Ioi 1) :=
      h.mono (Ioi_subset_Ioi zero_le_one) le_rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
hs : -1 < s.re
this : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 1) volume
⊢ s.re < -1

Tactic:
rw [integrableOn_Ioi_cpow_iff zero_lt_one] at this

Premises used: integrableOn_Ioi_cpow_iff, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
hs : -1 < s.re
this : s.re < -1
⊢ False

Tactic:
hs.not_gt this

Premises used: LT.lt.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
hs : -1 < s.re
this : s.re < -1
⊢ False

Tactic:
exact hs.not_gt this

Premises used: LT.lt.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ (↑x : ℂ) ^ s) 0

Tactic:
MeasureTheory.integral_undef (not_integrableOn_Ioi_cpow s)

Premises used: not_integrableOn_Ioi_cpow, MeasureTheory.integral_undef
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (t : ℝ) ↦ (↑t : ℂ) ^ a) =
    -(↑c : ℂ) ^ (a + 1) / (a + 1)

Tactic:
tendsto_nhds_unique
      (intervalIntegral_tendsto_integral_Ioi c (integrableOn_Ioi_cpow_of_lt ha hc) tendsto_id) ?_

Premises used: Filter.tendsto_id, MeasureTheory.intervalIntegral_tendsto_integral_Ioi, integrableOn_Ioi_cpow_of_lt, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
c₁ : Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in c..id i, (↑x : ℂ) ^ a) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (t : ℝ) ↦ (↑t : ℂ) ^ a) =
    -(↑c : ℂ) ^ (a + 1) / (a + 1)

Tactic:
refine
    tendsto_nhds_unique
      (intervalIntegral_tendsto_integral_Ioi c (integrableOn_Ioi_cpow_of_lt ha hc) tendsto_id) ?_

Premises used: Filter.tendsto_id, MeasureTheory.intervalIntegral_tendsto_integral_Ioi, integrableOn_Ioi_cpow_of_lt, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this :
  Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in c..id i, (↑x : ℂ) ^ a) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))

Tactic:
this.congr' ((eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx => ?_))

Premises used: Filter.Eventually.of_forall, Filter.Eventually.mp, Filter.Tendsto.congr', OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this :
  Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
refine :
  ∀ (x : ℝ) (hx : 0 < x),
    ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1) = (fun (i : ℝ) ↦ (∫ (x : ℝ) in c..id i, (↑x : ℂ) ^ a : ℂ)) x
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in c..id i, (↑x : ℂ) ^ a) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))

Tactic:
refine this.congr' ((eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx => ?_))

Premises used: Filter.Eventually.of_forall, Filter.Eventually.mp, Filter.Tendsto.congr', OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this :
  Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
rw : -1 < a.re ∨ a ≠ -1 ∧ 0 ∉ uIcc c (id x)
⊢ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1) = ∫ (x : ℝ) in c..id x, (↑x : ℂ) ^ a

Tactic:
rw [integral_cpow, id]

Premises used: integral_cpow, id
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this :
  Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ -1 < a.re ∨ a ≠ -1 ∧ 0 ∉ uIcc c (id x)

Tactic:
Or.inr ⟨?_, notMem_uIcc_of_lt hc hx⟩

Premises used: Set.notMem_uIcc_of_lt, And.intro, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this :
  Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
refine : a ≠ -1
⊢ -1 < a.re ∨ a ≠ -1 ∧ 0 ∉ uIcc c (id x)

Tactic:
refine Or.inr ⟨?_, notMem_uIcc_of_lt hc hx⟩

Premises used: Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this :
  Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
apply_fun : a.re ≠ Complex.re (-1)
⊢ a ≠ -1

Tactic:
apply_fun Complex.re

Premises used: Complex.re
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this :
  Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ a.re ≠ -1

Tactic:
ha.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this :
  Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ a.re ≠ -1

Tactic:
exact ha.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
Tendsto :
  Filter.Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop
    (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
⊢ Filter.Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in c..id i, (↑x : ℂ) ^ a) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))

Tactic:
suffices
    Tendsto (fun x : ℝ => ((x : ℂ) ^ (a + 1) - (c : ℂ) ^ (a + 1)) / (a + 1)) atTop
      (𝓝 <| -c ^ (a + 1) / (a + 1)) by
    refine this.congr' ((eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx => ?_))
    dsimp only
    rw [integral_cpow, id]
    refine Or.inr ⟨?_, notMem_uIcc_of_lt hc hx⟩
    apply_fun Complex.re
    rw [Complex.neg_re, Complex.one_re]
    exact ha.ne
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
simp_rw :
  Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) ^ (a + 1) / (a + 1) - (↑c : ℂ) ^ (a + 1) / (a + 1)) atTop
    (𝓝 (0 / (a + 1) - (↑c : ℂ) ^ (a + 1) / (a + 1)))
⊢ Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))

Tactic:
simp_rw [← zero_sub, sub_div]

Premises used: sub_div, zero_sub
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) ^ (a + 1) / (a + 1) - (↑c : ℂ) ^ (a + 1) / (a + 1)) atTop
    (𝓝 (0 / (a + 1) - (↑c : ℂ) ^ (a + 1) / (a + 1)))

Tactic:
(Tendsto.div_const ?_ _).sub_const _

Premises used: Filter.Tendsto.sub_const, Filter.Tendsto.div_const
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
refine : Tendsto (β := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (a + 1)) atTop (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) ^ (a + 1) / (a + 1) - (↑c : ℂ) ^ (a + 1) / (a + 1)) atTop
    (𝓝 (0 / (a + 1) - (↑c : ℂ) ^ (a + 1) / (a + 1)))

Tactic:
refine (Tendsto.div_const ?_ _).sub_const _

Premises used: Filter.Tendsto.sub_const, Filter.Tendsto.div_const
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (a + 1)‖) atTop (𝓝 0)
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (a + 1)) atTop (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Premises used: tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
linarith : -(a.re + 1) ≤ 0 → a.re - -1 + (-(a.re + 1) - 0) = 0
⊢ 0 < -(a.re + 1)

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
linarith : ∀ (x : ℝ) (hx : 0 < x), x ^ (- -(a.re + 1)) = (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (a + 1)‖) x
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (a + 1)‖) atTop (𝓝 0)

Tactic:
refine
    (tendsto_rpow_neg_atTop (by linarith : 0 < -(a.re + 1))).congr'
      ((eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx => ?_))

Premises used: Filter.Eventually.of_forall, Filter.Eventually.mp, tendsto_rpow_neg_atTop, Filter.Tendsto.congr', OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : 0 < x
simp_rw simp_rw₁ : x ^ (- -(a.re + 1)) = ‖(↑x : ℂ) ^ (a + 1)‖
simp_rw₂ : x ^ (a.re + 1) = ‖(↑x : ℂ) ^ (a + 1)‖
simp_rw₃ : x ^ (a.re + 1) = x ^ (a + 1).re
simp_rw₄ : x ^ (a.re + 1) = x ^ (a.re + Complex.re 1)
⊢ x ^ (- -(a.re + 1)) = (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (a + 1)‖) x

Tactic:
simp_rw [neg_neg, Complex.norm_cpow_eq_rpow_re_of_pos hx, Complex.add_re, Complex.one_re]

Premises used: Complex.add_re, neg_neg, Complex.one_re, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
this :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-2 / 2)) volume
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (1 + HPow.hPow (β := ℕ) x 2)⁻¹) volume

Tactic:
simpa [rpow_neg_one]

Premises used: Real.rpow_neg_one
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
suffices :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-2 / 2)) volume
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (1 + HPow.hPow (β := ℕ) x 2)⁻¹) volume

Tactic:
suffices Integrable fun (x : ℝ) ↦ (1 + ‖x‖ ^ 2) ^ ((-2 : ℝ) / 2) by simpa [rpow_neg_one]
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
⊢ LT.lt (α := ℝ) (↑(Module.finrank ℝ ℝ) : ℝ) 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-2 / 2)) volume

Tactic:
exact integrable_rpow_neg_one_add_norm_sq (by simp)

Premises used: integrable_rpow_neg_one_add_norm_sq
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
i : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic i)) fun (x : ℝ) ↦
      (1 + HPow.hPow (β := ℕ) x 2)⁻¹) =
    arctan i + π / 2

Tactic:
integral_Iic_of_hasDerivAt_of_tendsto' (fun x _ => hasDerivAt_arctan' x)
    integrable_inv_one_add_sq.integrableOn (tendsto_nhds_of_tendsto_nhdsWithin tendsto_arctan_atBot)
    |>.trans (sub_neg_eq_add _ _)

Premises used: integrable_inv_one_add_sq, tendsto_nhds_of_tendsto_nhdsWithin, Real.tendsto_arctan_atBot, Real.hasDerivAt_arctan', MeasureTheory.Integrable.integrableOn, MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto', sub_neg_eq_add, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
i : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi i)) fun (x : ℝ) ↦
      (1 + HPow.hPow (β := ℕ) x 2)⁻¹) =
    π / 2 - arctan i

Tactic:
integral_Ioi_of_hasDerivAt_of_tendsto' (fun x _ => hasDerivAt_arctan' x)
    integrable_inv_one_add_sq.integrableOn (tendsto_nhds_of_tendsto_nhdsWithin tendsto_arctan_atTop)

Premises used: MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto', integrable_inv_one_add_sq, Real.tendsto_arctan_atTop, tendsto_nhds_of_tendsto_nhdsWithin, Real.hasDerivAt_arctan', MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
⊢ π = π / 2 - -(π / 2)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
n : ℕ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ n) μ a b

Tactic:
(continuous_pow n).intervalIntegrable a b

Premises used: Continuous.intervalIntegrable, continuous_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
n : ℤ
h : 0 ≤ n ∨ 0 ∉ [[a, b]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ n) μ a b

Tactic:
(continuousOn_id.zpow₀ n fun _ hx => h.symm.imp (ne_of_mem_of_not_mem hx) id).intervalIntegrable

Premises used: id, ne_of_mem_of_not_mem, Or.symm, ContinuousOn.zpow₀, ContinuousOn.intervalIntegrable, continuousOn_id, Or.imp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℝ
h : 0 ≤ r ∨ 0 ∉ [[a, b]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) μ a b

Tactic:
(continuousOn_id.rpow_const fun _ hx =>
    h.symm.imp (ne_of_mem_of_not_mem hx) id).intervalIntegrable

Premises used: id, ne_of_mem_of_not_mem, Or.symm, ContinuousOn.intervalIntegrable, ContinuousOn.rpow_const, continuousOn_id, Or.imp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume a b

Tactic:
IntervalIntegrable.trans (this a).symm (this b)

Premises used: IntervalIntegrable.symm, IntervalIntegrable.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume a b

Tactic:
exact IntervalIntegrable.trans (this a).symm (this b)

Premises used: IntervalIntegrable.symm, IntervalIntegrable.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
suffices : ∀ (c : ℝ), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume a b

Tactic:
suffices ∀ c : ℝ, IntervalIntegrable (fun x => x ^ r) volume 0 c by
    exact IntervalIntegrable.trans (this a).symm (this b)