awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
hy : (y1, y2) ∈ s
h₁ :
  ∀ (u : Set α) (v : Set β) (u_open : IsOpen[inst] u) (v_open : IsOpen[inst_3] v) (yu : y1 ∈ u) (yv : y2 ∈ v)
    (huv : u ×ˢ v ⊆ s), Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis β, F a ×ˢ a) (y1, y2)
⊢ Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis β, F a ×ˢ a) (y1, y2)

Tactic:
rcases isOpen_prod_iff.1 hs y1 y2 hy with ⟨u, v, u_open, v_open, yu, yv, huv⟩

Premises used: isOpen_prod_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u_1 : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
hy : (y1, y2) ∈ s
u : Set α
v : Set β
u_open : IsOpen[inst] u
v_open : IsOpen[inst_3] v
yu : y1 ∈ u
yv : y2 ∈ v
huv : u ×ˢ v ⊆ s
⊢ ∃ a ∈ countableBasis β, y2 ∈ a ∧ a ⊆ v

Tactic:
IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis β) yv v_open

Premises used: TopologicalSpace.isBasis_countableBasis, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u_1 : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
hy : (y1, y2) ∈ s
u : Set α
v : Set β
u_open : IsOpen[inst] u
v_open : IsOpen[inst_3] v
yu : y1 ∈ u
yv : y2 ∈ v
huv : u ×ˢ v ⊆ s
h₁ :
  ∀ (a : Set β) (ha : a ∈ countableBasis β) (ya : y2 ∈ a) (au : a ⊆ v),
    Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis β, F a ×ˢ a) (y1, y2)
⊢ Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis β, F a ×ˢ a) (y1, y2)

Tactic:
obtain ⟨a, ha, ya, au⟩ : ∃ a ∈ countableBasis β, y2 ∈ a ∧ a ⊆ v :=
          IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis β) yv v_open

Premises used: TopologicalSpace.countableBasis, TopologicalSpace.isBasis_countableBasis, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u_1 : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
hy : (y1, y2) ∈ s
u : Set α
v : Set β
u_open : IsOpen[inst] u
v_open : IsOpen[inst_3] v
yu : y1 ∈ u
yv : y2 ∈ v
huv : u ×ˢ v ⊆ s
a : Set β
ha : a ∈ countableBasis β
ya : y2 ∈ a
au : a ⊆ v
h₁ : ∃ (i : Set β), y1 ∈ F i ∧ i ∈ countableBasis β ∧ y2 ∈ i
⊢ Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis β, F a ×ˢ a) (y1, y2)

Tactic:
simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop]

Premises used: Set.mem_iUnion, exists_and_left, exists_prop, Set.mem_prod
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u_1 : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
hy : (y1, y2) ∈ s
u : Set α
v : Set β
u_open : IsOpen[inst] u
v_open : IsOpen[inst_3] v
yu : y1 ∈ u
yv : y2 ∈ v
huv : u ×ˢ v ⊆ s
a : Set β
ha : a ∈ countableBasis β
ya : y2 ∈ a
au : a ⊆ v
⊢ ∃ (i : Set β), y1 ∈ F i ∧ i ∈ countableBasis β ∧ y2 ∈ i

Tactic:
⟨a, ⟨u, u_open, yu, (Set.prod_mono_right au).trans huv⟩, ha, ya⟩

Premises used: Set.prod_mono_right, HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u_1 : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
hy : (y1, y2) ∈ s
u : Set α
v : Set β
u_open : IsOpen[inst] u
v_open : IsOpen[inst_3] v
yu : y1 ∈ u
yv : y2 ∈ v
huv : u ×ˢ v ⊆ s
a : Set β
ha : a ∈ countableBasis β
ya : y2 ∈ a
au : a ⊆ v
⊢ ∃ (i : Set β), y1 ∈ F i ∧ i ∈ countableBasis β ∧ y2 ∈ i

Tactic:
exact ⟨a, ⟨u, u_open, yu, (Set.prod_mono_right au).trans huv⟩, ha, ya⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
hy : Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis β, F a ×ˢ a) (y1, y2)
⊢ ∃ (i : Set β), y1 ∈ F i ∧ i ∈ countableBasis β ∧ y2 ∈ i

Tactic:
simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop] at hy

Premises used: Set.mem_iUnion, exists_and_left, exists_prop, Set.mem_prod
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
hy : ∃ (i : Set β), y1 ∈ F i ∧ i ∈ countableBasis β ∧ y2 ∈ i
h₂ : ∀ (a : Set β) (b : Set α) (yb : y1 ∈ b) (hb : b ×ˢ a ⊆ s) (ya : y2 ∈ a), (y1, y2) ∈ s
⊢ (y1, y2) ∈ s

Tactic:
rcases hy with ⟨a, ⟨b, -, yb, hb⟩, -, ya⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
a : Set β
b : Set α
yb : y1 ∈ b
hb : b ×ˢ a ⊆ s
ya : y2 ∈ a
⊢ (y1, y2) ∈ s

Tactic:
hb (mem_prod.2 ⟨yb, ya⟩)

Premises used: Iff.mpr, Set.mem_prod, And.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
a : Set β
b : Set α
yb : y1 ∈ b
hb : b ×ˢ a ⊆ s
ya : y2 ∈ a
⊢ (y1, y2) ∈ s

Tactic:
exact hb (mem_prod.2 ⟨yb, ya⟩)

Premises used: Iff.mpr, Set.mem_prod, And.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
⊢ s = ⋃ a ∈ countableBasis β, F a ×ˢ a

Tactic:
have : s = ⋃ a ∈ countableBasis β, F a ×ˢ a := by
      apply Subset.antisymm
      · rintro ⟨y1, y2⟩ hy
        rcases isOpen_prod_iff.1 hs y1 y2 hy with ⟨u, v, u_open, v_open, yu, yv, huv⟩
        obtain ⟨a, ha, ya, au⟩ : ∃ a ∈ countableBasis β, y2 ∈ a ∧ a ⊆ v :=
          IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis β) yv v_open
        simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop]
        exact ⟨a, ⟨u, u_open, yu, (Set.prod_mono_right au).trans huv⟩, ha, ya⟩
      · rintro ⟨y1, y2⟩ hy
        simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop] at hy
        rcases hy with ⟨a, ⟨b, -, yb, hb⟩, -, ya⟩
        exact hb (mem_prod.2 ⟨yb, ya⟩)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
this : s = ⋃ a ∈ countableBasis β, F a ×ˢ a
inr : MeasurableSet (α := α × β) (⋃ a ∈ countableBasis β, F a ×ˢ a)
⊢ MeasurableSet s

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
this : s = ⋃ a ∈ countableBasis β, F a ×ˢ a
apply : ∀ (a : Set β) (ha : a ∈ countableBasis β), MeasurableSet (F a ×ˢ a)
⊢ MeasurableSet (α := α × β) (⋃ a ∈ countableBasis β, F a ×ˢ a)

Tactic:
apply MeasurableSet.biUnion (countable_countableBasis β) (fun a ha ↦ ?_)

Premises used: TopologicalSpace.countable_countableBasis, MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
this : s = ⋃ a ∈ countableBasis β, F a ×ˢ a
a : Set β
ha : a ∈ countableBasis β
⊢ MeasurableSet (F a ×ˢ a)

Tactic:
(A a).measurableSet.prod (isOpen_of_mem_countableBasis ha).measurableSet

Premises used: IsOpen.measurableSet, MeasurableSet.prod, TopologicalSpace.isOpen_of_mem_countableBasis
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
this : s = ⋃ a ∈ countableBasis β, F a ×ˢ a
a : Set β
ha : a ∈ countableBasis β
⊢ MeasurableSet (F a ×ˢ a)

Tactic:
exact (A a).measurableSet.prod (isOpen_of_mem_countableBasis ha).measurableSet

Premises used: IsOpen.measurableSet, MeasurableSet.prod, TopologicalSpace.isOpen_of_mem_countableBasis
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α' : Type u_6
inst : TopologicalSpace α'
inst_1 : MeasurableSpace α'
μ : Measure α'
s : Set α'
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ interior s =ᶠ[ae μ] s

Tactic:
interior_subset.eventuallyLE.antisymm <| subset_closure.eventuallyLE.trans (ae_le_set.2 h)

Premises used: Iff.mpr, interior_subset, subset_closure, HasSubset.Subset.eventuallyLE, Filter.EventuallyLE.antisymm, Filter.EventuallyLE.trans, MeasureTheory.ae_le_set
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α' : Type u_6
inst : TopologicalSpace α'
inst_1 : MeasurableSpace α'
μ : Measure α'
s : Set α'
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (interior s) : ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_congr (interior_ae_eq_of_null_frontier h)

Premises used: MeasureTheory.measure_congr, interior_ae_eq_of_null_frontier
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
μ : Measure α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet s μ

Tactic:
⟨interior s, isOpen_interior.measurableSet, (interior_ae_eq_of_null_frontier h).symm⟩

Premises used: MeasurableSet, isOpen_interior, MeasureTheory.NullMeasurableSet, IsOpen.measurableSet, interior_ae_eq_of_null_frontier, And.intro, interior, Exists.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α' : Type u_6
inst : TopologicalSpace α'
inst_1 : MeasurableSpace α'
μ : Measure α'
s : Set α'
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ closure[inst] s =ᶠ[ae μ] s

Tactic:
((ae_le_set.2 h).trans interior_subset.eventuallyLE).antisymm <| subset_closure.eventuallyLE

Premises used: Iff.mpr, interior_subset, subset_closure, HasSubset.Subset.eventuallyLE, Filter.EventuallyLE.antisymm, Filter.EventuallyLE.trans, MeasureTheory.ae_le_set
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α' : Type u_6
inst : TopologicalSpace α'
inst_1 : MeasurableSpace α'
μ : Measure α'
s : Set α'
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (closure[inst] s) : ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_congr (closure_ae_eq_of_null_frontier h)

Premises used: MeasureTheory.measure_congr, closure_ae_eq_of_null_frontier
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α' : Type u_6
inst : TopologicalSpace α'
inst_1 : MeasurableSpace α'
μ : Measure α'
s s' : Set α'
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s') : ℝ≥0∞) (0 : ℝ≥0∞)
h₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier (s ∩ s')) : ℝ≥0∞) (⊥ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier (s ∩ s')) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply bot_unique

Premises used: bot_unique
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α' : Type u_6
inst : TopologicalSpace α'
inst_1 : MeasurableSpace α'
μ : Measure α'
s s' : Set α'
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s') : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ frontier s ∩ closure[inst] s' ∪ closure[inst] s ∩ frontier s' ⊆ frontier s ∪ frontier s'

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α' : Type u_6
inst : TopologicalSpace α'
inst_1 : MeasurableSpace α'
μ : Measure α'
s s' : Set α'
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s') : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ : (a : Set α') → ℝ≥0∞) (frontier s ∪ frontier s') ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞)
      ((μ : (a : Set α') → ℝ≥0∞) (frontier s') : ℝ≥0∞)

Tactic:
measure_union_le _ _

Premises used: MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α' : Type u_6
inst : TopologicalSpace α'
inst_1 : MeasurableSpace α'
μ : Measure α'
s s' : Set α'
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s') : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞)
      ((μ : (a : Set α') → ℝ≥0∞) (frontier s') : ℝ≥0∞) =
    0

Tactic:
simp [h, h']
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α' : Type u_6
inst : TopologicalSpace α'
inst_1 : MeasurableSpace α'
μ : Measure α'
s s' : Set α'
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s') : ℝ≥0∞) (0 : ℝ≥0∞)
calc :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞)
      ((μ : (a : Set α') → ℝ≥0∞) (frontier s') : ℝ≥0∞) =
    0
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier (s ∩ s')) : ℝ≥0∞) (⊥ : ℝ≥0∞)

Tactic:
calc μ (frontier (s ∩ s'))
  _ ≤ μ (frontier s ∪ frontier s') := measure_mono <| (frontier_inter_subset _ _).trans (by grind)
  _ ≤ μ (frontier s) + μ (frontier s') := measure_union_le _ _
  _ = 0 := by simp [h, h']

Premises used: frontier, HasSubset.Subset.trans, Inter.inter, MeasureTheory.measure_mono, Union.union, DFunLike.coe, frontier_inter_subset, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
α' : Type u_6
inst_13 : TopologicalSpace α'
inst_14 : MeasurableSpace α'
inst_15 : T0Space α
x y : α
contrapose! : x ≠ y → ∃ (s : Set α), MeasurableSet s ∧ x ∈ s ∧ y ∉ s
⊢ (∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s) → x = y

Tactic:
contrapose!