awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₁ : ∀ (ha : a ≤ a₀), ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀) a
⊢ a ∈ Iic a₀ → ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀) a

Tactic:
(ha : a ≤ a₀)
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₀
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
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀) a

Tactic:
rw [continuousWithinAt_iff_continuous_left_right]

Premises used: continuousWithinAt_iff_continuous_left_right
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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
right : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀ ∩ Ici 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

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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

Tactic:
simpa [ha] using (hf.mono_set (Iio_subset_Iio ha)).continuousWithinAt_Iic_primitive_Iio

Premises used: Set.Iio_subset_Iio, MeasureTheory.IntegrableOn.mono_set, MeasureTheory.IntegrableOn.continuousWithinAt_Iic_primitive_Iio
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₀
right : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Icc a a₀) a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀ ∩ Ici a) a

Tactic:
rw [Iic_inter_Ici]

Premises used: Set.Iic_inter_Ici
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₀
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₀
b : ℝ
hb : 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:
simp [integral_symm b a₀, ← integral_Iio_sub_Iio' hf (hf.mono_set (Iio_subset_Iio hb.2))]

Premises used: intervalIntegral.integral_Iio_sub_Iio', intervalIntegral.integral_symm, Set.Iio_subset_Iio, MeasureTheory.IntegrableOn.mono_set, And.right
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₀
⊢ ∀ 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))]
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 ∂μ)
⊢ IntervalIntegrable f μ (min a₀ a) (max a₀ a₀)

Tactic:
simpa [ha]
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 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])
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 ∂μ)
h_cwa : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a₀..b, f x ∂μ) (Icc a a₀) a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Icc a a₀) a

Tactic:
(continuousWithinAt_const.add h_cwa).congr h_split (h_split a (left_mem_Icc.2 ha))

Premises used: Iff.mpr, Set.left_mem_Icc, ContinuousWithinAt.add, continuousWithinAt_const, ContinuousWithinAt.congr
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 ∂μ)
h_cwa : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a₀..b, f x ∂μ) (Icc a a₀) a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Icc a a₀) a

Tactic:
exact (continuousWithinAt_const.add h_cwa).congr h_split (h_split a (left_mem_Icc.2 ha))

Premises used: Iff.mpr, Set.left_mem_Icc, ContinuousWithinAt.add, continuousWithinAt_const, ContinuousWithinAt.congr
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ici a₀) μ
simp_rw : ContinuousOn.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀)
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ici b, f x ∂μ) (Ici a₀)

Tactic:
simp_rw [integral_Ici_eq_integral_Ioi]

Premises used: MeasureTheory.integral_Ici_eq_integral_Ioi
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 Ioi b, f x ∂μ) (Ici a₀)

Tactic:
(hf.mono_set Ioi_subset_Ici_self).continuousOn_Ici_primitive_Ioi

Premises used: Set.Ioi_subset_Ici_self, MeasureTheory.IntegrableOn.continuousOn_Ici_primitive_Ioi, MeasureTheory.IntegrableOn.mono_set
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 Ioi b, f x ∂μ) (Ici a₀)

Tactic:
exact (hf.mono_set Ioi_subset_Ici_self).continuousOn_Ici_primitive_Ioi

Premises used: Set.Ioi_subset_Ici_self, MeasureTheory.IntegrableOn.continuousOn_Ici_primitive_Ioi, MeasureTheory.IntegrableOn.mono_set
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Iic a₀) μ
simp_rw : ContinuousOn.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀)
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iic b, f x ∂μ) (Iic a₀)

Tactic:
simp_rw [integral_Iic_eq_integral_Iio]

Premises used: MeasureTheory.integral_Iic_eq_integral_Iio
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 Iio b, f x ∂μ) (Iic a₀)

Tactic:
(hf.mono_set Iio_subset_Iic_self).continuousOn_Iic_primitive_Iio

Premises used: MeasureTheory.IntegrableOn.continuousOn_Iic_primitive_Iio, MeasureTheory.IntegrableOn.mono_set, Set.Iio_subset_Iic_self
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 Iio b, f x ∂μ) (Iic a₀)

Tactic:
exact (hf.mono_set Iio_subset_Iic_self).continuousOn_Iic_primitive_Iio

Premises used: MeasureTheory.IntegrableOn.continuousOn_Iic_primitive_Iio, MeasureTheory.IntegrableOn.mono_set, Set.Iio_subset_Iic_self
-- Module: Mathlib.MeasureTheory.Integral.ExpDecay
Goal:
a b : ℝ
h : 0 < b
⊢ Tendsto (fun (x : ℝ) ↦ -rexp (-b * x) / b) atTop (𝓝 (-0 / b))

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

Premises used: Filter.Tendsto.neg, Filter.Tendsto.div_const
-- Module: Mathlib.MeasureTheory.Integral.ExpDecay
Goal:
a b : ℝ
h : 0 < b
refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-b * x)) atTop (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ -rexp (-b * x) / b) atTop (𝓝 (-0 / b))

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

Premises used: Filter.Tendsto.neg, Filter.Tendsto.div_const
-- Module: Mathlib.MeasureTheory.Integral.ExpDecay
Goal:
a b : ℝ
h : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-b * x)) atTop (𝓝 0)

Tactic:
tendsto_exp_atBot.comp (tendsto_id.const_mul_atTop_of_neg (neg_neg_iff_pos.2 h))

Premises used: Iff.mpr, neg_neg_iff_pos, Filter.tendsto_id, Real.exp, Real.tendsto_exp_atBot, Filter.Tendsto.const_mul_atTop_of_neg, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Integral.ExpDecay
Goal:
a b : ℝ
h : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-b * x)) atTop (𝓝 0)

Tactic:
exact tendsto_exp_atBot.comp (tendsto_id.const_mul_atTop_of_neg (neg_neg_iff_pos.2 h))

Premises used: Iff.mpr, neg_neg_iff_pos, Filter.tendsto_id, Real.tendsto_exp_atBot, Filter.Tendsto.const_mul_atTop_of_neg, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Integral.ExpDecay
Goal:
a b : ℝ
h : 0 < b
⊢ 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))
-- Module: Mathlib.MeasureTheory.Integral.ExpDecay
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

Tactic:
integrableOn_Ioi_deriv_of_nonneg' (fun x _ => ?_) (fun x _ => (exp_pos _).le) this

Premises used: HMul.hMul, LT.lt.le, MeasureTheory.integrableOn_Ioi_deriv_of_nonneg', Neg.neg, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Integral.ExpDecay
Goal:
a b : ℝ
h : 0 < b
this : Tendsto (fun (x : ℝ) ↦ -rexp (-b * x) / b) atTop (𝓝 (-0 / b))
refine : ∀ x ∈ Ici a, HasDerivAt (fun (x : ℝ) ↦ -rexp (-b * x) / b) (rexp (-b * x)) x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * x)) (Ioi a) volume

Tactic:
refine integrableOn_Ioi_deriv_of_nonneg' (fun x _ => ?_) (fun x _ => (exp_pos _).le) this

Premises used: LT.lt.le, MeasureTheory.integrableOn_Ioi_deriv_of_nonneg', Real.exp_pos
-- Module: Mathlib.MeasureTheory.Integral.ExpDecay
Goal:
a b : ℝ
h : 0 < b
this : Tendsto (fun (x : ℝ) ↦ -rexp (-b * x) / b) atTop (𝓝 (-0 / b))
x : ℝ
h_1 : x ∈ Ici a
⊢ HasDerivAt (fun (x : ℝ) ↦ -rexp (-b * x) / b) (rexp (-b * x)) x

Tactic:
simpa [h.ne'] using ((hasDerivAt_id x).const_mul b).neg.exp.neg.div_const b

Premises used: HasDerivAt.neg, HasDerivAt.exp, hasDerivAt_id, LT.lt.ne', HasDerivAt.const_mul, HasDerivAt.div_const
-- Module: Mathlib.MeasureTheory.Integral.ExpDecay
Goal:
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
hf : ContinuousOn f (Ici a)
ho : Asymptotics.IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ rexp (-b * x)
⊢ ‖f a‖ₑ ≠ ⊤

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddMonoid β
x x_1 : Set α
h : MeasurableSet x
h_1 : MeasurableSet x_1
h_2 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)
h_3 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
h_4 : Disjoint x x_1
⊢ 0 (x ∪ x_1) = HAdd.hAdd (α := β) (0 x) (0 x_1)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddMonoid β
inst_1 : DistribSMul 𝕜 β
hT : FinMeasAdditive μ T
c : 𝕜
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
⊢ (fun (s : Set α) ↦ c • T s) (s ∪ t) =
    HAdd.hAdd (α := β) ((fun (s : Set α) ↦ c • T s) s) ((fun (s : Set α) ↦ c • T s) t)

Tactic:
simp [hT s t hs ht hμs hμt hst]
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddMonoid β
μ' : Measure α
h :
  ∀ (s : Set α),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hT : FinMeasAdditive μ T
⊢ FinMeasAdditive μ' T

Tactic:
fun s t hs ht hμ's hμ't hst =>
  hT s t hs ht (mt (h s hs) hμ's) (mt (h t ht) hμ't) hst

Premises used: mt, MeasureTheory.FinMeasAdditive
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddMonoid β
ν : Measure α
hT : FinMeasAdditive μ T
⊢ FinMeasAdditive (μ + ν) T

Tactic:
hT.of_eq_top_imp_eq_top fun s _ hμs =>
    top_unique <| hμs.symm.trans_le (Measure.le_add_right le_rfl s)

Premises used: le_rfl, MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top, Eq.trans_le, top_unique, MeasureTheory.Measure.le_add_right, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddMonoid β
ν : Measure α
hT : FinMeasAdditive μ T
⊢ FinMeasAdditive (ν + μ) T

Tactic:
hT.of_eq_top_imp_eq_top fun s _ hμs =>
    top_unique <| hμs.symm.trans_le (Measure.le_add_left le_rfl s)

Premises used: le_rfl, MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top, Eq.trans_le, top_unique, MeasureTheory.Measure.le_add_left, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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

Tactic:
of_eq_top_imp_eq_top (fun s _ hμs => ?_) hT

Premises used: MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddMonoid β
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : FinMeasAdditive (c • μ) T
refine :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (hμs : Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ FinMeasAdditive μ T

Tactic:
refine of_eq_top_imp_eq_top (fun s _ hμs => ?_) hT

Premises used: MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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∞)
⊢ 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

Premises used: ENNReal.mul_eq_top, MeasureTheory.Measure.smul_apply, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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∞)
⊢ ¬c = 0 ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [hc_ne_top, or_false, Ne, false_and] at hμs

Premises used: false_and, Ne, or_false
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
hμs.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact hμs.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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

Tactic:
of_eq_top_imp_eq_top (fun s _ hμs => ?_) hT

Premises used: MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddMonoid β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
refine :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ FinMeasAdditive (c • μ) T

Tactic:
refine of_eq_top_imp_eq_top (fun s _ hμs => ?_) hT

Premises used: MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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∞)
rw :
  c ≠ 0 ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
    c = ∞ ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [Measure.smul_apply, smul_eq_mul, ENNReal.mul_eq_top]

Premises used: ENNReal.mul_eq_top, MeasureTheory.Measure.smul_apply, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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∞)
simp :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
    c = ∞ ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ c ≠ 0 ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
    c = ∞ ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [hc_ne_zero, true_and, Ne, not_false_iff]

Premises used: Ne, not_false_iff, true_and
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
    c = ∞ ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
Or.inl hμs

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
    c = ∞ ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact Or.inl hμs

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst : AddMonoid β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ FinMeasAdditive (c • μ) T ↔ FinMeasAdditive μ T

Tactic:
⟨fun hT => of_smul_measure hc_ne_top hT, fun hT => smul_measure c hc_ne_zero hT⟩

Premises used: MeasureTheory.FinMeasAdditive.smul_measure, MeasureTheory.FinMeasAdditive.of_smul_measure, Iff.intro
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : AddCancelMonoid β
T : Set α → β
hT : FinMeasAdditive μ T
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have h_empty : μ ∅ ≠ ∞ := (measure_empty.le.trans_lt ENNReal.coe_lt_top).ne
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 (∅ ∪ ∅) = T ∅ + T ∅

Tactic:
specialize hT ∅ ∅ MeasurableSet.empty MeasurableSet.empty h_empty h_empty (disjoint_empty _)

Premises used: MeasurableSet.empty, Set.disjoint_empty, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 ∅ = T ∅ + T ∅

Tactic:
rw [Set.union_empty] at hT

Premises used: Set.union_empty