awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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
rw : ∀ x ∈ s, x ∉ {x ∈ f.range | x ≠ 0} → μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x = 0
⊢ integral μ f = ∑ x ∈ s, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x

Tactic:
rw [SimpleFunc.integral_eq_sum_filter, Finset.sum_subset hs]

Premises used: MeasureTheory.SimpleFunc.integral_eq_sum_filter, Finset.sum_subset
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 : x ∉ {x ∈ f.range | x ≠ 0}
⊢ x ∉ f.range ∨ x = 0

Tactic:
rw [Finset.mem_filter, not_and_or, Ne, Classical.not_not] at hx

Premises used: Classical.not_not, Ne, not_and_or, Finset.mem_filter
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 : x ∉ f.range ∨ x = 0
inl :
  ∀ (hx : 0 ∉ f.range ∨ Eq.{u_3 + 1} (α := F) 0 0),
    HSMul.hSMul (β := F) (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {0})) 0 = 0
inr : ∀ (hx : x ∉ f.range), μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x = 0
⊢ μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x = 0

Tactic:
rcases hx.symm with (rfl | hx)

Premises used: Or.symm, rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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
hx : 0 ∉ f.range ∨ Eq.{u_3 + 1} (α := F) 0 0
⊢ HSMul.hSMul (β := F) (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {0})) 0 = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 ∉ f.range
⊢ x ∉ Set.range.{u_3, u_1 + 1} (ι := α) (⇑f : (a : α) → F)

Tactic:
rw [SimpleFunc.mem_range] at hx

Premises used: MeasureTheory.SimpleFunc.mem_range
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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
inr₁ : Disjoint (α := Set F) {x} (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f : (a : α) → F))
⊢ μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x = 0

Tactic:
rw [preimage_eq_empty]

Premises used: Set.preimage_eq_empty
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 ∅ • x = 0

Tactic:
simp [Set.disjoint_singleton_left, hx]

Premises used: Set.disjoint_singleton_left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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)
⊢ Disjoint (α := Set F) {x} (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f : (a : α) → F))

Tactic:
simp [Set.disjoint_singleton_left, hx]

Premises used: Set.disjoint_singleton_left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
y : F
⊢ integral μ (const α y) = ∑ z ∈ {y}, μ.real (Set.preimage (β := F) (⇑(const α y) : (a : α) → F) {z}) • z

Tactic:
integral_eq_sum_of_subset <| (filter_subset _ _).trans (range_const_subset _ _)

Premises used: Finset.filter_subset, HasSubset.Subset.trans, MeasureTheory.SimpleFunc.integral_eq_sum_of_subset, MeasureTheory.SimpleFunc.range_const_subset
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
y : F
⊢ ∑ z ∈ {y}, μ.real (Set.preimage (β := F) (⇑(const α y) : (a : α) → F) {z}) • z = μ.real Set.univ • y

Tactic:
simp [Set.preimage]

Premises used: Set.preimage
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
y : F
α₁ : ∑ z ∈ {y}, μ.real (Set.preimage (β := F) (⇑(const α y) : (a : α) → F) {z}) • z = μ.real Set.univ • y
⊢ integral μ (const α y) = μ.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]

Premises used: MeasureTheory.SimpleFunc.const, Set.univ, MeasureTheory.Measure.real, Finset.filter_subset, HasSubset.Subset.trans, MeasureTheory.SimpleFunc.integral_eq_sum_of_subset, MeasureTheory.SimpleFunc.integral, MeasureTheory.SimpleFunc.range_const_subset
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
y : F
α₁ : ∑ z ∈ {y}, μ.real (Set.preimage (β := F) (⇑(const α y) : (a : α) → F) {z}) • z = μ.real Set.univ • y
⊢ integral μ (const α y) = μ.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]

Premises used: MeasureTheory.SimpleFunc.const, Set.univ, MeasureTheory.Measure.real, Finset.filter_subset, HasSubset.Subset.trans, MeasureTheory.SimpleFunc.integral_eq_sum_of_subset, MeasureTheory.SimpleFunc.integral, MeasureTheory.SimpleFunc.range_const_subset
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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

Tactic:
(integral_eq_sum_of_subset ?_).trans
      ((sum_congr rfl fun y hy => ?_).trans (integral_eq_sum_filter _ _).symm)

Premises used: MeasureTheory.SimpleFunc.integral_eq_sum_filter, MeasureTheory.SimpleFunc.integral_eq_sum_of_subset, Eq.symm, Finset.sum_congr, rfl, Eq.trans
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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}
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
⊢ integral μ (piecewise s hs f 0) = integral (μ.restrict s) f

Tactic:
refine (integral_eq_sum_of_subset ?_).trans
      ((sum_congr rfl fun y hy => ?_).trans (integral_eq_sum_filter _ _).symm)

Premises used: MeasureTheory.SimpleFunc.integral_eq_sum_filter, MeasureTheory.SimpleFunc.integral_eq_sum_of_subset, Eq.symm, Finset.sum_congr, rfl, Eq.trans
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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}
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
⊢ y ∈ {x ∈ f.range | x ≠ 0}

Tactic:
simp only [mem_filter, mem_range, coe_piecewise, coe_zero, piecewise_eq_indicator,
      mem_range_indicator] at *

Premises used: MeasureTheory.SimpleFunc.mem_range, MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, Set.mem_range_indicator, Finset.mem_filter, Set.piecewise_eq_indicator
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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
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)
⊢ Membership.mem (γ := Set F) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f : (a : α) → F)) y ∧ y ≠ 0

Tactic:
rcases hy with ⟨⟨rfl, -⟩ | ⟨x, -, rfl⟩, h₀⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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
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:
(h₀ rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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
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:
⟨Set.mem_range_self _, h₀⟩

Premises used: Set.mem_range_self, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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
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:
exacts [(h₀ rfl).elim, ⟨Set.mem_range_self _, h₀⟩]

Premises used: False.elim, rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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}
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
⊢ μ.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:
dsimp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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}
refine_2 : 0 ∉ {y}
⊢ μ.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:
rw [Set.piecewise_eq_indicator, indicator_preimage_of_notMem,
      measureReal_restrict_apply (f.measurableSet_preimage _)]

Premises used: MeasureTheory.SimpleFunc.measurableSet_preimage, Set.piecewise_eq_indicator, MeasureTheory.measureReal_restrict_apply, Set.indicator_preimage_of_notMem
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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}
⊢ 0 ∉ {y}

Tactic:
fun h₀ => (mem_filter.1 hy).2 (Eq.symm h₀)

Premises used: And.right, Iff.mp, Finset.mem_filter, Eq.symm, Not
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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}
⊢ 0 ∉ {y}

Tactic:
exact fun h₀ => (mem_filter.1 hy).2 (Eq.symm h₀)

Premises used: And.right, Iff.mp, Finset.mem_filter, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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}
refine_2 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
⊢ integral μ (piecewise s hs f 0) = integral (μ.restrict s) f

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₀)

Premises used: MeasureTheory.SimpleFunc.integral_eq_sum_filter, MeasureTheory.SimpleFunc.mem_range, MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, Set.mem_range_indicator, MeasureTheory.SimpleFunc.integral_eq_sum_of_subset, MeasureTheory.SimpleFunc.measurableSet_preimage, Finset.mem_filter, Set.piecewise_eq_indicator, Eq.symm, Finset.sum_congr, MeasureTheory.measureReal_restrict_apply, rfl, Eq.trans, Set.indicator_preimage_of_notMem
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → F
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : g 0 = 0
⊢ integral μ (map g f) = ∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) • g x

Tactic:
map_setToSimpleFunc _ weightedSMul_union hf hg

Premises used: MeasureTheory.weightedSMul_union, MeasureTheory.SimpleFunc.integral, MeasureTheory.SimpleFunc.map_setToSimpleFunc
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 ≠ ∞
⊢ f.FinMeasSupp μ

Tactic:
have hf' : f.FinMeasSupp μ := integrable_iff_finMeasSupp.1 hf
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 μ
simp : integral μ (map (ENNReal.toReal ∘ g) f) = ((map g f).lintegral μ).toReal
⊢ integral μ (map (ENNReal.toReal ∘ g) f) = (∫⁻ (a : α), g ((f : (a : α) → E) a) ∂μ).toReal

Tactic:
simp only [← map_apply g f, lintegral_eq_lintegral]

Premises used: MeasureTheory.SimpleFunc.map_apply, MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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∞) ≠ ∞
rw₂ : (ENNReal.toReal ∘ g) 0 = 0
⊢ integral μ (map (ENNReal.toReal ∘ g) f) = ((map g f).lintegral μ).toReal

Tactic:
rw [map_integral f _ hf, map_lintegral, ENNReal.toReal_sum]

Premises used: MeasureTheory.SimpleFunc.map_lintegral, ENNReal.toReal_sum, MeasureTheory.SimpleFunc.map_integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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)

Tactic:
Finset.sum_congr rfl fun b _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 μ
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
⊢ 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:
refine Finset.sum_congr rfl fun b _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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}))
rw₄ 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}))
⊢ μ.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]

Premises used: ENNReal.toReal_mul, mul_comm, MeasureTheory.measureReal_def, Function.comp_apply, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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∞) ≠ ∞
neg :
  ∀ (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∞) ≠ ∞

Tactic:
by_cases a0 : a = 0
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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
pos : Ne (α := ℝ≥0∞) 0 ∞
⊢ HMul.hMul (β := ℝ≥0∞) (g a) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := E) (⇑f : (a : α) → E) {a}) : ℝ≥0∞) ≠ ∞

Tactic:
rw [a0, hg0, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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
⊢ Ne (α := ℝ≥0∞) 0 ∞

Tactic:
WithTop.zero_ne_top

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.zero_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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
⊢ Ne (α := ℝ≥0∞) 0 ∞

Tactic:
exact WithTop.zero_ne_top

Premises used: WithTop.zero_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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∞) ≠ ∞

Tactic:
apply mul_ne_top (ht a) (hf'.meas_preimage_singleton_ne_zero a0).ne

Premises used: MeasureTheory.SimpleFunc.FinMeasSupp.meas_preimage_singleton_ne_zero, ENNReal.mul_ne_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
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 μ
⊢ (ENNReal.toReal ∘ g) 0 = 0

Tactic:
simp [hg0]