awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
h'T : ¬T.Nonempty
⊢ False
have hT₁ : Eq.{u_1 + 1} (α := Set α) ∅ univ
Tactic: rw [not_nonempty_iff_eq_empty.1 h'T, sUnion_empty] at hT
Cleared hypotheses: hT, h'T
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
have T_ne : T.Nonempty
Tactic: have T_ne : T.Nonempty := by
    by_contra h'T
    rw [not_nonempty_iff_eq_empty.1 h'T, sUnion_empty] at hT
    simpa only [← hT] using mem_univ (default : α)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
have inr : ∀ (f : ℕ → Set α) (hf : T = range f), Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
Tactic: obtain ⟨f, hf⟩ : ∃ f : ℕ → Set α, T = range f := T_count.exists_eq_range T_ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
n : ℕ
⊢ f n ∈ S
have a : f n ∈ T
Tactic: apply TS
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
n : ℕ
⊢ f n ∈ T
have a : f n ∈ range f
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
have fS : ∀ (n : ℕ), f n ∈ S
Tactic: have fS : ∀ n, f n ∈ S := by
    intro n
    apply TS
    rw [hf]
    exact mem_range_self n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
have inr : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) univ
Tactic: refine
    ⟨{  set := f
        set_mem := fun n => (fS n).1
        finite := fun n => (fS n).2
        spanning := ?_ }⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f i) univ
have inr : ∀ (x : α), Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x
Tactic: refine eq_univ_of_forall fun x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
⊢ ∃ t ∈ range f, x ∈ t
have this : x ∈ ⋃₀ T
Tactic: have : x ∈ ⋃₀ T := by simp only [hT, mem_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x
have inr : ∀ (t : Set α) (tT : t ∈ range f) (xt : x ∈ t), Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x
Tactic: obtain ⟨t, tT, xt⟩ : ∃ t : Set α, t ∈ range f ∧ x ∈ t := by
    have : x ∈ ⋃₀ T := by simp only [hT, mem_univ]
    simpa only [mem_sUnion, exists_prop, ← hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
t : Set α
tT : t ∈ range f
xt : x ∈ t
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x
have inr : ∀ (n : ℕ) (tT : f n ∈ range f) (xt : x ∈ f n), Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x
Tactic: obtain ⟨n, rfl⟩ : ∃ n : ℕ, f n = t := by simpa only using tT
Cleared hypotheses: t, tT, xt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s_1 : Set α
inst : NoAtoms μ
s : Set α
⊢ NoAtoms (μ.restrict s)
have refine : ∀ (x : α), Eq (α := ENNReal) ((μ.restrict s : (a : Set α) → ENNReal) {x} : ENNReal) (0 : ENNReal)
Tactic: refine ⟨fun x => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s_1 : Set α
inst : NoAtoms μ
s : Set α
x : α
⊢ Eq (α := ENNReal) ((μ.restrict s : (a : Set α) → ENNReal) {x} : ENNReal) (0 : ENNReal)
have obtain : ∀ (t : Set α) (hxt : {x} ⊆ t) (ht1 : MeasurableSet t)
  (ht2 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)),
  Eq (α := ENNReal) ((μ.restrict s : (a : Set α) → ENNReal) {x} : ENNReal) (0 : ENNReal)
Tactic: obtain ⟨t, hxt, ht1, ht2⟩ := exists_measurable_superset_of_null (measure_singleton x : μ {x} = 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s_1 : Set α
inst : NoAtoms μ
s : Set α
x : α
t : Set α
hxt : {x} ⊆ t
ht1 : MeasurableSet t
ht2 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ.restrict s : (a : Set α) → ENNReal) {x} : ENNReal) (0 : ENNReal)
have apply : Eq (α := ENNReal) ((μ.restrict s : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
Tactic: apply measure_mono_null hxt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s_1 : Set α
inst : NoAtoms μ
s : Set α
x : α
t : Set α
hxt : {x} ⊆ t
ht1 : MeasurableSet t
ht2 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ.restrict s : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
have rw : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t ∩ s) : ENNReal) (0 : ENNReal)
Tactic: rw [Measure.restrict_apply ht1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : s.Countable
μ : Measure α
inst : NoAtoms μ
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
have rw : ∀ i ∈ s, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {i} : ENNReal) (0 : ENNReal)
Tactic: rw [← biUnion_of_singleton s, measure_biUnion_null_iff h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : NoAtoms μ
E : Set X
inst_3 : SeparableSpace.{u_2} (↑E : Type u_2)
hE : LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) E : ENNReal)
⊢ ∃ (x : X), AccPt x (𝓟 E)
have by_contra! : ∀ (h : ∀ (x : X), ¬AccPt x (𝓟 E)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms (hypothesis)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : NoAtoms μ
E : Set X
inst_3 : SeparableSpace.{u_2} (↑E : Type u_2)
hE : LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) E : ENNReal)
h : ∀ (x : X), ¬AccPt x (𝓟 E)
⊢ False
have this : DiscreteTopology.{u_2} (↑E : Type u_2)
Tactic: haveI : DiscreteTopology E := discreteTopology_of_noAccPts fun x _ => h x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
s : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: apply (measure_mono (subset_univ _)).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
s : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have inl : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
s : Set α
inl :
  ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have inr : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
⊢ Nonempty α
have by_contra! : ∀ (maybe_empty : IsEmpty α), False
Tactic: by_contra! maybe_empty
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
maybe_empty : IsEmpty α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Set.univ_eq_empty_iff.mpr maybe_empty, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
maybe_empty : IsEmpty α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [Set.univ_eq_empty_iff.mpr maybe_empty, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
maybe_empty : IsEmpty α
⊢ False
have this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have : μ Set.univ = 0 := by
    rw [Set.univ_eq_empty_iff.mpr maybe_empty, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 : Measure α
s : Set α
p : Prop
inst_1 : Decidable p
μ ν : Measure α
inst_2 : IsProbabilityMeasure μ
inst_3 : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure (if p then μ else ν)
have isTrue : p → IsProbabilityMeasure μ
Tactic: split
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 : Measure α
s : Set α
p : Prop
inst_1 : Decidable p
μ ν : Measure α
inst_2 : IsProbabilityMeasure μ
inst_3 : IsProbabilityMeasure ν
isTrue : p → IsProbabilityMeasure μ
⊢ IsProbabilityMeasure (if p then μ else ν)
have isFalse : ¬p → IsProbabilityMeasure ν
Tactic: split
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
inst_1 : IsProbabilityMeasure (m0 := inst) (map f μ)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have hf : AEMeasurable f μ
Tactic: have hf : AEMeasurable f μ := AEMeasurable.of_map_ne_zero (IsProbabilityMeasure.ne_zero _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
inst_1 : IsProbabilityMeasure (m0 := inst) (map f μ)
hf : AEMeasurable f μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [← Set.preimage_univ (f := f), ← map_apply_of_aemeasurable hf .univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
inst_1 : IsProbabilityMeasure μ
p : α → Prop
f_1 : β → α
f : β ≃ᵐ α
⊢ IsProbabilityMeasure.{u_2} (α := β) (m0 := inst) (Measure.comap (⇑f : (a : β) → α) μ)
have rw : IsProbabilityMeasure.{u_2} (α := β) (m0 := inst) (Measure.map (⇑f.symm : (a : α) → β) μ)
Tactic: rw [← MeasurableEquiv.map_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
h : NullMeasurableSet s μ
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [measure_compl₀ h (measure_ne_top _ _), measure_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
h : NullMeasurableSet s μ
rw :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [measure_compl₀ h (measure_ne_top _ _), measure_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
hs : NullMeasurableSet s μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = 0 ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [prob_compl_eq_one_sub₀ hs, tsub_eq_zero_iff_le, one_le_prob_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
hs : NullMeasurableSet s μ
rw :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = 0 ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₁ : LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [prob_compl_eq_one_sub₀ hs, tsub_eq_zero_iff_le, one_le_prob_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
hs : NullMeasurableSet s μ
rw :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = 0 ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
rw₁ :
  LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [prob_compl_eq_one_sub₀ hs, tsub_eq_zero_iff_le, one_le_prob_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
hs : NullMeasurableSet s μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (1 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← prob_compl_eq_zero_iff₀ hs.compl, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
hs : NullMeasurableSet s μ
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (1 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← prob_compl_eq_zero_iff₀ hs.compl, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : IsProbabilityMeasure μ
f : β → α
hf : Injective f
hf' : ∀ᵐ (a : α) ∂μ, a ∈ range f
hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : f '' univ ∈ ae μ
Tactic: rw [comap_apply _ hf hf'' _ MeasurableSet.univ,
      ← mem_ae_iff_prob_eq_one (hf'' _ MeasurableSet.univ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
⊢ IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
have inl : IsZeroOrProbabilityMeasure
  (HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) 0)
Tactic: rcases eq_zero_or_neZero μ with rfl | h
Cleared hypotheses: μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
inl :
  IsZeroOrProbabilityMeasure
    (HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) 0)
⊢ IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
have inr : ∀ (h : NeZero μ), IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
Tactic: rcases eq_zero_or_neZero μ with rfl | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
s : Set α
⊢ IsZeroOrProbabilityMeasure
    (HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) 0)
have inl : IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := m0) 0
Tactic: simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
h : NeZero μ
⊢ IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
have inr : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
  IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
Tactic: rcases eq_top_or_lt_top (μ univ) with h | h