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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
⊢ ∀ (a : Set α), IsOpen[inst_3] (F a)

Tactic:
have A : ∀ a, IsOpen (F a) := by
      intro a
      apply isOpen_iff_forall_mem_open.2
      rintro y ⟨b, b_open, yb, hb⟩
      exact ⟨b, fun z zb ↦ ⟨b, b_open, zb, hb⟩, b_open, yb⟩
-- 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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (F a)
h₁ : s ⊆ ⋃ a ∈ countableBasis α, a ×ˢ F a
h₂ : ⋃ a ∈ countableBasis α, a ×ˢ F a ⊆ s
⊢ s = ⋃ a ∈ countableBasis α, a ×ˢ F a

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- 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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (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 α, a ×ˢ F a) (y1, y2)
⊢ Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis α, a ×ˢ F 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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (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 α, y1 ∈ a ∧ a ⊆ u

Tactic:
IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis α) yu u_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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (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 : y1 ∈ a) (au : a ⊆ u),
    Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis α, a ×ˢ F a) (y1, y2)
⊢ Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis α, a ×ˢ F a) (y1, y2)

Tactic:
obtain ⟨a, ha, ya, au⟩ : ∃ a ∈ countableBasis α, y1 ∈ a ∧ a ⊆ u :=
          IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis α) yu u_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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (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 : y1 ∈ a
au : a ⊆ u
h₁ : ∃ (i : Set α), y1 ∈ i ∧ i ∈ countableBasis α ∧ y2 ∈ F i
⊢ Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis α, a ×ˢ F 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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (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 : y1 ∈ a
au : a ⊆ u
⊢ ∃ (i : Set α), y1 ∈ i ∧ i ∈ countableBasis α ∧ y2 ∈ F i

Tactic:
⟨a, ya, ha, v, v_open, yv, (Set.prod_mono_left au).trans huv⟩

Premises used: HasSubset.Subset.trans, Set.prod_mono_left, 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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (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 : y1 ∈ a
au : a ⊆ u
⊢ ∃ (i : Set α), y1 ∈ i ∧ i ∈ countableBasis α ∧ y2 ∈ F i

Tactic:
exact ⟨a, ya, ha, v, v_open, yv, (Set.prod_mono_left au).trans huv⟩
-- 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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (F a)
y1 : α
y2 : β
hy : Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis α, a ×ˢ F a) (y1, y2)
⊢ ∃ (i : Set α), y1 ∈ i ∧ i ∈ countableBasis α ∧ y2 ∈ F 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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (F a)
y1 : α
y2 : β
hy : ∃ (i : Set α), y1 ∈ i ∧ i ∈ countableBasis α ∧ y2 ∈ F i
h₂ : ∀ (a : Set α) (ya : y1 ∈ a) (b : Set β) (yb : y2 ∈ b) (hb : a ×ˢ b ⊆ s), (y1, y2) ∈ s
⊢ (y1, y2) ∈ s

Tactic:
rcases hy with ⟨a, ya, -, b, -, yb, hb⟩
-- 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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (F a)
y1 : α
y2 : β
a : Set α
ya : y1 ∈ a
b : Set β
yb : y2 ∈ b
hb : a ×ˢ b ⊆ s
⊢ (y1, y2) ∈ s

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

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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (F a)
y1 : α
y2 : β
a : Set α
ya : y1 ∈ a
b : Set β
yb : y2 ∈ b
hb : a ×ˢ b ⊆ s
⊢ (y1, y2) ∈ s

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

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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (F a)
⊢ s = ⋃ a ∈ countableBasis α, a ×ˢ F a

Tactic:
have : s = ⋃ a ∈ countableBasis α, a ×ˢ F 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 α, y1 ∈ a ∧ a ⊆ u :=
          IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis α) yu u_open
        simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop]
        exact ⟨a, ya, ha, v, v_open, yv, (Set.prod_mono_left au).trans huv⟩
      · rintro ⟨y1, y2⟩ hy
        simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop] at hy
        rcases hy with ⟨a, ya, -, b, -, yb, hb⟩
        exact hb (mem_prod.2 ⟨ya, yb⟩)
-- 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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (F a)
this : s = ⋃ a ∈ countableBasis α, a ×ˢ F a
inl : MeasurableSet (α := α × β) (⋃ a ∈ countableBasis α, a ×ˢ F 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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (F a)
this : s = ⋃ a ∈ countableBasis α, a ×ˢ F a
apply : ∀ (a : Set α) (ha : a ∈ countableBasis α), MeasurableSet (a ×ˢ F a)
⊢ MeasurableSet (α := α × β) (⋃ a ∈ countableBasis α, a ×ˢ F 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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (F a)
this : s = ⋃ a ∈ countableBasis α, a ×ˢ F a
a : Set α
ha : a ∈ countableBasis α
⊢ MeasurableSet (a ×ˢ F a)

Tactic:
(isOpen_of_mem_countableBasis ha).measurableSet.prod (A a).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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst_3] (F a)
this : s = ⋃ a ∈ countableBasis α, a ×ˢ F a
a : Set α
ha : a ∈ countableBasis α
⊢ MeasurableSet (a ×ˢ F a)

Tactic:
exact (isOpen_of_mem_countableBasis ha).measurableSet.prod (A a).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 : Set β
apply : ∀ x ∈ F a, ∃ t ⊆ F a, IsOpen[inst] t ∧ x ∈ t
⊢ IsOpen[inst] (F a)

Tactic:
apply isOpen_iff_forall_mem_open.2

Premises used: Iff.mpr, isOpen_iff_forall_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 : 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 : Set β
y : α
b : Set α
b_open : IsOpen[inst] b
yb : y ∈ b
hb : b ×ˢ a ⊆ s
⊢ ∃ t ⊆ F a, IsOpen[inst] t ∧ y ∈ t

Tactic:
⟨b, fun z zb ↦ ⟨b, b_open, zb, hb⟩, b_open, yb⟩

Premises used: 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 : 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 : Set β
y : α
b : Set α
b_open : IsOpen[inst] b
yb : y ∈ b
hb : b ×ˢ a ⊆ s
⊢ ∃ t ⊆ F a, IsOpen[inst] t ∧ y ∈ t

Tactic:
exact ⟨b, fun z zb ↦ ⟨b, b_open, zb, hb⟩, b_open, yb⟩
-- 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 : Set β), IsOpen[inst] (F a)

Tactic:
have A : ∀ a, IsOpen (F a) := by
      intro a
      apply isOpen_iff_forall_mem_open.2
      rintro y ⟨b, b_open, yb, hb⟩
      exact ⟨b, fun z zb ↦ ⟨b, b_open, zb, hb⟩, b_open, yb⟩
-- 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)
h₁ : s ⊆ ⋃ a ∈ countableBasis β, F a ×ˢ a
h₂ : ⋃ a ∈ countableBasis β, F a ×ˢ a ⊆ s
⊢ s = ⋃ a ∈ countableBasis β, F a ×ˢ a

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm