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 : 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) μ
h :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
h_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
a : α
hp : Membership.mem (α := E × E) (f.pair g).range ((f.pair g : (a : α) → E × E) a : E × E)
eq : ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)
h_eq :
  T
      (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
        (singleton (α := E × E) (((f : (a : α) → E) a, (g : (a : α) → E) a) : E × E))) =
    T
      (Set.preimage (β := E) (⇑f : (a : α) → E) (singleton (α := E) ((f : (a : α) → E) a : E)) ∩
        Set.preimage (β := E) (⇑g : (a : α) → E) (singleton (α := E) ((g : (a : α) → E) a : E)))
⊢ T
      (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
        (singleton (α := E × E) (((f : (a : α) → E) a, (g : (a : α) → E) a) : E × E))) =
    0
have rw : T
    (Set.preimage (β := E) (⇑f : (a : α) → E) (singleton (α := E) ((f : (a : α) → E) a : E)) ∩
      Set.preimage (β := E) (⇑g : (a : α) → E) (singleton (α := E) ((g : (a : α) → E) a : E))) =
  0
Tactic: rw [h_eq]
-- 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 : 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) μ
h :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
h_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
a : α
hp : Membership.mem (α := E × E) (f.pair g).range ((f.pair g : (a : α) → E × E) a : E × E)
eq : ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)
⊢ Eq.{u_3 + 1} (α := F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
          (a : E) → F)
        ((f.pair g : (a : α) → E × E) a).1 :
      F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
          (a : E) → F)
        ((f.pair g : (a : α) → E × E) a).2 :
      F)
have this : T
    (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
      (singleton (α := E × E) (((f : (a : α) → E) a, (g : (a : α) → E) a) : E × E))) =
  0
Tactic: have : T (pair f g ⁻¹' {(f a, g a)}) = 0 := by
        have h_eq : T ((⇑(f.pair g)) ⁻¹' {(f a, g a)}) = T (f ⁻¹' {f a} ∩ g ⁻¹' {g a}) := by
          congr; rw [pair_preimage_singleton f g]
        rw [h_eq]
        exact h eq
-- 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_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑g : (a : α) → E)
⊢ setToSimpleFunc T f = setToSimpleFunc T g
have refine : Pairwise fun (x y : E) ↦
  T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
Tactic: refine setToSimpleFunc_congr' T h_add hf ((integrable_congr h).mp 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_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑g : (a : α) → E)
⊢ Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
have refine : ∀ (x y : E) (hxy : x ≠ y),
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: refine fun x y hxy => h_zero _ ((measurableSet_fiber f x).inter (measurableSet_fiber g y)) ?_
-- 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_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑g : (a : α) → E)
x y : E
hxy : x ≠ y
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw : ∀
  (h :
    Eq (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)} :
        ℝ≥0∞)
      (0 : ℝ≥0∞))
  (x y : E) (hxy : x ≠ y),
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rw [EventuallyEq, ae_iff] at h
Cleared hypotheses: h, x, y, hxy
-- 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_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
x y : E
hxy : x ≠ y
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have refine : ∀ (z : α),
  Membership.mem (γ := Set α)
      (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) z →
    Membership.mem (γ := Set α) {a : α | ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)} z
Tactic: refine measure_mono_null (fun z => ?_) h
-- 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_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h_1 :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
x y : E
hxy : x ≠ y
z : α
h : (f : (a : α) → E) z = x ∧ (g : (a : α) → E) z = y
⊢ ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) z : E) ((g : (a : α) → E) z : E)
have rwa : ¬x = (g : (a : α) → E) z
Tactic: rwa [h.1, h.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_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h_1 :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
x y : E
hxy : x ≠ y
z : α
h : (f : (a : α) → E) z = x ∧ (g : (a : α) → E) z = y
rwa : ¬x = (g : (a : α) → E) z
⊢ ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) z : E) ((g : (a : α) → E) z : E)
have rwa₁ : ¬x = y
Tactic: rwa [h.1, h.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' : Set α → E →L[ℝ] F
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ 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)
have refine : ∀ x ∈ f.range,
  Eq.{u_3 + 1} (α := 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: refine sum_congr rfl fun 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 T' : Set α → E →L[ℝ] F
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
h_1 : x ∈ f.range
⊢ Eq.{u_3 + 1} (α := 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 pos : ∀ (hx0 : x = 0),
  Eq.{u_3 + 1} (α := 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: by_cases hx0 : x = 0
-- 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' : Set α → E →L[ℝ] F
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
h_1 : x ∈ f.range
pos :
  ∀ (hx0 : x = 0),
    Eq.{u_3 + 1} (α := 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)
⊢ Eq.{u_3 + 1} (α := 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 neg : ∀ (hx0 : ¬x = 0),
  Eq.{u_3 + 1} (α := 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: by_cases hx0 : x = 0
-- 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' : Set α → E →L[ℝ] F
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
h_1 : x ∈ f.range
hx0 : ¬x = 0
⊢ Eq.{u_3 + 1} (α := 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 neg : Eq.{u_3 + 1} (α := 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 [h (f ⁻¹' {x}) (SimpleFunc.measurableSet_fiber _ _)
        (SimpleFunc.measure_preimage_lt_top_of_integrable _ hf hx0)]
-- 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 T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ setToSimpleFunc (T + T') f = setToSimpleFunc T f + setToSimpleFunc T' f
have simp_rw : ∑ x ∈ f.range,
    (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) + T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) :
        (a : F) → F')
      x =
  HAdd.hAdd (α := F') (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
    (∑ x ∈ f.range, (T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
Tactic: simp_rw [setToSimpleFunc, Pi.add_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 T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x ∈ f.range,
      (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) + T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) :
          (a : F) → F')
        x =
    HAdd.hAdd (α := F') (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
      (∑ x ∈ f.range, (T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
have push_cast : ∑ x ∈ f.range,
    HAdd.hAdd (α := (a : F) → F') (β := (a : F) → F')
      (⇑(T (Set.preimage (β := F) (⇑f : (a : α) → F) {x})) : (a : F) → F')
      (⇑(T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x})) : (a : F) → F') x =
  HAdd.hAdd (α := F') (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
    (∑ x ∈ f.range, (T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
Tactic: push_cast
-- 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 T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x ∈ f.range,
      HAdd.hAdd (α := (a : F) → F') (β := (a : F) → F')
        (⇑(T (Set.preimage (β := F) (⇑f : (a : α) → F) {x})) : (a : F) → F')
        (⇑(T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x})) : (a : F) → F') x =
    HAdd.hAdd (α := F') (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
      (∑ x ∈ f.range, (T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
have simp_rw : ∑ x ∈ f.range,
    HAdd.hAdd (α := F') (β := F') ((T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x : F')
      ((T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x : F') =
  HAdd.hAdd (α := F') (∑ x ∈ f.range, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
    (∑ x ∈ f.range, (T' (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x)
Tactic: simp_rw [Pi.add_apply, 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 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: 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_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 ∈ 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 rw : Eq.{u_3 + 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,
    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 [← 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 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})
⊢ Eq.{u_3 + 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,
      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 refine : ∀ (x : E) (hx : x ∈ {x ∈ f.range | x ≠ 0}),
  (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)
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_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}
⊢ (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 : (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) + 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)
Tactic: rw [this x 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) μ
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}
⊢ (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) + 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 push_cast : 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)
Tactic: push_cast