awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
nontriviality : Subsingleton α → AEMeasurable f (μ.restrict s)
nontriviality₁ nontriviality₂ : Nontrivial α → AEMeasurable f (μ.restrict s)
nontriviality₃ : Nontrivial α → ∀ (inhabited_h : Inhabited α), AEMeasurable f (μ.restrict s)
nontriviality₄ :
  Nontrivial α →
    ∀ (inhabited_h : Inhabited α)
      (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f),
      AEMeasurable f (μ.restrict s)
nontriviality₅ :
  Nontrivial α →
    ∀ (inhabited_h : Inhabited α)
      (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f),
      Measurable (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default)
hf₁ hf₂ :
  Nontrivial α →
    ∀ (inhabited_h : Inhabited α)
      (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f) (t : Set β)
      (ht : IsOpen[inst_3] t), MeasurableSet ((s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) ⁻¹' t)
hf₃ :
  Nontrivial α →
    ∀ (inhabited_h : Inhabited α)
      (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f) (t : Set β)
      (ht : IsOpen[inst_3] t) (u : Set α) (u_open : IsOpen[inst] u) (hu : f ⁻¹' t ∩ s = u ∩ s),
      MeasurableSet ((s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) ⁻¹' t)
⊢ AEMeasurable f (μ.restrict s)
have hf₄ : Nontrivial α →
  ∀ (inhabited_h : Inhabited α)
    (this : (s.piecewise (β := fun (a : α) ↦ β) f fun (x : α) ↦ f default) =ᶠ[ae (μ.restrict s)] f) (t : Set β)
    (ht : IsOpen[inst_3] t) (u : Set α) (u_open : IsOpen[inst] u) (hu : f ⁻¹' t ∩ s = u ∩ s),
    MeasurableSet (u ∩ s ∪ (fun (x : α) ↦ f default) ⁻¹' t \ s)
Tactic: classical
  nontriviality α; inhabit α
  have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs
  refine ⟨Set.piecewise s f fun _ => f default, ?_, this.symm⟩
  apply measurable_of_isOpen
  intro t ht
  obtain ⟨u, u_open, hu⟩ : ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
    _root_.continuousOn_iff'.1 hf t ht
  rw [piecewise_preimage, Set.ite, hu]
  exact (u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : NullMeasurableSet s μ
⊢ AEMeasurable f (μ.restrict s)
have rcases : ∀ (t : Set α) (ts : t ⊆ s) (ht : MeasurableSet t) (t_eq_s : t =ᶠ[ae μ] s), AEMeasurable f (μ.restrict s)
Tactic: rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, ht, t_eq_s⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : NullMeasurableSet s μ
t : Set α
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
⊢ AEMeasurable f (μ.restrict s)
have rw : AEMeasurable f (μ.restrict t)
Tactic: rw [← Measure.restrict_congr_set t_eq_s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
⊢ AEStronglyMeasurable f (μ.restrict s)
have this₁ : let this := borel β;
BorelSpace β
Tactic: borelize β
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
⊢ AEStronglyMeasurable f (μ.restrict s)
have rw : AEMeasurable f (μ.restrict s) ∧ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ.restrict s, f x ∈ t
Tactic: rw [aestronglyMeasurable_iff_aemeasurable_separable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
⊢ AEMeasurable f (μ.restrict s) ∧ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ.restrict s, f x ∈ t
have refine : ∀ᵐ (x : α) ∂μ.restrict s, f x ∈ f '' s
Tactic: refine ⟨hf.aemeasurable hs, f '' s, hf.isSeparable_image h's, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
⊢ AEStronglyMeasurable f (μ.restrict s)
have this : let this := borel β;
BorelSpace β
Tactic: borelize β
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ AEStronglyMeasurable f (μ.restrict s)
have f₁ : IsSeparable (f '' s)
Tactic: refine
    aestronglyMeasurable_iff_aemeasurable_separable.2
      ⟨hf.aemeasurable hs, f '' s, ?_,
        mem_of_superset (self_mem_ae_restrict hs) (subset_preimage_image _ _)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ IsSeparable (f '' s)
have inl : SecondCountableTopology α → IsSeparable (f '' s)
Tactic: cases h.out
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
inl : SecondCountableTopology α → IsSeparable (f '' s)
⊢ IsSeparable (f '' s)
have inr : SecondCountableTopology β → IsSeparable (f '' s)
Tactic: cases h.out
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
h_1 : SecondCountableTopology α
⊢ IsSeparable (f '' s)
have inl : IsSeparable.{u_2} (α := β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
Tactic: rw [image_eq_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
⊢ AEStronglyMeasurable f (μ.restrict t)
have this : let this := borel β;
BorelSpace β
Tactic: borelize β
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ AEStronglyMeasurable f (μ.restrict t)
have rw : AEMeasurable f (μ.restrict t) ∧ ∃ (t_1 : Set β), IsSeparable t_1 ∧ ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ t_1
Tactic: rw [aestronglyMeasurable_iff_aemeasurable_separable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ AEMeasurable f (μ.restrict t) ∧ ∃ (t_1 : Set β), IsSeparable t_1 ∧ ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ t_1
have refine_1 : IsSeparable (f '' s)
Tactic: refine ⟨(hf.mono hts).aemeasurable ht, f '' s, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
refine_1 : IsSeparable (f '' s)
⊢ AEMeasurable f (μ.restrict t) ∧ ∃ (t_1 : Set β), IsSeparable t_1 ∧ ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ t_1
have refine_2 : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ f '' s
Tactic: refine ⟨(hf.mono hts).aemeasurable ht, f '' s, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ f '' s
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ t) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ f '' s) x} x}
    a
Tactic: filter_upwards [ae_restrict_mem ht] with a ha using image_mono hts (mem_image_of_mem f ha)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ t) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ f '' s) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ f '' s
have h₁ : ∀ a ∈ t, f a ∈ f '' s
Tactic: filter_upwards [ae_restrict_mem ht] with a ha using image_mono hts (mem_image_of_mem f ha)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopologyEither α E
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
a : α
⊢ IntegrableAtFilter f (𝓝 a) μ
have rw : IntegrableAtFilter f (𝓝[univ] a) μ
Tactic: rw [← nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ
have pos : ∀ (hab : a ≤ b), IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ
Tactic: by_cases hab : a ≤ b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
pos : ∀ (hab : a ≤ b), IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ
have neg : ∀ (hab : ¬a ≤ b), IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ
Tactic: by_cases hab : a ≤ b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
hab : a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ
have pos : IntegrableOn f (Ioc a b ∪ {a}) μ ↔ IntegrableOn f (Ioc a b) μ
Tactic: rw [← Ioc_union_left hab, integrableOn_union, eq_true (integrableOn_singleton ha'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
hab : a ≤ b
pos : IntegrableOn f (Ioc a b ∪ {a}) μ ↔ IntegrableOn f (Ioc a b) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ
have pos₁ : IntegrableOn f (Ioc a b) μ ∧ IntegrableOn f {a} μ ↔ IntegrableOn f (Ioc a b) μ
Tactic: rw [← Ioc_union_left hab, integrableOn_union, eq_true (integrableOn_singleton ha'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
hab : a ≤ b
pos : IntegrableOn f (Ioc a b ∪ {a}) μ ↔ IntegrableOn f (Ioc a b) μ
pos₁ : IntegrableOn f (Ioc a b) μ ∧ IntegrableOn f {a} μ ↔ IntegrableOn f (Ioc a b) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ
have pos₂ : IntegrableOn f (Ioc a b) μ ∧ True ↔ IntegrableOn f (Ioc a b) μ
Tactic: rw [← Ioc_union_left hab, integrableOn_union, eq_true (integrableOn_singleton ha'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
hab : a ≤ b
pos : IntegrableOn f (Ioc a b ∪ {a}) μ ↔ IntegrableOn f (Ioc a b) μ
pos₁ : IntegrableOn f (Ioc a b) μ ∧ IntegrableOn f {a} μ ↔ IntegrableOn f (Ioc a b) μ
pos₂ : IntegrableOn f (Ioc a b) μ ∧ True ↔ IntegrableOn f (Ioc a b) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ
have pos₃ : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioc a b) μ
Tactic: rw [← Ioc_union_left hab, integrableOn_union, eq_true (integrableOn_singleton ha'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
hab : ¬a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ
have neg : ¬a < b
Tactic: rw [Icc_eq_empty hab, Ioc_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
hab : ¬a ≤ b
⊢ ¬a < b
have neg : ∀ (hab : a < b), a ≤ b
Tactic: contrapose hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
have pos : ∀ (hab : a ≤ b), IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
Tactic: by_cases hab : a ≤ b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
pos : ∀ (hab : a ≤ b), IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
have neg : ∀ (hab : ¬a ≤ b), IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
Tactic: by_cases hab : a ≤ b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
hab : a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
have pos : IntegrableOn f (Ico a b ∪ {b}) μ ↔ IntegrableOn f (Ico a b) μ
Tactic: rw [← Ico_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
hab : a ≤ b
pos : IntegrableOn f (Ico a b ∪ {b}) μ ↔ IntegrableOn f (Ico a b) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
have pos₁ : IntegrableOn f (Ico a b) μ ∧ IntegrableOn f {b} μ ↔ IntegrableOn f (Ico a b) μ
Tactic: rw [← Ico_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
hab : a ≤ b
pos : IntegrableOn f (Ico a b ∪ {b}) μ ↔ IntegrableOn f (Ico a b) μ
pos₁ : IntegrableOn f (Ico a b) μ ∧ IntegrableOn f {b} μ ↔ IntegrableOn f (Ico a b) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
have pos₂ : IntegrableOn f (Ico a b) μ ∧ True ↔ IntegrableOn f (Ico a b) μ
Tactic: rw [← Ico_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
hab : a ≤ b
pos : IntegrableOn f (Ico a b ∪ {b}) μ ↔ IntegrableOn f (Ico a b) μ
pos₁ : IntegrableOn f (Ico a b) μ ∧ IntegrableOn f {b} μ ↔ IntegrableOn f (Ico a b) μ
pos₂ : IntegrableOn f (Ico a b) μ ∧ True ↔ IntegrableOn f (Ico a b) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
have pos₃ : IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ico a b) μ
Tactic: rw [← Ico_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
hab : ¬a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
have neg : ¬a < b
Tactic: rw [Icc_eq_empty hab, Ico_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
hab : ¬a ≤ b
⊢ ¬a < b
have neg : ∀ (hab : a < b), a ≤ b
Tactic: contrapose hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ
have pos : ∀ (hab : a < b), IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: by_cases hab : a < b