awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
⊢ AEStronglyMeasurable ((Iio a).indicator f) μ
have h : AEStronglyMeasurable f (μ.restrict (Iio a))
Tactic: rw [aestronglyMeasurable_indicator_iff measurableSet_Iio]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, ∀ᵐ (a : ℝ) ∂μ, ‖(Iio n).indicator f a‖ ≤ (Iio a₀).indicator (norm ∘ f) a
have h : ∀ (a : ℝ) (ha : a ∈ Iic a₀), ∀ᵐ (a_1 : ℝ) ∂μ, ‖(Iio a).indicator f a_1‖ ≤ (Iio a₀).indicator (norm ∘ f) a_1
Tactic: filter_upwards [self_mem_nhdsWithin] with a ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
⊢ ∀ᵐ (a_1 : ℝ) ∂μ, ‖(Iio a).indicator f a_1‖ ≤ (Iio a₀).indicator (norm ∘ f) a_1
have h : ∀ (x : ℝ), ‖(Iio a).indicator f x‖ ≤ (Iio a₀).indicator (norm ∘ f) x
Tactic: refine ae_of_all _ fun x ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
x : ℝ
⊢ ‖(Iio a).indicator f x‖ ≤ (Iio a₀).indicator (norm ∘ f) x
have h : (Iio a).indicator (fun (a : ℝ) ↦ ‖f a‖) x ≤ (Iio a₀).indicator (norm ∘ f) x
Tactic: rw [norm_indicator_eq_indicator_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
⊢ ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun (n : ℝ) ↦ (Iio n).indicator f a) (𝓝[≤] a₀) (𝓝 ((Iio a₀).indicator f a))
have h_lim : ∀ (x : ℝ), Tendsto (fun (n : ℝ) ↦ (Iio n).indicator f x) (𝓝[≤] a₀) (𝓝 ((Iio a₀).indicator f x))
Tactic: refine ae_of_all _ fun x ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
⊢ Tendsto (fun (n : ℝ) ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))
have pos : ∀ (hx : x < a₀), Tendsto (fun (n : ℝ) ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))
Tactic: by_cases hx : x < a₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
pos : ∀ (hx : x < a₀), Tendsto (fun (n : ℝ) ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))
⊢ Tendsto (fun (n : ℝ) ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))
have neg : ∀ (hx : ¬x < a₀), Tendsto (fun (n : ℝ) ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))
Tactic: by_cases hx : x < a₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : x < a₀
⊢ Tendsto (fun (n : ℝ) ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))
have pos : EventuallyEq.{0, u_1} (β := E) (𝓝[≤] a₀) (fun (x_1 : ℝ) ↦ if x < a₀ then f x else 0) fun (n : ℝ) ↦
  if x < n then f x else 0
Tactic: apply tendsto_const_nhds.congr'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : ¬x < a₀
⊢ Tendsto (fun (n : ℝ) ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))
have neg : EventuallyEq.{0, u_1} (β := E) (𝓝[≤] a₀) (fun (x_1 : ℝ) ↦ if x < a₀ then f x else 0) fun (n : ℝ) ↦
  if x < n then f x else 0
Tactic: apply tendsto_const_nhds.congr'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : x < a₀
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≤] a₀) (fun (x_1 : ℝ) ↦ if x < a₀ then f x else 0) fun (n : ℝ) ↦
    if x < n then f x else 0
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x_1 : ℝ |
      x_1 ∈ Ioi x →
        Membership.mem (γ := Set ℝ)
          {x_2 : ℝ |
            (fun (x_3 : ℝ) ↦
                Eq.{u_1 + 1} (α := E) ((fun (x_4 : ℝ) ↦ if x < a₀ then f x else 0) x_3)
                  ((fun (n : ℝ) ↦ if x < n then f x else 0) x_3))
              x_2}
          x_1}
    a
Tactic: filter_upwards [mem_nhdsWithin_of_mem_nhds (Ioi_mem_nhds hx)] with a ha using by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : x < a₀
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x_1 : ℝ |
        x_1 ∈ Ioi x →
          Membership.mem (γ := Set ℝ)
            {x_2 : ℝ |
              (fun (x_3 : ℝ) ↦
                  Eq.{u_1 + 1} (α := E) ((fun (x_4 : ℝ) ↦ if x < a₀ then f x else 0) x_3)
                    ((fun (n : ℝ) ↦ if x < n then f x else 0) x_3))
                x_2}
            x_1}
      a
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≤] a₀) (fun (x_1 : ℝ) ↦ if x < a₀ then f x else 0) fun (n : ℝ) ↦
    if x < n then f x else 0
have h₁ : ∀ a ∈ Ioi x, (if x < a₀ then f x else 0) = if x < a then f x else 0
Tactic: filter_upwards [mem_nhdsWithin_of_mem_nhds (Ioi_mem_nhds hx)] with a ha using by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : ¬x < a₀
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≤] a₀) (fun (x_1 : ℝ) ↦ if x < a₀ then f x else 0) fun (n : ℝ) ↦
    if x < n then f x else 0
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x_1 : ℝ |
      x_1 ∈ Iic a₀ →
        Membership.mem (γ := Set ℝ)
          {x_2 : ℝ |
            (fun (x_3 : ℝ) ↦
                Eq.{u_1 + 1} (α := E) ((fun (x_4 : ℝ) ↦ if x < a₀ then f x else 0) x_3)
                  ((fun (n : ℝ) ↦ if x < n then f x else 0) x_3))
              x_2}
          x_1}
    a
Tactic: filter_upwards [self_mem_nhdsWithin] with a ha using by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : ¬x < a₀
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x_1 : ℝ |
        x_1 ∈ Iic a₀ →
          Membership.mem (γ := Set ℝ)
            {x_2 : ℝ |
              (fun (x_3 : ℝ) ↦
                  Eq.{u_1 + 1} (α := E) ((fun (x_4 : ℝ) ↦ if x < a₀ then f x else 0) x_3)
                    ((fun (n : ℝ) ↦ if x < n then f x else 0) x_3))
                x_2}
            x_1}
      a
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≤] a₀) (fun (x_1 : ℝ) ↦ if x < a₀ then f x else 0) fun (n : ℝ) ↦
    if x < n then f x else 0
have h₁ : ∀ a ∈ Iic a₀, (if x < a₀ then f x else 0) = if x < a then f x else 0
Tactic: filter_upwards [self_mem_nhdsWithin] with a ha using by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
⊢ a ∈ Iic a₀ → ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀) a
have a₁ : ∀ (ha : a ≤ a₀), ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀) a
Tactic: (ha : a ≤ a₀)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀) a
have rw : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀ ∩ Iic a) a ∧
  ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀ ∩ Ici a) a
Tactic: rw [continuousWithinAt_iff_continuous_left_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀ ∩ Iic a) a ∧
    ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀ ∩ Ici a) a
have left : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀ ∩ Iic a) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
left : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀ ∩ Iic a) a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀ ∩ Iic a) a ∧
    ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀ ∩ Ici a) a
have right : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀ ∩ Ici a) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀ ∩ Ici a) a
have right : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Icc a a₀) a
Tactic: rw [Iic_inter_Ici]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Icc a a₀) a
have h_int : IntervalIntegrable f μ a a₀
Tactic: have h_int : IntervalIntegrable f μ a a₀ :=
      (intervalIntegrable_iff_integrableOn_Ico_of_le ha).2 <| hf.mono_set Ico_subset_Iio_self
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
h_int : IntervalIntegrable f μ a a₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Icc a a₀) a
have h_split : ∀ b ∈ Icc a a₀,
  ∫ (x : ℝ) in Iio b, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in Iio a₀, f x ∂μ) (∫ (x : ℝ) in a₀..b, f x ∂μ)
Tactic: have h_split : ∀ b ∈ Icc a a₀, ∫ x in Iio b, f x ∂μ =
        (∫ x in Iio a₀, f x ∂μ) + ∫ x in a₀..b, f x ∂μ := by
      intro b hb
      simp [integral_symm b a₀, ← integral_Iio_sub_Iio' hf (hf.mono_set (Iio_subset_Iio hb.2))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
h_int : IntervalIntegrable f μ a a₀
h_split :
  ∀ b ∈ Icc a a₀,
    ∫ (x : ℝ) in Iio b, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in Iio a₀, f x ∂μ) (∫ (x : ℝ) in a₀..b, f x ∂μ)
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Icc a a₀) a
have h_cwa : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a₀..b, f x ∂μ) (Icc a a₀) a
Tactic: have h_cwa : ContinuousWithinAt (fun b ↦ ∫ x in a₀..b, f x ∂μ) (Icc a a₀) a :=
      continuousWithinAt_primitive (measure_singleton a) (by simpa [ha])
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ici a₀) μ
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ici b, f x ∂μ) (Ici a₀)
have simp_rw : ContinuousOn.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀)
Tactic: simp_rw [integral_Ici_eq_integral_Ioi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Iic a₀) μ
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iic b, f x ∂μ) (Iic a₀)
have simp_rw : ContinuousOn.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀)
Tactic: simp_rw [integral_Iic_eq_integral_Iio]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.ExpDecay (goal)
Goal:
a b : ℝ
h : 0 < b
⊢ Tendsto (fun (x : ℝ) ↦ -rexp (-b * x) / b) atTop (𝓝 (-0 / b))
have refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-b * x)) atTop (𝓝 0)
Tactic: refine Tendsto.div_const (Tendsto.neg ?_) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.ExpDecay (hypothesis)
Goal:
a b : ℝ
h : 0 < b
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * x)) (Ioi a) volume
have this : Tendsto (fun (x : ℝ) ↦ -rexp (-b * x) / b) atTop (𝓝 (-0 / b))
Tactic: have : Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b)) := by
    refine Tendsto.div_const (Tendsto.neg ?_) _
    exact tendsto_exp_atBot.comp (tendsto_id.const_mul_atTop_of_neg (neg_neg_iff_pos.2 h))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.ExpDecay (goal)
Goal:
a b : ℝ
h : 0 < b
this : Tendsto (fun (x : ℝ) ↦ -rexp (-b * x) / b) atTop (𝓝 (-0 / b))
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * x)) (Ioi a) volume
have refine : ∀ x ∈ Ici a, HasDerivAt (fun (x : ℝ) ↦ -rexp (-b * x) / b) (rexp (-b * x)) x
Tactic: refine integrableOn_Ioi_deriv_of_nonneg' (fun x _ => ?_) (fun x _ => (exp_pos _).le) this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddMonoid β
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : FinMeasAdditive (c • μ) T
⊢ FinMeasAdditive μ T
have refine : ∀ (s : Set α),
  MeasurableSet s →
    ∀ (hμs : Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine of_eq_top_imp_eq_top (fun s _ hμs => ?_) hT
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddMonoid β
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : FinMeasAdditive (c • μ) T
s : Set α
h : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have hμs₁ : c ≠ 0 ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
  c = ∞ ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Measure.smul_apply, smul_eq_mul, ENNReal.mul_eq_top] at hμs
Cleared hypotheses: hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddMonoid β
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : FinMeasAdditive (c • μ) T
s : Set α
h : MeasurableSet s
hμs :
  c ≠ 0 ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
    c = ∞ ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have hμs₁ : ¬c = 0 ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: simp only [hc_ne_top, or_false, Ne, false_and] at hμs
Cleared hypotheses: hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddMonoid β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
⊢ FinMeasAdditive (c • μ) T
have refine : ∀ (s : Set α),
  MeasurableSet s →
    ∀ (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
      Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine of_eq_top_imp_eq_top (fun s _ hμs => ?_) hT
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddMonoid β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
h : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : c ≠ 0 ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
  c = ∞ ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Measure.smul_apply, smul_eq_mul, ENNReal.mul_eq_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddMonoid β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
h : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ c ≠ 0 ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
    c = ∞ ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
  c = ∞ ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [hc_ne_zero, true_and, Ne, not_false_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : AddCancelMonoid β
T : Set α → β
hT : FinMeasAdditive μ T
⊢ T ∅ = 0
have h_empty : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have h_empty : μ ∅ ≠ ∞ := (measure_empty.le.trans_lt ENNReal.coe_lt_top).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : AddCancelMonoid β
T : Set α → β
hT : FinMeasAdditive μ T
h_empty : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ T ∅ = 0
have hT₁ : T (∅ ∪ ∅) = T ∅ + T ∅
Tactic: specialize hT ∅ ∅ MeasurableSet.empty MeasurableSet.empty h_empty h_empty (disjoint_empty _)
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : AddCancelMonoid β
T : Set α → β
h_empty : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)
hT : T (∅ ∪ ∅) = T ∅ + T ∅
⊢ T ∅ = 0
have hT₁ : T ∅ = T ∅ + T ∅
Tactic: rw [Set.union_empty] at hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : AddCancelMonoid β
T : Set α → β
h_empty : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)
hT : T ∅ = T ∅ + T ∅
⊢ T ∅ = 0
have hT₁ : T ∅ + 0 = T ∅ + T ∅
Tactic: nth_rw 1 [← add_zero (T ∅)] at hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T T' : Set α → β
inst : AddCommMonoid β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
⊢ (T + T') (s ∪ t) = (T + T') s + (T + T') t
have simp : T s + T t + (T' s + T' t) = T s + T' s + (T t + T' t)
Tactic: simp only [hT s t hs ht hμs hμt hst, hT' s t hs ht hμs hμt hst, Pi.add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
hSp : ∀ i ∈ sι, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
have revert : ∀ (hSp : ∀ i ∈ sι, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
  (h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
Tactic: revert hSp h_disj
Cleared hypotheses: hSp, h_disj
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
⊢ ∀ (hSp : ∀ i ∈ sι, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
have refine_1 : ∀
  (hSp :
    ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
  (h_disj :
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → i ≠ j → Disjoint (S i) (S j)),
  T (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), S i) = ∑ i ∈ ∅, T (S i)
Tactic: refine Finset.induction_on sι ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
refine_1 :
  ∀
    (hSp :
      ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → i ≠ j → Disjoint (S i) (S j)),
    T (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), S i) = ∑ i ∈ ∅, T (S i)
⊢ ∀ (hSp : ∀ i ∈ sι, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
have refine_2 : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    (∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)) →
      ∀ (hSp : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
        T (⋃ i ∈ insert a s, S i) = ∑ i ∈ insert a s, T (S i)
Tactic: refine Finset.induction_on sι ?_ ?_