awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν_1 : Measure α
s t : Set α
a : α
μ ν : Measure α
inst_1 : SigmaFinite μ
inst_2 : SigmaFinite ν
⊢ SigmaFinite.{u_1} (α := α) (m0 := m0) (sum fun (b : Bool) ↦ bif b then μ else ν)
have refine_1 : SigmaFinite (bif false then μ else ν)
Tactic: refine @sum.sigmaFinite _ _ _ _ _ (Bool.rec ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν_1 : Measure α
s t : Set α
a : α
μ ν : Measure α
inst_1 : SigmaFinite μ
inst_2 : SigmaFinite ν
refine_1 : SigmaFinite (bif false then μ else ν)
⊢ SigmaFinite.{u_1} (α := α) (m0 := m0) (sum fun (b : Bool) ↦ bif b then μ else ν)
have refine_2 : SigmaFinite (bif true then μ else ν)
Tactic: refine @sum.sigmaFinite _ _ _ _ _ (Bool.rec ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν : Measure α
s t : Set α
a : α
μ : Measure α
inst_1 : SigmaFinite μ
c : ℝ≥0
i : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)
have simp : HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i) : ℝ≥0∞) < ∞
Tactic: simp only [Measure.coe_smul, Pi.smul_apply, nnreal_smul_coe_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
h : SigmaFinite (m0 := inst) (Measure.map f μ)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f ⁻¹' spanningSets (m0 := inst) (Measure.map f μ) n) i) univ
have rw : f ⁻¹' ⋃ (i : ℕ), spanningSets (m0 := inst) (Measure.map f μ) i = univ
Tactic: rw [← preimage_iUnion, iUnion_spanningSets, preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
h : SigmaFinite (m0 := inst) (Measure.map f μ)
rw : f ⁻¹' ⋃ (i : ℕ), spanningSets (m0 := inst) (Measure.map f μ) i = univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f ⁻¹' spanningSets (m0 := inst) (Measure.map f μ) n) i) univ
have rw₁ : f ⁻¹' univ = univ
Tactic: rw [← preimage_iUnion, iUnion_spanningSets, preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
h : SigmaFinite (m0 := inst) (Measure.map f μ)
rw : f ⁻¹' ⋃ (i : ℕ), spanningSets (m0 := inst) (Measure.map f μ) i = univ
rw₁ : f ⁻¹' univ = univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f ⁻¹' spanningSets (m0 := inst) (Measure.map f μ) n) i) univ
have rw₂ : Eq.{u_1 + 1} (α := Set α) univ univ
Tactic: rw [← preimage_iUnion, iUnion_spanningSets, preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
⊢ SigmaFinite (m0 := inst) (Measure.map f μ)
have refine_1 : ∀ (n : ℕ),
  LT.lt (α := ℝ≥0∞)
    (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) ((fun (n : ℕ) ↦ f '' spanningSets μ n ∪ (range f)ᶜ) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: refine ⟨fun n ↦ f '' (spanningSets μ n) ∪ (Set.range f)ᶜ, by simp, fun n ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
refine_1 :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) ((fun (n : ℕ) ↦ f '' spanningSets μ n ∪ (range f)ᶜ) n) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ SigmaFinite (m0 := inst) (Measure.map f μ)
have refine_2 : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f '' spanningSets μ n ∪ (range f)ᶜ) i) univ
Tactic: refine ⟨fun n ↦ f '' (spanningSets μ n) ∪ (Set.range f)ᶜ, by simp, fun n ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) ((fun (n : ℕ) ↦ f '' spanningSets μ n ∪ (range f)ᶜ) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have refine_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' spanningSets μ n ∪ f ⁻¹' (range f)ᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [hf.map_apply, Set.preimage_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' spanningSets μ n ∪ f ⁻¹' (range f)ᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (spanningSets μ n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: simp only [Set.preimage_compl, Set.preimage_range, Set.compl_univ, Set.union_empty,
      Set.preimage_image_eq _ hf.injective]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f '' spanningSets μ n ∪ (range f)ᶜ) i) univ
have refine_2 : (⋃ (i : ℕ), f '' spanningSets μ i) ∪ (range f)ᶜ = univ
Tactic: rw [← Set.iUnion_union, ← Set.image_iUnion, iUnion_spanningSets,
      Set.image_univ, Set.union_compl_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
refine_2 : (⋃ (i : ℕ), f '' spanningSets μ i) ∪ (range f)ᶜ = univ
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f '' spanningSets μ n ∪ (range f)ᶜ) i) univ
have refine_2₁ : (f '' ⋃ (i : ℕ), spanningSets μ i) ∪ (range f)ᶜ = univ
Tactic: rw [← Set.iUnion_union, ← Set.image_iUnion, iUnion_spanningSets,
      Set.image_univ, Set.union_compl_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
refine_2 : (⋃ (i : ℕ), f '' spanningSets μ i) ∪ (range f)ᶜ = univ
refine_2₁ : (f '' ⋃ (i : ℕ), spanningSets μ i) ∪ (range f)ᶜ = univ
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f '' spanningSets μ n ∪ (range f)ᶜ) i) univ
have refine_2₂ : f '' univ ∪ (range f)ᶜ = univ
Tactic: rw [← Set.iUnion_union, ← Set.image_iUnion, iUnion_spanningSets,
      Set.image_univ, Set.union_compl_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
refine_2 : (⋃ (i : ℕ), f '' spanningSets μ i) ∪ (range f)ᶜ = univ
refine_2₁ : (f '' ⋃ (i : ℕ), spanningSets μ i) ∪ (range f)ᶜ = univ
refine_2₂ : f '' univ ∪ (range f)ᶜ = univ
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f '' spanningSets μ n ∪ (range f)ᶜ) i) univ
have refine_2₃ : range f ∪ (range f)ᶜ = univ
Tactic: rw [← Set.iUnion_union, ← Set.image_iUnion, iUnion_spanningSets,
      Set.image_univ, Set.union_compl_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
refine_2 : (⋃ (i : ℕ), f '' spanningSets μ i) ∪ (range f)ᶜ = univ
refine_2₁ : (f '' ⋃ (i : ℕ), spanningSets μ i) ∪ (range f)ᶜ = univ
refine_2₂ : f '' univ ∪ (range f)ᶜ = univ
refine_2₃ : range f ∪ (range f)ᶜ = univ
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f '' spanningSets μ n ∪ (range f)ᶜ) i) univ
have refine_2₄ : Eq.{u_2 + 1} (α := Set β) univ univ
Tactic: rw [← Set.iUnion_union, ← Set.image_iUnion, iUnion_spanningSets,
      Set.image_univ, Set.union_compl_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
P : α → Prop
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∀ᵐ (x : α) ∂μ.restrict s, P x
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
have this : ∀ᵐ (x : α) ∂μ.restrict (spanningSets (μ + ν) n), P x
Tactic: have := h
      (spanningSets (μ + ν) n) (measurableSet_spanningSets _ _)
      ((self_le_add_right _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
      ((self_le_add_left _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
P : α → Prop
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∀ᵐ (x : α) ∂μ.restrict s, P x
⊢ ∀ᵐ (x : α) ∂μ, P x
have this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
Tactic: have : ∀ n, ∀ᵐ x ∂μ, x ∈ spanningSets (μ + ν) n → P x := by
    intro n
    have := h
      (spanningSets (μ + ν) n) (measurableSet_spanningSets _ _)
      ((self_le_add_right _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
      ((self_le_add_left _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
    exact (ae_restrict_iff' (measurableSet_spanningSets _ _)).mp this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
P : α → Prop
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∀ᵐ (x : α) ∂μ.restrict s, P x
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
⊢ ∀ᵐ (x : α) ∂μ, P x
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ℕ), a ∈ spanningSets (μ + ν) i → P a) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ P x) x} x}
    a
Tactic: filter_upwards [ae_all_iff.2 this] with _ hx using hx _ (mem_spanningSetsIndex _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
P : α → Prop
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∀ᵐ (x : α) ∂μ.restrict s, P x
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ℕ), a ∈ spanningSets (μ + ν) i → P a) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ P x) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ, P x
have h₂ : ∀ (a : α), (∀ (i : ℕ), a ∈ spanningSets (μ + ν) i → P a) → P a
Tactic: filter_upwards [ae_all_iff.2 this] with _ hx using hx _ (mem_spanningSetsIndex _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsLocallyFiniteMeasure μ
⊢ SigmaFinite μ
have choose : ∀ (s : (x : α) → Set α) (hsx : ∀ (x : α), s x ∈ 𝓝 x)
  (hsμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s x) : ℝ≥0∞) (∞ : ℝ≥0∞)), SigmaFinite μ
Tactic: choose s hsx hsμ using μ.finiteAt_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
s_1 t : Set α
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsLocallyFiniteMeasure μ
s : (x : α) → Set α
hsx : ∀ (x : α), s x ∈ 𝓝 x
hsμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s x) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ SigmaFinite μ
have rcases : ∀ (t : Set α) (htc : t.Countable) (htU : Eq.{u_1 + 1} (α := Set α) (⋃ x ∈ t, s x) univ), SigmaFinite μ
Tactic: rcases TopologicalSpace.countable_cover_nhds hsx with ⟨t, htc, htU⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
s_1 t_1 : Set α
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsLocallyFiniteMeasure μ
s : (x : α) → Set α
hsx : ∀ (x : α), s x ∈ 𝓝 x
hsμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s x) : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α
htc : t.Countable
htU : Eq.{u_1 + 1} (α := Set α) (⋃ x ∈ t, s x) univ
⊢ SigmaFinite μ
have refine : ⋃₀ (s '' t) = univ
Tactic: refine Measure.sigmaFinite_of_countable (htc.image s) (forall_mem_image.2 fun x _ => hsμ x) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
have pos : ∀ (hs : MeasurableSet s),
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
Tactic: by_cases hs : MeasurableSet s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
pos :
  ∀ (hs : MeasurableSet s),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
      Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
have neg : ∀ (hs : ¬MeasurableSet s),
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
Tactic: by_cases hs : MeasurableSet s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
hs : ¬MeasurableSet s
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
have neg : ∀ (t : Set α),
  s ⊆ t →
    ∀ (mt : MeasurableSet t)
      (ht : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)),
      Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
        Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
Tactic: obtain ⟨t, _, mt, ht⟩ := exists_measurable_superset μ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
hs : ¬MeasurableSet s
t : Set α
left : s ⊆ t
mt : MeasurableSet t
ht : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
have neg : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal) ∨
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
Tactic: rw [← ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
⊢ (∃ (s : Set α), Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)) ↔
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
have mp : (∃ (s : Set α), Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)) →
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
mp :
  (∃ (s : Set α), Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)) →
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
⊢ (∃ (s : Set α), Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)) ↔
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
have mpr : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal) →
  ∃ (s : Set α), Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
have mp : ∀ (h₀ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (0 : ENNReal)),
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
Tactic: rcases μ.zero_one univ with (h₀ | h₁)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
mp :
  ∀ (h₀ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (0 : ENNReal)),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
have mp₁ : ∀ (h₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)),
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
Tactic: rcases μ.zero_one univ with (h₀ | h₁)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h₀ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
have this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal)
Tactic: have := measure_mono (μ := μ) <| subset_univ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h₀ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (0 : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
have this₁ : LE.le (α := ENNReal) (1 : ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal)
Tactic: rw [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
Tactic: have : μ (s ∩ t) ≤ μ s := measure_mono inter_subset_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have this₁ : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: have : μ (s ∩ t) ≤ μ t := measure_mono inter_subset_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inl : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) →
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
Tactic: rcases μ.zero_one s with (_ | hμs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
inl :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) →
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inr : ∀ (hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)),
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
Tactic: rcases μ.zero_one s with (_ | hμs)