awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
refine :
  ∀ (i : G') (hi : i ∈ f.range),
    LE.le.{u_8} (α := G'') (0 : G'') ((T (Set.preimage (β := G') (⇑f : (a : α) → G') {i}) : (a : G') → G'') i : G'')
⊢ 0 ≤ setToSimpleFunc T f

Tactic:
refine sum_nonneg fun i hi => ?_

Premises used: Finset.sum_nonneg
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
i : G'
hi : i ∈ f.range
pos :
  ∀ (h0 : i = 0),
    LE.le.{u_8} (α := G'') (0 : G'') ((T (Set.preimage (β := G') (⇑f : (a : α) → G') {i}) : (a : G') → G'') i : G'')
neg :
  ∀ (h0 : ¬i = 0),
    LE.le.{u_8} (α := G'') (0 : G'') ((T (Set.preimage (β := G') (⇑f : (a : α) → G') {i}) : (a : G') → G'') i : G'')
⊢ LE.le.{u_8} (α := G'') (0 : G'') ((T (Set.preimage (β := G') (⇑f : (a : α) → G') {i}) : (a : G') → G'') i : G'')

Tactic:
by_cases h0 : i = 0
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
i : G'
hi : i ∈ f.range
h0 : i = 0
⊢ LE.le.{u_8} (α := G'') (0 : G'') ((T (Set.preimage (β := G') (⇑f : (a : α) → G') {i}) : (a : G') → G'') i : G'')

Tactic:
simp [h0]
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
i : G'
hi : i ∈ f.range
h0 : ¬i = 0
⊢ LE.le.{u_8} (α := G'') (0 : G'') ((T (Set.preimage (β := G') (⇑f : (a : α) → G') {i}) : (a : G') → G'') i : G'')

Tactic:
hT_nonneg _ (measurableSet_fiber _ _) (measure_preimage_lt_top_of_integrable _ hfi h0) i ?_

Premises used: MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable, MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
i : G'
hi : i ∈ f.range
h0 : ¬i = 0
neg : 0 ≤ i
⊢ LE.le.{u_8} (α := G'') (0 : G'') ((T (Set.preimage (β := G') (⇑f : (a : α) → G') {i}) : (a : G') → G'') i : G'')

Tactic:
refine
    hT_nonneg _ (measurableSet_fiber _ _) (measure_preimage_lt_top_of_integrable _ hfi h0) i ?_

Premises used: MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable, MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
i : G'
hi : i ∈ f.range
h0 : ¬i = 0
⊢ Membership.mem (γ := Set G') (Set.range.{u_7, u_1 + 1} (ι := α) (⇑f : (a : α) → G')) i

Tactic:
rw [mem_range] at hi

Premises used: MeasureTheory.SimpleFunc.mem_range
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
i : G'
hi : i ∈ f.range
h0 : ¬i = 0
hi₁ : Membership.mem (γ := Set G') (Set.range.{u_7, u_1 + 1} (ι := α) (⇑f : (a : α) → G')) i
⊢ ¬i = 0

Tactic:
rw [mem_range] at hi

Premises used: MeasureTheory.SimpleFunc.mem_range
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
i : G'
hi : Membership.mem (γ := Set G') (Set.range.{u_7, u_1 + 1} (ι := α) (⇑f : (a : α) → G')) i
h0 : ¬i = 0
neg : ∀ (y : α) (hy : (f : (a : α) → G') y = i), 0 ≤ i
⊢ 0 ≤ i

Tactic:
obtain ⟨y, hy⟩ := Set.mem_range.mp hi

Premises used: Set.mem_range, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
i : G'
hi : Membership.mem (γ := Set G') (Set.range.{u_7, u_1 + 1} (ι := α) (⇑f : (a : α) → G')) i
h0 : ¬i = 0
y : α
hy : (f : (a : α) → G') y = i
neg : LE.le.{u_7} (α := G') (0 : G') ((f : (a : α) → G') y : G')
⊢ 0 ≤ i

Tactic:
rw [← hy]
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
i : G'
hi : Membership.mem (γ := Set G') (Set.range.{u_7, u_1 + 1} (ι := α) (⇑f : (a : α) → G')) i
h0 : ¬i = 0
y : α
hy : (f : (a : α) → G') y = i
⊢ LE.le.{u_7} (α := G') ((0 : (a : α) → G') y : G') ((f : (a : α) → G') y : G')

Tactic:
hf y
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
i : G'
hi : Membership.mem (γ := Set G') (Set.range.{u_7, u_1 + 1} (ι := α) (⇑f : (a : α) → G')) i
h0 : ¬i = 0
y : α
hy : (f : (a : α) → G') y = i
⊢ LE.le.{u_7} (α := G') (0 : G') ((f : (a : α) → G') y : G')

Tactic:
convert! hf y
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
inst_7 : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
h_add : FinMeasAdditive μ T
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f g : α →ₛ G'
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
hgi : Integrable.{u_7, u_1} (ε := G') (⇑g : (a : α) → G') μ
hfg : f ≤ g
rw : 0 ≤ setToSimpleFunc T (g - f)
⊢ setToSimpleFunc T f ≤ setToSimpleFunc T g

Tactic:
rw [← sub_nonneg, ← setToSimpleFunc_sub T h_add hgi hfi]

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_sub, sub_nonneg
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
inst_7 : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
h_add : FinMeasAdditive μ T
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f g : α →ₛ G'
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
hgi : Integrable.{u_7, u_1} (ε := G') (⇑g : (a : α) → G') μ
hfg : f ≤ g
⊢ 0 ≤ setToSimpleFunc T (g - f)

Tactic:
setToSimpleFunc_nonneg' T hT_nonneg _ ?_ (hgi.sub hfi)

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg'
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
inst_7 : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
h_add : FinMeasAdditive μ T
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f g : α →ₛ G'
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
hgi : Integrable.{u_7, u_1} (ε := G') (⇑g : (a : α) → G') μ
hfg : f ≤ g
refine : 0 ≤ g - f
⊢ 0 ≤ setToSimpleFunc T (g - f)

Tactic:
refine setToSimpleFunc_nonneg' T hT_nonneg _ ?_ (hgi.sub hfi)

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg'
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
inst_7 : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
h_add : FinMeasAdditive μ T
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f g : α →ₛ G'
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
hgi : Integrable.{u_7, u_1} (ε := G') (⇑g : (a : α) → G') μ
hfg : f ≤ g
x : α
simp : LE.le.{u_7} (α := G') ((f : (a : α) → G') x : G') ((g : (a : α) → G') x : G')
⊢ LE.le.{u_7} (α := G') ((0 : (a : α) → G') x : G') ((g - f : (a : α) → G') x : G')

Tactic:
simp only [coe_sub, sub_nonneg, coe_zero, Pi.zero_apply, Pi.sub_apply]

Premises used: MeasureTheory.SimpleFunc.coe_zero, Pi.zero_apply, MeasureTheory.SimpleFunc.coe_sub, sub_nonneg, Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
inst_7 : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
h_add : FinMeasAdditive μ T
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f g : α →ₛ G'
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
hgi : Integrable.{u_7, u_1} (ε := G') (⇑g : (a : α) → G') μ
hfg : f ≤ g
x : α
⊢ LE.le.{u_7} (α := G') ((f : (a : α) → G') x : G') ((g : (a : α) → G') x : G')

Tactic:
hfg x
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst : NormedAddCommGroup G''
inst_1 : PartialOrder G''
inst_2 : IsOrderedAddMonoid G''
inst_3 : NormedSpace ℝ G''
inst_4 : NormedAddCommGroup G'
inst_5 : PartialOrder G'
inst_6 : NormedSpace ℝ G'
inst_7 : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
h_add : FinMeasAdditive μ T
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f g : α →ₛ G'
hfi : Integrable.{u_7, u_1} (ε := G') (⇑f : (a : α) → G') μ
hgi : Integrable.{u_7, u_1} (ε := G') (⇑g : (a : α) → G') μ
hfg : f ≤ g
x : α
⊢ LE.le.{u_7} (α := G') ((f : (a : α) → G') x : G') ((g : (a : α) → G') x : G')

Tactic:
exact hfg x
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
m : MeasurableSpace α
T : Set α → F' →L[ℝ] F
f : α →ₛ F'
h :
  ∀ b ∈ f.range,
    norm.{u_3} (E := F) ((T (Set.preimage (β := F') (⇑f : (a : α) → F') {b}) : (a : F') → F) b : F) ≤
      ‖T (Set.preimage (β := F') (⇑f : (a : α) → F') {b})‖ * ‖b‖
⊢ LE.le (α := ℝ)
    (∑ x ∈ f.range, norm.{u_3} (E := F) ((T (Set.preimage (β := F') (⇑f : (a : α) → F') {x}) : (a : F') → F) x : F))
    (∑ x ∈ f.range, ‖T (Set.preimage (β := F') (⇑f : (a : α) → F') {x})‖ * ‖x‖)

Tactic:
gcongr with b
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
m : MeasurableSpace α
T : Set α → F' →L[ℝ] F
f : α →ₛ F'
b : F'
h : b ∈ f.range
⊢ norm.{u_3} (E := F) ((T (Set.preimage (β := F') (⇑f : (a : α) → F') {b}) : (a : F') → F) b : F) ≤
    ‖T (Set.preimage (β := F') (⇑f : (a : α) → F') {b})‖ * ‖b‖

Tactic:
apply ContinuousLinearMap.le_opNorm

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * μ.real s
f : α →ₛ F
h :
  ∀ i ∈ f.range,
    ‖T (Set.preimage (β := F) (⇑f : (a : α) → F) {i})‖ ≤ C * μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i})
⊢ LE.le (α := ℝ) (∑ x ∈ f.range, ‖T (Set.preimage (β := F) (⇑f : (a : α) → F) {x})‖ * ‖x‖)
    (∑ x ∈ f.range, C * μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) * ‖x‖)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * μ.real s
f : α →ₛ F
i : F
h : i ∈ f.range
⊢ ‖T (Set.preimage (β := F) (⇑f : (a : α) → F) {i})‖ ≤ C * μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i})

Tactic:
hT_norm _ <| SimpleFunc.measurableSet_fiber _ _

Premises used: MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * μ.real s
f : α →ₛ F
i : F
h : i ∈ f.range
⊢ ‖T (Set.preimage (β := F) (⇑f : (a : α) → F) {i})‖ ≤ C * μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i})

Tactic:
exact hT_norm _ <| SimpleFunc.measurableSet_fiber _ _

Premises used: MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * μ.real s
f : α →ₛ F
simp_rw :
  LE.le (α := ℝ) (∑ x ∈ f.range, C * μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) * ‖x‖)
    (∑ x ∈ f.range, C * μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) * ‖x‖)
⊢ ∑ x ∈ f.range, C * μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) * ‖x‖ ≤
    C * ∑ x ∈ f.range, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) * ‖x‖

Tactic:
simp_rw [mul_sum, ← mul_assoc]

Premises used: Finset.mul_sum, mul_assoc
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * μ.real s
f : α →ₛ F
⊢ LE.le (α := ℝ) (∑ x ∈ f.range, C * μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) * ‖x‖)
    (∑ x ∈ f.range, C * μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) * ‖x‖)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ LE.le (α := ℝ) (∑ x ∈ f.range, ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})‖ * ‖x‖)
    (∑ x ∈ f.range, C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖)

Tactic:
Finset.sum_le_sum fun b hb => ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
refine :
  ∀ (b : E) (hb : b ∈ f.range),
    ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {b})‖ * ‖b‖ ≤
      C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * ‖b‖
⊢ LE.le (α := ℝ) (∑ x ∈ f.range, ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})‖ * ‖x‖)
    (∑ x ∈ f.range, C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖)

Tactic:
refine Finset.sum_le_sum fun b hb => ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
b : E
hb : b ∈ f.range
inl :
  ∀ (hb : 0 ∈ f.range),
    ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {0})‖ * norm.{u_2} (E := E) 0 ≤
      C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {0}) * norm.{u_2} (E := E) 0
inr :
  ∀ (hb : b ≠ 0),
    ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {b})‖ * ‖b‖ ≤
      C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * ‖b‖
⊢ ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {b})‖ * ‖b‖ ≤
    C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * ‖b‖

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
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_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hb : 0 ∈ f.range
⊢ ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {0})‖ * norm.{u_2} (E := E) 0 ≤
    C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {0}) * norm.{u_2} (E := E) 0

Tactic:
simp