awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : DecidablePred fun (x : F) ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx_1 : x ∉ f.range ∨ x = 0
hx : x ∉ Set.range.{u_3, u_1 + 1} (ι := α) (⇑f : (a : α) → F)
⊢ μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x = 0
have inr : μ.real ∅ • x = 0
Tactic: rw [preimage_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : DecidablePred fun (x : F) ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx_1 : x ∉ f.range ∨ x = 0
hx : x ∉ Set.range.{u_3, u_1 + 1} (ι := α) (⇑f : (a : α) → F)
inr : μ.real ∅ • x = 0
⊢ μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x = 0
have inr₁ : Disjoint (α := Set F) {x} (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f : (a : α) → F))
Tactic: rw [preimage_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
y : F
⊢ integral μ (const α y) = μ.real Set.univ • y
have α₁ : ∑ z ∈ {y}, μ.real (Set.preimage (β := F) (⇑(const α y) : (a : α) → F) {z}) • z = μ.real Set.univ • y
Tactic: calc
    (const α y).integral μ = ∑ z ∈ {y}, μ.real (const α y ⁻¹' {z}) • z :=
      integral_eq_sum_of_subset <| (filter_subset _ _).trans (range_const_subset _ _)
    _ = μ.real univ • y := by simp [Set.preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
y : F
⊢ integral μ (const α y) = μ.real Set.univ • y
have α₁ : ∑ z ∈ {y}, μ.real (Set.preimage (β := F) (⇑(const α y) : (a : α) → F) {z}) • z = μ.real Set.univ • y
Tactic: classical
  calc
    (const α y).integral μ = ∑ z ∈ {y}, μ.real (const α y ⁻¹' {z}) • z :=
      integral_eq_sum_of_subset <| (filter_subset _ _).trans (range_const_subset _ _)
    _ = μ.real univ • y := by simp [Set.preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ integral μ (piecewise s hs f 0) = integral (μ.restrict s) f
have refine_1 : {x ∈ (piecewise s hs f 0).range | x ≠ 0} ⊆ {x ∈ f.range | x ≠ 0}
Tactic: refine (integral_eq_sum_of_subset ?_).trans
      ((sum_congr rfl fun y hy => ?_).trans (integral_eq_sum_filter _ _).symm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
refine_1 : {x ∈ (piecewise s hs f 0).range | x ≠ 0} ⊆ {x ∈ f.range | x ≠ 0}
⊢ integral μ (piecewise s hs f 0) = integral (μ.restrict s) f
have refine_2 : ∀ (y : F) (hy : y ∈ {x ∈ f.range | x ≠ 0}),
  μ.real (Set.preimage (β := F) (⇑(piecewise s hs f 0) : (a : α) → F) {y}) • y =
    (μ.restrict s).real (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) • y
Tactic: refine (integral_eq_sum_of_subset ?_).trans
      ((sum_congr rfl fun y hy => ?_).trans (integral_eq_sum_filter _ _).symm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ {x ∈ (piecewise s hs f 0).range | x ≠ 0}
⊢ y ∈ {x ∈ f.range | x ≠ 0}
have refine_1 : ∀ (hy : (y = 0 ∧ s ≠ Set.univ ∨ Membership.mem (γ := Set F) ((⇑f : (a : α) → F) '' s) y) ∧ y ≠ 0),
  Membership.mem (γ := Set F) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f : (a : α) → F)) y ∧ y ≠ 0
Tactic: simp only [mem_filter, mem_range, coe_piecewise, coe_zero, piecewise_eq_indicator,
      mem_range_indicator] at *
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : (y = 0 ∧ s ≠ Set.univ ∨ Membership.mem (γ := Set F) ((⇑f : (a : α) → F) '' s) y) ∧ y ≠ 0
⊢ Membership.mem (γ := Set F) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f : (a : α) → F)) y ∧ y ≠ 0
have refine_1 : ∀ (h₀ : Ne.{u_3 + 1} (α := F) 0 0),
  Membership.mem (γ := Set F) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f : (a : α) → F)) 0 ∧ Ne.{u_3 + 1} (α := F) 0 0
Tactic: rcases hy with ⟨⟨rfl, -⟩ | ⟨x, -, rfl⟩, h₀⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : (y = 0 ∧ s ≠ Set.univ ∨ Membership.mem (γ := Set F) ((⇑f : (a : α) → F) '' s) y) ∧ y ≠ 0
refine_1 :
  ∀ (h₀ : Ne.{u_3 + 1} (α := F) 0 0),
    Membership.mem (γ := Set F) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f : (a : α) → F)) 0 ∧ Ne.{u_3 + 1} (α := F) 0 0
⊢ Membership.mem (γ := Set F) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f : (a : α) → F)) y ∧ y ≠ 0
have refine_1₁ : ∀ (x : α) (h₀ : Ne.{u_3 + 1} (α := F) ((f : (a : α) → F) x : F) (0 : F)),
  Membership.mem.{u_3, u_3} (α := F) (γ := Set F) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f : (a : α) → F))
      ((f : (a : α) → F) x : F) ∧
    Ne.{u_3 + 1} (α := F) ((f : (a : α) → F) x : F) (0 : F)
Tactic: rcases hy with ⟨⟨rfl, -⟩ | ⟨x, -, rfl⟩, h₀⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ {x ∈ f.range | x ≠ 0}
⊢ μ.real (Set.preimage (β := F) (⇑(piecewise s hs f 0) : (a : α) → F) {y}) • y =
    (μ.restrict s).real (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) • y
have refine_2 : μ.real (Set.preimage (β := F) (s.piecewise (β := fun (a : α) ↦ F) (⇑f : (a : α) → F) 0) {y}) • y =
  (μ.restrict s).real (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) • y
Tactic: dsimp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ {x ∈ f.range | x ≠ 0}
⊢ μ.real (Set.preimage (β := F) (s.piecewise (β := fun (a : α) ↦ F) (⇑f : (a : α) → F) 0) {y}) • y =
    (μ.restrict s).real (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) • y
have refine_2 : 0 ∉ {y}
Tactic: rw [Set.piecewise_eq_indicator, indicator_preimage_of_notMem,
      measureReal_restrict_apply (f.measurableSet_preimage _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ integral μ (piecewise s hs f 0) = integral (μ.restrict s) f
have refine_1 : {x ∈ (piecewise s hs f 0).range | x ≠ 0} ⊆ {x ∈ f.range | x ≠ 0}
Tactic: classical
  refine (integral_eq_sum_of_subset ?_).trans
      ((sum_congr rfl fun y hy => ?_).trans (integral_eq_sum_filter _ _).symm)
  · intro y hy
    simp only [mem_filter, mem_range, coe_piecewise, coe_zero, piecewise_eq_indicator,
      mem_range_indicator] at *
    rcases hy with ⟨⟨rfl, -⟩ | ⟨x, -, rfl⟩, h₀⟩
    exacts [(h₀ rfl).elim, ⟨Set.mem_range_self _, h₀⟩]
  · dsimp
    rw [Set.piecewise_eq_indicator, indicator_preimage_of_notMem,
      measureReal_restrict_apply (f.measurableSet_preimage _)]
    exact fun h₀ => (mem_filter.1 hy).2 (Eq.symm h₀)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
refine_1 : {x ∈ (piecewise s hs f 0).range | x ≠ 0} ⊆ {x ∈ f.range | x ≠ 0}
⊢ integral μ (piecewise s hs f 0) = integral (μ.restrict s) f
have refine_2 : ∀ (y : F) (hy : y ∈ {x ∈ f.range | x ≠ 0}),
  μ.real (Set.preimage (β := F) (⇑(piecewise s hs f 0) : (a : α) → F) {y}) • y =
    (μ.restrict s).real (Set.preimage (β := F) (⇑f : (a : α) → F) {y}) • y
Tactic: classical
  refine (integral_eq_sum_of_subset ?_).trans
      ((sum_congr rfl fun y hy => ?_).trans (integral_eq_sum_filter _ _).symm)
  · intro y hy
    simp only [mem_filter, mem_range, coe_piecewise, coe_zero, piecewise_eq_indicator,
      mem_range_indicator] at *
    rcases hy with ⟨⟨rfl, -⟩ | ⟨x, -, rfl⟩, h₀⟩
    exacts [(h₀ rfl).elim, ⟨Set.mem_range_self _, h₀⟩]
  · dsimp
    rw [Set.piecewise_eq_indicator, indicator_preimage_of_notMem,
      measureReal_restrict_apply (f.measurableSet_preimage _)]
    exact fun h₀ => (mem_filter.1 hy).2 (Eq.symm h₀)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
⊢ integral μ (map (ENNReal.toReal ∘ g) f) = (∫⁻ (a : α), g ((f : (a : α) → E) a) ∂μ).toReal
have hf' : f.FinMeasSupp μ
Tactic: have hf' : f.FinMeasSupp μ := integrable_iff_finMeasSupp.1 hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ integral μ (map (ENNReal.toReal ∘ g) f) = (∫⁻ (a : α), g ((f : (a : α) → E) a) ∂μ).toReal
have simp : integral μ (map (ENNReal.toReal ∘ g) f) = ((map g f).lintegral μ).toReal
Tactic: simp only [← map_apply g f, lintegral_eq_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ integral μ (map (ENNReal.toReal ∘ g) f) = ((map g f).lintegral μ).toReal
have rw : Eq (α := ℝ) (∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) • (ENNReal.toReal ∘ g) x)
  (∑ a ∈ f.range,
    (HMul.hMul (β := ℝ≥0∞) (g a)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞)).toReal)
Tactic: rw [map_integral f _ hf, map_lintegral, ENNReal.toReal_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
rw :
  Eq (α := ℝ) (∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) • (ENNReal.toReal ∘ g) x)
    (∑ a ∈ f.range,
      (HMul.hMul (β := ℝ≥0∞) (g a)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞)).toReal)
⊢ integral μ (map (ENNReal.toReal ∘ g) f) = ((map g f).lintegral μ).toReal
have rw₁ : ∀ a ∈ f.range,
  HMul.hMul (β := ℝ≥0∞) (g a) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) ≠ ∞
Tactic: rw [map_integral f _ hf, map_lintegral, ENNReal.toReal_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
rw :
  Eq (α := ℝ) (∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) • (ENNReal.toReal ∘ g) x)
    (∑ a ∈ f.range,
      (HMul.hMul (β := ℝ≥0∞) (g a)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞)).toReal)
rw₁ :
  ∀ a ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) (g a) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) ≠ ∞
⊢ integral μ (map (ENNReal.toReal ∘ g) f) = ((map g f).lintegral μ).toReal
have rw₂ : (ENNReal.toReal ∘ g) 0 = 0
Tactic: rw [map_integral f _ hf, map_lintegral, ENNReal.toReal_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ Eq (α := ℝ) (∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) • (ENNReal.toReal ∘ g) x)
    (∑ a ∈ f.range,
      (HMul.hMul (β := ℝ≥0∞) (g a)
          ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞)).toReal)
have refine : ∀ b ∈ f.range,
  μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) • (ENNReal.toReal ∘ g) b =
    (HMul.hMul (β := ℝ≥0∞) (g b)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : ℝ≥0∞)).toReal
Tactic: refine Finset.sum_congr rfl fun b _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
b : E
h : b ∈ f.range
⊢ μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) • (ENNReal.toReal ∘ g) b =
    (HMul.hMul (β := ℝ≥0∞) (g b)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : ℝ≥0∞)).toReal
have rw : μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * (ENNReal.toReal ∘ g) b =
  (HMul.hMul (β := ℝ≥0∞) (g b) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : ℝ≥0∞)).toReal
Tactic: rw [smul_eq_mul, toReal_mul, mul_comm, Function.comp_apply, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
b : E
h : b ∈ f.range
rw :
  μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * (ENNReal.toReal ∘ g) b =
    (HMul.hMul (β := ℝ≥0∞) (g b)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : ℝ≥0∞)).toReal
⊢ μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) • (ENNReal.toReal ∘ g) b =
    (HMul.hMul (β := ℝ≥0∞) (g b)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : ℝ≥0∞)).toReal
have rw₁ : μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * (ENNReal.toReal ∘ g) b =
  (g b).toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}))
Tactic: rw [smul_eq_mul, toReal_mul, mul_comm, Function.comp_apply, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
b : E
h : b ∈ f.range
rw :
  μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * (ENNReal.toReal ∘ g) b =
    (HMul.hMul (β := ℝ≥0∞) (g b)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : ℝ≥0∞)).toReal
rw₁ :
  μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * (ENNReal.toReal ∘ g) b =
    (g b).toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}))
⊢ μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) • (ENNReal.toReal ∘ g) b =
    (HMul.hMul (β := ℝ≥0∞) (g b)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : ℝ≥0∞)).toReal
have rw₂ : (ENNReal.toReal ∘ g) b * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) =
  (g b).toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}))
Tactic: rw [smul_eq_mul, toReal_mul, mul_comm, Function.comp_apply, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
b : E
h : b ∈ f.range
rw :
  μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * (ENNReal.toReal ∘ g) b =
    (HMul.hMul (β := ℝ≥0∞) (g b)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : ℝ≥0∞)).toReal
rw₁ :
  μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * (ENNReal.toReal ∘ g) b =
    (g b).toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}))
rw₂ :
  (ENNReal.toReal ∘ g) b * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) =
    (g b).toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}))
⊢ μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) • (ENNReal.toReal ∘ g) b =
    (HMul.hMul (β := ℝ≥0∞) (g b)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : ℝ≥0∞)).toReal
have rw₃ : (g b).toReal * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) =
  (g b).toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}))
Tactic: rw [smul_eq_mul, toReal_mul, mul_comm, Function.comp_apply, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
b : E
h : b ∈ f.range
rw :
  μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * (ENNReal.toReal ∘ g) b =
    (HMul.hMul (β := ℝ≥0∞) (g b)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : ℝ≥0∞)).toReal
rw₁ :
  μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * (ENNReal.toReal ∘ g) b =
    (g b).toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}))
rw₂ :
  (ENNReal.toReal ∘ g) b * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) =
    (g b).toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}))
rw₃ :
  (g b).toReal * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) =
    (g b).toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}))
⊢ μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) • (ENNReal.toReal ∘ g) b =
    (HMul.hMul (β := ℝ≥0∞) (g b)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) : ℝ≥0∞)).toReal
have rw₄ : (g b).toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b})) =
  (g b).toReal * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {b}))
Tactic: rw [smul_eq_mul, toReal_mul, mul_comm, Function.comp_apply, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
a : E
⊢ HMul.hMul (β := ℝ≥0∞) (g a) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) ≠ ∞
have pos : ∀ (a0 : a = 0),
  HMul.hMul (β := ℝ≥0∞) (g a) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) ≠ ∞
Tactic: by_cases a0 : a = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
a : E
pos :
  ∀ (a0 : a = 0),
    HMul.hMul (β := ℝ≥0∞) (g a) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) ≠ ∞
⊢ HMul.hMul (β := ℝ≥0∞) (g a) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) ≠ ∞
have neg : ∀ (a0 : ¬a = 0),
  HMul.hMul (β := ℝ≥0∞) (g a) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) ≠ ∞
Tactic: by_cases a0 : a = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
a : E
a0 : a = 0
⊢ HMul.hMul (β := ℝ≥0∞) (g a) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) ≠ ∞
have pos : Ne (α := ℝ≥0∞) 0 ∞
Tactic: rw [a0, hg0, zero_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (ε := ℝ) (⇑f : (a : α) → ℝ) μ
h_pos : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : α) → ℝ)
⊢ integral μ f = (∫⁻ (a : α), ENNReal.ofReal ((f : (a : α) → ℝ) a) ∂μ).toReal
have this : (ae μ).EventuallyEq (β := ℝ) (⇑f : (a : α) → ℝ) (⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f) : (a : α) → ℝ)
Tactic: have : f =ᵐ[μ] f.map (ENNReal.toReal ∘ ENNReal.ofReal) :=
    h_pos.mono fun a h => (ENNReal.toReal_ofReal h).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (ε := ℝ) (⇑f : (a : α) → ℝ) μ
h_pos : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : α) → ℝ)
this : (ae μ).EventuallyEq (β := ℝ) (⇑f : (a : α) → ℝ) (⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f) : (a : α) → ℝ)
⊢ integral μ f = (∫⁻ (a : α), ENNReal.ofReal ((f : (a : α) → ℝ) a) ∂μ).toReal
have rw : integral μ f = integral μ (map (ENNReal.toReal ∘ ENNReal.ofReal) f)
Tactic: rw [← integral_eq_lintegral' hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (ε := ℝ) (⇑f : (a : α) → ℝ) μ
h_pos : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : α) → ℝ)
this : (ae μ).EventuallyEq (β := ℝ) (⇑f : (a : α) → ℝ) (⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f) : (a : α) → ℝ)
rw : integral μ f = integral μ (map (ENNReal.toReal ∘ ENNReal.ofReal) f)
⊢ integral μ f = (∫⁻ (a : α), ENNReal.ofReal ((f : (a : α) → ℝ) a) ∂μ).toReal
have hg0 : ENNReal.ofReal 0 = 0
Tactic: rw [← integral_eq_lintegral' hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (ε := ℝ) (⇑f : (a : α) → ℝ) μ
h_pos : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : α) → ℝ)
this : (ae μ).EventuallyEq (β := ℝ) (⇑f : (a : α) → ℝ) (⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f) : (a : α) → ℝ)
rw : integral μ f = integral μ (map (ENNReal.toReal ∘ ENNReal.ofReal) f)
hg0 : ENNReal.ofReal 0 = 0
⊢ integral μ f = (∫⁻ (a : α), ENNReal.ofReal ((f : (a : α) → ℝ) a) ∂μ).toReal
have ht : ∀ (b : ℝ), ENNReal.ofReal b ≠ ∞
Tactic: rw [← integral_eq_lintegral' hf]