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
ι : 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
⊢ Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis α, a ×ˢ F a) (y1, y2)
have h₁ : ∃ (i : Set α), y1 ∈ i ∧ i ∈ countableBasis α ∧ y2 ∈ F i
Tactic: simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop]
-- 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}
A : ∀ (a : Set α), IsOpen[inst_3] (F a)
y1 : α
y2 : β
hy : Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis α, a ×ˢ F a) (y1, y2)
⊢ (y1, y2) ∈ s
have hy₁ : ∃ (i : Set α), y1 ∈ i ∧ i ∈ countableBasis α ∧ y2 ∈ F i
Tactic: simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop] at hy
Cleared hypotheses: hy
-- 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 : ∃ (i : Set α), y1 ∈ i ∧ i ∈ countableBasis α ∧ y2 ∈ F i
⊢ (y1, y2) ∈ s
have h₂ : ∀ (a : Set α) (ya : y1 ∈ a) (b : Set β) (yb : y2 ∈ b) (hb : a ×ˢ b ⊆ s), (y1, y2) ∈ s
Tactic: rcases hy with ⟨a, ya, -, b, -, yb, hb⟩
Cleared hypotheses: hy
-- 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}
A : ∀ (a : Set α), IsOpen[inst_3] (F a)
⊢ MeasurableSet s
have this : 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⟩)
-- 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)
this : s = ⋃ a ∈ countableBasis α, a ×ˢ F a
⊢ MeasurableSet s
have inl : MeasurableSet (α := α × β) (⋃ a ∈ countableBasis α, a ×ˢ F a)
Tactic: rw [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
ι : 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
⊢ MeasurableSet (α := α × β) (⋃ a ∈ countableBasis α, a ×ˢ F a)
have apply : ∀ (a : Set α) (ha : a ∈ countableBasis α), MeasurableSet (a ×ˢ F a)
Tactic: apply MeasurableSet.biUnion (countable_countableBasis α) (fun a ha ↦ ?_)
-- 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] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
a : Set β
⊢ IsOpen[inst] (F a)
have apply : ∀ x ∈ F a, ∃ t ⊆ F a, IsOpen[inst] 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] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
⊢ MeasurableSet s
have A : ∀ (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⟩
-- 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] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
⊢ s = ⋃ a ∈ countableBasis β, F a ×ˢ a
have h₁ : s ⊆ ⋃ a ∈ countableBasis β, F a ×ˢ 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] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
h₁ : s ⊆ ⋃ a ∈ countableBasis β, F a ×ˢ a
⊢ s = ⋃ a ∈ countableBasis β, F a ×ˢ a
have h₂ : ⋃ a ∈ countableBasis β, F a ×ˢ 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] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
hy : (y1, y2) ∈ s
⊢ Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis β, F a ×ˢ 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 β, F a ×ˢ a) (y1, y2)
Tactic: rcases isOpen_prod_iff.1 hs y1 y2 hy with ⟨u, v, u_open, v_open, yu, yv, huv⟩
-- 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] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
hy : (y1, y2) ∈ s
u : Set α
v : Set β
u_open : IsOpen[inst] u
v_open : IsOpen[inst_3] v
yu : y1 ∈ u
yv : y2 ∈ v
huv : u ×ˢ v ⊆ s
⊢ Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis β, F a ×ˢ a) (y1, y2)
have h₁ : ∀ (a : Set β) (ha : a ∈ countableBasis β) (ya : y2 ∈ a) (au : a ⊆ v),
  Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis β, F a ×ˢ a) (y1, y2)
Tactic: obtain ⟨a, ha, ya, au⟩ : ∃ a ∈ countableBasis β, y2 ∈ a ∧ a ⊆ v :=
          IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis β) yv v_open
-- 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] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
hy : (y1, y2) ∈ s
u : Set α
v : Set β
u_open : IsOpen[inst] u
v_open : IsOpen[inst_3] v
yu : y1 ∈ u
yv : y2 ∈ v
huv : u ×ˢ v ⊆ s
a : Set β
ha : a ∈ countableBasis β
ya : y2 ∈ a
au : a ⊆ v
⊢ Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis β, F a ×ˢ a) (y1, y2)
have h₁ : ∃ (i : Set β), y1 ∈ F i ∧ i ∈ countableBasis β ∧ y2 ∈ i
Tactic: simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop]
-- 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] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
hy : Membership.mem (γ := Set (α × β)) (⋃ a ∈ countableBasis β, F a ×ˢ a) (y1, y2)
⊢ (y1, y2) ∈ s
have hy₁ : ∃ (i : Set β), y1 ∈ F i ∧ i ∈ countableBasis β ∧ y2 ∈ i
Tactic: simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop] at hy
Cleared hypotheses: hy
-- 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] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
y1 : α
y2 : β
hy : ∃ (i : Set β), y1 ∈ F i ∧ i ∈ countableBasis β ∧ y2 ∈ i
⊢ (y1, y2) ∈ s
have h₂ : ∀ (a : Set β) (b : Set α) (yb : y1 ∈ b) (hb : b ×ˢ a ⊆ s) (ya : y2 ∈ a), (y1, y2) ∈ s
Tactic: rcases hy with ⟨a, ⟨b, -, yb, hb⟩, -, ya⟩
Cleared hypotheses: hy
-- 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] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
⊢ MeasurableSet s
have this : s = ⋃ a ∈ countableBasis β, F a ×ˢ a
Tactic: have : s = ⋃ a ∈ countableBasis β, F a ×ˢ a := by
      apply Subset.antisymm
      · rintro ⟨y1, y2⟩ hy
        rcases isOpen_prod_iff.1 hs y1 y2 hy with ⟨u, v, u_open, v_open, yu, yv, huv⟩
        obtain ⟨a, ha, ya, au⟩ : ∃ a ∈ countableBasis β, y2 ∈ a ∧ a ⊆ v :=
          IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis β) yv v_open
        simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop]
        exact ⟨a, ⟨u, u_open, yu, (Set.prod_mono_right au).trans huv⟩, ha, ya⟩
      · rintro ⟨y1, y2⟩ hy
        simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop] at hy
        rcases hy with ⟨a, ⟨b, -, yb, hb⟩, -, ya⟩
        exact hb (mem_prod.2 ⟨yb, ya⟩)
-- 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] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
this : s = ⋃ a ∈ countableBasis β, F a ×ˢ a
⊢ MeasurableSet s
have inr : MeasurableSet (α := α × β) (⋃ a ∈ countableBasis β, F a ×ˢ a)
Tactic: rw [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
ι : Sort y
s_1 t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun (a : Set β) ↦ {y : α | ∃ (b : Set α), IsOpen[inst] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst] (F a)
this : s = ⋃ a ∈ countableBasis β, F a ×ˢ a
⊢ MeasurableSet (α := α × β) (⋃ a ∈ countableBasis β, F a ×ˢ a)
have apply : ∀ (a : Set β) (ha : a ∈ countableBasis β), MeasurableSet (F a ×ˢ a)
Tactic: apply MeasurableSet.biUnion (countable_countableBasis β) (fun a ha ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α' : Type u_6
inst : TopologicalSpace α'
inst_1 : MeasurableSpace α'
μ : Measure α'
s s' : Set α'
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s') : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier (s ∩ s')) : ℝ≥0∞) (0 : ℝ≥0∞)
have h₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier (s ∩ s')) : ℝ≥0∞) (⊥ : ℝ≥0∞)
Tactic: apply bot_unique
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α' : Type u_6
inst : TopologicalSpace α'
inst_1 : MeasurableSpace α'
μ : Measure α'
s s' : Set α'
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s') : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier (s ∩ s')) : ℝ≥0∞) (⊥ : ℝ≥0∞)
have calc : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α') → ℝ≥0∞) (frontier s) : ℝ≥0∞)
    ((μ : (a : Set α') → ℝ≥0∞) (frontier s') : ℝ≥0∞) =
  0
Tactic: calc μ (frontier (s ∩ s'))
  _ ≤ μ (frontier s ∪ frontier s') := measure_mono <| (frontier_inter_subset _ _).trans (by grind)
  _ ≤ μ (frontier s) + μ (frontier s') := measure_union_le _ _
  _ = 0 := by simp [h, h']
-- 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 δ
α' : Type u_6
inst_13 : TopologicalSpace α'
inst_14 : MeasurableSpace α'
inst_15 : T0Space α
x y : α
⊢ (∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s) → x = y
have contrapose! : x ≠ y → ∃ (s : Set α), MeasurableSet s ∧ x ∈ s ∧ y ∉ s
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
⊢ Measurable (s.piecewise (β := fun (a : α) ↦ γ) f g)
have refine : ∀ (t : Set γ) (ht : IsOpen[inst_3] t), MeasurableSet (s.piecewise (β := fun (a : α) ↦ γ) f g ⁻¹' t)
Tactic: refine measurable_of_isOpen fun t ht => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
⊢ MeasurableSet (s.piecewise (β := fun (a : α) ↦ γ) f g ⁻¹' t)
have rw : MeasurableSet (f ⁻¹' t ∩ s ∪ g ⁻¹' t \ s)
Tactic: rw [piecewise_preimage, Set.ite]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
⊢ MeasurableSet (f ⁻¹' t ∩ s ∪ g ⁻¹' t \ s)
have h₁ : MeasurableSet (f ⁻¹' t ∩ s)
Tactic: apply MeasurableSet.union