awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → MeasurableSet (f ⁻¹' s)
hf₁ : ∀ (s : Set γ), IsOpen[inst] s → MeasurableSet (f ⁻¹' s)
⊢ Measurable f

Tactic:
apply measurable_of_isOpen

Premises used: measurable_of_isOpen
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen[inst] s
hf₁ : MeasurableSet (f ⁻¹' sᶜ)
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
rw [← MeasurableSet.compl_iff, ← preimage_compl]

Premises used: MeasurableSet.compl_iff, Set.preimage_compl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen[inst] s
hf₁ : IsClosed[inst] sᶜ
⊢ MeasurableSet (f ⁻¹' sᶜ)

Tactic:
apply hf
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs hf₁ : IsOpen[inst] s
⊢ IsClosed[inst] sᶜ

Tactic:
rw [isClosed_compl_iff]

Premises used: isClosed_compl_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen[inst] s
⊢ IsOpen[inst] s

Tactic:
hs
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen[inst] s
⊢ IsOpen[inst] s

Tactic:
exact hs
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
hf₁ : ∀ (s : Set γ), IsClosed[inst] s → MeasurableSet (f ⁻¹' s)
⊢ Measurable f

Tactic:
apply measurable_of_isClosed

Premises used: measurable_of_isClosed
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst] s
hf₁ : ∀ (h1 : s = ∅), MeasurableSet (f ⁻¹' s)
hf₂ : ∀ (h1 : s.Nonempty), MeasurableSet (f ⁻¹' s)
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
rcases eq_empty_or_nonempty s with h1 | h1

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst] s
h1 : s = ∅
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
simp [h1]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst] s
h1 : s.Nonempty
pos : ∀ (h2 : s = univ), MeasurableSet (f ⁻¹' s)
neg : ∀ (h2 : ¬s = univ), MeasurableSet (f ⁻¹' s)
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
by_cases h2 : s = univ

Premises used: Set.univ
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst] s
h1 : s.Nonempty
h2 : s = univ
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
simp [h2]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst] s
h1 : s.Nonempty
h2 : ¬s = univ
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
hf s hs h1 h2
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst] s
h1 : s.Nonempty
h2 : ¬s = univ
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
exact hf s hs h1 h2
-- 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 δ
a : α
rw :
  IsMeasurablyGenerated.{u_1} (α := α)
    (⨅ (x : Subtype (Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ IsOpen[inst] s})), 𝓟 (↑x : Set α))
⊢ (𝓝 a).IsMeasurablyGenerated

Tactic:
rw [nhds, iInf_subtype']

Premises used: nhds, iInf_subtype'
-- 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 δ
a : α
⊢ IsMeasurablyGenerated.{u_1} (α := α)
    (⨅ (x : Subtype (Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ IsOpen[inst] s})), 𝓟 (↑x : Set α))

Tactic:
@Filter.iInf_isMeasurablyGenerated α _ _ _ fun i => ?_

Premises used: Filter.iInf_isMeasurablyGenerated
-- 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 δ
a : α
refine :
  ∀ (i : Subtype (Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ IsOpen[inst] s})),
    (𝓟 (↑i : Set α)).IsMeasurablyGenerated
⊢ IsMeasurablyGenerated.{u_1} (α := α)
    (⨅ (x : Subtype (Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ IsOpen[inst] s})), 𝓟 (↑x : Set α))

Tactic:
refine @Filter.iInf_isMeasurablyGenerated α _ _ _ fun i => ?_

Premises used: Filter.iInf_isMeasurablyGenerated
-- 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 δ
a : α
i : Subtype (Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ IsOpen[inst] s})
⊢ (𝓟 (↑i : Set α)).IsMeasurablyGenerated

Tactic:
i.2.2.measurableSet.principal_isMeasurablyGenerated

Premises used: IsOpen.measurableSet, And.right, MeasurableSet.principal_isMeasurablyGenerated, Subtype.property
-- 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 δ
a : α
i : Subtype (Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ IsOpen[inst] s})
⊢ (𝓟 (↑i : Set α)).IsMeasurablyGenerated

Tactic:
exact i.2.2.measurableSet.principal_isMeasurablyGenerated

Premises used: IsOpen.measurableSet, And.right, MeasurableSet.principal_isMeasurablyGenerated, Subtype.property
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
hs : MeasurableSet s
a : α
⊢ (𝓝[s] a).IsMeasurablyGenerated

Tactic:
haveI := hs.principal_isMeasurablyGenerated
  Filter.inf_isMeasurablyGenerated _ _

Premises used: Filter.inf_isMeasurablyGenerated, nhdsWithin, nhds, Filter.principal
-- 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 δ
inst_13 : T0Space α
rw : ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y
⊢ MeasurableSpace.SeparatesPoints α

Tactic:
rw [separatesPoints_iff]

Premises used: MeasurableSpace.separatesPoints_iff
-- 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 δ
inst_13 : T0Space α
x y : α
hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
h : Inseparable x y
⊢ x = y

Tactic:
apply Inseparable.eq

Premises used: Inseparable.eq
-- 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 δ
inst_13 : T0Space α
x y : α
hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
h : ∀ (s : Set α), IsOpen[inst] s → (x ∈ s ↔ y ∈ s)
⊢ Inseparable x y

Tactic:
rw [inseparable_iff_forall_isOpen]

Premises used: inseparable_iff_forall_isOpen
-- 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 δ
inst_13 : T0Space α
x y : α
hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
⊢ ∀ (s : Set α), IsOpen[inst] s → (x ∈ s ↔ y ∈ s)

Tactic:
fun s hs => hxy _ hs.measurableSet

Premises used: IsOpen.measurableSet
-- 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 δ
inst_13 : T0Space α
x y : α
hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
⊢ ∀ (s : Set α), IsOpen[inst] s → (x ∈ s ↔ y ∈ s)

Tactic:
exact fun s hs => hxy _ hs.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_6
inst : TopologicalSpace α
inst_1 : T0Space α
inst_2 : Countable α
⊢ borel α = ⊤

Tactic:
top_unique fun s _ ↦ ?_

Premises used: top_unique
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_6
inst : TopologicalSpace α
inst_1 : T0Space α
inst_2 : Countable α
refine : ∀ (s : Set α), MeasurableSet s → MeasurableSet s
⊢ borel α = ⊤

Tactic:
refine top_unique fun s _ ↦ ?_

Premises used: top_unique
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_6
inst : TopologicalSpace α
inst_1 : T0Space α
inst_2 : Countable α
s : Set α
h : MeasurableSet s
⊢ let this := borel α;
  BorelSpace α

Tactic:
borelize α
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_6
inst : TopologicalSpace α
inst_1 : T0Space α
inst_2 : Countable α
s : Set α
h : MeasurableSet s
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
⊢ MeasurableSet s

Tactic:
.of_discrete

Premises used: MeasurableSet.of_discrete
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_6
inst : TopologicalSpace α
inst_1 : T0Space α
inst_2 : Countable α
s : Set α
h : MeasurableSet s
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
⊢ MeasurableSet s

Tactic:
exact .of_discrete
-- 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 δ
inst_13 : T1Space α
⊢ MeasurableSingletonClass α

Tactic:
⟨fun _ => isClosed_singleton.measurableSet⟩

Premises used: IsClosed.measurableSet, MeasurableSingletonClass.mk, isClosed_singleton
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι_1 : 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
X : ι → Type u_7
inst_13 : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst_14 : (i : ι) → MeasurableSpace (X i)
inst_15 : ∀ (i : ι), SecondCountableTopology.{u_7} (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
borel_le : LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))
⊢ OpensMeasurableSpace ((i : ι) → X i)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι_1 : 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
X : ι → Type u_7
inst_13 : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst_14 : (i : ι) → MeasurableSpace (X i)
inst_15 : ∀ (i : ι), SecondCountableTopology.{u_7} (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
⊢ Eq (α := TopologicalSpace ((i : ι) → X i)) (topologicalSpace (Y := X))
    (TopologicalSpace.generateFrom
      {t : Set ((i : ι) → X i) |
        ∃ (s : (a : ι) → Set (X a)) (i : Finset ι),
          (∀ a ∈ i, Membership.mem (γ := Set (Set (X a))) (countableBasis (X a)) (s a)) ∧
            t = (↑i : Set ι).pi (α := X) s})

Tactic:
simp +instances only [funext fun a => @eq_generateFrom_countableBasis (X a) _ _,
      pi_generateFrom_eq]

Premises used: funext, pi_generateFrom_eq, TopologicalSpace.eq_generateFrom_countableBasis
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι_1 : 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
X : ι → Type u_7
inst_13 : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst_14 : (i : ι) → MeasurableSpace (X i)
inst_15 : ∀ (i : ι), SecondCountableTopology.{u_7} (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
⊢ Eq (α := TopologicalSpace ((i : ι) → X i)) (topologicalSpace (Y := X))
    (TopologicalSpace.generateFrom
      {t : Set ((i : ι) → X i) |
        ∃ (s : (a : ι) → Set (X a)) (i : Finset ι),
          (∀ a ∈ i, Membership.mem (γ := Set (Set (X a))) (countableBasis (X a)) (s a)) ∧
            t = (↑i : Set ι).pi (α := X) s})

Tactic:
have : Pi.topologicalSpace = .generateFrom { t | ∃ (s : ∀ a, Set (X a)) (i : Finset ι),
      (∀ a ∈ i, s a ∈ countableBasis (X a)) ∧ t = pi (↑i) s } := by
    simp +instances only [funext fun a => @eq_generateFrom_countableBasis (X a) _ _,
      pi_generateFrom_eq]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι_1 : 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
X : ι → Type u_7
inst_13 : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst_14 : (i : ι) → MeasurableSpace (X i)
inst_15 : ∀ (i : ι), SecondCountableTopology.{u_7} (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
this :
  Eq (α := TopologicalSpace ((i : ι) → X i)) (topologicalSpace (Y := X))
    (TopologicalSpace.generateFrom
      {t : Set ((i : ι) → X i) |
        ∃ (s : (a : ι) → Set (X a)) (i : Finset ι),
          (∀ a ∈ i, Membership.mem (γ := Set (Set (X a))) (countableBasis (X a)) (s a)) ∧
            t = (↑i : Set ι).pi (α := X) s})
borel_le :
  LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.generateFrom
      {t : Set ((i : ι) → X i) |
        ∃ (s : (a : ι) → Set (X a)) (i : Finset ι),
          (∀ a ∈ i, Membership.mem (γ := Set (Set (X a))) (countableBasis (X a)) (s a)) ∧
            t = (↑i : Set ι).pi (α := X) s})
    (MeasurableSpace.pi (X := X))
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))

Tactic:
rw [borel_eq_generateFrom_of_subbasis this]

Premises used: borel_eq_generateFrom_of_subbasis
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι_1 : 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
X : ι → Type u_7
inst_13 : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst_14 : (i : ι) → MeasurableSpace (X i)
inst_15 : ∀ (i : ι), SecondCountableTopology.{u_7} (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
this :
  Eq (α := TopologicalSpace ((i : ι) → X i)) (topologicalSpace (Y := X))
    (TopologicalSpace.generateFrom
      {t : Set ((i : ι) → X i) |
        ∃ (s : (a : ι) → Set (X a)) (i : Finset ι),
          (∀ a ∈ i, Membership.mem (γ := Set (Set (X a))) (countableBasis (X a)) (s a)) ∧
            t = (↑i : Set ι).pi (α := X) s})
borel_le :
  ∀ (t : Set ((i : ι) → X i)),
    Membership.mem (γ := Set (Set ((i : ι) → X i)))
        {t : Set ((i : ι) → X i) |
          ∃ (s : (a : ι) → Set (X a)) (i : Finset ι),
            (∀ a ∈ i, Membership.mem (γ := Set (Set (X a))) (countableBasis (X a)) (s a)) ∧
              t = (↑i : Set ι).pi (α := X) s}
        t →
      MeasurableSet t
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.generateFrom
      {t : Set ((i : ι) → X i) |
        ∃ (s : (a : ι) → Set (X a)) (i : Finset ι),
          (∀ a ∈ i, Membership.mem (γ := Set (Set (X a))) (countableBasis (X a)) (s a)) ∧
            t = (↑i : Set ι).pi (α := X) s})
    (MeasurableSpace.pi (X := X))

Tactic:
apply generateFrom_le

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι_1 : 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 δ
ι : Type u_6
X : ι → Type u_7
inst_13 : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst_14 : (i : ι) → MeasurableSpace (X i)
inst_15 : ∀ (i : ι), SecondCountableTopology.{u_7} (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
this :
  Eq (α := TopologicalSpace ((i : ι) → X i)) (topologicalSpace (Y := X))
    (TopologicalSpace.generateFrom
      {t : Set ((i : ι) → X i) |
        ∃ (s : (a : ι) → Set (X a)) (i : Finset ι),
          (∀ a ∈ i, Membership.mem (γ := Set (Set (X a))) (countableBasis (X a)) (s a)) ∧
            t = (↑i : Set ι).pi (α := X) s})
s : (a : ι) → Set (X a)
i : Finset ι
hi : ∀ a ∈ i, Membership.mem (γ := Set (Set (X a))) (countableBasis (X a)) (s a)
⊢ MeasurableSet ((↑i : Set ι).pi (α := X) s)

Tactic:
MeasurableSet.pi i.countable_toSet fun a ha => IsOpen.measurableSet ?_

Premises used: IsOpen.measurableSet, Finset.countable_toSet, MeasurableSet.pi