awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c c' : ℝ≥0∞
hc : c ≠ ∞
hc' : c' ≠ ∞
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hf : ¬Integrable f μ
h_int : ∀ (g : α → E), ¬Integrable g μ → ¬Integrable g μ'
neg : 0 = setToFun μ' T hT' f
⊢ setToFun μ T hT f = setToFun μ' T hT' f

Tactic:
simp_rw [setToFun_undef _ hf, setToFun_undef _ (h_int f hf)]

Premises used: MeasureTheory.setToFun_undef
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f (μ + μ')
⊢ setToFun (μ + μ') T hT_add f = setToFun μ T hT f

Tactic:
setToFun_congr_measure_of_integrable 1 one_ne_top ?_ hT_add hT f hf

Premises used: OfNat.ofNat, MeasureTheory.setToFun_congr_measure_of_integrable, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f (μ + μ')
refine : μ ≤ HSMul.hSMul (α := ℝ≥0∞) 1 (μ + μ')
⊢ setToFun (μ + μ') T hT_add f = setToFun μ T hT f

Tactic:
refine setToFun_congr_measure_of_integrable 1 one_ne_top ?_ hT_add hT f hf

Premises used: OfNat.ofNat, MeasureTheory.setToFun_congr_measure_of_integrable, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f (μ + μ')
rw : μ ≤ μ + μ'
⊢ μ ≤ HSMul.hSMul (α := ℝ≥0∞) 1 (μ + μ')

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f (μ + μ')
nth_rw : μ + 0 ≤ μ + μ'
⊢ μ ≤ μ + μ'

Tactic:
nth_rw 1 [← add_zero μ]

Premises used: add_zero
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f (μ + μ')
⊢ μ + 0 ≤ μ + μ'

Tactic:
add_le_add le_rfl bot_le

Premises used: le_rfl, add_le_add, bot_le
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f (μ + μ')
⊢ μ + 0 ≤ μ + μ'

Tactic:
exact add_le_add le_rfl bot_le

Premises used: le_rfl, add_le_add, bot_le
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ' T C
f : α → E
hf : Integrable f (μ + μ')
⊢ setToFun (μ + μ') T hT_add f = setToFun μ' T hT f

Tactic:
setToFun_congr_measure_of_integrable 1 one_ne_top ?_ hT_add hT f hf

Premises used: OfNat.ofNat, MeasureTheory.setToFun_congr_measure_of_integrable, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ' T C
f : α → E
hf : Integrable f (μ + μ')
refine : μ' ≤ HSMul.hSMul (α := ℝ≥0∞) 1 (μ + μ')
⊢ setToFun (μ + μ') T hT_add f = setToFun μ' T hT f

Tactic:
refine setToFun_congr_measure_of_integrable 1 one_ne_top ?_ hT_add hT f hf

Premises used: OfNat.ofNat, MeasureTheory.setToFun_congr_measure_of_integrable, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ' T C
f : α → E
hf : Integrable f (μ + μ')
rw : μ' ≤ μ + μ'
⊢ μ' ≤ HSMul.hSMul (α := ℝ≥0∞) 1 (μ + μ')

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ' T C
f : α → E
hf : Integrable f (μ + μ')
⊢ μ' ≤ μ + μ'

Tactic:
Measure.le_add_left le_rfl

Premises used: le_rfl, MeasureTheory.Measure.le_add_left
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ' T C
f : α → E
hf : Integrable f (μ + μ')
⊢ μ' ≤ μ + μ'

Tactic:
exact Measure.le_add_left le_rfl

Premises used: le_rfl, MeasureTheory.Measure.le_add_left
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
f : α → E
ν : Measure α
hTμ : DominatedFinMeasAdditive μ T C
hTν : DominatedFinMeasAdditive ν T' C'
hμ : Integrable f μ
hν : Integrable f ν
hTμ_add : DominatedFinMeasAdditive (μ + ν) T (max C 0)
hTν_add : DominatedFinMeasAdditive (μ + ν) T' (max C' 0)
rw : setToFun μ T hTμ f + setToFun (μ + ν) T' hTν_add f = setToFun μ T hTμ f + setToFun ν T' hTν f
rw₁ rw₂ : setToFun μ T hTμ f + setToFun ν T' hTν f = setToFun μ T hTμ f + setToFun ν T' hTν f
⊢ setToFun (μ + ν) T hTμ_add f + setToFun (μ + ν) T' hTν_add f = setToFun μ T hTμ f + setToFun ν T' hTν f

Tactic:
rw [setToFun_congr_measure_of_add_right hTμ_add hTμ f (hμ.add_measure hν),
        setToFun_congr_measure_of_add_left hTν_add hTν f (hμ.add_measure hν)]

Premises used: MeasureTheory.Integrable.add_measure, MeasureTheory.setToFun_congr_measure_of_add_left, MeasureTheory.setToFun_congr_measure_of_add_right
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
f : α → E
ν : Measure α
hTμ : DominatedFinMeasAdditive μ T C
hTν : DominatedFinMeasAdditive ν T' C'
hμ : Integrable f μ
hν : Integrable f ν
⊢ setToFun (μ + ν) (T - T') ⋯ f = setToFun μ T hTμ f - setToFun ν T' hTν f

Tactic:
simp [sub_eq_add_neg, setToFun_add_measure hTμ hTν.neg hμ hν, setToFun_neg' hTν]

Premises used: MeasureTheory.DominatedFinMeasAdditive.neg, sub_eq_add_neg, MeasureTheory.setToFun_add_measure, MeasureTheory.setToFun_neg'
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
f : α → E
ι : Type u_7
s : Finset ι
μ : ι → Measure α
T : ι → Set α → E →L[ℝ] F
C : ι → ℝ
hTs : ∀ (i : ι), DominatedFinMeasAdditive (μ i) (T i) (C i)
i : ι
hf : ∀ (i_1 : ι), Membership.mem (γ := Finset ι) {i} i_1 → Integrable f (μ i_1)
⊢ setToFun (∑ i ∈ {i}, μ i) (∑ i ∈ {i}, T i) ⋯ f = ∑ i ∈ {i}, setToFun (μ i) (T i) ⋯ f

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
f : α → E
ι : Type u_7
s_1 : Finset ι
μ : ι → Measure α
T : ι → Set α → E →L[ℝ] F
C : ι → ℝ
hTs : ∀ (i : ι), DominatedFinMeasAdditive (μ i) (T i) (C i)
i : ι
s : Finset ι
his : i ∉ s
hs' : s.Nonempty
ih :
  ∀ (hf : ∀ i ∈ s, Integrable f (μ i)), setToFun (∑ i ∈ s, μ i) (∑ i ∈ s, T i) ⋯ f = ∑ i ∈ s, setToFun (μ i) (T i) ⋯ f
hf : ∀ i_1 ∈ Finset.cons i s his, Integrable f (μ i_1)
⊢ setToFun (∑ i ∈ Finset.cons i s his, μ i) (∑ i ∈ Finset.cons i s his, T i) ⋯ f =
    ∑ i ∈ Finset.cons i s his, setToFun (μ i) (T i) ⋯ f

Tactic:
simpa [his, ih fun j hj => hf j (Finset.mem_cons_of_mem hj)] using
      setToFun_add_measure (hTs i) (DominatedFinMeasAdditive.finsetSum_measure hs' μ T C hTs)
      (hf i (Finset.mem_cons_self i s))
      (integrable_finsetSum_measure.2 fun j hj => hf j (Finset.mem_cons_of_mem hj))

Premises used: Iff.mpr, Finset.mem_cons_of_mem, MeasureTheory.integrable_finsetSum_measure, MeasureTheory.DominatedFinMeasAdditive.finsetSum_measure, MeasureTheory.setToFun_add_measure, Finset.mem_cons_self
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
f : α → E
ι : Type u_7
s : Finset ι
hs : s.Nonempty
μ : ι → Measure α
T : ι → Set α → E →L[ℝ] F
C : ι → ℝ
hTs : ∀ (i : ι), DominatedFinMeasAdditive (μ i) (T i) (C i)
hf : ∀ i ∈ s, Integrable f (μ i)
singleton :
  ∀ (i : ι) (hf : ∀ (i_1 : ι), Membership.mem (γ := Finset ι) {i} i_1 → Integrable f (μ i_1)),
    setToFun (∑ i ∈ {i}, μ i) (∑ i ∈ {i}, T i) ⋯ f = ∑ i ∈ {i}, setToFun (μ i) (T i) ⋯ f
cons :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s) (hs' : s.Nonempty)
    (ih :
      ∀ (hf : ∀ i ∈ s, Integrable f (μ i)),
        setToFun (∑ i ∈ s, μ i) (∑ i ∈ s, T i) ⋯ f = ∑ i ∈ s, setToFun (μ i) (T i) ⋯ f)
    (hf : ∀ i_1 ∈ Finset.cons i s his, Integrable f (μ i_1)),
    setToFun (∑ i ∈ Finset.cons i s his, μ i) (∑ i ∈ Finset.cons i s his, T i) ⋯ f =
      ∑ i ∈ Finset.cons i s his, setToFun (μ i) (T i) ⋯ f
⊢ setToFun (∑ i ∈ s, μ i) (∑ i ∈ s, T i) ⋯ f = ∑ i ∈ s, setToFun (μ i) (T i) ⋯ f

Tactic:
induction hs using Finset.Nonempty.cons_induction with
  | singleton i => simp
  | @cons i s his hs' ih =>
    simpa [his, ih fun j hj => hf j (Finset.mem_cons_of_mem hj)] using
      setToFun_add_measure (hTs i) (DominatedFinMeasAdditive.finsetSum_measure hs' μ T C hTs)
      (hf i (Finset.mem_cons_self i s))
      (integrable_finsetSum_measure.2 fun j hj => hf j (Finset.mem_cons_of_mem hj))

Premises used: Singleton.singleton
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive (HSMul.hSMul (α := ℝ≥0∞) ∞ μ) T C
f : α → E
⊢ setToFun (HSMul.hSMul (α := ℝ≥0∞) ∞ μ) T hT f = 0

Tactic:
setToFun_measure_zero' hT fun s _ hμs => ?_

Premises used: MeasureTheory.setToFun_measure_zero'
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive (HSMul.hSMul (α := ℝ≥0∞) ∞ μ) T C
f : α → E
refine :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (hμs : LT.lt (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ setToFun (HSMul.hSMul (α := ℝ≥0∞) ∞ μ) T hT f = 0

Tactic:
refine setToFun_measure_zero' hT fun s _ hμs => ?_

Premises used: MeasureTheory.setToFun_measure_zero'
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive (HSMul.hSMul (α := ℝ≥0∞) ∞ μ) T C
f : α → E
s : Set α
h : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [lt_top_iff_ne_top] at hμs

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive (HSMul.hSMul (α := ℝ≥0∞) ∞ μ) T C
f : α → E
s : Set α
h : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [true_and, Measure.smul_apply, ENNReal.mul_eq_top,
    top_ne_zero, Ne, not_false_iff, not_or, Classical.not_not, smul_eq_mul] at hμs

Premises used: Classical.not_not, Ne, ENNReal.mul_eq_top, not_or, MeasureTheory.Measure.smul_apply, smul_eq_mul, not_false_iff, ENNReal.top_ne_zero, true_and
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive (HSMul.hSMul (α := ℝ≥0∞) ∞ μ) T C
f : α → E
s : Set α
h : MeasurableSet s
hμs :
  ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [hμs.right, Measure.smul_apply, mul_zero, smul_eq_mul]

Premises used: MulZeroClass.mul_zero, And.right, MeasureTheory.Measure.smul_apply, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
pos : ∀ (hc0 : c = 0), setToFun μ T hT f = setToFun (c • μ) T hT_smul f
neg : ∀ (hc0 : ¬c = 0), setToFun μ T hT f = setToFun (c • μ) T hT_smul f
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul f

Tactic:
by_cases hc0 : c = 0
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : c = 0
⊢ @DominatedFinMeasAdditive _ _ _ m 0 T C'

Tactic:
simp [hc0] at hT_smul
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive μ T C
hT_smul_1 : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : c = 0
hT_smul : @DominatedFinMeasAdditive _ _ _ m 0 T C'
⊢ ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0

Tactic:
have h : ∀ s, MeasurableSet s → μ s < ∞ → T s = 0 := fun s hs _ => hT_smul.eq_zero hs
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive μ T C
hT_smul_1 : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : c = 0
hT_smul : @DominatedFinMeasAdditive _ _ _ m 0 T C'
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
pos : c • μ = 0
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul_1 f

Tactic:
rw [setToFun_zero_left' _ h, setToFun_measure_zero]

Premises used: MeasureTheory.setToFun_measure_zero, MeasureTheory.setToFun_zero_left'
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive μ T C
hT_smul_1 : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : c = 0
hT_smul : @DominatedFinMeasAdditive _ _ _ m 0 T C'
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
⊢ c • μ = 0

Tactic:
simp [hc0]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : ¬c = 0
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul f

Tactic:
setToFun_congr_measure c⁻¹ c ?_ hc_ne_top (le_of_eq ?_) le_rfl hT hT_smul f

Premises used: le_rfl, Inv.inv, MeasureTheory.setToFun_congr_measure, le_of_eq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : ¬c = 0
neg : c⁻¹ ≠ ∞
neg₁ : μ = c⁻¹ • c • μ
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul f

Tactic:
refine setToFun_congr_measure c⁻¹ c ?_ hc_ne_top (le_of_eq ?_) le_rfl hT hT_smul f

Premises used: le_rfl, Inv.inv, MeasureTheory.setToFun_congr_measure, le_of_eq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : ¬c = 0
⊢ c⁻¹ ≠ ∞

Tactic:
simp [hc0]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : ¬c = 0
neg : μ = (c⁻¹ * c) • μ
neg₁ : μ = HSMul.hSMul (α := ℝ≥0∞) 1 μ
neg₂ neg₃ : μ = μ
⊢ μ = c⁻¹ • c • μ

Tactic:
rw [smul_smul, ENNReal.inv_mul_cancel hc0 hc_ne_top, one_smul]

Premises used: smul_smul, one_smul, ENNReal.inv_mul_cancel
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
⊢ (↑c : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
⊢ setToFun μ T hT f = setToFun ((↑c : ℝ≥0∞) • μ) T hT_smul f

Tactic:
apply setToFun_congr_smul_measure _ (by simp)

Premises used: MeasureTheory.setToFun_congr_smul_measure
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' μ'' : Measure α
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T' C'
hT'' : DominatedFinMeasAdditive μ'' T'' C''
h :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ + μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
⊢ DominatedFinMeasAdditive (μ + μ') T C

Tactic:
have I : DominatedFinMeasAdditive (μ + μ') T C := .add_measure_right _ _ hT hC
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' μ'' : Measure α
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T' C'
hT'' : DominatedFinMeasAdditive μ'' T'' C''
h :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ + μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
⊢ setToFun (μ + μ') T I f = setToFun μ T hT f

Tactic:
have A : setToFun (μ + μ') T I f = setToFun μ T hT f :=
    setToFun_congr_measure_of_add_right _ _ _ (hf.add_measure hf')