awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
x : α
hx : g x ∈ s
⊢ g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
have h : g x ∈ range g ∩ s
Tactic: apply subset_closure
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
⊢ ∫ (a : α), g a ∂μ ∈ s
have hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
Tactic: have hg : ∀ᵐ x ∂μ, g x ∈ closure (range g ∩ s) := by
    filter_upwards [hfg.rw (fun _ y => y ∈ s) hf] with x hx
    apply subset_closure
    exact ⟨mem_range_self _, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
⊢ ∫ (a : α), g a ∂μ ∈ s
have refine_1 : ∀ (n : ℕ), ∀ i ∈ (G n).range, 0 ≤ μ.real (preimage (β := E) (⇑(G n) : (a : α) → E) {i})
Tactic: refine hsc.mem_of_tendsto this (Eventually.of_forall fun n => hs.sum_mem ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
refine_1 : ∀ (n : ℕ), ∀ i ∈ (G n).range, 0 ≤ μ.real (preimage (β := E) (⇑(G n) : (a : α) → E) {i})
⊢ ∫ (a : α), g a ∂μ ∈ s
have refine_2 : ∀ (n : ℕ), Eq (α := ℝ) (∑ i ∈ (G n).range, μ.real (preimage (β := E) (⇑(G n) : (a : α) → E) {i})) 1
Tactic: refine hsc.mem_of_tendsto this (Eventually.of_forall fun n => hs.sum_mem ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
refine_1 : ∀ (n : ℕ), ∀ i ∈ (G n).range, 0 ≤ μ.real (preimage (β := E) (⇑(G n) : (a : α) → E) {i})
refine_2 : ∀ (n : ℕ), Eq (α := ℝ) (∑ i ∈ (G n).range, μ.real (preimage (β := E) (⇑(G n) : (a : α) → E) {i})) 1
⊢ ∫ (a : α), g a ∂μ ∈ s
have refine_3 : ∀ (n : ℕ),
  ∀ i ∈ (G n).range, Membership.mem (α := E) s (((↑(ContinuousLinearMap.id ℝ E) : E →ₗ[ℝ] E) : (a : E) → E) i : E)
Tactic: refine hsc.mem_of_tendsto this (Eventually.of_forall fun n => hs.sum_mem ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
⊢ Eq (α := ℝ)
    (∑ x ∈ (G n).range, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := E) (⇑(G n) : (a : α) → E) {x}))) 1
have refine_2 : ∀ a ∈ (G n).range,
  Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := E) (⇑(G n) : (a : α) → E) {a}) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← ENNReal.toReal_sum, (G n).sum_range_measure_preimage_singleton, measure_univ,
      ENNReal.toReal_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
⊢ ∀ i ∈ (G n).range, Membership.mem (α := E) s (((↑(ContinuousLinearMap.id ℝ E) : E →ₗ[ℝ] E) : (a : E) → E) i : E)
have refine_3 : ∀ (i : α),
  Membership.mem (α := E) s
    (((↑(ContinuousLinearMap.id ℝ E) : E →ₗ[ℝ] E) : (a : E) → E) ((G n : (a : α) → E) i : E) : E)
Tactic: simp only [SimpleFunc.mem_range, forall_mem_range]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
x : α
⊢ Membership.mem (α := E) s
    (((↑(ContinuousLinearMap.id ℝ E) : E →ₗ[ℝ] E) : (a : E) → E) ((G n : (a : α) → E) x : E) : E)
have refine_3 : Membership.mem (α := E) (range g ∩ s)
  (((↑(ContinuousLinearMap.id ℝ E) : E →ₗ[ℝ] E) : (a : E) → E) ((G n : (a : α) → E) x : E) : E)
Tactic: apply (range g).inter_subset_right
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst_3 : IsFiniteMeasure μ
inst_4 : NeZero μ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ Membership.mem (γ := Set (E × ℝ)) {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ)
have ht_mem : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set (E × ℝ)) {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} (f x, g (f x))
Tactic: have ht_mem : ∀ᵐ x ∂μ, (f x, g (f x)) ∈ {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} :=
    hfs.mono fun x hx => ⟨hx, le_rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨
    ∃ (t : Set α),
      MeasurableSet t ∧
        Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∧
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            Ne.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
have refine : ∀
  (H :
    ¬∃ (t : Set α),
        MeasurableSet t ∧
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
              Ne.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)),
  f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ)
Tactic: refine or_iff_not_imp_right.mpr fun H => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ¬∃ (t : Set α),
      MeasurableSet t ∧
        Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∧
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            Ne.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ)
have H₁ : ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
  (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
Tactic: push Not at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ)
have refine : ∀ (t : Set α) (ht : MeasurableSet t) (ht' : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ) (∫ (x : α) in t, const α (⨍ (x : α), f x ∂μ) x ∂μ)
Tactic: refine hfi.ae_eq_of_forall_setIntegral_eq _ _ (integrable_const _) fun t ht ht' => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ) (∫ (x : α) in t, const α (⨍ (x : α), f x ∂μ) x ∂μ)
have simp : ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
Tactic: simp only [const_apply, setIntegral_const]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have pos : ∀ (h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
Tactic: by_cases h₀ : μ t = 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
pos :
  ∀ (h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have neg : ∀ (h₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
Tactic: by_cases h₀ : μ t = 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have pos : (@integral _ _ _ _ m0 0 fun (x : α) ↦ f x) = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
Tactic: rw [restrict_eq_zero.2 h₀, integral_zero_measure, measureReal_def, h₀,
      ENNReal.toReal_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
pos : (@integral _ _ _ _ m0 0 fun (x : α) ↦ f x) = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have pos₁ : 0 = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
Tactic: rw [restrict_eq_zero.2 h₀, integral_zero_measure, measureReal_def, h₀,
      ENNReal.toReal_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
pos : (@integral _ _ _ _ m0 0 fun (x : α) ↦ f x) = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
pos₁ : 0 = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have pos₂ : 0 = HSMul.hSMul (β := E) (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)) (⨍ (x : α), f x ∂μ)
Tactic: rw [restrict_eq_zero.2 h₀, integral_zero_measure, measureReal_def, h₀,
      ENNReal.toReal_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
pos : (@integral _ _ _ _ m0 0 fun (x : α) ↦ f x) = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
pos₁ : 0 = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
pos₂ : 0 = HSMul.hSMul (β := E) (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)) (⨍ (x : α), f x ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have pos₃ : 0 = HSMul.hSMul (β := E) (ENNReal.toReal 0) (⨍ (x : α), f x ∂μ)
Tactic: rw [restrict_eq_zero.2 h₀, integral_zero_measure, measureReal_def, h₀,
      ENNReal.toReal_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
pos : (@integral _ _ _ _ m0 0 fun (x : α) ↦ f x) = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
pos₁ : 0 = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
pos₂ : 0 = HSMul.hSMul (β := E) (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)) (⨍ (x : α), f x ∂μ)
pos₃ : 0 = HSMul.hSMul (β := E) (ENNReal.toReal 0) (⨍ (x : α), f x ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have pos₄ : 0 = HSMul.hSMul (α := ℝ) (β := E) 0 (⨍ (x : α), f x ∂μ)
Tactic: rw [restrict_eq_zero.2 h₀, integral_zero_measure, measureReal_def, h₀,
      ENNReal.toReal_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
pos : (@integral _ _ _ _ m0 0 fun (x : α) ↦ f x) = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
pos₁ : 0 = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
pos₂ : 0 = HSMul.hSMul (β := E) (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)) (⨍ (x : α), f x ∂μ)
pos₃ : 0 = HSMul.hSMul (β := E) (ENNReal.toReal 0) (⨍ (x : α), f x ∂μ)
pos₄ : 0 = HSMul.hSMul (α := ℝ) (β := E) 0 (⨍ (x : α), f x ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have pos₅ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [restrict_eq_zero.2 h₀, integral_zero_measure, measureReal_def, h₀,
      ENNReal.toReal_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have pos : ∀ (h₀' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
Tactic: by_cases h₀' : μ tᶜ = 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀ (h₀' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have neg : ∀ (h₀' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
Tactic: by_cases h₀' : μ tᶜ = 0