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

Tactic:
have H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) :=
    H.mono (Set.Ioi_subset_Ioi (le_max_right _ _)) le_rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
apply : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi (max 1 t)), ‖a⁻¹‖ ≤ a ^ s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ioi (max 1 t)) volume

Tactic:
apply H'.mono' measurable_inv.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, MeasureTheory.Integrable.mono', MeasurableInv.measurable_inv
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
h₁ : ∀ (x : ℝ) (hx : x ∈ Ioi (max 1 t)), ‖x⁻¹‖ ≤ x ^ s
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi (max 1 t)), ‖a⁻¹‖ ≤ a ^ s

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
x : ℝ
hx : x ∈ Ioi (max 1 t)
⊢ 1 ≤ x

Tactic:
have x_one : 1 ≤ x := ((le_max_left _ _).trans_lt (mem_Ioi.1 hx)).le
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
x : ℝ
hx : x ∈ Ioi (max 1 t)
x_one : 1 ≤ x
h₁ : x⁻¹ ≤ x ^ s
⊢ ‖x⁻¹‖ ≤ x ^ s

Tactic:
simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (zero_le_one.trans x_one)]

Premises used: norm_inv, zero_le_one, abs_of_nonneg, LE.le.trans, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
x : ℝ
hx : x ∈ Ioi (max 1 t)
x_one : 1 ≤ x
h₁ : HPow.hPow (β := ℝ) x (-1) ≤ x ^ s
⊢ x⁻¹ ≤ x ^ s

Tactic:
rw [← Real.rpow_neg_one x]

Premises used: Real.rpow_neg_one
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
x : ℝ
hx : x ∈ Ioi (max 1 t)
x_one : 1 ≤ x
⊢ HPow.hPow (β := ℝ) x (-1) ≤ x ^ s

Tactic:
Real.rpow_le_rpow_of_exponent_le x_one h

Premises used: Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
x : ℝ
hx : x ∈ Ioi (max 1 t)
x_one : 1 ≤ x
⊢ HPow.hPow (β := ℝ) x (-1) ≤ x ^ s

Tactic:
exact Real.rpow_le_rpow_of_exponent_le x_one h

Premises used: Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ioi (max 1 t)) volume

Tactic:
have : IntegrableOn (fun x ↦ x⁻¹) (Ioi (max 1 t)) := by
    apply H'.mono' measurable_inv.aestronglyMeasurable
    filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
    have x_one : 1 ≤ x := ((le_max_left _ _).trans_lt (mem_Ioi.1 hx)).le
    simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (zero_le_one.trans x_one)]
    rw [← Real.rpow_neg_one x]
    exact Real.rpow_le_rpow_of_exponent_le x_one h
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
this : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ioi (max 1 t)) volume
⊢ False

Tactic:
not_integrableOn_Ioi_inv this

Premises used: not_integrableOn_Ioi_inv
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
this : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ioi (max 1 t)) volume
⊢ False

Tactic:
exact not_integrableOn_Ioi_inv this

Premises used: not_integrableOn_Ioi_inv
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℝ
⊢ IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) atTop volume ↔ s < -1

Tactic:
⟨fun ⟨t, ht, hint⟩ ↦ ?_, fun h ↦
    ⟨Set.Ioi 1, Ioi_mem_atTop 1, (integrableOn_Ioi_rpow_iff zero_lt_one).mpr h⟩⟩

Premises used: Iff.mpr, Set.Ioi, Filter.Ioi_mem_atTop, zero_lt_one, integrableOn_Ioi_rpow_iff, And.intro, LT.lt, Iff.intro, Exists.intro, _private.0.integrableAtFilter_rpow_atTop_iff.match_1, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℝ
refine :
  IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) atTop volume →
    ∀ (t : Set ℝ) (ht : Membership.mem (γ := Filter ℝ) atTop t)
      (hint : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) t volume), s < -1
⊢ IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) atTop volume ↔ s < -1

Tactic:
refine ⟨fun ⟨t, ht, hint⟩ ↦ ?_, fun h ↦
    ⟨Set.Ioi 1, Ioi_mem_atTop 1, (integrableOn_Ioi_rpow_iff zero_lt_one).mpr h⟩⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℝ
h : IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) atTop volume
t : Set ℝ
ht : Membership.mem (γ := Filter ℝ) atTop t
hint : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) t volume
obtain : ∀ (a : ℝ) (ha : ∀ b ≥ a, b ∈ t), s < -1
⊢ s < -1

Tactic:
obtain ⟨a, ha⟩ := mem_atTop_sets.mp ht

Premises used: Filter.mem_atTop_sets, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℝ
h : IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) atTop volume
t : Set ℝ
ht : Membership.mem (γ := Filter ℝ) atTop t
hint : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) t volume
a : ℝ
ha : ∀ b ≥ a, b ∈ t
⊢ s < -1

Tactic:
(integrableOn_Ioi_rpow_iff (zero_lt_one.trans_le (le_max_right a 1))).mp ?_

Premises used: le_max_right, zero_lt_one, integrableOn_Ioi_rpow_iff, LT.lt.trans_le, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℝ
h : IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) atTop volume
t : Set ℝ
ht : Membership.mem (γ := Filter ℝ) atTop t
hint : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) t volume
a : ℝ
ha : ∀ b ≥ a, b ∈ t
refine : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max a 1)) volume
⊢ s < -1

Tactic:
refine (integrableOn_Ioi_rpow_iff (zero_lt_one.trans_le (le_max_right a 1))).mp ?_

Premises used: le_max_right, zero_lt_one, integrableOn_Ioi_rpow_iff, LT.lt.trans_le, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℝ
h : IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) atTop volume
t : Set ℝ
ht : Membership.mem (γ := Filter ℝ) atTop t
hint : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) t volume
a : ℝ
ha : ∀ b ≥ a, b ∈ t
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max a 1)) volume

Tactic:
hint.mono_set <| fun x hx ↦ ha _ <| (le_max_left a 1).trans hx.le

Premises used: LT.lt.le, MeasureTheory.IntegrableOn.mono_set, LE.le.trans, OfNat.ofNat, le_max_left
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℝ
h : IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) atTop volume
t : Set ℝ
ht : Membership.mem (γ := Filter ℝ) atTop t
hint : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) t volume
a : ℝ
ha : ∀ b ≥ a, b ∈ t
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max a 1)) volume

Tactic:
exact hint.mono_set <| fun x hx ↦ ha _ <| (le_max_left a 1).trans hx.le

Premises used: MeasureTheory.IntegrableOn.mono_set, LE.le.trans, OfNat.ofNat, le_max_left
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℝ
h : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi 0) volume
inl : ∀ (hs : s ≤ -1), False
inr : ∀ (hs : -1 < s), False
⊢ False

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

Premises used: 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 ≤ -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 ≤ -1
this : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 1) volume
⊢ -1 < s

Tactic:
rw [integrableOn_Ioo_rpow_iff zero_lt_one] at this

Premises used: intervalIntegral.integrableOn_Ioo_rpow_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 ≤ -1
this : -1 < s
⊢ 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 ≤ -1
this : -1 < s
⊢ 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
⊢ 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
this : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi 1) volume
⊢ s < -1

Tactic:
rw [integrableOn_Ioi_rpow_iff zero_lt_one] at this

Premises used: zero_lt_one, integrableOn_Ioi_rpow_iff
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℝ
h : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi 0) volume
hs : -1 < s
this : s < -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
this : s < -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_rpow s)

Premises used: MeasureTheory.integral_undef, not_integrableOn_Ioi_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ HasDerivAt (fun (x : ℝ) ↦ x ^ (a + 1) / (a + 1)) ((a + 1) * x ^ (a + 1 - 1) / (a + 1)) x

Tactic:
(hasDerivAt_rpow_const (p := a + 1) (Or.inl (hc.trans_le hx).ne')).div_const _

Premises used: Real.hasDerivAt_rpow_const, LT.lt.ne', LT.lt.trans_le, HasDerivAt.div_const, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
h : x ^ a = (a + 1) * x ^ (a + 1 - 1) / (a + 1)
⊢ HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x

Tactic:
convert! (hasDerivAt_rpow_const (p := a + 1) (Or.inl (hc.trans_le hx).ne')).div_const _ using 1

Premises used: Real.hasDerivAt_rpow_const, LT.lt.ne', LT.lt.trans_le, HasDerivAt.div_const, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
linarith : 0 ≤ a + 1 → a - -1 + (0 - (a + 1)) = 0
⊢ a + 1 < 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ x ^ a = (a + 1) * x ^ (a + 1 - 1) / (a + 1)

Tactic:
simp [show a + 1 ≠ 0 from ne_of_lt (by linarith), mul_comm]

Premises used: mul_comm, ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
⊢ ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x

Tactic:
have hd : ∀ x ∈ Ici c, HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x := by
    intro x hx
    convert! (hasDerivAt_rpow_const (p := a + 1) (Or.inl (hc.trans_le hx).ne')).div_const _ using 1
    simp [show a + 1 ≠ 0 from ne_of_lt (by linarith), mul_comm]
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
hf : Tendsto (β := ℝ) (fun (a_1 : ℝ) ↦ a_1 ^ (a + 1)) atTop (𝓝 0)
⊢ Tendsto (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))

Tactic:
apply Tendsto.div_const

Premises used: Filter.Tendsto.div_const
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
linarith : -(a + 1) ≤ 0 → a - -1 + (-(a + 1) - 0) = 0
⊢ 0 < -(a + 1)

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ Tendsto (β := ℝ) (fun (a_1 : ℝ) ↦ a_1 ^ (a + 1)) atTop (𝓝 0)

Tactic:
simpa only [neg_neg] using tendsto_rpow_neg_atTop (by linarith : 0 < -(a + 1))

Premises used: neg_neg, tendsto_rpow_neg_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ Tendsto (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))

Tactic:
have ht : Tendsto (fun t => t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1))) := by
    apply Tendsto.div_const
    simpa only [neg_neg] using tendsto_rpow_neg_atTop (by linarith : 0 < -(a + 1))
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
ht : Tendsto (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (x : ℝ) ↦ x ^ a) =
    0 / (a + 1) - c ^ (a + 1) / (a + 1)

Tactic:
integral_Ioi_of_hasDerivAt_of_tendsto' hd (integrableOn_Ioi_rpow_of_lt ha hc) ht

Premises used: integrableOn_Ioi_rpow_of_lt, MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto'
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
ht : Tendsto (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
h : -c ^ (a + 1) / (a + 1) = 0 / (a + 1) - c ^ (a + 1) / (a + 1)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (t : ℝ) ↦ t ^ a) =
    -c ^ (a + 1) / (a + 1)

Tactic:
convert! integral_Ioi_of_hasDerivAt_of_tendsto' hd (integrableOn_Ioi_rpow_of_lt ha hc) ht using 1

Premises used: integrableOn_Ioi_rpow_of_lt, MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto'
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
ht : Tendsto (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
⊢ -c ^ (a + 1) / (a + 1) = 0 / (a + 1) - c ^ (a + 1) / (a + 1)

Tactic:
simp only [neg_div, zero_div, zero_sub]

Premises used: neg_div, zero_div, zero_sub
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ a‖) (Ioi c) volume

Tactic:
(integrableOn_Ioi_rpow_of_lt ha hc).congr_fun (fun x hx => ?_) measurableSet_Ioi

Premises used: integrableOn_Ioi_rpow_of_lt, measurableSet_Ioi, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
refine : ∀ (x : ℝ) (hx : x ∈ Ioi c), x ^ a.re = ‖(↑x : ℂ) ^ a‖
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ a‖) (Ioi c) volume

Tactic:
refine (integrableOn_Ioi_rpow_of_lt ha hc).congr_fun (fun x hx => ?_) measurableSet_Ioi

Premises used: integrableOn_Ioi_rpow_of_lt, measurableSet_Ioi, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ioi c
rw rw₁ : x ^ a.re = x ^ a.re
⊢ x ^ a.re = ‖(↑x : ℂ) ^ a‖

Tactic:
rw [Complex.norm_cpow_eq_rpow_re_of_pos (hc.trans hx)]

Premises used: LT.lt.trans, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a) (Ioi c) volume

Tactic:
(integrable_norm_iff ?_).mp <| integrableOn_Ioi_norm_cpow_of_lt ha hc

Premises used: integrableOn_Ioi_norm_cpow_of_lt, MeasureTheory.IntegrableOn, MeasureTheory.integrable_norm_iff, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
refine :
  AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a)
    (Measure.restrict volume (Ioi c))
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a) (Ioi c) volume

Tactic:
refine (integrable_norm_iff ?_).mp <| integrableOn_Ioi_norm_cpow_of_lt ha hc

Premises used: integrableOn_Ioi_norm_cpow_of_lt, MeasureTheory.integrable_norm_iff, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a)
    (Measure.restrict volume (Ioi c))

Tactic:
ContinuousOn.aestronglyMeasurable (fun t ht ↦ ?_) measurableSet_Ioi

Premises used: ContinuousOn.aestronglyMeasurable, measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
refine : ∀ (t : ℝ) (ht : t ∈ Ioi c), ContinuousWithinAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a) (Ioi c) t
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a)
    (Measure.restrict volume (Ioi c))

Tactic:
refine ContinuousOn.aestronglyMeasurable (fun t ht ↦ ?_) measurableSet_Ioi

Premises used: ContinuousOn.aestronglyMeasurable, measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
t : ℝ
ht : t ∈ Ioi c
⊢ ContinuousWithinAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a) (Ioi c) t

Tactic:
(Complex.continuousAt_ofReal_cpow_const _ _ (Or.inr (hc.trans ht).ne')).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, LT.lt.ne', LT.lt.trans, Or.inr, Complex.continuousAt_ofReal_cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
t : ℝ
ht : t ∈ Ioi c
⊢ ContinuousWithinAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a) (Ioi c) t

Tactic:
exact (Complex.continuousAt_ofReal_cpow_const _ _ (Or.inr (hc.trans ht).ne')).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, LT.lt.ne', LT.lt.trans, Or.inr, Complex.continuousAt_ofReal_cpow_const
-- 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 ↦ ?_, fun h ↦ integrableOn_Ioi_norm_cpow_of_lt h ht⟩

Premises used: integrableOn_Ioi_norm_cpow_of_lt, Iff.intro
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
refine :
  ∀ (h : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ s‖) (Ioi t) volume),
    s.re < -1
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ s‖) (Ioi t) volume ↔ s.re < -1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ integrableOn_Ioi_norm_cpow_of_lt h ht⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ s‖) (Ioi t) volume
⊢ s.re < -1

Tactic:
(integrableOn_Ioi_rpow_iff ht).mp <| h.congr_fun (fun a ha ↦ ?_) measurableSet_Ioi

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

Tactic:
refine (integrableOn_Ioi_rpow_iff ht).mp <| h.congr_fun (fun a ha ↦ ?_) measurableSet_Ioi

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

Tactic:
rw [Complex.norm_cpow_eq_rpow_re_of_pos (ht.trans ha)]

Premises used: LT.lt.trans, Complex.norm_cpow_eq_rpow_re_of_pos