awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
y : α
hy : (f : (a : α) → G') y = i
⊢ 0 ≤ i
have rw : LE.le.{u_7} (α := G') (0 : G') ((f : (a : α) → G') y : G')
Tactic: rw [← hy]
-- 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
y : α
hy : (f : (a : α) → G') y = i
⊢ LE.le.{u_7} (α := G') (0 : G') ((f : (a : α) → G') y : G')
have refine : LE.le.{u_7} (α := G') (0 : G') ((0 : (a : α) → G') y : G')
Tactic: refine le_trans ?_ (hf y)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
have 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'')
Tactic: refine sum_nonneg fun i hi => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
⊢ LE.le.{u_8} (α := G'') (0 : G'') ((T (Set.preimage (β := G') (⇑f : (a : α) → G') {i}) : (a : G') → G'') i : G'')
have pos : ∀ (h0 : i = 0),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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'')
⊢ LE.le.{u_8} (α := G'') (0 : G'') ((T (Set.preimage (β := G') (⇑f : (a : α) → G') {i}) : (a : G') → G'') i : G'')
have neg : ∀ (h0 : ¬i = 0),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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'')
have neg : 0 ≤ i
Tactic: refine
    hT_nonneg _ (measurableSet_fiber _ _) (measure_preimage_lt_top_of_integrable _ hfi h0) i ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
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
⊢ 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, h0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
⊢ 0 ≤ i
have neg : ∀ (y : α) (hy : (f : (a : α) → G') y = i), 0 ≤ i
Tactic: obtain ⟨y, hy⟩ := Set.mem_range.mp hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
⊢ 0 ≤ i
have neg : LE.le.{u_7} (α := G') (0 : G') ((f : (a : α) → G') y : G')
Tactic: rw [← hy]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
⊢ setToSimpleFunc T f ≤ setToSimpleFunc T g
have rw : 0 ≤ setToSimpleFunc T (g - f)
Tactic: rw [← sub_nonneg, ← setToSimpleFunc_sub T h_add hgi hfi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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)
have refine : 0 ≤ g - f
Tactic: refine setToSimpleFunc_nonneg' T hT_nonneg _ ?_ (hgi.sub hfi)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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') ((0 : (a : α) → G') x : G') ((g - f : (a : α) → G') x : G')
have simp : LE.le.{u_7} (α := G') ((f : (a : α) → G') x : G') ((g : (a : α) → G') x : G')
Tactic: simp only [coe_sub, sub_nonneg, coe_zero, Pi.zero_apply, Pi.sub_apply]
-- 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
f : α →ₛ F'
⊢ 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‖)
have 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: gcongr with b
-- 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 α
μ : 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, ‖T (Set.preimage (β := F) (⇑f : (a : α) → F) {x})‖ * ‖x‖)
    (∑ x ∈ f.range, C * μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) * ‖x‖)
have h : ∀ i ∈ f.range,
  ‖T (Set.preimage (β := F) (⇑f : (a : α) → F) {i})‖ ≤ C * μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i})
Tactic: gcongr
-- 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 α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * μ.real s
f : α →ₛ F
⊢ ∑ 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‖
have 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‖)
Tactic: simp_rw [mul_sum, ← mul_assoc]
-- 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 : 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‖)
have 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‖
Tactic: refine Finset.sum_le_sum fun b hb => ?_
-- 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 : 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
⊢ ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {b})‖ * ‖b‖ ≤
    C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * ‖b‖
have 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
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b, hb
-- 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 : 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
⊢ ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {b})‖ * ‖b‖ ≤
    C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * ‖b‖
have inr : ∀ (hb : b ≠ 0),
  ‖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
-- 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 : 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_1 : b ∈ f.range
hb : b ≠ 0
⊢ ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {b})‖ * ‖b‖ ≤
    C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * ‖b‖
have inr : ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {b})‖ ≤ C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b})
Tactic: gcongr
-- 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 : 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) μ
⊢ ∑ x ∈ f.range, C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖ ≤
    C * ∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖
have simp_rw : LE.le (α := ℝ) (∑ x ∈ f.range, C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖)
  (∑ x ∈ f.range, C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖)
Tactic: simp_rw [mul_sum, ← mul_assoc]
-- 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'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
have inl : ∀ (hs : MeasurableSet.{u_1} (α := α) ∅),
  setToSimpleFunc T (piecewise ∅ hs (const α x) (const α 0)) = (T ∅ : (a : F) → F') x
Tactic: obtain rfl | hs_empty := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs
-- 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'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
inl :
  ∀ (hs : MeasurableSet.{u_1} (α := α) ∅),
    setToSimpleFunc T (piecewise ∅ hs (const α x) (const α 0)) = (T ∅ : (a : F) → F') x
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
have inr : ∀ (hs_empty : s.Nonempty), setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
Tactic: obtain rfl | hs_empty := s.eq_empty_or_nonempty
-- 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'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
⊢ Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range,
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F')
    ((T s : (a : F) → F') x : F')
have inr : ∀ (hs : MeasurableSet.{u_1} (α := α) Set.univ) (hs_empty : Set.Nonempty.{u_1} (α := α) Set.univ),
  Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ (piecewise Set.univ hs (const α x) (const α 0)).range,
        (T (Set.preimage (β := F) (⇑(piecewise Set.univ hs (const α x) (const α 0)) : (a : α) → F) {x_1}) :
            (a : F) → F')
          x_1 :
      F')
    ((T Set.univ : (a : F) → F') x : F')
Tactic: obtain rfl | hs_univ := eq_or_ne s univ
Cleared hypotheses: s, hs, hs_empty
-- 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'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
inr :
  ∀ (hs : MeasurableSet.{u_1} (α := α) Set.univ) (hs_empty : Set.Nonempty.{u_1} (α := α) Set.univ),
    Eq.{u_4 + 1} (α := F')
      (∑ x_1 ∈ (piecewise Set.univ hs (const α x) (const α 0)).range,
          (T (Set.preimage (β := F) (⇑(piecewise Set.univ hs (const α x) (const α 0)) : (a : α) → F) {x_1}) :
              (a : F) → F')
            x_1 :
        F')
      ((T Set.univ : (a : F) → F') x : F')
⊢ Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range,
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F')
    ((T s : (a : F) → F') x : F')
have inr₁ : ∀ (hs_univ : s ≠ Set.univ),
  Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range,
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F')
    ((T s : (a : F) → F') x : F')
Tactic: obtain rfl | hs_univ := eq_or_ne s univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
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'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
x : F
hs : MeasurableSet.{u_1} (α := α) Set.univ
hs_empty : Set.Nonempty.{u_1} (α := α) Set.univ
⊢ Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ (piecewise Set.univ hs (const α x) (const α 0)).range,
        (T (Set.preimage (β := F) (⇑(piecewise Set.univ hs (const α x) (const α 0)) : (a : α) → F) {x_1}) :
            (a : F) → F')
          x_1 :
      F')
    ((T Set.univ : (a : F) → F') x : F')
have hα : Nonempty α
Tactic: haveI hα := hs_empty.to_type
-- 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'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
⊢ Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range,
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F')
    ((T s : (a : F) → F') x : F')
have inr : Eq.{u_4 + 1} (α := F')
  (∑ x_1 ∈ {x, 0},
      (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
    F')
  ((T s : (a : F) → F') x : F')
Tactic: rw [range_indicator hs hs_empty hs_univ]
-- 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'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
⊢ Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ {x, 0},
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F')
    ((T s : (a : F) → F') x : F')
have pos : ∀ (hx0 : x = 0),
  Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ {x, 0},
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F')
    ((T s : (a : F) → F') x : F')
Tactic: by_cases hx0 : x = 0