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
ι_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)
borel_le : ∀ (a : ι) (ha : a ∈ (↑i : Set ι)), IsOpen[t' a] (s a)
⊢ MeasurableSet ((↑i : Set ι).pi (α := X) s)

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

Premises used: IsOpen.measurableSet, Finset.countable_toSet, MeasurableSet.pi
-- 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)
a : ι
ha : a ∈ (↑i : Set ι)
borel_le : IsOpen[TopologicalSpace.generateFrom (countableBasis (X a))] (s a)
⊢ IsOpen[t' a] (s a)

Tactic:
rw [eq_generateFrom_countableBasis (X a)]

Premises used: 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_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)
a : ι
ha : a ∈ (↑i : Set ι)
⊢ IsOpen[TopologicalSpace.generateFrom (countableBasis (X a))] (s a)

Tactic:
.basic _ (hi a ha)

Premises used: TopologicalSpace.GenerateOpen.basic, IsOpen
-- 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)
a : ι
ha : a ∈ (↑i : Set ι)
⊢ IsOpen[TopologicalSpace.generateFrom (countableBasis (X a))] (s a)

Tactic:
exact .basic _ (hi a ha)
-- 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 : Subsingleton ι
inst_14 : (i : ι) → TopologicalSpace (X i)
inst_15 : (i : ι) → MeasurableSpace (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
inl :
  ∀ (h : IsEmpty ι), LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))
inr :
  ∀ (h : Nonempty ι), LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))

Tactic:
obtain h | h := isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- 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 : Subsingleton ι
inst_14 : (i : ι) → TopologicalSpace (X i)
inst_15 : (i : ι) → MeasurableSpace (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
h : IsEmpty ι
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))

Tactic:
fun s _ ↦ Subsingleton.set_cases .empty .univ s

Premises used: Subsingleton.set_cases
-- 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 : Subsingleton ι
inst_14 : (i : ι) → TopologicalSpace (X i)
inst_15 : (i : ι) → MeasurableSpace (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
h : IsEmpty ι
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))

Tactic:
exact fun s _ ↦ Subsingleton.set_cases .empty .univ s
-- 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 : Subsingleton ι
inst_14 : (i : ι) → TopologicalSpace (X i)
inst_15 : (i : ι) → MeasurableSpace (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
h : Nonempty ι
inr :
  ∀ (this : Unique ι),
    LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))

Tactic:
have := Classical.choice (nonempty_unique ι)
-- 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 : Subsingleton ι
inst_14 : (i : ι) → TopologicalSpace (X i)
inst_15 : (i : ι) → MeasurableSpace (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
h : Nonempty ι
this : Unique ι
inr :
  LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.generateFrom {s : Set ((i : ι) → X i) | IsOpen[topologicalSpace] s})
    (MeasurableSpace.comap (β := X default) (fun (b : (a : ι) → X a) ↦ b default) (inst_15 default))
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))

Tactic:
rw [borel, MeasurableSpace.pi, ciSup_unique]

Premises used: ciSup_unique, borel, MeasurableSpace.pi
-- 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 : Subsingleton ι
inst_14 : (i : ι) → TopologicalSpace (X i)
inst_15 : (i : ι) → MeasurableSpace (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
h : Nonempty ι
this : Unique ι
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.generateFrom {s : Set ((i : ι) → X i) | IsOpen[topologicalSpace] s})
    (MeasurableSpace.comap (β := X default) (fun (b : (a : ι) → X a) ↦ b default) (inst_15 default))

Tactic:
MeasurableSpace.generateFrom_le fun s hs ↦ MeasurableSpace.measurableSet_comap.2 ?_

Premises used: Iff.mpr, MeasurableSpace.measurableSet_comap, 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 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 : Subsingleton ι
inst_14 : (i : ι) → TopologicalSpace (X i)
inst_15 : (i : ι) → MeasurableSpace (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
h : Nonempty ι
this : Unique ι
inr :
  ∀ (s : Set ((i : ι) → X i))
    (hs : Membership.mem (γ := Set (Set ((i : ι) → X i))) {s : Set ((i : ι) → X i) | IsOpen[topologicalSpace] s} s),
    ∃ (s' : Set (X default)), MeasurableSet s' ∧ (fun (b : (a : ι) → X a) ↦ b default) ⁻¹' s' = s
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.generateFrom {s : Set ((i : ι) → X i) | IsOpen[topologicalSpace] s})
    (MeasurableSpace.comap (β := X default) (fun (b : (a : ι) → X a) ↦ b default) (inst_15 default))

Tactic:
refine MeasurableSpace.generateFrom_le fun s hs ↦ MeasurableSpace.measurableSet_comap.2 ?_

Premises used: Iff.mpr, MeasurableSpace.measurableSet_comap, 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 : Subsingleton ι
inst_14 : (i : ι) → TopologicalSpace (X i)
inst_15 : (i : ι) → MeasurableSpace (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
h : Nonempty ι
this : Unique ι
s : Set ((i : ι) → X i)
hs : Membership.mem (γ := Set (Set ((i : ι) → X i))) {s : Set ((i : ι) → X i) | IsOpen[topologicalSpace] s} s
⊢ ∃ (x : Set (X default)), IsOpen[inst_14 default] x ∧ (fun (f : (i : ι) → X i) ↦ f default) ⁻¹' x = s

Tactic:
simp +instances only [Pi.topologicalSpace, ciInf_unique, isOpen_induced_eq, Set.mem_image,
      Set.mem_setOf_eq] at hs

Premises used: isOpen_induced_eq, Pi.topologicalSpace, Set.mem_image, Set.mem_setOf_eq, ciInf_unique
-- 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 : Subsingleton ι
inst_14 : (i : ι) → TopologicalSpace (X i)
inst_15 : (i : ι) → MeasurableSpace (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
h : Nonempty ι
this : Unique ι
s : Set ((i : ι) → X i)
hs : ∃ (x : Set (X default)), IsOpen[inst_14 default] x ∧ (fun (f : (i : ι) → X i) ↦ f default) ⁻¹' x = s
inr :
  ∀ (t : Set (X default)) (ht : IsOpen[inst_14 default] t),
    ∃ (s' : Set (X default)),
      MeasurableSet s' ∧
        Eq (α := Set ((i : ι) → X i)) ((fun (b : (a : ι) → X a) ↦ b default) ⁻¹' s')
          ((fun (f : (i : ι) → X i) ↦ f default) ⁻¹' t)
⊢ ∃ (s' : Set (X default)), MeasurableSet s' ∧ (fun (b : (a : ι) → X a) ↦ b default) ⁻¹' s' = s

Tactic:
obtain ⟨t, ht, rfl⟩ := hs

Premises used: rfl
-- 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_1 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 : Subsingleton ι
inst_14 : (i : ι) → TopologicalSpace (X i)
inst_15 : (i : ι) → MeasurableSpace (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
h : Nonempty ι
this : Unique ι
t : Set (X default)
ht : IsOpen[inst_14 default] t
⊢ ∃ (s' : Set (X default)),
    MeasurableSet s' ∧
      Eq (α := Set ((i : ι) → X i)) ((fun (b : (a : ι) → X a) ↦ b default) ⁻¹' s')
        ((fun (f : (i : ι) → X i) ↦ f default) ⁻¹' t)

Tactic:
⟨t, ht.measurableSet, rfl⟩

Premises used: IsOpen.measurableSet, And.intro, Exists.intro, rfl
-- 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_1 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 : Subsingleton ι
inst_14 : (i : ι) → TopologicalSpace (X i)
inst_15 : (i : ι) → MeasurableSpace (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
h : Nonempty ι
this : Unique ι
t : Set (X default)
ht : IsOpen[inst_14 default] t
⊢ ∃ (s' : Set (X default)),
    MeasurableSet s' ∧
      Eq (α := Set ((i : ι) → X i)) ((fun (b : (a : ι) → X a) ↦ b default) ⁻¹' s')
        ((fun (f : (i : ι) → X i) ↦ f default) ⁻¹' t)

Tactic:
exact ⟨t, ht.measurableSet, rfl⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α_1
inst : TopologicalSpace α_1
inst_1 : MeasurableSpace α_1
inst_2 : OpensMeasurableSpace α_1
inst_3 : TopologicalSpace β_1
inst_4 : MeasurableSpace β_1
inst_5 : OpensMeasurableSpace β_1
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
α : Type u_6
β : Type u_7
inst_13 : TopologicalSpace α
inst_14 : TopologicalSpace β
inst_15 : SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α_1
inst : TopologicalSpace α_1
inst_1 : MeasurableSpace α_1
inst_2 : OpensMeasurableSpace α_1
inst_3 : TopologicalSpace β_1
inst_4 : MeasurableSpace β_1
inst_5 : OpensMeasurableSpace β_1
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
α : Type u_6
β : Type u_7
inst_13 : TopologicalSpace α
inst_14 : TopologicalSpace β
inst_15 : SecondCountableTopology β
⊢ SecondCountableTopology β

Tactic:
infer_instance
-- 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 δ
h : SecondCountableTopologyEither α β
apply : ∀ (s : Set (α × β)) (hs : IsOpen[instTopologicalSpaceProd] s), MeasurableSet s
⊢ OpensMeasurableSpace (α × β)

Tactic:
apply opensMeasurableSpace_iff_forall_measurableSet.2 (fun s hs ↦ ?_)

Premises used: Iff.mpr, opensMeasurableSpace_iff_forall_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_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
inl : ∀ (hα : SecondCountableTopology α), MeasurableSet s
inr : ∀ (hβ : SecondCountableTopology β), MeasurableSet s
⊢ MeasurableSet s

Tactic:
rcases h.out with hα | hβ

Premises used: SecondCountableTopologyEither.out
-- 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 α
apply : ∀ x ∈ F a, ∃ t ⊆ F a, IsOpen[inst_3] t ∧ x ∈ t
⊢ IsOpen[inst_3] (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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
a : Set α
y : β
b : Set β
b_open : IsOpen[inst_3] b
yb : y ∈ b
hb : a ×ˢ b ⊆ s
⊢ ∃ t ⊆ F a, IsOpen[inst_3] 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_3] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
a : Set α
y : β
b : Set β
b_open : IsOpen[inst_3] b
yb : y ∈ b
hb : a ×ˢ b ⊆ s
⊢ ∃ t ⊆ F a, IsOpen[inst_3] t ∧ y ∈ t

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