awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
rw₂ : SProd.sprod (α := Filter X) (β := Filter Y) (pure a) (pure b) = pure (a, b)
⊢ 𝓝 (a, b) = pure (a, b)
have rw₃ : Eq (α := Filter (X × Y)) (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
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
x : X
y : Y
⊢ s ×ˢ t ∈ 𝓝 (x, y) ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y
have rw : s ×ˢ t ∈ 𝓝 x ×ˢ 𝓝 y ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y
Tactic: rw [nhds_prod_eq, prod_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
s : Set X
t : Set Y
x : X
y : Y
rw : s ×ˢ t ∈ 𝓝 x ×ˢ 𝓝 y ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y
⊢ s ×ˢ t ∈ 𝓝 (x, y) ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y
have rw₁ : s ∈ 𝓝 x ∧ t ∈ 𝓝 y ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y
Tactic: rw [nhds_prod_eq, prod_mem_prod_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsOpen[instTopologicalSpaceProd] {p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2)}
have simp : ∀ (a b : X), Disjoint (𝓝 a) (𝓝 b) → {p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (a, b)
Tactic: simp only [isOpen_iff_mem_nhds, Prod.forall, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
h : Disjoint (𝓝 x) (𝓝 y)
⊢ {p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)
have 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)
Tactic: obtain ⟨U, hU, V, hV, hd⟩ := ((nhds_basis_opens x).disjoint_iff (nhds_basis_opens y)).mp h
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
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₂
have rw : Prod.map f₁ g₁ =ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂
Tactic: rw [nhds_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
α : 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₂
have rw : Prod.map f₁ g₁ ≤ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂
Tactic: rw [nhds_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
⊢ 𝓝 (x, y) = map Prod.swap (𝓝 (y, x))
have rw : 𝓝 x ×ˢ 𝓝 y = map Prod.swap (𝓝 (y, x))
Tactic: rw [nhds_prod_eq, Filter.prod_comm, nhds_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
rw : 𝓝 x ×ˢ 𝓝 y = map Prod.swap (𝓝 (y, x))
⊢ 𝓝 (x, y) = map Prod.swap (𝓝 (y, x))
have rw₁ : map Prod.swap (𝓝 y ×ˢ 𝓝 x) = map Prod.swap (𝓝 (y, x))
Tactic: rw [nhds_prod_eq, Filter.prod_comm, nhds_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
rw : 𝓝 x ×ˢ 𝓝 y = map Prod.swap (𝓝 (y, x))
rw₁ : map Prod.swap (𝓝 y ×ˢ 𝓝 x) = map Prod.swap (𝓝 (y, x))
⊢ 𝓝 (x, y) = map Prod.swap (𝓝 (y, x))
have rw₂ : map Prod.swap (𝓝 y ×ˢ 𝓝 x) = map Prod.swap (𝓝 y ×ˢ 𝓝 x)
Tactic: rw [nhds_prod_eq, Filter.prod_comm, nhds_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
γ : 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))
have rw : Tendsto (fun (c : γ) ↦ (mx c, my c)) f (𝓝 x ×ˢ 𝓝 y)
Tactic: rw [nhds_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
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))
have rw : Tendsto (Prod.map f g) (𝓝 x ×ˢ 𝓝 z) (𝓝 y ×ˢ 𝓝 w)
Tactic: rw [nhds_prod_eq, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
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')
have h₁ : ∀ᶠ (x : X × Y) in 𝓝 x ×ˢ 𝓝 y, p x
Tactic: rw [nhds_prod_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
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.{u, u_1} (Y := W) (fun (x : X) ↦ f (g x, h x)) x
have hf₁ : ContinuousAt f (g x, h x)
Tactic: rw [← e] at hf
Cleared hypotheses: hf, hg, hh, e
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
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
⊢ Eq (α := Set (X × Y)) (⋃ v ∈ t, u ×ˢ v) (Prod.fst ⁻¹' u)
have simp_rw : SProd.sprod (β := Set Y) u (⋃ i ∈ t, i) = Prod.fst ⁻¹' u
Tactic: simp_rw [← prod_iUnion, ← sUnion_eq_biUnion, ht, prod_univ]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
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
⊢ Eq (α := Set (X × Y)) (⋃ v ∈ t, u ×ˢ v) (Prod.fst ⁻¹' u)
have simp_rw₁ : u ×ˢ ⋃₀ t = Prod.fst ⁻¹' u
Tactic: simp_rw [← prod_iUnion, ← sUnion_eq_biUnion, ht, prod_univ]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
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
⊢ Eq (α := Set (X × Y)) (⋃ v ∈ t, u ×ˢ v) (Prod.fst ⁻¹' u)
have simp_rw₂ : SProd.sprod (β := Set Y) u univ = Prod.fst ⁻¹' u
Tactic: simp_rw [← prod_iUnion, ← sUnion_eq_biUnion, ht, prod_univ]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
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) (Prod.fst ⁻¹' u)
have rw : TopologicalSpace.IsOpen (X := X × Y) (⋃ v ∈ t, u ×ˢ v)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
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
⊢ Eq (α := Set (X × Y)) (⋃ u ∈ s, u ×ˢ v) (Prod.snd ⁻¹' v)
have simp_rw : SProd.sprod (α := Set X) (⋃ i ∈ s, i) v = Prod.snd ⁻¹' v
Tactic: simp_rw [← iUnion_prod_const, ← sUnion_eq_biUnion, hs, univ_prod]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
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
⊢ Eq (α := Set (X × Y)) (⋃ u ∈ s, u ×ˢ v) (Prod.snd ⁻¹' v)
have simp_rw₁ : ⋃₀ s ×ˢ v = Prod.snd ⁻¹' v
Tactic: simp_rw [← iUnion_prod_const, ← sUnion_eq_biUnion, hs, univ_prod]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
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
⊢ Eq (α := Set (X × Y)) (⋃ u ∈ s, u ×ˢ v) (Prod.snd ⁻¹' v)
have simp_rw₂ : SProd.sprod (α := Set X) univ v = Prod.snd ⁻¹' v
Tactic: simp_rw [← iUnion_prod_const, ← sUnion_eq_biUnion, hs, univ_prod]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
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) (Prod.snd ⁻¹' v)
have rw : TopologicalSpace.IsOpen (X := X × Y) (⋃ u ∈ s, u ×ˢ v)
Tactic: rw [← this]
-- 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)
⊢ (∀ 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
have 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
Tactic: simp_rw [Prod.forall, mem_nhds_prod_iff', and_left_comm]
-- 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)
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
⊢ (∀ 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
have 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
Tactic: simp_rw [Prod.forall, mem_nhds_prod_iff', and_left_comm]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
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 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)
have 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
Tactic: simp_rw [induced_inf, induced_compose]
-- 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
⊢ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x) = 𝓝 x.1
have refine : ∀ (s : Set X) (hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x)), s ∈ 𝓝 x.1
Tactic: refine le_antisymm (continuousAt_fst.mono_left inf_le_left) fun s hs => ?_
-- 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
s : Set X
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x)
⊢ s ∈ 𝓝 x.1
have rcases : ∀ (x : X) (y : Y) (hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {(x, y).2}] (x, y))), s ∈ 𝓝 (x, y).1
Tactic: rcases x with ⟨x, y⟩
Cleared hypotheses: x, hs
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
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))
⊢ s ∈ 𝓝 (x, y).1
have 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}
Tactic: rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs
Cleared hypotheses: hs
-- 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
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}
⊢ s ∈ 𝓝 (x, y).1
have 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
Tactic: rcases hs with ⟨u, hu, v, hv, H⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
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}
⊢ s ∈ 𝓝 (x, y).1
have H₁ : ∀ 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
Cleared hypotheses: H
-- 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
⊢ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x) = 𝓝 x.2
have refine : ∀ (s : Set Y) (hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x)), s ∈ 𝓝 x.2
Tactic: refine le_antisymm (continuousAt_snd.mono_left inf_le_left) fun s hs => ?_
-- 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
s : Set Y
hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x)
⊢ s ∈ 𝓝 x.2
have rcases : ∀ (x : X) (y : Y) (hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {(x, y).1}] (x, y))), s ∈ 𝓝 (x, y).2
Tactic: rcases x with ⟨x, y⟩
Cleared hypotheses: x, hs
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
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))
⊢ s ∈ 𝓝 (x, y).2
have 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}
Tactic: rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs
Cleared hypotheses: hs
-- 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 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}
⊢ s ∈ 𝓝 (x, y).2
have 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
Tactic: rcases hs with ⟨u, hu, v, hv, H⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
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}
⊢ s ∈ 𝓝 (x, y).2
have H₁ : ∀ 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
Cleared hypotheses: H
-- 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
t : Set Y
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅
have inl : ∀ (h : 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
-- 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
t : Set Y
inl : ∀ (h : s ×ˢ t = ∅), 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 = ∅
have inr : ∀ (h : (s ×ˢ t).Nonempty), IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅
Tactic: rcases (s ×ˢ t).eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅
have st : s.Nonempty ∧ t.Nonempty
Tactic: have st : s.Nonempty ∧ t.Nonempty := prod_nonempty_iff.1 h
-- 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
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅
have inr : IsOpen[instTopologicalSpaceProd] (s ×ˢ t) → IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅
Tactic: constructor
-- 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
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 = ∅
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅
have inr₁ : IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅ → IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
Tactic: constructor
-- 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
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
⊢ IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅
have inr : IsOpen[inst] s
Tactic: refine Or.inl ⟨?_, ?_⟩
-- 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
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
inr : IsOpen[inst] s
⊢ IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅
have inr₁ : IsOpen[inst_1] t
Tactic: refine Or.inl ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
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
H : IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
have H₁ : IsOpen[inst] s ∧ IsOpen[inst_1] t
Tactic: simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H
Cleared hypotheses: H
-- 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
t : Set Y
x : X × Y
a : X
b : Y
⊢ (a, b) ∈ closure[instTopologicalSpaceProd] (s ×ˢ t) ↔ (a, b) ∈ closure[inst] s ×ˢ closure[inst_1] t
have simp_rw : (a, b) ∈ closure[instTopologicalSpaceProd] (s ×ˢ t) ↔ a ∈ closure[inst] s ∧ b ∈ closure[inst_1] t
Tactic: simp_rw [mem_prod, mem_closure_iff_nhdsWithin_neBot, nhdsWithin_prod_eq, prod_neBot]
-- 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
t : Set Y
x : X × Y
a : X
b : Y
simp_rw : (a, b) ∈ closure[instTopologicalSpaceProd] (s ×ˢ t) ↔ a ∈ closure[inst] s ∧ b ∈ closure[inst_1] t
⊢ (a, b) ∈ closure[instTopologicalSpaceProd] (s ×ˢ t) ↔ (a, b) ∈ closure[inst] s ×ˢ closure[inst_1] t
have simp_rw₁ : (𝓝[s ×ˢ t] (a, b)).NeBot ↔ (𝓝[s] a).NeBot ∧ (𝓝[t] b).NeBot
Tactic: simp_rw [mem_prod, mem_closure_iff_nhdsWithin_neBot, nhdsWithin_prod_eq, prod_neBot]
-- 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
t : Set Y
x : X × Y
a : X
b : Y
simp_rw : (a, b) ∈ closure[instTopologicalSpaceProd] (s ×ˢ t) ↔ a ∈ closure[inst] s ∧ b ∈ closure[inst_1] t
simp_rw₁ : (𝓝[s ×ˢ t] (a, b)).NeBot ↔ (𝓝[s] a).NeBot ∧ (𝓝[t] b).NeBot
⊢ (a, b) ∈ closure[instTopologicalSpaceProd] (s ×ˢ t) ↔ (a, b) ∈ closure[inst] s ×ˢ closure[inst_1] t
have simp_rw₂ : (𝓝[s] a ×ˢ 𝓝[t] b).NeBot ↔ (𝓝[s] a).NeBot ∧ (𝓝[t] b).NeBot
Tactic: simp_rw [mem_prod, mem_closure_iff_nhdsWithin_neBot, nhdsWithin_prod_eq, prod_neBot]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
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
y : Y
s : Set X
t : Set Y
u : Set Z
hf₁ : ∀ (x : X), Continuous[inst_1, inst_2] (f x)
hf₂ : ∀ (y : Y), Continuous[inst, inst_2] fun (x : X) ↦ f x y
hx : x ∈ closure[inst] s
hy : y ∈ closure[inst_1] t
h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u
⊢ f x y ∈ closure[inst_2] u
have rw : f x y ∈ closure[inst_2] (closure[inst_2] u)
Tactic: rw [← isClosed_closure.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
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
y : Y
s : Set X
t : Set Y
u : Set Z
hf₁ : ∀ (x : X), Continuous[inst_1, inst_2] (f x)
hf₂ : ∀ (y : Y), Continuous[inst, inst_2] fun (x : X) ↦ f x y
hx : x ∈ closure[inst] s
hy : y ∈ closure[inst_1] t
h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u
⊢ f x y ∈ closure[inst_2] (closure[inst_2] u)
have apply : ∀ (b : Y) (hb : b ∈ t), f x b ∈ closure[inst_2] u
Tactic: apply map_mem_closure (hf₁ x) hy fun b hb ↦ ?_