awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set (↑(↑(U i) : Set X) : Type u_2)
hVx : V ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) x hi)
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ (↑(U i) : Set X) ↓∩ s)
e : (↑V : Type u_2) ≃ₜ (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) '' V) : Type u_2) :=
  (Equiv.Set.image (Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X))) V ⋯).toHomeomorphOfIsInducing ⋯
⊢ IsConstructible (X := (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2))
    ((Subtype.val '' V) ↓∩ s)
have h : (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2) =
    (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) '' V) : Type u_2) →
  Eq (α := Set (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2)) ((Subtype.val '' V) ↓∩ s)
    (preimage (β := (↑V : Type u_2)) (⇑e.symm : (a : (↑(Subtype.val '' V) : Type u_2)) → (↑V : Type u_2))
      (V ↓∩ (↑(U i) : Set X) ↓∩ s))
Tactic: convert! hV'.preimage_of_isOpenEmbedding e.symm.isOpenEmbedding
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set (↑(↑(U i) : Set X) : Type u_2)
hVx : V ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) x hi)
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ (↑(U i) : Set X) ↓∩ s)
e : (↑V : Type u_2) ≃ₜ (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) '' V) : Type u_2) :=
  (Equiv.Set.image (Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X))) V ⋯).toHomeomorphOfIsInducing ⋯
e_1 :
  (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2) =
    (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) '' V) : Type u_2)
⊢ Eq (α := Set (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2)) ((Subtype.val '' V) ↓∩ s)
    (preimage (β := (↑V : Type u_2)) (⇑e.symm : (a : (↑(Subtype.val '' V) : Type u_2)) → (↑V : Type u_2))
      (V ↓∩ (↑(U i) : Set X) ↓∩ s))
have h : ∀ (x : { x : X // x ∈ (U i).carrier }) (hx : x ∈ V),
  Membership.mem (γ := Set (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2))
      ((Subtype.val '' V) ↓∩ s)
      (Subtype.mk (p := fun (x : X) ↦ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) (↑x : X) sorry) ↔
    Membership.mem (γ := Set (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2))
      (preimage (β := (↑V : Type u_2)) (⇑e.symm : (a : (↑(Subtype.val '' V) : Type u_2)) → (↑V : Type u_2))
        (V ↓∩ (↑(U i) : Set X) ↓∩ s))
      (Subtype.mk (p := fun (x : X) ↦ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) (↑x : X) sorry)
Tactic: ext ⟨_, x, hx, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (s ∩ (↑(U i) : Set X))
i : ι
⊢ IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
have rw : IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2))
  (Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) ⁻¹' (s ∩ (↑(U i) : Set X)))
Tactic: rw [← Subtype.preimage_coe_inter_self]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
⊢ Prop
have haveI : (this : TopologicalSpace X) → Prop
Tactic: haveI := ta1
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
this : TopologicalSpace X
⊢ Prop
have haveI : (this : TopologicalSpace Y) → Prop
Tactic: haveI := tb1
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
⊢ Prop
have haveI : (this : TopologicalSpace X) → Prop
Tactic: haveI := ta1 ⊓ ta2
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
this : TopologicalSpace X
⊢ Prop
have haveI : (this : TopologicalSpace Y) → Prop
Tactic: haveI := tb1 ⊓ tb2
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
⊢ Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
have ha : Continuous[ta1 ⊓ ta2, ta1] id
Tactic: have ha := @continuous_inf_dom_left _ _ id ta1 ta2 ta1 (@continuous_id _ (id _))
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
ha : Continuous[ta1 ⊓ ta2, ta1] id
⊢ Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
have hb : Continuous[tb1 ⊓ tb2, tb1] id
Tactic: have hb := @continuous_inf_dom_left _ _ id tb1 tb2 tb1 (@continuous_id _ (id _))
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
ha : Continuous[ta1 ⊓ ta2, ta1] id
hb : Continuous[tb1 ⊓ tb2, tb1] id
⊢ Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
have h_continuous_id : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)
Tactic: have h_continuous_id := @Continuous.prodMap _ _ _ _ ta1 tb1 (ta1 ⊓ ta2) (tb1 ⊓ tb2) _ _ ha hb
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
⊢ Prop
have haveI : (this : TopologicalSpace X) → Prop
Tactic: haveI := ta2
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
this : TopologicalSpace X
⊢ Prop
have haveI : (this : TopologicalSpace Y) → Prop
Tactic: haveI := tb2
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
⊢ Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
have ha : Continuous[ta1 ⊓ ta2, ta2] id
Tactic: have ha := @continuous_inf_dom_right _ _ id ta1 ta2 ta2 (@continuous_id _ (id _))
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
ha : Continuous[ta1 ⊓ ta2, ta2] id
⊢ Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
have hb : Continuous[tb1 ⊓ tb2, tb2] id
Tactic: have hb := @continuous_inf_dom_right _ _ id tb1 tb2 tb2 (@continuous_id _ (id _))
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
ha : Continuous[ta1 ⊓ ta2, ta2] id
hb : Continuous[tb1 ⊓ tb2, tb2] id
⊢ Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
have h_continuous_id : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)
Tactic: have h_continuous_id := @Continuous.prodMap _ _ _ _ ta2 tb2 (ta1 ⊓ ta2) (tb1 ⊓ tb2) _ _ ha hb
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
⊢ Prop
have haveI : (this : TopologicalSpace X) → Prop
Tactic: haveI := sInf tas
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
this : TopologicalSpace X
⊢ Prop
have haveI : (this : TopologicalSpace Y) → Prop
Tactic: haveI := sInf tbs
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
⊢ Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
have hX₁ : Continuous[sInf tas, tX] id
Tactic: have hX := continuous_sInf_dom hX continuous_id
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX_1 : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
hX : Continuous[sInf tas, tX] id
⊢ Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
have hY₁ : Continuous[sInf tbs, tY] id
Tactic: have hY := continuous_sInf_dom hY continuous_id
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX_1 : tX ∈ tas
hY_1 : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
hX : Continuous[sInf tas, tX] id
hY : Continuous[sInf tbs, tY] id
⊢ Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
have h_continuous_id : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)
Tactic: have h_continuous_id := @Continuous.prodMap _ _ _ _ tX tY (sInf tas) (sInf tbs) _ _ hX hY
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed[instTopologicalSpaceProd] s
⊢ IsClosed[instTopologicalSpaceProd] (Prod.swap '' s)
have rw : IsClosed[instTopologicalSpaceProd] (Prod.swap ⁻¹' s)
Tactic: rw [image_swap_eq_preimage_swap]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
⊢ 𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y
have rw : 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
Tactic: rw [prod_eq_inf, instTopologicalSpaceProd, nhds_inf (t₁ := TopologicalSpace.induced Prod.fst _)
    (t₂ := TopologicalSpace.induced Prod.snd _), nhds_induced, nhds_induced]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
rw : 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
rw₁ : 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
⊢ 𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y
have rw₂ : 𝓝 (x, y) ⊓ 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
Tactic: rw [prod_eq_inf, instTopologicalSpaceProd, nhds_inf (t₁ := TopologicalSpace.induced Prod.fst _)
    (t₂ := TopologicalSpace.induced Prod.snd _), nhds_induced, nhds_induced]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
rw : 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
rw₁ : 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
rw₂ : 𝓝 (x, y) ⊓ 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
⊢ 𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y
have rw₃ : comap Prod.fst (𝓝 (x, y).1) ⊓ 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
Tactic: rw [prod_eq_inf, instTopologicalSpaceProd, nhds_inf (t₁ := TopologicalSpace.induced Prod.fst _)
    (t₂ := TopologicalSpace.induced Prod.snd _), nhds_induced, nhds_induced]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
rw : 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
rw₁ : 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
rw₂ : 𝓝 (x, y) ⊓ 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
rw₃ : comap Prod.fst (𝓝 (x, y).1) ⊓ 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
⊢ 𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y
have rw₄ : comap Prod.fst (𝓝 (x, y).1) ⊓ comap Prod.snd (𝓝 (x, y).2) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
Tactic: rw [prod_eq_inf, instTopologicalSpaceProd, nhds_inf (t₁ := TopologicalSpace.induced Prod.fst _)
    (t₂ := TopologicalSpace.induced Prod.snd _), nhds_induced, nhds_induced]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
inst_6 : Preorder X
inst_7 : Preorder Y
x : X × Y
hx₁ : (𝓝[<] x.1).NeBot
hx₂ : (𝓝[<] x.2).NeBot
⊢ (𝓝[<] x).NeBot
have refine : 𝓝[<] x.1 ×ˢ 𝓝[<] x.2 ≤ 𝓝[<] x
Tactic: refine (hx₁.prod hx₂).mono ?_
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
inst_6 : Preorder X
inst_7 : Preorder Y
x : X × Y
hx₁ : (𝓝[<] x.1).NeBot
hx₂ : (𝓝[<] x.2).NeBot
⊢ 𝓝[<] x.1 ×ˢ 𝓝[<] x.2 ≤ 𝓝[<] x
have rw : 𝓝[Iio x.1 ×ˢ Iio x.2] (x.1, x.2) ≤ 𝓝[<] x
Tactic: rw [← nhdsWithin_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
inst_6 : Preorder X
inst_7 : Preorder Y
x : X × Y
hx₁ : (𝓝[>] x.1).NeBot
hx₂ : (𝓝[>] x.2).NeBot
⊢ (𝓝[>] x).NeBot
have refine : 𝓝[>] x.1 ×ˢ 𝓝[>] x.2 ≤ 𝓝[>] x
Tactic: refine (hx₁.prod hx₂).mono ?_
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
inst_6 : Preorder X
inst_7 : Preorder Y
x : X × Y
hx₁ : (𝓝[>] x.1).NeBot
hx₂ : (𝓝[>] x.2).NeBot
⊢ 𝓝[>] x.1 ×ˢ 𝓝[>] x.2 ≤ 𝓝[>] x
have rw : 𝓝[Ioi x.1 ×ˢ Ioi x.2] (x.1, x.2) ≤ 𝓝[>] x
Tactic: rw [← nhdsWithin_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
⊢ s ∈ 𝓝 (x, y) ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s
have rw : s ∈ 𝓝 x ×ˢ 𝓝 y ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s
Tactic: rw [nhds_prod_eq, mem_prod_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
rw : s ∈ 𝓝 x ×ˢ 𝓝 y ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s
⊢ s ∈ 𝓝 (x, y) ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s
have rw₁ : (∃ t₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 y, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s
Tactic: rw [nhds_prod_eq, mem_prod_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
tx : Set X
ty : Set Y
⊢ s ∈ 𝓝[tx ×ˢ ty] (x, y) ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s
have rw : s ∈ 𝓝[tx] x ×ˢ 𝓝[ty] y ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s
Tactic: rw [nhdsWithin_prod_eq, mem_prod_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
tx : Set X
ty : Set Y
rw : s ∈ 𝓝[tx] x ×ˢ 𝓝[ty] y ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s
⊢ s ∈ 𝓝[tx ×ˢ ty] (x, y) ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s
have rw₁ : (∃ t₁ ∈ 𝓝[tx] x, ∃ t₂ ∈ 𝓝[ty] y, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s
Tactic: rw [nhdsWithin_prod_eq, mem_prod_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
ιX : Type u_5
ιY : Type u_6
px : ιX → Prop
py : ιY → Prop
sx : ιX → Set X
sy : ιY → Set Y
x : X
y : Y
hx : (𝓝 x).HasBasis px sx
hy : (𝓝 y).HasBasis py sy
⊢ (𝓝 (x, y)).HasBasis (fun (i : ιX × ιY) ↦ px i.1 ∧ py i.2) fun (i : ιX × ιY) ↦ sx i.1 ×ˢ sy i.2
have rw : (𝓝 x ×ˢ 𝓝 y).HasBasis (fun (i : ιX × ιY) ↦ px i.1 ∧ py i.2) fun (i : ιX × ιY) ↦ sx i.1 ×ˢ sy i.2
Tactic: rw [nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
Y : Type v
Z : Type u_2
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
X : Type u_5
seq : X → Y × Z
f : Filter X
p : Y × Z
⊢ Tendsto seq f (𝓝 p) ↔ Tendsto (fun (n : X) ↦ (seq n).1) f (𝓝 p.1) ∧ Tendsto (fun (n : X) ↦ (seq n).2) f (𝓝 p.2)
have rw : Tendsto seq f (𝓝 p.1 ×ˢ 𝓝 p.2) ↔
  Tendsto (fun (n : X) ↦ (seq n).1) f (𝓝 p.1) ∧ Tendsto (fun (n : X) ↦ (seq n).2) f (𝓝 p.2)
Tactic: rw [nhds_prod_eq, Filter.tendsto_prod_iff']
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
Y : Type v
Z : Type u_2
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
X : Type u_5
seq : X → Y × Z
f : Filter X
p : Y × Z
rw :
  Tendsto seq f (𝓝 p.1 ×ˢ 𝓝 p.2) ↔
    Tendsto (fun (n : X) ↦ (seq n).1) f (𝓝 p.1) ∧ Tendsto (fun (n : X) ↦ (seq n).2) f (𝓝 p.2)
⊢ Tendsto seq f (𝓝 p) ↔ Tendsto (fun (n : X) ↦ (seq n).1) f (𝓝 p.1) ∧ Tendsto (fun (n : X) ↦ (seq n).2) f (𝓝 p.2)
have rw₁ : Tendsto (fun (n : X) ↦ (seq n).1) f (𝓝 p.1) ∧ Tendsto (fun (n : X) ↦ (seq n).2) f (𝓝 p.2) ↔
  Tendsto (fun (n : X) ↦ (seq n).1) f (𝓝 p.1) ∧ Tendsto (fun (n : X) ↦ (seq n).2) f (𝓝 p.2)
Tactic: rw [nhds_prod_eq, Filter.tendsto_prod_iff']
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
inst_6 : DiscreteTopology X
inst_7 : DiscreteTopology Y
x : X × Y
a : X
b : Y
⊢ 𝓝 (a, b) = pure (a, b)
have rw : 𝓝 a ×ˢ 𝓝 b = pure (a, b)
Tactic: rw [nhds_prod_eq, nhds_discrete X, nhds_discrete Y, prod_pure_pure]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
inst_6 : DiscreteTopology X
inst_7 : DiscreteTopology Y
x : X × Y
a : X
b : Y
rw : 𝓝 a ×ˢ 𝓝 b = pure (a, b)
⊢ 𝓝 (a, b) = pure (a, b)
have rw₁ : SProd.sprod (α := Filter X) (pure a) (𝓝 b) = pure (a, b)
Tactic: rw [nhds_prod_eq, nhds_discrete X, nhds_discrete Y, prod_pure_pure]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
inst_6 : DiscreteTopology X
inst_7 : DiscreteTopology Y
x : X × Y
a : X
b : Y
rw : 𝓝 a ×ˢ 𝓝 b = pure (a, b)
rw₁ : SProd.sprod (α := Filter X) (pure a) (𝓝 b) = pure (a, b)
⊢ 𝓝 (a, b) = pure (a, b)
have rw₂ : SProd.sprod (α := Filter X) (β := Filter Y) (pure a) (pure b) = pure (a, b)
Tactic: rw [nhds_prod_eq, nhds_discrete X, nhds_discrete Y, prod_pure_pure]