awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : 0 < a.re
⊢ ∑' (n : ℤ), cexp (-(↑π : ℂ) * a * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / a * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)

Tactic:
simpa only [mul_zero, zero_mul, add_zero] using Complex.tsum_exp_neg_quadratic ha 0

Premises used: MulZeroClass.zero_mul, Complex.tsum_exp_neg_quadratic, MulZeroClass.mul_zero, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℝ
ha rwa rwa₁ rwa₂ rwa₃ : 0 < a
⊢ 0 < (↑a : ℂ).re

Tactic:
rwa [ofReal_re]

Premises used: Complex.ofReal_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℝ
ha : 0 < a
⊢ ∑' (n : ℤ), rexp (-π * a * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), rexp (-π / a * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2)

Tactic:
simpa only [← ofReal_inj, ofReal_tsum, ofReal_exp, ofReal_mul, ofReal_neg, ofReal_pow,
    ofReal_intCast, ofReal_div, ofReal_one, ofReal_cpow ha.le, ofReal_ofNat, mul_zero, zero_mul,
    add_zero] using Complex.tsum_exp_neg_quadratic (by rwa [ofReal_re] : 0 < (a : ℂ).re) 0

Premises used: Complex.ofReal_cpow, MulZeroClass.zero_mul, Complex.ofReal_neg, Complex.ofReal_intCast, LT.lt.le, Complex.ofReal_one, Complex.ofReal_exp, Complex.tsum_exp_neg_quadratic, MulZeroClass.mul_zero, Complex.ofReal_div, Complex.ofReal_inj, Complex.ofReal_tsum, Complex.ofReal_ofNat, add_zero, OfNat.ofNat, Complex.ofReal_pow, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
c : ℝ
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) rexp (Iic c) volume

Tactic:
integrableOn_Iic_of_intervalIntegral_norm_bounded (exp c) c
      (fun y => intervalIntegrable_exp.1) tendsto_id
      (eventually_of_mem (Iic_mem_atBot 0) fun y _ => ?_)

Premises used: Filter.tendsto_id, MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_bounded, Real.exp, Filter.eventually_of_mem, Filter.Iic_mem_atBot, intervalIntegral.intervalIntegrable_exp, And.left, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
c : ℝ
integrableOn_Iic_of_intervalIntegral_norm_bounded :
  ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Iic 0) y → ∫ (x : ℝ) in id y..c, ‖rexp x‖ ≤ rexp c
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) rexp (Iic c) volume

Tactic:
refine
    integrableOn_Iic_of_intervalIntegral_norm_bounded (exp c) c
      (fun y => intervalIntegrable_exp.1) tendsto_id
      (eventually_of_mem (Iic_mem_atBot 0) fun y _ => ?_)

Premises used: Filter.tendsto_id, MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_bounded, Real.exp, Filter.eventually_of_mem, Filter.Iic_mem_atBot, intervalIntegral.intervalIntegrable_exp, And.left, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
c y : ℝ
h : Membership.mem (γ := Set ℝ) (Iic 0) y
simp_rw : 0 ≤ rexp (id y)
⊢ ∫ (x : ℝ) in id y..c, ‖rexp x‖ ≤ rexp c

Tactic:
simp_rw [norm_of_nonneg (exp_pos _).le, integral_exp, sub_le_self_iff]

Premises used: integral_exp, LT.lt.le, sub_le_self_iff, Real.norm_of_nonneg, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
c y : ℝ
h : Membership.mem (γ := Set ℝ) (Iic 0) y
⊢ 0 ≤ rexp (id y)

Tactic:
(exp_pos _).le

Premises used: LT.lt.le, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
c y : ℝ
h : Membership.mem (γ := Set ℝ) (Iic 0) y
⊢ 0 ≤ rexp (id y)

Tactic:
exact (exp_pos _).le

Premises used: LT.lt.le, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
c : ℝ
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x)) (Ioi c) volume

Tactic:
Iff.mp integrableOn_Ici_iff_integrableOn_Ioi (integrableOn_exp_Iic (-c)).comp_neg_Ici

Premises used: integrableOn_exp_Iic, integrableOn_Ici_iff_integrableOn_Ioi, Iff.mp, MeasureTheory.IntegrableOn.comp_neg_Ici, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
c : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ rexp x) = rexp c

Tactic:
tendsto_nhds_unique
      (intervalIntegral_tendsto_integral_Iic _ (integrableOn_exp_Iic _) tendsto_id) ?_

Premises used: integrableOn_exp_Iic, MeasureTheory.intervalIntegral_tendsto_integral_Iic, Filter.tendsto_id, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
c : ℝ
_ : Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in id i..c, rexp x) atBot (𝓝 (rexp c))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ rexp x) = rexp c

Tactic:
refine
    tendsto_nhds_unique
      (intervalIntegral_tendsto_integral_Iic _ (integrableOn_exp_Iic _) tendsto_id) ?_

Premises used: integrableOn_exp_Iic, MeasureTheory.intervalIntegral_tendsto_integral_Iic, Filter.tendsto_id, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
c : ℝ
rw rw₁ : 𝓝 (rexp c) = 𝓝 (rexp c)
⊢ 𝓝 (rexp c) = 𝓝 (rexp c - 0)

Tactic:
rw [sub_zero]

Premises used: sub_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
c : ℝ
simp_rw : Tendsto (fun (i : ℝ) ↦ rexp c - rexp (id i)) atBot (𝓝 (rexp c - 0))
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in id i..c, rexp x) atBot (𝓝 (rexp c))

Tactic:
simp_rw [integral_exp, show 𝓝 (exp c) = 𝓝 (exp c - 0) by rw [sub_zero]]

Premises used: integral_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
c : ℝ
⊢ Tendsto (fun (i : ℝ) ↦ rexp c - rexp (id i)) atBot (𝓝 (rexp c - 0))

Tactic:
tendsto_exp_atBot.const_sub _

Premises used: Filter.Tendsto.const_sub, Real.tendsto_exp_atBot
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
c : ℝ
⊢ Tendsto (fun (i : ℝ) ↦ rexp c - rexp (id i)) atBot (𝓝 (rexp c - 0))

Tactic:
exact tendsto_exp_atBot.const_sub _

Premises used: Filter.Tendsto.const_sub, Real.tendsto_exp_atBot
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ rexp x)
    1

Tactic:
exp_zero ▸ integral_exp_Iic 0

Premises used: integral_exp_Iic, Eq.rec, Real.exp_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
c : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (x : ℝ) ↦ rexp (-x)) =
    rexp (-c)

Tactic:
simpa only [integral_comp_neg_Ioi] using integral_exp_Iic (-c)

Premises used: integral_exp_Iic, integral_comp_neg_Ioi, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-x)) 1

Tactic:
simpa only [neg_zero, exp_zero] using integral_exp_neg_Ioi 0

Premises used: integral_exp_neg_Ioi, Real.exp_zero, OfNat.ofNat, neg_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ))) (Ioi c) volume

Tactic:
(integrable_norm_iff ?_).mp ?_

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.integrable_norm_iff, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
refine_1 :
  AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ)))
    (Measure.restrict volume (Ioi c))
refine_2 :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (a_1 : ℝ) ↦ ‖Complex.exp (a * (↑a_1 : ℂ))‖)
    (Measure.restrict volume (Ioi c))
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ))) (Ioi c) volume

Tactic:
refine (integrable_norm_iff ?_).mp ?_

Premises used: MeasureTheory.integrable_norm_iff, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
refine_1 : Continuous (Y := ℂ) fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ))
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ)))
    (Measure.restrict volume (Ioi c))

Tactic:
apply Continuous.aestronglyMeasurable

Premises used: Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
⊢ 0 < -a.re

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (a_1 : ℝ) ↦ ‖Complex.exp (a * (↑a_1 : ℂ))‖)
    (Measure.restrict volume (Ioi c))

Tactic:
simpa [Complex.norm_exp] using
      (integrableOn_Ioi_comp_mul_left_iff (fun x => exp (-x)) c (a := -a.re) (by simpa)).mpr <|
        integrableOn_exp_neg_Ioi _

Premises used: Iff.mpr, MeasureTheory.integrableOn_Ioi_comp_mul_left_iff, Real.exp, integrableOn_exp_neg_Ioi, Complex.norm_exp, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : 0 < a.re
c : ℝ
⊢ (-a).re < 0

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : 0 < a.re
c : ℝ
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ))) (Iic c) volume

Tactic:
simpa using Iff.mpr integrableOn_Iic_iff_integrableOn_Iio
    (integrableOn_exp_mul_complex_Ioi (a := -a) (by simpa) (-c)).comp_neg_Iio

Premises used: Iff.mpr, MeasureTheory.IntegrableOn.comp_neg_Iio, integrableOn_Iic_iff_integrableOn_Iio, Neg.neg, integrableOn_exp_mul_complex_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < 0
c : ℝ
⊢ (↑a : ℂ).re < 0

Tactic:
simpa using ha
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < 0
c : ℝ
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (a_1 : ℝ) ↦ ‖Complex.exp ((↑a : ℂ) * (↑a_1 : ℂ))‖)
    (Measure.restrict volume (Ioi c))

Tactic:
have := Integrable.norm <| integrableOn_exp_mul_complex_Ioi (a := a) (by simpa using ha) c
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < 0
c : ℝ
this :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (a_1 : ℝ) ↦ ‖Complex.exp ((↑a : ℂ) * (↑a_1 : ℂ))‖)
    (Measure.restrict volume (Ioi c))
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (a * x)) (Ioi c) volume

Tactic:
simpa [Complex.norm_exp] using this

Premises used: Complex.norm_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : 0 < a
c : ℝ
⊢ 0 < (↑a : ℂ).re

Tactic:
simpa using ha
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : 0 < a
c : ℝ
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (a_1 : ℝ) ↦ ‖Complex.exp ((↑a : ℂ) * (↑a_1 : ℂ))‖)
    (Measure.restrict volume (Iic c))

Tactic:
have := Integrable.norm <| integrableOn_exp_mul_complex_Iic (a := a) (by simpa using ha) c
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : 0 < a
c : ℝ
this :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (a_1 : ℝ) ↦ ‖Complex.exp ((↑a : ℂ) * (↑a_1 : ℂ))‖)
    (Measure.restrict volume (Iic c))
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (a * x)) (Iic c) volume

Tactic:
simpa [Complex.norm_exp] using this

Premises used: Complex.norm_exp
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (x : ℝ) ↦
      Complex.exp (a * (↑x : ℂ))) =
    -Complex.exp (a * (↑c : ℂ)) / a

Tactic:
tendsto_nhds_unique (intervalIntegral_tendsto_integral_Ioi c
    (integrableOn_exp_mul_complex_Ioi ha c) tendsto_id) ?_

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

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

Premises used: Filter.tendsto_id, MeasureTheory.intervalIntegral_tendsto_integral_Ioi, tendsto_nhds_unique, integrableOn_exp_mul_complex_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
⊢ a ≠ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
simp_rw :
  Tendsto (fun (i : ℝ) ↦ (Complex.exp (a * (↑i : ℂ)) - Complex.exp (a * (↑c : ℂ))) / a) atTop
    (𝓝 (-Complex.exp (a * (↑c : ℂ)) / a))
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in c..id i, Complex.exp (a * (↑x : ℂ))) atTop (𝓝 (-Complex.exp (a * (↑c : ℂ)) / a))

Tactic:
simp_rw [integral_exp_mul_complex (c := a) (by aesop), id_eq]

Premises used: integral_exp_mul_complex, id_eq
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
this : Tendsto (β := ℂ) (fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ))) atTop (𝓝 0)
⊢ Tendsto (fun (i : ℝ) ↦ (Complex.exp (a * (↑i : ℂ)) - Complex.exp (a * (↑c : ℂ))) / a) atTop
    (𝓝 (-Complex.exp (a * (↑c : ℂ)) / a))

Tactic:
simpa using this.sub_const _ |>.div_const _

Premises used: Filter.Tendsto.sub_const, Filter.Tendsto.div_const
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
suffices : Tendsto (β := ℂ) (fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ))) atTop (𝓝 0)
⊢ Tendsto (fun (i : ℝ) ↦ (Complex.exp (a * (↑i : ℂ)) - Complex.exp (a * (↑c : ℂ))) / a) atTop
    (𝓝 (-Complex.exp (a * (↑c : ℂ)) / a))

Tactic:
suffices Tendsto (fun x : ℝ ↦ Complex.exp (a * x)) atTop (𝓝 0) by
    simpa using this.sub_const _ |>.div_const _
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ))) atTop (𝓝 0)

Tactic:
simpa [Complex.tendsto_exp_nhds_zero_iff] using tendsto_const_nhds.neg_mul_atTop ha tendsto_id

Premises used: Complex.tendsto_exp_nhds_zero_iff, Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.neg_mul_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℂ
ha : 0 < a.re
c : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦
      Complex.exp (a * (↑x : ℂ))) =
    Complex.exp (a * (↑c : ℂ)) / a

Tactic:
simpa [neg_mul, ← mul_neg, ← Complex.ofReal_neg,
    integral_comp_neg_Ioi (f := fun x : ℝ ↦ Complex.exp (a * x))]
    using integral_exp_mul_complex_Ioi (a := -a) (by simpa) (-c)

Premises used: HMul.hMul, integral_exp_mul_complex_Ioi, Complex.ofReal_neg, Complex.ofReal, Complex.exp, integral_comp_neg_Ioi, neg_mul, Neg.neg, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < 0
c : ℝ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (x : ℝ) ↦
      (RCLike.re : (a : ℂ) → ℝ) (Complex.exp ((↑a : ℂ) * (↑x : ℂ)))) =
    HDiv.hDiv (α := ℝ) (-(RCLike.re : (a : ℂ) → ℝ) (Complex.exp ((↑a : ℂ) * (↑c : ℂ))) : ℝ) a
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (x : ℝ) ↦ rexp (a * x)) =
    -rexp (a * c) / a

Tactic:
simp_rw [Real.exp, ← RCLike.re_to_complex, Complex.ofReal_mul]

Premises used: Real.exp, RCLike.re_to_complex, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < 0
c : ℝ
rw :
  @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ Complex.exp ((↑a : ℂ) * (↑x : ℂ)))
    (Measure.restrict volume (Ioi c))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (x : ℝ) ↦
      (RCLike.re : (a : ℂ) → ℝ) (Complex.exp ((↑a : ℂ) * (↑x : ℂ)))) =
    HDiv.hDiv (α := ℝ) (-(RCLike.re : (a : ℂ) → ℝ) (Complex.exp ((↑a : ℂ) * (↑c : ℂ))) : ℝ) a

Tactic:
rw [integral_re, integral_exp_mul_complex_Ioi (by simpa using ha), RCLike.re_to_complex,
    RCLike.re_to_complex, Complex.div_ofReal_re, Complex.neg_re]

Premises used: Complex.div_ofReal_re, integral_exp_mul_complex_Ioi, Complex.neg_re, integral_re, RCLike.re_to_complex
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : a < 0
c : ℝ
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ Complex.exp ((↑a : ℂ) * (↑x : ℂ)))
    (Measure.restrict volume (Ioi c))

Tactic:
exact integrableOn_exp_mul_complex_Ioi (by simpa using ha) _

Premises used: integrableOn_exp_mul_complex_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : 0 < a
c : ℝ
⊢ -a < 0

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a : ℝ
ha : 0 < a
c : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ rexp (a * x)) =
    rexp (a * c) / a

Tactic:
simpa [neg_mul, ← mul_neg, integral_comp_neg_Ioi (f := fun x : ℝ ↦ Real.exp (a * x))]
    using integral_exp_mul_Ioi (a := -a) (by simpa) (-c)

Premises used: HMul.hMul, Real.exp, integral_exp_mul_Ioi, integral_comp_neg_Ioi, neg_mul, Neg.neg, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
⊢ HasDerivAt (fun (x : ℝ) ↦ (id x + m) ^ (a + 1) / (a + 1)) (1 * (a + 1) * (id x + m) ^ (a + 1 - 1) / (a + 1)) x

Tactic:
(((hasDerivAt_id _).add_const _).rpow_const _).div_const _

Premises used: HasDerivAt.add_const, HasDerivAt.div_const, HasDerivAt.rpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
h : (x + m) ^ a = 1 * (a + 1) * (id x + m) ^ (a + 1 - 1) / (a + 1)
convert_3 : id x + m ≠ 0 ∨ 1 ≤ a + 1
⊢ HasDerivAt (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x

Tactic:
convert! (((hasDerivAt_id _).add_const _).rpow_const _).div_const _ using 1

Premises used: HasDerivAt.add_const, HasDerivAt.div_const, HasDerivAt.rpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
linarith : a + 1 = 0 → a - -1 + -(a + 1 - 0) = 0
⊢ a + 1 ≠ 0

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

Tactic:
simp [show a + 1 ≠ 0 by linarith]
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
convert_3 : id x + m ≠ 0
⊢ id x + m ≠ 0 ∨ 1 ≤ a + 1

Tactic:
left
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
linarith : id x + m = 0 → -m - c + (id x + m - 0) + (c - x) + -(id x - x) = 0
⊢ id x + m ≠ 0

Tactic:
linarith [mem_Ici.mp hx, id_eq x]

Premises used: Set.mem_Ici, Iff.mp, id_eq
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
⊢ ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x

Tactic:
have hd : ∀ x ∈ Ici c, HasDerivAt (fun t ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x := by
    intro x hx
    convert! (((hasDerivAt_id _).add_const _).rpow_const _).div_const _ using 1
    · simp [show a + 1 ≠ 0 by linarith]
    left; linarith [mem_Ici.mp hx, id_eq x]
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x
rw : Tendsto (fun (t : ℝ) ↦ (t + m) ^ (- -(a + 1)) / - -(a + 1)) atTop (𝓝 (0 / - -(a + 1)))
⊢ Tendsto (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))

Tactic:
rw [← neg_neg (a + 1)]

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

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

Tactic:
exact (tendsto_rpow_neg_atTop (by linarith)).comp
      (tendsto_atTop_add_const_right _ m tendsto_id) |>.div_const _

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

Tactic:
have ht : Tendsto (fun t ↦ ((t + m) ^ (a + 1)) / (a + 1)) atTop (nhds (0 / (a + 1))) := by
    rw [← neg_neg (a + 1)]
    exact (tendsto_rpow_neg_atTop (by linarith)).comp
      (tendsto_atTop_add_const_right _ m tendsto_id) |>.div_const _
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x
ht_1 : Tendsto (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
t : ℝ
ht : t ∈ Ioi c
linarith : t + m < 0 → -m - c + (t + m - 0) + (c - t) = 0
⊢ 0 ≤ t + m

Tactic:
linarith [mem_Ioi.mp ht]

Premises used: Set.mem_Ioi, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x
ht : Tendsto (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (x + m) ^ a) (Ioi c) volume

Tactic:
exact integrableOn_Ioi_deriv_of_nonneg' hd
    (fun t ht ↦ rpow_nonneg (by linarith [mem_Ioi.mp ht]) a) ht

Premises used: MeasureTheory.integrableOn_Ioi_deriv_of_nonneg', Real.rpow_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a c : ℝ
ha : a < -1
hc : 0 < c
⊢ -0 < c

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
a c : ℝ
ha : a < -1
hc : 0 < c
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ a) (Ioi c) volume

Tactic:
simpa using integrableOn_add_rpow_Ioi_of_lt ha (by simpa : -0 < c)

Premises used: integrableOn_add_rpow_Ioi_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
Goal:
s t : ℝ
ht : 0 < t
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume ↔ s < -1

Tactic:
⟨fun h ↦ ?_, fun h ↦ integrableOn_Ioi_rpow_of_lt h ht⟩

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

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ integrableOn_Ioi_rpow_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
contrapose! :
  ∀ (h : -1 ≤ s), ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
⊢ s < -1

Tactic:
contrapose! h