awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X × Y → Prop
x : X
y : Y
h : ∀ᶠ (x : X × Y) in 𝓝 x ×ˢ 𝓝 y, p x
⊢ ∀ᶠ (x' : X) in 𝓝 x, ∀ᶠ (y' : Y) in 𝓝 y, p (x', y')

Tactic:
h.curry

Premises used: Filter.Eventually.curry
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X × Y → Prop
x : X
y : Y
h : ∀ᶠ (x : X × Y) in 𝓝 x ×ˢ 𝓝 y, p x
⊢ ∀ᶠ (x' : X) in 𝓝 x, ∀ᶠ (y' : Y) in 𝓝 y, p (x', y')

Tactic:
exact h.curry

Premises used: Filter.Eventually.curry
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : X → Z
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt (Y := Y × Z) (fun (x : X) ↦ (f x, g x)) x

Tactic:
hf.prodMk_nhds hg

Premises used: ContinuousAt, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : X → Z
g : Y → W
p : X × Y
hf : ContinuousAt f p.1
hg : ContinuousAt g p.2
⊢ ContinuousAt (Prod.map f g) p

Tactic:
hf.fst''.prodMk hg.snd''

Premises used: ContinuousAt.fst'', Prod.map, ContinuousAt.snd'', ContinuousAt.prodMk
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : X → Z
g : Y → W
x : X
y : Y
hf : ContinuousAt f x
hg : ContinuousAt g y
⊢ ContinuousAt (Prod.map f g) (x, y)

Tactic:
hf.prodMap hg

Premises used: ContinuousAt.prodMap
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : Y × Z → W
g : X → Y
h : X → Z
x : X
hf : ContinuousAt f (g x, h x)
hg : ContinuousAt g x
hh : ContinuousAt h x
⊢ ContinuousAt.{u, u_1} (Y := W) (fun (x : X) ↦ f (g x, h x)) x

Tactic:
ContinuousAt.comp hf (hg.prodMk hh)

Premises used: ContinuousAt.comp, ContinuousAt.prodMk
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : Y × Z → W
g : X → Y
h : X → Z
x : X
y : Y × Z
hf : ContinuousAt f y
hg : ContinuousAt g x
hh : ContinuousAt h x
e : (g x, h x) = y
⊢ ContinuousAt f (g x, h x)

Tactic:
rw [← e] at hf
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : Y × Z → W
g : X → Y
h : X → Z
x : X
y : Y × Z
hf : ContinuousAt f y
hg : ContinuousAt g x
hh : ContinuousAt h x
e : (g x, h x) = y
hf₁ : ContinuousAt f (g x, h x)
⊢ ContinuousAt g x

Tactic:
rw [← e] at hf
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : Y × Z → W
g : X → Y
h : X → Z
x : X
y : Y × Z
hf : ContinuousAt f y
hg : ContinuousAt g x
hh : ContinuousAt h x
e : (g x, h x) = y
hf₁ : ContinuousAt f (g x, h x)
hg₁ : ContinuousAt g x
⊢ ContinuousAt h x

Tactic:
rw [← e] at hf
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : Y × Z → W
g : X → Y
h : X → Z
x : X
y : Y × Z
hf : ContinuousAt f y
hg : ContinuousAt g x
hh : ContinuousAt h x
e : (g x, h x) = y
hf₁ : ContinuousAt f (g x, h x)
hg₁ : ContinuousAt g x
hh₁ : ContinuousAt h x
⊢ (g x, h x) = y

Tactic:
rw [← e] at hf
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : Y × Z → W
g : X → Y
h : X → Z
x : X
y : Y × Z
hf : ContinuousAt f (g x, h x)
hg : ContinuousAt g x
hh : ContinuousAt h x
e : (g x, h x) = y
⊢ ContinuousAt.{u, u_1} (Y := W) (fun (x : X) ↦ f (g x, h x)) x

Tactic:
hf.comp₂ hg hh

Premises used: ContinuousAt.comp₂
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : Y × Z → W
g : X → Y
h : X → Z
x : X
y : Y × Z
hf : ContinuousAt f (g x, h x)
hg : ContinuousAt g x
hh : ContinuousAt h x
e : (g x, h x) = y
⊢ ContinuousAt.{u, u_1} (Y := W) (fun (x : X) ↦ f (g x, h x)) x

Tactic:
exact hf.comp₂ hg hh

Premises used: ContinuousAt.comp₂
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X × Y → Z
hf : Continuous[instTopologicalSpaceProd, inst_2] f
y : Y
⊢ Continuous[inst, inst_2] fun (x : X) ↦ f (x, y)

Tactic:
hf.comp (.prodMk_left _)

Premises used: Continuous.comp, Continuous.prodMk_left
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X × Y → Z
hf : Continuous[instTopologicalSpaceProd, inst_2] f
x : X
⊢ Continuous[inst_1, inst_2] fun (y : Y) ↦ f (x, y)

Tactic:
hf.comp (.prodMk_right _)

Premises used: Continuous.comp, Continuous.prodMk_right
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun (x1 : Set X) (x2 : Set Y) ↦ x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
simp_rw : SProd.sprod (β := Set Y) u (⋃ i ∈ t, i) = Prod.fst ⁻¹' u
simp_rw₁ : u ×ˢ ⋃₀ t = Prod.fst ⁻¹' u
simp_rw₂ : SProd.sprod (β := Set Y) u univ = Prod.fst ⁻¹' u
⊢ Eq (α := Set (X × Y)) (⋃ v ∈ t, u ×ˢ v) (Prod.fst ⁻¹' u)

Tactic:
simp_rw [← prod_iUnion, ← sUnion_eq_biUnion, ht, prod_univ]

Premises used: Set.prod_univ, Set.prod_iUnion, Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun (x1 : Set X) (x2 : Set Y) ↦ x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
this : Eq (α := Set (X × Y)) (⋃ v ∈ t, u ×ˢ v) (Prod.fst ⁻¹' u)
rw : TopologicalSpace.IsOpen (X := X × Y) (⋃ v ∈ t, u ×ˢ v)
⊢ TopologicalSpace.IsOpen (X := X × Y) (Prod.fst ⁻¹' u)

Tactic:
rw [← this]
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun (x1 : Set X) (x2 : Set Y) ↦ x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
this : Eq (α := Set (X × Y)) (⋃ v ∈ t, u ×ˢ v) (Prod.fst ⁻¹' u)
⊢ TopologicalSpace.IsOpen (X := X × Y) (⋃ v ∈ t, u ×ˢ v)

Tactic:
isOpen_iUnion fun v =>
                isOpen_iUnion fun hv => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩

Premises used: SProd.sprod, TopologicalSpace.GenerateOpen.basic, isOpen_iUnion, And.intro, Exists.intro, IsOpen, rfl
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun (x1 : Set X) (x2 : Set Y) ↦ x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
this : Eq (α := Set (X × Y)) (⋃ v ∈ t, u ×ˢ v) (Prod.fst ⁻¹' u)
⊢ TopologicalSpace.IsOpen (X := X × Y) (⋃ v ∈ t, u ×ˢ v)

Tactic:
exact
              isOpen_iUnion fun v =>
                isOpen_iUnion fun hv => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun (x1 : Set X) (x2 : Set Y) ↦ x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
simp_rw : SProd.sprod (α := Set X) (⋃ i ∈ s, i) v = Prod.snd ⁻¹' v
simp_rw₁ : ⋃₀ s ×ˢ v = Prod.snd ⁻¹' v
simp_rw₂ : SProd.sprod (α := Set X) univ v = Prod.snd ⁻¹' v
⊢ Eq (α := Set (X × Y)) (⋃ u ∈ s, u ×ˢ v) (Prod.snd ⁻¹' v)

Tactic:
simp_rw [← iUnion_prod_const, ← sUnion_eq_biUnion, hs, univ_prod]

Premises used: Set.univ_prod, Set.iUnion_prod_const, Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun (x1 : Set X) (x2 : Set Y) ↦ x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
this : Eq (α := Set (X × Y)) (⋃ u ∈ s, u ×ˢ v) (Prod.snd ⁻¹' v)
rw : TopologicalSpace.IsOpen (X := X × Y) (⋃ u ∈ s, u ×ˢ v)
⊢ TopologicalSpace.IsOpen (X := X × Y) (Prod.snd ⁻¹' v)

Tactic:
rw [← this]
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun (x1 : Set X) (x2 : Set Y) ↦ x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
this : Eq (α := Set (X × Y)) (⋃ u ∈ s, u ×ˢ v) (Prod.snd ⁻¹' v)
⊢ TopologicalSpace.IsOpen (X := X × Y) (⋃ u ∈ s, u ×ˢ v)

Tactic:
isOpen_iUnion fun u =>
                isOpen_iUnion fun hu => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩

Premises used: SProd.sprod, TopologicalSpace.GenerateOpen.basic, isOpen_iUnion, And.intro, Exists.intro, IsOpen, rfl
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun (x1 : Set X) (x2 : Set Y) ↦ x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
this : Eq (α := Set (X × Y)) (⋃ u ∈ s, u ×ˢ v) (Prod.snd ⁻¹' v)
⊢ TopologicalSpace.IsOpen (X := X × Y) (⋃ u ∈ s, u ×ˢ v)

Tactic:
exact
              isOpen_iUnion fun u =>
                isOpen_iUnion fun hu => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Eq (α := TopologicalSpace (X × Y)) instTopologicalSpaceProd
    (generateFrom {g : Set (X × Y) | ∃ (s : Set X) (t : Set Y), IsOpen[inst] s ∧ IsOpen[inst_1] t ∧ g = s ×ˢ t})

Tactic:
le_antisymm (le_generateFrom fun _ ⟨_, _, hs, ht, g_eq⟩ => g_eq.symm ▸ hs.prod ht)
    (le_inf
      (coinduced_le_iff_le_induced.mp fun U hU ↦
        .basic _ ⟨U, univ, hU, isOpen_univ, prod_univ.symm⟩)
      (coinduced_le_iff_le_induced.mp fun U hU ↦
        .basic _ ⟨univ, U, isOpen_univ, hU, univ_prod.symm⟩))

Premises used: Set.univ, TopologicalSpace.GenerateOpen.basic, Set.univ_prod, _private.0.prod_eq_generateFrom.match_1, Set.prod_univ, Eq.rec, le_inf, coinduced_le_iff_le_induced, Prod.fst, isOpen_univ, le_antisymm, Set.preimage, And.intro, Exists.intro, Iff.mp, IsOpen, Eq.symm, Prod.snd, le_generateFrom, IsOpen.prod
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set (X × Y)
simp_rw :
  (∀ (a : X) (b : Y), (a, b) ∈ s → s ∈ 𝓝 (a, b)) ↔
    ∀ (a : X) (b : Y),
      (a, b) ∈ s → ∃ (u : Set X) (v : Set Y), IsOpen[inst] u ∧ IsOpen[inst_1] v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s
simp_rw₁ :
  (∀ (a : X) (b : Y),
      (a, b) ∈ s → ∃ (u : Set X) (v : Set Y), IsOpen[inst] u ∧ a ∈ u ∧ IsOpen[inst_1] v ∧ b ∈ v ∧ u ×ˢ v ⊆ s) ↔
    ∀ (a : X) (b : Y),
      (a, b) ∈ s → ∃ (u : Set X) (v : Set Y), IsOpen[inst] u ∧ IsOpen[inst_1] v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s
⊢ (∀ x ∈ s, s ∈ 𝓝 x) ↔
    ∀ (a : X) (b : Y),
      (a, b) ∈ s → ∃ (u : Set X) (v : Set Y), IsOpen[inst] u ∧ IsOpen[inst_1] v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s

Tactic:
simp_rw [Prod.forall, mem_nhds_prod_iff', and_left_comm]

Premises used: mem_nhds_prod_iff', and_left_comm, Prod.forall
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
Y : Type v
W : Type u_1
inst : TopologicalSpace Y
inst_1 : TopologicalSpace W
X : Type u_5
Z : Type u_6
f : X → Y
g : Z → W
simp_rw :
  induced (f ∘ Prod.fst) inst ⊓ induced (g ∘ Prod.snd) inst_1 =
    induced (comp (β := Y × W) Prod.fst fun (p : X × Z) ↦ (f p.1, g p.2)) inst ⊓
      induced (comp (β := Y × W) Prod.snd fun (p : X × Z) ↦ (f p.1, g p.2)) inst_1
⊢ induced Prod.fst (induced f inst) ⊓ induced Prod.snd (induced g inst_1) =
    induced (fun (p : X × Z) ↦ (f p.1, g p.2)) (induced Prod.fst inst ⊓ induced Prod.snd inst_1)

Tactic:
simp_rw [induced_inf, induced_compose]

Premises used: induced_inf, induced_compose
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
Y : Type v
W : Type u_1
inst : TopologicalSpace Y
inst_1 : TopologicalSpace W
X : Type u_5
Z : Type u_6
f : X → Y
g : Z → W
⊢ induced (f ∘ Prod.fst) inst ⊓ induced (g ∘ Prod.snd) inst_1 =
    induced (comp (β := Y × W) Prod.fst fun (p : X × Z) ↦ (f p.1, g p.2)) inst ⊓
      induced (comp (β := Y × W) Prod.snd fun (p : X × Z) ↦ (f p.1, g p.2)) inst_1

Tactic:
rfl
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (X × X)
x : X
hx : s ∈ 𝓝 (x, x)
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ U ×ˢ U ⊆ s

Tactic:
simpa [nhds_prod_eq, (nhds_basis_opens x).prod_self.mem_iff, and_assoc, and_left_comm] using hx

Premises used: Filter.HasBasis.mem_iff, Filter.HasBasis.prod_self, and_left_comm, and_assoc, nhds_prod_eq, nhds_basis_opens
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X × Y
⊢ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x) = 𝓝 x.1

Tactic:
le_antisymm (continuousAt_fst.mono_left inf_le_left) fun s hs => ?_

Premises used: le_antisymm, Filter.Tendsto.mono_left, inf_le_left, continuousAt_fst
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X × Y
refine : ∀ (s : Set X) (hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x)), s ∈ 𝓝 x.1
⊢ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x) = 𝓝 x.1

Tactic:
refine le_antisymm (continuousAt_fst.mono_left inf_le_left) fun s hs => ?_

Premises used: le_antisymm, Filter.Tendsto.mono_left, inf_le_left, continuousAt_fst
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X × Y
s : Set X
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x)
rcases : ∀ (x : X) (y : Y) (hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {(x, y).2}] (x, y))), s ∈ 𝓝 (x, y).1
⊢ s ∈ 𝓝 x.1

Tactic:
rcases x with ⟨x, y⟩
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
x : X
y : Y
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {(x, y).2}] (x, y))
⊢ ∃ u ∈ 𝓝 x,
    ∃ v ∈ 𝓝 y,
      u ×ˢ v ⊆
        {x_1 : X × Y |
          Membership.mem (γ := Set (X × Y)) (Prod.snd ⁻¹' {(x, y).2}) x_1 →
            Membership.mem (γ := Set (X × Y)) (Prod.fst ⁻¹' s) x_1}

Tactic:
rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs

Premises used: mem_nhds_prod_iff, nhdsWithin, Filter.mem_inf_principal, Filter.mem_map
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
x : X
y : Y
hs :
  ∃ u ∈ 𝓝 x,
    ∃ v ∈ 𝓝 y,
      u ×ˢ v ⊆
        {x_1 : X × Y |
          Membership.mem (γ := Set (X × Y)) (Prod.snd ⁻¹' {(x, y).2}) x_1 →
            Membership.mem (γ := Set (X × Y)) (Prod.fst ⁻¹' s) x_1}
rcases :
  ∀ (u : Set X) (hu : u ∈ 𝓝 x) (v : Set Y) (hv : v ∈ 𝓝 y)
    (H :
      u ×ˢ v ⊆
        {x_1 : X × Y |
          Membership.mem (γ := Set (X × Y)) (Prod.snd ⁻¹' {(x, y).2}) x_1 →
            Membership.mem (γ := Set (X × Y)) (Prod.fst ⁻¹' s) x_1}),
    s ∈ 𝓝 (x, y).1
⊢ s ∈ 𝓝 (x, y).1

Tactic:
rcases hs with ⟨u, hu, v, hv, H⟩
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H :
  u ×ˢ v ⊆
    {x_1 : X × Y |
      Membership.mem (γ := Set (X × Y)) (Prod.snd ⁻¹' {(x, y).2}) x_1 →
        Membership.mem (γ := Set (X × Y)) (Prod.fst ⁻¹' s) x_1}
⊢ ∀ x ∈ u, ∀ y_1 ∈ v, y_1 = y → x ∈ s

Tactic:
simp only [prod_subset_iff, mem_singleton_iff, mem_setOf_eq, mem_preimage] at H

Premises used: Set.prod_subset_iff, Set.mem_setOf_eq, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H : ∀ x ∈ u, ∀ y_1 ∈ v, y_1 = y → x ∈ s
⊢ s ∈ 𝓝 (x, y).1

Tactic:
mem_of_superset hu fun z hz => H _ hz _ (mem_of_mem_nhds hv) rfl

Premises used: mem_of_mem_nhds, rfl, Filter.mem_of_superset
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H : ∀ x ∈ u, ∀ y_1 ∈ v, y_1 = y → x ∈ s
⊢ s ∈ 𝓝 (x, y).1

Tactic:
exact mem_of_superset hu fun z hz => H _ hz _ (mem_of_mem_nhds hv) rfl

Premises used: mem_of_mem_nhds, rfl, Filter.mem_of_superset
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X × Y
⊢ map Prod.fst (𝓝 x) = 𝓝 x.1

Tactic:
le_antisymm continuousAt_fst <| (map_fst_nhdsWithin x).symm.trans_le (map_mono inf_le_left)

Premises used: Filter.map_mono, map_fst_nhdsWithin, Eq.trans_le, le_antisymm, inf_le_left, Eq.symm, continuousAt_fst
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsOpenMap (X := X × Y) Prod.fst

Tactic:
isOpenMap_iff_nhds_le.2 fun x => (map_fst_nhds x).ge

Premises used: Iff.mpr, Eq.ge, isOpenMap_iff_nhds_le, map_fst_nhds
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X × Y
⊢ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x) = 𝓝 x.2

Tactic:
le_antisymm (continuousAt_snd.mono_left inf_le_left) fun s hs => ?_

Premises used: le_antisymm, Filter.Tendsto.mono_left, inf_le_left, continuousAt_snd
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X × Y
refine : ∀ (s : Set Y) (hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x)), s ∈ 𝓝 x.2
⊢ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x) = 𝓝 x.2

Tactic:
refine le_antisymm (continuousAt_snd.mono_left inf_le_left) fun s hs => ?_

Premises used: le_antisymm, Filter.Tendsto.mono_left, inf_le_left, continuousAt_snd
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X × Y
s : Set Y
hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x)
rcases : ∀ (x : X) (y : Y) (hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {(x, y).1}] (x, y))), s ∈ 𝓝 (x, y).2
⊢ s ∈ 𝓝 x.2

Tactic:
rcases x with ⟨x, y⟩
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {(x, y).1}] (x, y))
⊢ ∃ u ∈ 𝓝 x,
    ∃ v ∈ 𝓝 y,
      u ×ˢ v ⊆
        {x_1 : X × Y |
          Membership.mem (γ := Set (X × Y)) (Prod.fst ⁻¹' {(x, y).1}) x_1 →
            Membership.mem (γ := Set (X × Y)) (Prod.snd ⁻¹' s) x_1}

Tactic:
rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs

Premises used: mem_nhds_prod_iff, nhdsWithin, Filter.mem_inf_principal, Filter.mem_map
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs :
  ∃ u ∈ 𝓝 x,
    ∃ v ∈ 𝓝 y,
      u ×ˢ v ⊆
        {x_1 : X × Y |
          Membership.mem (γ := Set (X × Y)) (Prod.fst ⁻¹' {(x, y).1}) x_1 →
            Membership.mem (γ := Set (X × Y)) (Prod.snd ⁻¹' s) x_1}
rcases :
  ∀ (u : Set X) (hu : u ∈ 𝓝 x) (v : Set Y) (hv : v ∈ 𝓝 y)
    (H :
      u ×ˢ v ⊆
        {x_1 : X × Y |
          Membership.mem (γ := Set (X × Y)) (Prod.fst ⁻¹' {(x, y).1}) x_1 →
            Membership.mem (γ := Set (X × Y)) (Prod.snd ⁻¹' s) x_1}),
    s ∈ 𝓝 (x, y).2
⊢ s ∈ 𝓝 (x, y).2

Tactic:
rcases hs with ⟨u, hu, v, hv, H⟩
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H :
  u ×ˢ v ⊆
    {x_1 : X × Y |
      Membership.mem (γ := Set (X × Y)) (Prod.fst ⁻¹' {(x, y).1}) x_1 →
        Membership.mem (γ := Set (X × Y)) (Prod.snd ⁻¹' s) x_1}
⊢ ∀ x_1 ∈ u, ∀ y ∈ v, x_1 = x → y ∈ s

Tactic:
simp only [prod_subset_iff, mem_singleton_iff, mem_setOf_eq, mem_preimage] at H

Premises used: Set.prod_subset_iff, Set.mem_setOf_eq, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H : ∀ x_1 ∈ u, ∀ y ∈ v, x_1 = x → y ∈ s
⊢ s ∈ 𝓝 (x, y).2

Tactic:
mem_of_superset hv fun z hz => H _ (mem_of_mem_nhds hu) _ hz rfl

Premises used: mem_of_mem_nhds, rfl, Filter.mem_of_superset
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H : ∀ x_1 ∈ u, ∀ y ∈ v, x_1 = x → y ∈ s
⊢ s ∈ 𝓝 (x, y).2

Tactic:
exact mem_of_superset hv fun z hz => H _ (mem_of_mem_nhds hu) _ hz rfl

Premises used: mem_of_mem_nhds, rfl, Filter.mem_of_superset
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X × Y
⊢ map Prod.snd (𝓝 x) = 𝓝 x.2

Tactic:
le_antisymm continuousAt_snd <| (map_snd_nhdsWithin x).symm.trans_le (map_mono inf_le_left)

Premises used: Filter.map_mono, map_snd_nhdsWithin, Eq.trans_le, le_antisymm, inf_le_left, Eq.symm, continuousAt_snd
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsOpenMap (X := X × Y) Prod.snd

Tactic:
isOpenMap_iff_nhds_le.2 fun x => (map_snd_nhds x).ge

Premises used: Iff.mpr, Eq.ge, isOpenMap_iff_nhds_le, map_snd_nhds
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
inl : ∀ (h : s ×ˢ t = ∅), IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅
inr :
  ∀ (h : (s ×ˢ t).Nonempty),
    IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅

Tactic:
rcases (s ×ˢ t).eq_empty_or_nonempty with h | h

Premises used: SProd.sprod, Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
h : s ×ˢ t = ∅
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅

Tactic:
simp [h, prod_eq_empty_iff.1 h]

Premises used: Iff.mp, Set.prod_eq_empty_iff
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
⊢ s.Nonempty ∧ t.Nonempty

Tactic:
have st : s.Nonempty ∧ t.Nonempty := prod_nonempty_iff.1 h
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
inr : IsOpen[instTopologicalSpaceProd] (s ×ˢ t) → IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅
inr₁ : IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅ → IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅

Tactic:
constructor