awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s r) : ℝ≥0∞) (∞ : ℝ≥0∞)
ha : Order.IsPredPrelimit a
this : IsCountablyGenerated.{u_8} (α := (↑(Ioi a) : Type u_8)) atBot
pos : ∀ (i : { x : ι // x ∈ Ioi a }), NullMeasurableSet (s (↑i : ι)) μ
pos₁ : Monotone.{u_8, u_1} (β := Set α) fun (x : { x : ι // x ∈ Ioi a }) ↦ s (↑x : ι)
⊢ Tendsto (α := { x : ι // x ∈ Ioi a }) (β := ℝ≥0∞)
    (((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ Ioi a) : { x : ι // x ∈ Ioi a } → ℝ≥0∞) atBot
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (x : (↑(Ioi a) : Type u_8)), s (↑x : ι))) : Filter ℝ≥0∞)
have pos₂ : ∃ (i : { x : ι // x ∈ Ioi a }), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply tendsto_measure_iInter_atBot
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s r) : ℝ≥0∞) (∞ : ℝ≥0∞)
ha : Order.IsPredPrelimit a
this : IsCountablyGenerated.{u_8} (α := (↑(Ioi a) : Type u_8)) atBot
⊢ ∀ (i : { x : ι // x ∈ Ioi a }), NullMeasurableSet (s (↑i : ι)) μ
have pos : ∀ (a_1 : ι) (b : a_1 ∈ Ioi a), NullMeasurableSet (s (↑(Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioi a) a_1 b) : ι)) μ
Tactic: rwa [Subtype.forall]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s r) : ℝ≥0∞) (∞ : ℝ≥0∞)
ha : ¬Order.IsPredPrelimit a
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) (𝓝[>] a)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (r : ι), ⋂ (_ : r > a), s r)) : Filter ℝ≥0∞)
have ha₁ : ∃ (b : ι), a ⋖ b
Tactic: rw [Order.not_isPredPrelimit_iff] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s r) : ℝ≥0∞) (∞ : ℝ≥0∞)
ha : ∃ (b : ι), a ⋖ b
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) (𝓝[>] a)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (r : ι), ⋂ (_ : r > a), s r)) : Filter ℝ≥0∞)
have neg : ∀ (b : ι) (hab : a ⋖ b),
  Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) (𝓝[>] a)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (r : ι), ⋂ (_ : r > a), s r)) : Filter ℝ≥0∞)
Tactic: rcases ha with ⟨b, hab⟩
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x : β
t : Set β
s : Set α
inst : Decidable (x ∈ t)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (if x ∈ t then s else ∅) : ℝ≥0∞)
    (t.indicator (fun (x : β) ↦ (μ : (a : Set α) → ℝ≥0∞) s) x : ℝ≥0∞)
have pos : ∀ (h : x ∈ t),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (t.indicator (fun (x : β) ↦ (μ : (a : Set α) → ℝ≥0∞) s) x : ℝ≥0∞)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x : β
t : Set β
s : Set α
inst : Decidable (x ∈ t)
pos :
  ∀ (h : x ∈ t),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (t.indicator (fun (x : β) ↦ (μ : (a : Set α) → ℝ≥0∞) s) x : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (if x ∈ t then s else ∅) : ℝ≥0∞)
    (t.indicator (fun (x : β) ↦ (μ : (a : Set α) → ℝ≥0∞) s) x : ℝ≥0∞)
have neg : ∀ (h : x ∉ t),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (t.indicator (fun (x : β) ↦ (μ : (a : Set α) → ℝ≥0∞) s) x : ℝ≥0∞)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
⊢ μ = ν
have h₁ : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
⊢ s = ⋃ x ∈ s, measurableAtom x
have h₁ : ∀ (y : α), y ∈ s ↔ Membership.mem (γ := Set α) (⋃ x ∈ s, measurableAtom x) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
y : α
⊢ y ∈ s ↔ Membership.mem (γ := Set α) (⋃ x ∈ s, measurableAtom x) y
have h₁ : y ∈ s ↔ ∃ i ∈ s, y ∈ measurableAtom i
Tactic: simp only [mem_iUnion, exists_prop]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
y : α
⊢ y ∈ s ↔ ∃ i ∈ s, y ∈ measurableAtom i
have h₁ : ∀ (hy : y ∈ s), ∃ i ∈ s, y ∈ measurableAtom i
Tactic: refine ⟨fun hy ↦ ?_, fun ⟨x, hx, hy⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
y : α
h₁ : ∀ (hy : y ∈ s), ∃ i ∈ s, y ∈ measurableAtom i
⊢ y ∈ s ↔ ∃ i ∈ s, y ∈ measurableAtom i
have h₂ : (∃ i ∈ s, y ∈ measurableAtom i) → ∀ (x : α) (hx : x ∈ s) (hy : y ∈ measurableAtom x), y ∈ s
Tactic: refine ⟨fun hy ↦ ?_, fun ⟨x, hx, hy⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h1 : s = ⋃ x ∈ s, measurableAtom x
Tactic: have h1 : s = ⋃ x ∈ s, measurableAtom x := by
    ext y
    simp only [mem_iUnion, exists_prop]
    refine ⟨fun hy ↦ ?_, fun ⟨x, hx, hy⟩ ↦ ?_⟩
    · exact ⟨y, hy, mem_measurableAtom_self y⟩
    · exact mem_of_mem_measurableAtom hy hs hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃ x ∈ s, measurableAtom x
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h1₁ : s = ⋃₀ (measurableAtom '' s)
Tactic: rw [← sUnion_image] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ (measurableAtom '' s)) : ℝ≥0∞)
  ((ν : (a : Set α) → ℝ≥0∞) (⋃₀ (measurableAtom '' s)) : ℝ≥0∞)
Tactic: rw [h1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ (measurableAtom '' s)) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (⋃₀ (measurableAtom '' s)) : ℝ≥0∞)
have h_count : (measurableAtom '' s).Countable
Tactic: have h_count : (measurableAtom '' s).Countable := s.to_countable.image _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
t : Set α
ht : t ∈ measurableAtom '' s
t' : Set α
ht' : t' ∈ measurableAtom '' s
h_eq : t ≠ t'
⊢ Disjoint t t'
have obtain : ∀ (y : α) (hys : y ∈ s) (hy : measurableAtom y = t), Disjoint t t'
Tactic: obtain ⟨y, hys, hy⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
t t' : Set α
h_eq : t ≠ t'
y : α
hys : y ∈ s
hy : measurableAtom y = t
y' : α
hy's : y' ∈ s
hy' : measurableAtom y' = t'
⊢ Disjoint t t'
have rw : ∀ (hys : y ∈ s) (hy : measurableAtom y = t) (y' : α) (h_eq : measurableAtom y ≠ measurableAtom y') (hy's : y' ∈ s)
  (hy' : measurableAtom y' = t'), Disjoint (measurableAtom y) (measurableAtom y')
Tactic: rw [← hy, ← hy'] at h_eq ⊢
Cleared hypotheses: h_eq, hys, hy, y', hy's, hy'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
t t' : Set α
y : α
hys : y ∈ s
hy : measurableAtom y = t
y' : α
h_eq : measurableAtom y ≠ measurableAtom y'
hy's : y' ∈ s
hy' : measurableAtom y' = t'
⊢ Disjoint (measurableAtom y) (measurableAtom y')
have refine : ∀ (hyy' : y ∈ measurableAtom y'), measurableAtom y = measurableAtom y'
Tactic: refine disjoint_measurableAtom_of_notMem fun hyy' ↦ h_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ (measurableAtom '' s)) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (⋃₀ (measurableAtom '' s)) : ℝ≥0∞)
have h_disj : (measurableAtom '' s).Pairwise Disjoint
Tactic: have h_disj : (measurableAtom '' s).Pairwise Disjoint := by
    intro t ht t' ht' h_eq
    obtain ⟨y, hys, hy⟩ := ht
    obtain ⟨y', hy's, hy'⟩ := ht'
    rw [← hy, ← hy'] at h_eq ⊢
    refine disjoint_measurableAtom_of_notMem fun hyy' ↦ h_eq ?_
    exact measurableAtom_eq_of_mem hyy'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
t : Set α
ht : t ∈ measurableAtom '' s
⊢ MeasurableSet t
have obtain : ∀ (x : α) (hxs : x ∈ s) (hx : measurableAtom x = t), MeasurableSet t
Tactic: obtain ⟨x, hxs, hx⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
t : Set α
x : α
hxs : x ∈ s
hx : measurableAtom x = t
⊢ MeasurableSet t
have rw : MeasurableSet (measurableAtom x)
Tactic: rw [← hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ (measurableAtom '' s)) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (⋃₀ (measurableAtom '' s)) : ℝ≥0∞)
have h_meas : ∀ (t : Set α) (ht : t ∈ measurableAtom '' s), MeasurableSet t
Tactic: have h_meas (t) (ht : t ∈ measurableAtom '' s) : MeasurableSet t := by
    obtain ⟨x, hxs, hx⟩ := ht
    rw [← hx]
    exact MeasurableSet.measurableAtom_of_countable x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ (t : Set α) (ht : t ∈ measurableAtom '' s), MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ (measurableAtom '' s)) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (⋃₀ (measurableAtom '' s)) : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (∑' (s_1 : (↑(measurableAtom '' s) : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s_1 : Set α))
  (∑' (s_1 : (↑(measurableAtom '' s) : Type u_1)), (ν : (a : Set α) → ℝ≥0∞) (↑s_1 : Set α))
Tactic: rw [measure_sUnion h_count h_disj h_meas, measure_sUnion h_count h_disj h_meas]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ (t : Set α) (ht : t ∈ measurableAtom '' s), MeasurableSet t
⊢ Eq (α := ℝ≥0∞) (∑' (s_1 : (↑(measurableAtom '' s) : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s_1 : Set α))
    (∑' (s_1 : (↑(measurableAtom '' s) : Type u_1)), (ν : (a : Set α) → ℝ≥0∞) (↑s_1 : Set α))
have h₁ : ∀ (s' : (↑(measurableAtom '' s) : Type u_1)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞)
Tactic: congr with s'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ (t : Set α) (ht : t ∈ measurableAtom '' s), MeasurableSet t
s' : (↑(measurableAtom '' s) : Type u_1)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞)
have hs' : (↑s' : Set α) ∈ measurableAtom '' s
Tactic: have hs' := s'.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ (t : Set α) (ht : t ∈ measurableAtom '' s), MeasurableSet t
s' : (↑(measurableAtom '' s) : Type u_1)
hs' : (↑s' : Set α) ∈ measurableAtom '' s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞)
have h₁ : ∀ (x : α) (hxs : x ∈ s) (hx : measurableAtom x = (↑s' : Set α)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞)
Tactic: obtain ⟨x, hxs, hx⟩ := hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ (t : Set α) (ht : t ∈ measurableAtom '' s), MeasurableSet t
s' : (↑(measurableAtom '' s) : Type u_1)
x : α
hxs : x ∈ s
hx : measurableAtom x = (↑s' : Set α)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
Tactic: rw [← hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
⊢ Eq (α := ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine le_antisymm ?_ (le_toMeasure_apply _ _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
⊢ LE.le (α := ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rcases : ∀ (t : Set α) (hts : t ⊆ s) (htm : MeasurableSet t) (heq : t =ᶠ[ae (m.toMeasure h)] s),
  LE.le (α := ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases hs.exists_measurable_subset_ae_eq with ⟨t, hts, htm, heq⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
htu : t ⊆ u
ht_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
have ht_ne_top₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [h] at ht_ne_top
Cleared hypotheses: ht_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
htu : t ⊆ u
ht_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: refine le_antisymm (by gcongr) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
htu : t ⊆ u
ht_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have A : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞)
Tactic: have A : μ (u ∩ s) + μ (u \ s) ≤ μ (t ∩ s) + μ (u \ s) :=
    calc
      μ (u ∩ s) + μ (u \ s) = μ u := measure_inter_add_diff _ hs
      _ = μ t := h.symm
      _ = μ (t ∩ s) + μ (t \ s) := (measure_inter_add_diff _ hs).symm
      _ ≤ μ (t ∩ s) + μ (u \ s) := by gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
htu : t ⊆ u
ht_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have B : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have B : μ (u \ s) ≠ ∞ := (lt_of_le_of_lt (measure_mono diff_subset) ht_ne_top.lt_top).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: refine le_antisymm (measure_mono inter_subset_right) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have H : s ≤ᶠ[ae μ] t ∩ s
Tactic: apply EventuallyLE.measure_le