awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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 T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
simp_rw :
  ∑ x ∈ f.range with x ≠ 0, (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x =
    HSMul.hSMul (β := F') c
      (∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x)
simp_rw₁ simp_rw₂ :
  ∀ (x : E) (hx : x ∈ {x ∈ f.range | x ≠ 0}),
    T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
simp_rw₃ : ∀ (x : E) (hx : x ∈ {x ∈ f.range | x ≠ 0}), x ≠ 0
⊢ setToSimpleFunc T' f = c • setToSimpleFunc T f
have simp_rw₄ : ∀ (x : E) (hx : x ∈ f.range ∧ x ≠ 0), x ≠ 0
Tactic: classical
  simp_rw [setToSimpleFunc_eq_sum_filter]
  suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T' (f ⁻¹' {x}) = c • T (f ⁻¹' {x}) by
    rw [smul_sum]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx, ContinuousLinearMap.smul_apply]
  intro x hx
  refine
    h_smul (f ⁻¹' {x}) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)
  rw [mem_filter] at hx
  exact hx.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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 : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
hp_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
⊢ setToSimpleFunc T (f + g) =
    ∑ x ∈ (f.pair g).range,
      (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) (x.1 + x.2)
have rw : HAdd.hAdd (α := E) 0.1 0.2 = 0
Tactic: rw [add_eq_map₂, map_setToSimpleFunc T h_add hp_pair]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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 : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
hp_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
⊢ ∑ x ∈ (f.pair g).range,
      HAdd.hAdd (α := F) (β := F)
        ((T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1 : F)
        ((T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2 : F) =
    HAdd.hAdd (α := F)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2)
have rw : HAdd.hAdd (α := F)
    (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
    (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2) =
  HAdd.hAdd (α := F)
    (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
    (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2)
Tactic: rw [Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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 : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
hp_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
⊢ HAdd.hAdd (α := F)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2) =
    setToSimpleFunc T (map Prod.fst (f.pair g)) + setToSimpleFunc T (map Prod.snd (f.pair g))
have rw : HAdd.hAdd (α := F)
    (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
    (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2) =
  setToSimpleFunc T (map Prod.fst (f.pair g)) +
    ∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2
Tactic: rw [map_setToSimpleFunc T h_add hp_pair Prod.snd_zero,
        map_setToSimpleFunc T h_add hp_pair Prod.fst_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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 : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
hp_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
rw :
  HAdd.hAdd (α := F)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2) =
    setToSimpleFunc T (map Prod.fst (f.pair g)) +
      ∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2
⊢ HAdd.hAdd (α := F)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
      (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2) =
    setToSimpleFunc T (map Prod.fst (f.pair g)) + setToSimpleFunc T (map Prod.snd (f.pair g))
have rw₁ : HAdd.hAdd (α := F)
    (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
    (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2) =
  HAdd.hAdd (α := F)
    (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
    (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2)
Tactic: rw [map_setToSimpleFunc T h_add hp_pair Prod.snd_zero,
        map_setToSimpleFunc T h_add hp_pair Prod.fst_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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 : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ setToSimpleFunc T (map Neg.neg f) = -setToSimpleFunc T f
have rw : Eq.{u_3 + 1} (α := F) (∑ x ∈ f.range, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) (-x))
  (∑ x ∈ f.range, -(T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x)
Tactic: rw [map_setToSimpleFunc T h_add hf neg_zero, setToSimpleFunc, ← sum_neg_distrib]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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 : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
⊢ setToSimpleFunc T (f - g) = setToSimpleFunc T f - setToSimpleFunc T g
have rw : Integrable.{u_2, u_1} (ε := E) (⇑(-g) : (a : α) → E) μ
Tactic: rw [sub_eq_add_neg, setToSimpleFunc_add T h_add hf, setToSimpleFunc_neg T h_add hg,
    sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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 : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
⊢ Integrable.{u_2, u_1} (ε := E) (⇑(-g) : (a : α) → E) μ
have rw : ∀
  (hg :
    ∀ (y : E),
      y ≠ 0 →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑g : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞))
  (y : E),
  y ≠ 0 →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑(-g) : (a : α) → E) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [integrable_iff] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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∞)
have rw : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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∞)
have refine : -x ≠ 0
Tactic: refine hg (-x) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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) μ
⊢ setToSimpleFunc T (c • f) = ∑ x ∈ f.range, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) (c • x)
have rw : HSMul.hSMul (β := E) c 0 = 0
Tactic: rw [smul_eq_map c f, map_setToSimpleFunc T h_add hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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) μ
⊢ HSMul.hSMul (β := E) c 0 = 0
have rw : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
⊢ (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)
have 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)
Tactic: rw [map_smul (T (f ⁻¹' {b})) c b]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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) μ
⊢ setToSimpleFunc T (c • f) = ∑ x ∈ f.range, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) (c • x)
have rw : HSMul.hSMul (β := E) c 0 = 0
Tactic: rw [smul_eq_map c f, map_setToSimpleFunc T h_add hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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) μ
⊢ HSMul.hSMul (β := E) c 0 = 0
have rw : Eq.{u_7 + 1} (α := E) 0 0
Tactic: rw [smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
⊢ (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)
have 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)
Tactic: rw [h_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
⊢ setToSimpleFunc T f ≤ setToSimpleFunc T' f
have 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)
Tactic: simp_rw [setToSimpleFunc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
⊢ 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)
have 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: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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) μ
⊢ setToSimpleFunc T f ≤ setToSimpleFunc T' f
have 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)
Tactic: unfold setToSimpleFunc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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) μ
⊢ 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)
have 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'')
Tactic: gcongr with i _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
⊢ 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'')
have 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'')
Tactic: by_cases h0 : i = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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'')
⊢ 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'')
have 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'')
Tactic: by_cases h0 : i = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
have refine : ∀ (i : G') (hi : i ∈ f.range), 0 ≤ i
Tactic: refine sum_nonneg fun i hi => hT_nonneg _ i ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
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
⊢ 0 ≤ i
have hi₁ : Membership.mem (γ := Set G') (Set.range.{u_7, u_1 + 1} (ι := α) (⇑f : (a : α) → G')) i
Tactic: rw [mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
⊢ 0 ≤ i
have obtain : ∀ (y : α) (hy : (f : (a : α) → G') y = i), 0 ≤ i
Tactic: obtain ⟨y, hy⟩ := Set.mem_range.mp hi