awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑g : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
hx_ne : x ≠ 0
rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑g : (a : α) → E) {-x}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑(-g) : (a : α) → E) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [SimpleFunc.coe_neg, Pi.neg_def, ← Function.comp_def, preimage_comp, neg_preimage,
    Set.neg_singleton]

Premises used: Set.preimage_comp, Function.comp_def, MeasureTheory.SimpleFunc.coe_neg, Set.neg_preimage, Set.neg_singleton, Pi.neg_def
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑g : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
hx_ne : x ≠ 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑g : (a : α) → E) {-x}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
hg (-x) ?_

Premises used: Neg.neg
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑g : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
hx_ne : x ≠ 0
refine : -x ≠ 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑g : (a : α) → E) {-x}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine hg (-x) ?_

Premises used: Neg.neg
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg :
  ∀ (y : E),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑g : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
hx_ne : x ≠ 0
⊢ -x ≠ 0

Tactic:
simp [hx_ne]
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
c : ℝ
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
rw : HSMul.hSMul (β := E) c 0 = 0
⊢ setToSimpleFunc T (c • f) = ∑ x ∈ f.range, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) (c • x)

Tactic:
rw [smul_eq_map c f, map_setToSimpleFunc T h_add hf]

Premises used: MeasureTheory.SimpleFunc.smul_eq_map, MeasureTheory.SimpleFunc.map_setToSimpleFunc
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
c : ℝ
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
rw rw₁ : Eq.{u_2 + 1} (α := E) 0 0
⊢ HSMul.hSMul (β := E) c 0 = 0

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
c : ℝ
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
b : E
h : b ∈ f.range
rw rw₁ :
  HSMul.hSMul (β := F) c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : (a : E) → F) b : F) =
    HSMul.hSMul (β := F) c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : (a : E) → F) b : F)
⊢ (T (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : (a : E) → F) (c • b) =
    HSMul.hSMul (β := F) c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : (a : E) → F) b : F)

Tactic:
rw [map_smul (T (f ⁻¹' {b})) c b]

Premises used: Set.preimage, Singleton.singleton, DFunLike.coe, map_smul
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
h_add : FinMeasAdditive μ T
c : ℝ
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ ∑ x ∈ f.range, HSMul.hSMul (β := F) c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x : F) =
    c • setToSimpleFunc T f

Tactic:
simp only [setToSimpleFunc, smul_sum]

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.smul_sum
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst_2 : NormedAddCommGroup E
inst_3 : SMulZeroClass 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α →ₛ E
hf : Integrable.{u_7, u_1} (ε := E) (⇑f : (a : α) → E) μ
rw : HSMul.hSMul (β := E) c 0 = 0
⊢ setToSimpleFunc T (c • f) = ∑ x ∈ f.range, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) (c • x)

Tactic:
rw [smul_eq_map c f, map_setToSimpleFunc T h_add hf]

Premises used: MeasureTheory.SimpleFunc.smul_eq_map, MeasureTheory.SimpleFunc.map_setToSimpleFunc
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst_2 : NormedAddCommGroup E
inst_3 : SMulZeroClass 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α →ₛ E
hf : Integrable.{u_7, u_1} (ε := E) (⇑f : (a : α) → E) μ
rw rw₁ : Eq.{u_7 + 1} (α := E) 0 0
⊢ HSMul.hSMul (β := E) c 0 = 0

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst_2 : NormedAddCommGroup E
inst_3 : SMulZeroClass 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α →ₛ E
hf : Integrable.{u_7, u_1} (ε := E) (⇑f : (a : α) → E) μ
b : E
h : b ∈ f.range
rw rw₁ :
  HSMul.hSMul (β := F) c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : (a : E) → F) b : F) =
    HSMul.hSMul (β := F) c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : (a : E) → F) b : F)
⊢ (T (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : (a : E) → F) (c • b) =
    HSMul.hSMul (β := F) c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : (a : E) → F) b : F)

Tactic:
rw [h_smul]
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst_2 : NormedAddCommGroup E
inst_3 : SMulZeroClass 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α →ₛ E
hf : Integrable.{u_7, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ ∑ x ∈ f.range, HSMul.hSMul (β := F) c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x : F) =
    c • setToSimpleFunc T f

Tactic:
simp only [setToSimpleFunc, smul_sum]

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.smul_sum
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
G'' : Type u_8
inst_2 : NormedAddCommGroup G''
inst_3 : PartialOrder G''
inst_4 : IsOrderedAddMonoid G''
inst_5 : NormedSpace ℝ G''
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] G''
hTT' : ∀ (s : Set α) (x : F), LE.le.{u_8} (α := G'') ((T s : (a : F) → G'') x : G'') ((T' s : (a : F) → G'') x : G'')
f : α →ₛ F
simp_rw :
  LE.le.{u_8} (α := G'') (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → G'') x)
    (∑ x ∈ f.range, (T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → G'') x)
⊢ setToSimpleFunc T f ≤ setToSimpleFunc T' f

Tactic:
simp_rw [setToSimpleFunc]

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
G'' : Type u_8
inst_2 : NormedAddCommGroup G''
inst_3 : PartialOrder G''
inst_4 : IsOrderedAddMonoid G''
inst_5 : NormedSpace ℝ G''
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] G''
hTT' : ∀ (s : Set α) (x : F), LE.le.{u_8} (α := G'') ((T s : (a : F) → G'') x : G'') ((T' s : (a : F) → G'') x : G'')
f : α →ₛ F
h :
  ∀ i ∈ f.range,
    LE.le.{u_8} (α := G'') ((T (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) : (a : F) → G'') i : G'')
      ((T' (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) : (a : F) → G'') i : G'')
⊢ LE.le.{u_8} (α := G'') (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → G'') x)
    (∑ x ∈ f.range, (T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → G'') x)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
G'' : Type u_8
inst_2 : NormedAddCommGroup G''
inst_3 : PartialOrder G''
inst_4 : IsOrderedAddMonoid G''
inst_5 : NormedSpace ℝ G''
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] G''
hTT' : ∀ (s : Set α) (x : F), LE.le.{u_8} (α := G'') ((T s : (a : F) → G'') x : G'') ((T' s : (a : F) → G'') x : G'')
f : α →ₛ F
i : F
h : i ∈ f.range
⊢ LE.le.{u_8} (α := G'') ((T (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) : (a : F) → G'') i : G'')
    ((T' (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) : (a : F) → G'') i : G'')

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

Tactic:
unfold setToSimpleFunc

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

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

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

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

Tactic:
hTT' _ (measurableSet_fiber _ _) (measure_preimage_lt_top_of_integrable _ hf 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
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst_2 : NormedAddCommGroup G''
inst_3 : PartialOrder G''
inst_4 : IsOrderedAddMonoid G''
inst_5 : NormedSpace ℝ G''
T T' : Set α → E →L[ℝ] G''
hTT' :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : E), LE.le.{u_8} (α := G'') ((T s : (a : E) → G'') x : G'') ((T' s : (a : E) → G'') x : G'')
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
i : E
h : i ∈ f.range
h0 : ¬i = 0
⊢ LE.le.{u_8} (α := G'') ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {i}) : (a : E) → G'') i : G'')
    ((T' (Set.preimage (β := E) (⇑f : (a : α) → E) {i}) : (a : E) → G'') i : G'')

Tactic:
exact hTT' _ (measurableSet_fiber _ _) (measure_preimage_lt_top_of_integrable _ hf 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
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'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
⊢ 0 ≤ setToSimpleFunc T f

Tactic:
sum_nonneg fun i hi => hT_nonneg _ i ?_

Premises used: Finset.sum_nonneg, Set.preimage, MeasureTheory.SimpleFunc.setToSimpleFunc, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
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'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
refine : ∀ (i : G') (hi : i ∈ f.range), 0 ≤ i
⊢ 0 ≤ setToSimpleFunc T f

Tactic:
refine sum_nonneg fun i hi => hT_nonneg _ i ?_

Premises used: Finset.sum_nonneg
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
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'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
i : G'
hi : i ∈ f.range
⊢ 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
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'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
i : G'
hi : Membership.mem (γ := Set G') (Set.range.{u_7, u_1 + 1} (ι := α) (⇑f : (a : α) → G')) i
obtain : ∀ (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
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'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
i : G'
hi : Membership.mem (γ := Set G') (Set.range.{u_7, u_1 + 1} (ι := α) (⇑f : (a : α) → G')) i
y : α
hy : (f : (a : α) → G') y = i
rw : 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
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'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
i : G'
hi : Membership.mem (γ := Set G') (Set.range.{u_7, u_1 + 1} (ι := α) (⇑f : (a : α) → G')) i
y : α
hy : (f : (a : α) → G') y = i
⊢ LE.le.{u_7} (α := G') (0 : G') ((f : (a : α) → G') y : G')

Tactic:
le_trans ?_ (hf y)

Premises used: le_trans
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
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'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
i : G'
hi : Membership.mem (γ := Set G') (Set.range.{u_7, u_1 + 1} (ι := α) (⇑f : (a : α) → G')) i
y : α
hy : (f : (a : α) → G') y = i
refine : LE.le.{u_7} (α := G') (0 : G') ((0 : (a : α) → G') y : G')
⊢ LE.le.{u_7} (α := G') (0 : G') ((f : (a : α) → G') y : G')

Tactic:
refine le_trans ?_ (hf y)

Premises used: le_trans
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
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'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → LE.le.{u_8} (α := G'') (0 : G'') ((T s : (a : G') → G'') x : G'')
f : α →ₛ G'
hf : 0 ≤ f
i : G'
hi : Membership.mem (γ := Set G') (Set.range.{u_7, u_1 + 1} (ι := α) (⇑f : (a : α) → G')) i
y : α
hy : (f : (a : α) → G') y = i
⊢ LE.le.{u_7} (α := G') (0 : G') ((0 : (a : α) → G') y : G')

Tactic:
simp
-- 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') μ
⊢ 0 ≤ setToSimpleFunc T f

Tactic:
sum_nonneg fun i hi => ?_

Premises used: Finset.sum_nonneg, MeasureTheory.SimpleFunc.setToSimpleFunc