awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 : ι)
pos₂ : ∃ (i : { x : ι // x ∈ Ioi a }), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 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∞)

Tactic:
apply tendsto_measure_iInter_atBot

Premises used: MeasureTheory.tendsto_measure_iInter_atBot
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 pos₁ pos₂ pos₃ :
  ∀ (a_1 : ι) (b : a_1 ∈ Ioi a), NullMeasurableSet (s (↑(Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioi a) a_1 b) : ι)) μ
⊢ ∀ (i : { x : ι // x ∈ Ioi a }), NullMeasurableSet (s (↑i : ι)) μ

Tactic:
rwa [Subtype.forall]

Premises used: Subtype.forall
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
⊢ Monotone.{u_8, u_1} (β := Set α) fun (x : { x : ι // x ∈ Ioi a }) ↦ s (↑x : ι)

Tactic:
fun i j h ↦ hm i j i.2 h

Premises used: Monotone, Subtype.val, Subtype.property
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
⊢ Monotone.{u_8, u_1} (β := Set α) fun (x : { x : ι // x ∈ Ioi a }) ↦ s (↑x : ι)

Tactic:
exact fun i j h ↦ hm i j i.2 h
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 }), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s (↑i : ι)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa only [Subtype.exists, exists_prop]

Premises used: Subtype.exists, exists_prop
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
⊢ ∃ (b : ι), a ⋖ b

Tactic:
rw [Order.not_isPredPrelimit_iff] at ha

Premises used: Order.not_isPredPrelimit_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
neg :
  ∀ (b : ι) (hab : a ⋖ b),
    Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) (𝓝[>] a)
      (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (r : ι), ⋂ (_ : r > a), s r)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) (𝓝[>] a)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (r : ι), ⋂ (_ : r > a), s r)) : Filter ℝ≥0∞)

Tactic:
rcases ha with ⟨b, hab⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
b : ι
hab : a ⋖ b
⊢ Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s : ι → ℝ≥0∞) (𝓝[>] a)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (r : ι), ⋂ (_ : r > a), s r)) : Filter ℝ≥0∞)

Tactic:
simp [hab.nhdsGT]

Premises used: CovBy.nhdsGT
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
neg :
  ∀ (h : x ∉ t),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥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∞)

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x : β
t : Set β
s : Set α
inst : Decidable (x ∈ t)
h : x ∈ t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (t.indicator (fun (x : β) ↦ (μ : (a : Set α) → ℝ≥0∞) s) x : ℝ≥0∞)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x : β
t : Set β
s : Set α
inst : Decidable (x ∈ t)
h : x ∉ t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (t.indicator (fun (x : β) ↦ (μ : (a : Set α) → ℝ≥0∞) s) x : ℝ≥0∞)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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∞)
h₁ :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
h₁ : ∀ (y : α), y ∈ s ↔ Membership.mem (γ := Set α) (⋃ x ∈ s, measurableAtom x) y
⊢ s = ⋃ x ∈ s, measurableAtom x

Tactic:
ext y
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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₁ : y ∈ s ↔ ∃ i ∈ s, y ∈ measurableAtom i
⊢ y ∈ s ↔ Membership.mem (γ := Set α) (⋃ x ∈ s, measurableAtom x) y

Tactic:
simp only [mem_iUnion, exists_prop]

Premises used: Set.mem_iUnion, exists_prop
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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

Tactic:
⟨fun hy ↦ ?_, fun ⟨x, hx, hy⟩ ↦ ?_⟩

Premises used: Membership.mem, Iff.intro, _private.0.MeasureTheory.ext_of_measurableAtoms.match_1
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
h₂ : (∃ i ∈ s, y ∈ measurableAtom i) → ∀ (x : α) (hx : x ∈ s) (hy : y ∈ measurableAtom x), y ∈ s
⊢ y ∈ s ↔ ∃ i ∈ s, y ∈ measurableAtom i

Tactic:
refine ⟨fun hy ↦ ?_, fun ⟨x, hx, hy⟩ ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 : α
hy : y ∈ s
⊢ ∃ i ∈ s, y ∈ measurableAtom i

Tactic:
⟨y, hy, mem_measurableAtom_self y⟩

Premises used: mem_measurableAtom_self, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 : α
hy : y ∈ s
⊢ ∃ i ∈ s, y ∈ measurableAtom i

Tactic:
exact ⟨y, hy, mem_measurableAtom_self y⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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_1 : ∃ i ∈ s, y ∈ measurableAtom i
x : α
hx : x ∈ s
hy : y ∈ measurableAtom x
⊢ y ∈ s

Tactic:
mem_of_mem_measurableAtom hy hs hx

Premises used: mem_of_mem_measurableAtom
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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_1 : ∃ i ∈ s, y ∈ measurableAtom i
x : α
hx : x ∈ s
hy : y ∈ measurableAtom x
⊢ y ∈ s

Tactic:
exact mem_of_mem_measurableAtom hy hs hx

Premises used: mem_of_mem_measurableAtom
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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

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
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
⊢ s = ⋃₀ (measurableAtom '' s)

Tactic:
rw [← sUnion_image] at h1

Premises used: Set.sUnion_image
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ (measurableAtom '' s)) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (⋃₀ (measurableAtom '' s)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [h1]
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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)
⊢ (measurableAtom '' s).Countable

Tactic:
have h_count : (measurableAtom '' s).Countable := s.to_countable.image _
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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'
obtain : ∀ (y : α) (hys : y ∈ s) (hy : measurableAtom y = t), Disjoint t t'
⊢ Disjoint t t'

Tactic:
obtain ⟨y, hys, hy⟩ := ht
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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'
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')
⊢ Disjoint t t'

Tactic:
rw [← hy, ← hy'] at h_eq ⊢
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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')

Tactic:
disjoint_measurableAtom_of_notMem fun hyy' ↦ h_eq ?_

Premises used: disjoint_measurableAtom_of_notMem
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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'
refine : ∀ (hyy' : y ∈ measurableAtom y'), measurableAtom y = measurableAtom y'
⊢ Disjoint (measurableAtom y) (measurableAtom y')

Tactic:
refine disjoint_measurableAtom_of_notMem fun hyy' ↦ h_eq ?_

Premises used: disjoint_measurableAtom_of_notMem
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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'
hyy' : y ∈ measurableAtom y'
⊢ measurableAtom y = measurableAtom y'

Tactic:
measurableAtom_eq_of_mem hyy'

Premises used: measurableAtom_eq_of_mem
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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'
hyy' : y ∈ measurableAtom y'
⊢ measurableAtom y = measurableAtom y'

Tactic:
exact measurableAtom_eq_of_mem hyy'

Premises used: measurableAtom_eq_of_mem
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
⊢ (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'
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
obtain : ∀ (x : α) (hxs : x ∈ s) (hx : measurableAtom x = t), MeasurableSet t
⊢ MeasurableSet t

Tactic:
obtain ⟨x, hxs, hx⟩ := ht
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
rw : MeasurableSet (measurableAtom x)
⊢ MeasurableSet t

Tactic:
rw [← hx]
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 (measurableAtom x)

Tactic:
MeasurableSet.measurableAtom_of_countable x

Premises used: MeasurableSet.measurableAtom_of_countable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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 (measurableAtom x)

Tactic:
exact MeasurableSet.measurableAtom_of_countable x

Premises used: MeasurableSet.measurableAtom_of_countable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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

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
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
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 α))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ (measurableAtom '' s)) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (⋃₀ (measurableAtom '' s)) : ℝ≥0∞)

Tactic:
rw [measure_sUnion h_count h_disj h_meas, measure_sUnion h_count h_disj h_meas]

Premises used: MeasureTheory.measure_sUnion
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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
h₁ :
  ∀ (s' : (↑(measurableAtom '' s) : Type u_1)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞)
⊢ 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:
congr with s'
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
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)
⊢ (↑s' : Set α) ∈ measurableAtom '' s

Tactic:
have hs' := s'.2