awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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})
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))
have 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))
Tactic: rw [borel_eq_generateFrom_of_subbasis this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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})
⊢ 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))
have 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
Tactic: apply generateFrom_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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)
have borel_le : ∀ (a : ι) (ha : a ∈ (↑i : Set ι)), IsOpen[t' a] (s a)
Tactic: refine MeasurableSet.pi i.countable_toSet fun a ha => IsOpen.measurableSet ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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[t' a] (s a)
have borel_le : IsOpen[TopologicalSpace.generateFrom (countableBasis (X a))] (s a)
Tactic: rw [eq_generateFrom_countableBasis (X a)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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)
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))
have inl : ∀ (h : IsEmpty ι), LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))
Tactic: obtain h | h := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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))
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))
have inr : ∀ (h : Nonempty ι), LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))
Tactic: obtain h | h := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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 ι
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))
have inr : ∀ (this : Unique ι), LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))
Tactic: have := Classical.choice (nonempty_unique ι)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))
have 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))
Tactic: rw [borel, MeasurableSpace.pi, ciSup_unique]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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))
have 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
Tactic: refine MeasurableSpace.generateFrom_le fun s hs ↦ MeasurableSpace.measurableSet_comap.2 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (hypothesis)
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
⊢ ∃ (s' : Set (X default)), MeasurableSet s' ∧ (fun (b : (a : ι) → X a) ↦ b default) ⁻¹' s' = s
have hs₁ : ∃ (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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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
⊢ ∃ (s' : Set (X default)), MeasurableSet s' ∧ (fun (b : (a : ι) → X a) ↦ b default) ⁻¹' s' = s
have 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)
Tactic: obtain ⟨t, ht, rfl⟩ := hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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 α β
⊢ OpensMeasurableSpace (α × β)
have apply : ∀ (s : Set (α × β)) (hs : IsOpen[instTopologicalSpaceProd] s), MeasurableSet s
Tactic: apply opensMeasurableSpace_iff_forall_measurableSet.2 (fun s hs ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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
⊢ MeasurableSet s
have inl : ∀ (hα : SecondCountableTopology α), MeasurableSet s
Tactic: rcases h.out with hα | hβ
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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
⊢ MeasurableSet s
have inr : ∀ (hβ : SecondCountableTopology β), MeasurableSet s
Tactic: rcases h.out with hα | hβ
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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)
have apply : ∀ x ∈ F a, ∃ t ⊆ F a, IsOpen[inst_3] t ∧ x ∈ t
Tactic: apply isOpen_iff_forall_mem_open.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (hypothesis)
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}
⊢ MeasurableSet s
have A : ∀ (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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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
have h₁ : s ⊆ ⋃ a ∈ countableBasis α, a ×ˢ F a
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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
⊢ s = ⋃ a ∈ countableBasis α, a ×ˢ F a
have h₂ : ⋃ a ∈ countableBasis α, a ×ˢ F a ⊆ s
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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
⊢ Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis α, a ×ˢ F a) (y1, y2)
have 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)
Tactic: rcases isOpen_prod_iff.1 hs y1 y2 hy with ⟨u, v, u_open, v_open, yu, yv, huv⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
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
⊢ Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis α, a ×ˢ F a) (y1, y2)
have h₁ : ∀ (a : Set α) (ha : a ∈ countableBasis α) (ya : y1 ∈ a) (au : a ⊆ u),
  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