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_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
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
this :
  ∀ x ∈ {x ∈ f.range | x ≠ 0},
    T'' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) =
      T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) + T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
⊢ HAdd.hAdd (α := (a : E) → F) (β := (a : E) → F) (⇑(T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})) : (a : E) → F)
      (⇑(T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x})) : (a : E) → F) x =
    HAdd.hAdd (α := F) (β := F) ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x : F)
      ((T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x : F)
have rw : HAdd.hAdd (α := F) (β := F) ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x : F)
    ((T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x : F) =
  HAdd.hAdd (α := F) (β := F) ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x : F)
    ((T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x : F)
Tactic: rw [Pi.add_apply]
-- 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 T' T'' : Set α → E →L[ℝ] F
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ ∑ x ∈ f.range with x ≠ 0, (T'' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x =
    HAdd.hAdd (α := F) (∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x)
      (∑ x ∈ f.range with x ≠ 0, (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x)
have suffices : ∀ x ∈ {x ∈ f.range | x ≠ 0},
  T'' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) =
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) + T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
Tactic: suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (f ⁻¹' {x}) = T (f ⁻¹' {x}) + T' (f ⁻¹' {x}) by
    rw [← sum_add_distrib]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx]
    push_cast
    rw [Pi.add_apply]
-- 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 T' T'' : Set α → E →L[ℝ] F
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
⊢ T'' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) =
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) + T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
have h_add₁ : x ≠ 0
Tactic: refine
    h_add (f ⁻¹' {x}) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
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
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
⊢ x ≠ 0
have hx₁ : x ∈ f.range ∧ x ≠ 0
Tactic: rw [mem_filter] at hx
Cleared hypotheses: hx
-- 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 T' T'' : Set α → E →L[ℝ] F
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ setToSimpleFunc T'' f = setToSimpleFunc T f + setToSimpleFunc T' f
have simp_rw : ∑ x ∈ f.range with x ≠ 0, (T'' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x =
  HAdd.hAdd (α := F) (∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x)
    (∑ x ∈ f.range with x ≠ 0, (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x)
Tactic: classical
  simp_rw [setToSimpleFunc_eq_sum_filter]
  suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (f ⁻¹' {x}) = T (f ⁻¹' {x}) + T' (f ⁻¹' {x}) by
    rw [← sum_add_distrib]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx]
    push_cast
    rw [Pi.add_apply]
  intro x hx
  refine
    h_add (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 T' T'' : Set α → E →L[ℝ] F
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + 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 =
    HAdd.hAdd (α := F) (∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x)
      (∑ x ∈ f.range with x ≠ 0, (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x)
⊢ setToSimpleFunc T'' f = setToSimpleFunc T f + setToSimpleFunc T' f
have simp_rw₁ : ∀ x ∈ {x ∈ f.range | x ≠ 0},
  T'' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) =
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) + T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
Tactic: classical
  simp_rw [setToSimpleFunc_eq_sum_filter]
  suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (f ⁻¹' {x}) = T (f ⁻¹' {x}) + T' (f ⁻¹' {x}) by
    rw [← sum_add_distrib]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx]
    push_cast
    rw [Pi.add_apply]
  intro x hx
  refine
    h_add (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 T' T'' : Set α → E →L[ℝ] F
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + 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 =
    HAdd.hAdd (α := F) (∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x)
      (∑ 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}) =
      T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) + T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
⊢ setToSimpleFunc T'' f = setToSimpleFunc T f + setToSimpleFunc T' f
have simp_rw₃ : ∀ (x : E) (hx : x ∈ {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}) = T (f ⁻¹' {x}) + T' (f ⁻¹' {x}) by
    rw [← sum_add_distrib]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx]
    push_cast
    rw [Pi.add_apply]
  intro x hx
  refine
    h_add (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 T' T'' : Set α → E →L[ℝ] F
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + 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 =
    HAdd.hAdd (α := F) (∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x)
      (∑ 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}) =
      T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) + T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
simp_rw₃ : ∀ (x : E) (hx : x ∈ {x ∈ f.range | x ≠ 0}), x ≠ 0
⊢ setToSimpleFunc T'' f = setToSimpleFunc T f + 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}) = T (f ⁻¹' {x}) + T' (f ⁻¹' {x}) by
    rw [← sum_add_distrib]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx]
    push_cast
    rw [Pi.add_apply]
  intro x hx
  refine
    h_add (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
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'
c : ℝ
f : α →ₛ F
⊢ setToSimpleFunc (fun (s : Set α) ↦ c • T s) f = c • setToSimpleFunc T f
have simp_rw : ∑ x ∈ f.range, (c • T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x =
  HSMul.hSMul (β := F') c (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
Tactic: simp_rw [setToSimpleFunc, ContinuousLinearMap.smul_apply, smul_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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'
c : ℝ
f : α →ₛ F
simp_rw :
  ∑ x ∈ f.range, (c • T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x =
    HSMul.hSMul (β := F') c (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
⊢ setToSimpleFunc (fun (s : Set α) ↦ c • T s) f = c • setToSimpleFunc T f
have simp_rw₁ : ∑ x ∈ f.range, HSMul.hSMul (β := F') c ((T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x : F') =
  HSMul.hSMul (β := F') c (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
Tactic: simp_rw [setToSimpleFunc, ContinuousLinearMap.smul_apply, smul_sum]
-- 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) μ
⊢ setToSimpleFunc T' f = c • setToSimpleFunc T f
have 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)
Tactic: simp_rw [setToSimpleFunc_eq_sum_filter]
-- 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) μ
this :
  ∀ x ∈ {x ∈ f.range | x ≠ 0},
    T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
⊢ ∑ 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)
have rw : Eq.{u_4 + 1} (α := F') (∑ x ∈ f.range with x ≠ 0, (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x)
  (∑ x ∈ f.range with x ≠ 0,
    HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F'))
Tactic: rw [smul_sum]
-- 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) μ
this :
  ∀ x ∈ {x ∈ f.range | x ≠ 0},
    T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
⊢ Eq.{u_4 + 1} (α := F')
    (∑ x ∈ f.range with x ≠ 0, (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x)
    (∑ x ∈ f.range with x ≠ 0,
      HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F'))
have refine : ∀ (x : E) (hx : x ∈ {x ∈ f.range | x ≠ 0}),
  (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x =
    HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F')
Tactic: refine Finset.sum_congr rfl fun x hx => ?_
-- 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) μ
this :
  ∀ x ∈ {x ∈ f.range | x ≠ 0},
    T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
⊢ (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x =
    HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F')
have rw : (c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x =
  HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F')
Tactic: rw [this x hx, ContinuousLinearMap.smul_apply]
-- 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) μ
this :
  ∀ x ∈ {x ∈ f.range | x ≠ 0},
    T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
rw :
  (c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x =
    HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F')
⊢ (T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x =
    HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F')
have rw₁ : HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F') =
  HSMul.hSMul (β := F') c ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F')
Tactic: rw [this x hx, ContinuousLinearMap.smul_apply]
-- 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) μ
⊢ ∑ 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)
have suffices : ∀ x ∈ {x ∈ f.range | x ≠ 0},
  T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
Tactic: 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]
-- 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) μ
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})
have h_smul₁ : x ≠ 0
Tactic: refine
    h_smul (f ⁻¹' {x}) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
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) μ
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
⊢ x ≠ 0
have hx₁ : x ∈ f.range ∧ x ≠ 0
Tactic: rw [mem_filter] at hx
Cleared hypotheses: hx
-- 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) μ
⊢ setToSimpleFunc T' f = c • setToSimpleFunc T f
have 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)
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_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)
⊢ setToSimpleFunc T' f = c • setToSimpleFunc T f
have simp_rw₁ : ∀ x ∈ {x ∈ f.range | x ≠ 0},
  T' (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) = c • T (Set.preimage (β := E) (⇑f : (a : α) → E) {x})
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_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})
⊢ setToSimpleFunc T' f = c • setToSimpleFunc T f
have simp_rw₃ : ∀ (x : E) (hx : x ∈ {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