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 : Y → Prop
y : Y
h : ∀ᶠ (x : Y) in 𝓝 y, p x
x : X
⊢ ∀ᶠ (x : X × Y) in 𝓝 (x, y), p x.2

Tactic:
continuousAt_snd h

Premises used: Set.Mem, Filter.Eventually, setOf, Set.preimage, continuousAt_snd
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
px : X → Prop
x : X
hx : ∀ᶠ (x : X) in 𝓝 x, px x
py : Y → Prop
y : Y
hy : ∀ᶠ (y : Y) in 𝓝 y, py y
⊢ ∀ᶠ (p : X × Y) in 𝓝 (x, y), px p.1 ∧ py p.2

Tactic:
(hx.prod_inl_nhds y).and (hy.prod_inr_nhds x)

Premises used: Filter.Eventually.prod_inl_nhds, Filter.Eventually.and, Filter.Eventually.prod_inr_nhds
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] Prod.swap

Tactic:
continuous_snd.prodMk continuous_fst

Premises used: continuous_snd, continuous_fst, Prod.swap, Continuous.prodMk
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed[instTopologicalSpaceProd] s
rw : IsClosed[instTopologicalSpaceProd] (Prod.swap ⁻¹' s)
⊢ IsClosed[instTopologicalSpaceProd] (Prod.swap '' s)

Tactic:
rw [image_swap_eq_preimage_swap]

Premises used: Set.image_swap_eq_preimage_swap
-- Module: Mathlib.Topology.Constructions.SumProd
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)

Tactic:
hs.preimage continuous_swap

Premises used: continuous_swap, IsClosed.preimage
-- Module: Mathlib.Topology.Constructions.SumProd
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)

Tactic:
exact hs.preimage continuous_swap

Premises used: continuous_swap, IsClosed.preimage
-- 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
x : X
h : Continuous[instTopologicalSpaceProd, inst_2] (uncurry f)
⊢ Continuous[inst_1, inst_2] (f x)

Tactic:
h.comp (.prodMk_right _)

Premises used: Continuous.comp, Continuous.prodMk_right
-- 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
y : Y
h : Continuous[instTopologicalSpaceProd, inst_2] (uncurry f)
⊢ Continuous[inst, inst_2] fun (a : X) ↦ f a y

Tactic:
h.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
g : X × Y → Z
x : X
h : Continuous[instTopologicalSpaceProd, inst_2] g
⊢ Continuous[inst_1, inst_2] (Function.curry g x)

Tactic:
Continuous.uncurry_left x h

Premises used: Continuous.uncurry_left
-- 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
hs : IsOpen[inst] s
ht : IsOpen[inst_1] t
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t)

Tactic:
(hs.preimage continuous_fst).inter (ht.preimage continuous_snd)

Premises used: Set.Mem, setOf, Set.prod, continuous_snd, continuous_fst, Set.preimage, IsOpen.inter, IsOpen.preimage
-- Module: Mathlib.Topology.Constructions.SumProd
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)
rw₄ rw₅ : comap Prod.fst (𝓝 (x, y).1) ⊓ comap Prod.snd (𝓝 (x, y).2) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
⊢ 𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y

Tactic:
rw [prod_eq_inf, instTopologicalSpaceProd, nhds_inf (t₁ := TopologicalSpace.induced Prod.fst _)
    (t₂ := TopologicalSpace.induced Prod.snd _), nhds_induced, nhds_induced]

Premises used: instTopologicalSpaceProd, Filter.prod_eq_inf, nhds_inf, nhds_induced
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
s : Set X
t : Set Y
⊢ 𝓝[s ×ˢ t] (x, y) = 𝓝[s] x ×ˢ 𝓝[t] y

Tactic:
simp only [nhdsWithin, nhds_prod_eq, ← prod_inf_prod, prod_principal_principal]

Premises used: Filter.prod_inf_prod, nhdsWithin, Filter.prod_principal_principal, nhds_prod_eq
-- Module: Mathlib.Topology.Constructions.SumProd
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

Tactic:
(hx₁.prod hx₂).mono ?_

Premises used: Filter.NeBot.mono, Filter.NeBot.prod
-- Module: Mathlib.Topology.Constructions.SumProd
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
refine : 𝓝[<] x.1 ×ˢ 𝓝[<] x.2 ≤ 𝓝[<] x
⊢ (𝓝[<] x).NeBot

Tactic:
refine (hx₁.prod hx₂).mono ?_

Premises used: Filter.NeBot.mono, Filter.NeBot.prod
-- Module: Mathlib.Topology.Constructions.SumProd
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
rw : 𝓝[Iio x.1 ×ˢ Iio x.2] (x.1, x.2) ≤ 𝓝[<] x
⊢ 𝓝[<] x.1 ×ˢ 𝓝[<] x.2 ≤ 𝓝[<] x

Tactic:
rw [← nhdsWithin_prod_eq]

Premises used: nhdsWithin_prod_eq
-- Module: Mathlib.Topology.Constructions.SumProd
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
⊢ 𝓝[Iio x.1 ×ˢ Iio x.2] (x.1, x.2) ≤ 𝓝[<] x

Tactic:
nhdsWithin_mono _ fun _ ⟨h₁, h₂⟩ ↦ Prod.lt_iff.2 <| .inl ⟨h₁, h₂.le⟩

Premises used: Iff.mpr, Set.Mem, setOf, Membership.mem, LT.lt.le, Prod.lt_iff, And.intro, _private.0.Prod.instNeBotNhdsWithinIio.match_1, Or.inl, Set.Iio, nhdsWithin_mono
-- Module: Mathlib.Topology.Constructions.SumProd
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
⊢ 𝓝[Iio x.1 ×ˢ Iio x.2] (x.1, x.2) ≤ 𝓝[<] x

Tactic:
exact nhdsWithin_mono _ fun _ ⟨h₁, h₂⟩ ↦ Prod.lt_iff.2 <| .inl ⟨h₁, h₂.le⟩
-- Module: Mathlib.Topology.Constructions.SumProd
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

Tactic:
(hx₁.prod hx₂).mono ?_

Premises used: Filter.NeBot.mono, Filter.NeBot.prod
-- Module: Mathlib.Topology.Constructions.SumProd
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
refine : 𝓝[>] x.1 ×ˢ 𝓝[>] x.2 ≤ 𝓝[>] x
⊢ (𝓝[>] x).NeBot

Tactic:
refine (hx₁.prod hx₂).mono ?_

Premises used: Filter.NeBot.mono, Filter.NeBot.prod
-- Module: Mathlib.Topology.Constructions.SumProd
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
rw : 𝓝[Ioi x.1 ×ˢ Ioi x.2] (x.1, x.2) ≤ 𝓝[>] x
⊢ 𝓝[>] x.1 ×ˢ 𝓝[>] x.2 ≤ 𝓝[>] x

Tactic:
rw [← nhdsWithin_prod_eq]

Premises used: nhdsWithin_prod_eq
-- Module: Mathlib.Topology.Constructions.SumProd
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
⊢ 𝓝[Ioi x.1 ×ˢ Ioi x.2] (x.1, x.2) ≤ 𝓝[>] x

Tactic:
nhdsWithin_mono _ fun _ ⟨h₁, h₂⟩ ↦ Prod.lt_iff.2 <| .inl ⟨h₁, h₂.le⟩

Premises used: Iff.mpr, Set.Ioi, Set.Mem, _private.0.Prod.instNeBotNhdsWithinIoi.match_1, setOf, Membership.mem, LT.lt.le, Prod.lt_iff, And.intro, Or.inl, nhdsWithin_mono
-- Module: Mathlib.Topology.Constructions.SumProd
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
⊢ 𝓝[Ioi x.1 ×ˢ Ioi x.2] (x.1, x.2) ≤ 𝓝[>] x

Tactic:
exact nhdsWithin_mono _ fun _ ⟨h₁, h₂⟩ ↦ Prod.lt_iff.2 <| .inl ⟨h₁, h₂.le⟩
-- Module: Mathlib.Topology.Constructions.SumProd
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
rw₁ rw₂ : (∃ t₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 y, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s
⊢ s ∈ 𝓝 (x, y) ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s

Tactic:
rw [nhds_prod_eq, mem_prod_iff]

Premises used: nhds_prod_eq, Filter.mem_prod_iff
-- Module: Mathlib.Topology.Constructions.SumProd
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
rw₁ rw₂ : (∃ t₁ ∈ 𝓝[tx] x, ∃ t₂ ∈ 𝓝[ty] y, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s
⊢ s ∈ 𝓝[tx ×ˢ ty] (x, y) ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s

Tactic:
rw [nhdsWithin_prod_eq, mem_prod_iff]

Premises used: nhdsWithin_prod_eq, Filter.mem_prod_iff
-- Module: Mathlib.Topology.Constructions.SumProd
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
rw : (𝓝 x ×ˢ 𝓝 y).HasBasis (fun (i : ιX × ιY) ↦ px i.1 ∧ py i.2) fun (i : ιX × ιY) ↦ sx i.1 ×ˢ sy i.2
⊢ (𝓝 (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]

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.Constructions.SumProd
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

Tactic:
hx.prod hy

Premises used: Filter.HasBasis.prod
-- Module: Mathlib.Topology.Constructions.SumProd
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

Tactic:
exact hx.prod hy

Premises used: Filter.HasBasis.prod
-- Module: Mathlib.Topology.Constructions.SumProd
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
p : X × Y
hx : (𝓝 p.1).HasBasis pX sx
hy : (𝓝 p.2).HasBasis pY sy
⊢ (𝓝 p).HasBasis (fun (i : ιX × ιY) ↦ pX i.1 ∧ pY i.2) fun (i : ιX × ιY) ↦ sx i.1 ×ˢ sy i.2

Tactic:
hx.prod_nhds hy

Premises used: Filter.HasBasis.prod_nhds
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
⊢ (∃ (i : Prod.{u, v} (Set X) (Set Y)),
      ((x ∈ i.1 ∧ IsOpen[inst] i.1) ∧ y ∈ i.2 ∧ IsOpen[inst_1] i.2) ∧ i.1 ×ˢ i.2 ⊆ s) ↔
    ∃ (u : Set X) (v : Set Y), IsOpen[inst] u ∧ x ∈ u ∧ IsOpen[inst_1] v ∧ y ∈ v ∧ u ×ˢ v ⊆ s

Tactic:
simp only [Prod.exists, and_comm, and_assoc, and_left_comm]

Premises used: and_left_comm, and_comm, and_assoc, Prod.exists
-- Module: Mathlib.Topology.Constructions.SumProd
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)
rw₁ 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)
⊢ Tendsto seq f (𝓝 p) ↔ 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']

Premises used: Filter.tendsto_prod_iff', nhds_prod_eq
-- Module: Mathlib.Topology.Constructions.SumProd
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)
rw₂ : SProd.sprod (α := Filter X) (β := Filter Y) (pure a) (pure b) = pure (a, b)
rw₃ rw₄ : Eq (α := Filter (X × Y)) (pure (a, b)) (pure (a, b))
⊢ 𝓝 (a, b) = pure (a, b)

Tactic:
rw [nhds_prod_eq, nhds_discrete X, nhds_discrete Y, prod_pure_pure]

Premises used: Filter.prod_pure_pure, nhds_prod_eq, nhds_discrete
-- 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
x : X
y : Y
rw : s ×ˢ t ∈ 𝓝 x ×ˢ 𝓝 y ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y
rw₁ rw₂ : s ∈ 𝓝 x ∧ t ∈ 𝓝 y ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y
⊢ s ×ˢ t ∈ 𝓝 (x, y) ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y

Tactic:
rw [nhds_prod_eq, prod_mem_prod_iff]

Premises used: Filter.prod_mem_prod_iff, nhds_prod_eq
-- 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
x : X
y : Y
hx : s ∈ 𝓝 x
hy : t ∈ 𝓝 y
⊢ s ×ˢ t ∈ 𝓝 (x, y)

Tactic:
prod_mem_nhds_iff.2 ⟨hx, hy⟩

Premises used: Iff.mpr, prod_mem_nhds_iff, And.intro
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
inst : TopologicalSpace X
simp : ∀ (a b : X), Disjoint (𝓝 a) (𝓝 b) → {p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (a, b)
⊢ IsOpen[instTopologicalSpaceProd] {p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2)}

Tactic:
simp only [isOpen_iff_mem_nhds, Prod.forall, mem_setOf_eq]

Premises used: Set.mem_setOf_eq, Prod.forall, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
h : Disjoint (𝓝 x) (𝓝 y)
obtain :
  ∀ (U : Set X) (hU : x ∈ U ∧ IsOpen[inst] U) (V : Set X) (hV : y ∈ V ∧ IsOpen[inst] V) (hd : Disjoint U V),
    {p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)
⊢ {p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)

Tactic:
obtain ⟨U, hU, V, hV, hd⟩ := ((nhds_basis_opens x).disjoint_iff (nhds_basis_opens y)).mp h

Premises used: Filter.HasBasis.disjoint_iff, Iff.mp, nhds_basis_opens
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
h : Disjoint (𝓝 x) (𝓝 y)
U : Set X
hU : x ∈ U ∧ IsOpen[inst] U
V : Set X
hV : y ∈ V ∧ IsOpen[inst] V
hd : Disjoint U V
⊢ {p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)

Tactic:
mem_nhds_prod_iff'.mpr ⟨U, V, hU.2, hU.1, hV.2, hV.1, fun ⟨x', y'⟩ ⟨hx', hy'⟩ =>
    disjoint_of_disjoint_of_mem hd (hU.2.mem_nhds hx') (hV.2.mem_nhds hy')⟩

Premises used: Iff.mpr, _private.0.isOpen_setOf_disjoint_nhds_nhds.match_2, mem_nhds_prod_iff', _private.0.isOpen_setOf_disjoint_nhds_nhds.match_3, setOf, Disjoint, Membership.mem, nhds, Prod.mk, Filter.disjoint_of_disjoint_of_mem, Prod.fst, And.right, And.left, And.intro, IsOpen.mem_nhds, Exists.intro, Prod.snd
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
h : Disjoint (𝓝 x) (𝓝 y)
U : Set X
hU : x ∈ U ∧ IsOpen[inst] U
V : Set X
hV : y ∈ V ∧ IsOpen[inst] V
hd : Disjoint U V
⊢ {p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)

Tactic:
exact mem_nhds_prod_iff'.mpr ⟨U, V, hU.2, hU.1, hV.2, hV.1, fun ⟨x', y'⟩ ⟨hx', hy'⟩ =>
    disjoint_of_disjoint_of_mem hd (hU.2.mem_nhds hx') (hV.2.mem_nhds hy')⟩

Premises used: Iff.mpr, _private.0.isOpen_setOf_disjoint_nhds_nhds.match_2, mem_nhds_prod_iff', _private.0.isOpen_setOf_disjoint_nhds_nhds.match_3, Membership.mem, Prod.mk, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
q : Y → Prop
x : X
y : Y
hx : ∀ᶠ (x : X) in 𝓝 x, p x
hy : ∀ᶠ (y : Y) in 𝓝 y, q y
⊢ ∀ᶠ (z : X × Y) in 𝓝 (x, y), p z.1 ∧ q z.2

Tactic:
prod_mem_nhds hx hy

Premises used: prod_mem_nhds, Set.Mem, Filter.Eventually, setOf, Set.prod
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ =ᶠ[𝓝 x] f₂
hg : g₁ =ᶠ[𝓝 y] g₂
rw : Prod.map f₁ g₁ =ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂
⊢ Prod.map f₁ g₁ =ᶠ[𝓝 (x, y)] Prod.map f₂ g₂

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ =ᶠ[𝓝 x] f₂
hg : g₁ =ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ =ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂

Tactic:
hf.prodMap hg

Premises used: Filter.EventuallyEq.prodMap
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ =ᶠ[𝓝 x] f₂
hg : g₁ =ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ =ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂

Tactic:
exact hf.prodMap hg

Premises used: Filter.EventuallyEq.prodMap
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
inst_2 : LE α
inst_3 : LE β
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ ≤ᶠ[𝓝 x] f₂
hg : g₁ ≤ᶠ[𝓝 y] g₂
rw : Prod.map f₁ g₁ ≤ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂
⊢ Prod.map f₁ g₁ ≤ᶠ[𝓝 (x, y)] Prod.map f₂ g₂

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
inst_2 : LE α
inst_3 : LE β
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ ≤ᶠ[𝓝 x] f₂
hg : g₁ ≤ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ ≤ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂

Tactic:
hf.prodMap hg

Premises used: Filter.EventuallyLE.prodMap
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
α : Type u_5
β : Type u_6
inst_2 : LE α
inst_3 : LE β
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ ≤ᶠ[𝓝 x] f₂
hg : g₁ ≤ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ ≤ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂

Tactic:
exact hf.prodMap hg

Premises used: Filter.EventuallyLE.prodMap
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
rw : 𝓝 x ×ˢ 𝓝 y = map Prod.swap (𝓝 (y, x))
rw₁ : map Prod.swap (𝓝 y ×ˢ 𝓝 x) = map Prod.swap (𝓝 (y, x))
rw₂ rw₃ : map Prod.swap (𝓝 y ×ˢ 𝓝 x) = map Prod.swap (𝓝 y ×ˢ 𝓝 x)
⊢ 𝓝 (x, y) = map Prod.swap (𝓝 (y, x))

Tactic:
rw [nhds_prod_eq, Filter.prod_comm, nhds_prod_eq]

Premises used: Filter.prod_comm, nhds_prod_eq
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
γ : Type u_5
x : X
y : Y
f : Filter γ
mx : γ → X
my : γ → Y
hx : Tendsto mx f (𝓝 x)
hy : Tendsto my f (𝓝 y)
rw : Tendsto (fun (c : γ) ↦ (mx c, my c)) f (𝓝 x ×ˢ 𝓝 y)
⊢ Tendsto (fun (c : γ) ↦ (mx c, my c)) f (𝓝 (x, y))

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
γ : Type u_5
x : X
y : Y
f : Filter γ
mx : γ → X
my : γ → Y
hx : Tendsto mx f (𝓝 x)
hy : Tendsto my f (𝓝 y)
⊢ Tendsto (fun (c : γ) ↦ (mx c, my c)) f (𝓝 x ×ˢ 𝓝 y)

Tactic:
hx.prodMk hy

Premises used: Filter.Tendsto.prodMk
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
γ : Type u_5
x : X
y : Y
f : Filter γ
mx : γ → X
my : γ → Y
hx : Tendsto mx f (𝓝 x)
hy : Tendsto my f (𝓝 y)
⊢ Tendsto (fun (c : γ) ↦ (mx c, my c)) f (𝓝 x ×ˢ 𝓝 y)

Tactic:
exact hx.prodMk hy

Premises used: Filter.Tendsto.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
x : X
y : Y
z : Z
w : W
f : X → Y
g : Z → W
hf : Tendsto f (𝓝 x) (𝓝 y)
hg : Tendsto g (𝓝 z) (𝓝 w)
rw : Tendsto (Prod.map f g) (𝓝 x ×ˢ 𝓝 z) (𝓝 y ×ˢ 𝓝 w)
⊢ Tendsto (Prod.map f g) (𝓝 (x, z)) (𝓝 (y, w))

Tactic:
rw [nhds_prod_eq, nhds_prod_eq]

Premises used: nhds_prod_eq
-- 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
x : X
y : Y
z : Z
w : W
f : X → Y
g : Z → W
hf : Tendsto f (𝓝 x) (𝓝 y)
hg : Tendsto g (𝓝 z) (𝓝 w)
⊢ Tendsto (Prod.map f g) (𝓝 x ×ˢ 𝓝 z) (𝓝 y ×ˢ 𝓝 w)

Tactic:
hf.prodMap hg

Premises used: Filter.Tendsto.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
x : X
y : Y
z : Z
w : W
f : X → Y
g : Z → W
hf : Tendsto f (𝓝 x) (𝓝 y)
hg : Tendsto g (𝓝 z) (𝓝 w)
⊢ Tendsto (Prod.map f g) (𝓝 x ×ˢ 𝓝 z) (𝓝 y ×ˢ 𝓝 w)

Tactic:
exact hf.prodMap hg

Premises used: Filter.Tendsto.prodMap
-- 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 × Y) in 𝓝 x ×ˢ 𝓝 y, p x

Tactic:
rw [nhds_prod_eq] at h

Premises used: nhds_prod_eq