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
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 = ∅

Tactic:
Or.inl ⟨?_, ?_⟩

Premises used: And.intro, Or.inl
-- 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
H : IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
inr : IsOpen[inst] s
inr₁ : IsOpen[inst_1] t
⊢ IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅

Tactic:
refine Or.inl ⟨?_, ?_⟩

Premises used: Or.inl
-- 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
H : IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
⊢ IsOpen[inst] s

Tactic:
simpa only [fst_image_prod _ st.2] using isOpenMap_fst _ H

Premises used: Set.fst_image_prod, isOpenMap_fst, And.right
-- 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
H : IsOpen[instTopologicalSpaceProd] (s ×ˢ t)
⊢ IsOpen[inst_1] t

Tactic:
simpa only [snd_image_prod st.1 t] using isOpenMap_snd _ H

Premises used: And.left, isOpenMap_snd, Set.snd_image_prod
-- 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
H : IsOpen[inst] s ∧ IsOpen[inst_1] t ∨ s = ∅ ∨ t = ∅
⊢ IsOpen[inst] s ∧ IsOpen[inst_1] t

Tactic:
simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H

Premises used: Set.Nonempty.ne_empty, And.right, And.left, or_false
-- 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
H : IsOpen[inst] s ∧ IsOpen[inst_1] t
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t)

Tactic:
H.1.prod H.2

Premises used: And.right, And.left, IsOpen.prod
-- 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
H : IsOpen[inst] s ∧ IsOpen[inst_1] t
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t)

Tactic:
exact H.1.prod H.2

Premises used: And.right, And.left, IsOpen.prod
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Nonempty Y
⊢ IsQuotientMap (X := X × Y) Prod.fst

Tactic:
isOpenMap_fst.isQuotientMap continuous_fst Prod.fst_surjective

Premises used: IsOpenMap.isQuotientMap, Prod.fst_surjective, continuous_fst, isOpenMap_fst
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Nonempty X
⊢ IsQuotientMap (X := X × Y) Prod.snd

Tactic:
isOpenMap_snd.isQuotientMap continuous_snd Prod.snd_surjective

Premises used: IsOpenMap.isQuotientMap, continuous_snd, isOpenMap_snd, Prod.snd_surjective
-- 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
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
simp_rw₂ : (𝓝[s] a ×ˢ 𝓝[t] b).NeBot ↔ (𝓝[s] a).NeBot ∧ (𝓝[t] b).NeBot
⊢ (a, b) ∈ closure[instTopologicalSpaceProd] (s ×ˢ t) ↔ (a, b) ∈ closure[inst] s ×ˢ closure[inst_1] t

Tactic:
simp_rw [mem_prod, mem_closure_iff_nhdsWithin_neBot, nhdsWithin_prod_eq, prod_neBot]

Premises used: mem_closure_iff_nhdsWithin_neBot, Set.mem_prod, Filter.prod_neBot, nhdsWithin_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
a : X
b : Y
⊢ (a, b) ∈ interior (s ×ˢ t) ↔ (a, b) ∈ interior s ×ˢ interior t

Tactic:
simp only [mem_interior_iff_mem_nhds, mem_prod, prod_mem_nhds_iff]

Premises used: mem_interior_iff_mem_nhds, prod_mem_nhds_iff, Set.mem_prod
-- 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
⊢ frontier (s ×ˢ t) = closure[inst] s ×ˢ frontier t ∪ frontier s ×ˢ closure[inst_1] t

Tactic:
simp only [frontier, closure_prod_eq, interior_prod_eq, prod_diff_prod]

Premises used: Set.prod_diff_prod, frontier, interior_prod_eq, closure_prod_eq
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
⊢ frontier (SProd.sprod (β := Set Y) s univ) = SProd.sprod (β := Set Y) (frontier s) univ

Tactic:
simp [frontier_prod_eq]

Premises used: frontier_prod_eq
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
⊢ frontier (SProd.sprod (α := Set X) univ s) = SProd.sprod (α := Set X) univ (frontier s)

Tactic:
simp [frontier_prod_eq]

Premises used: frontier_prod_eq
-- 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
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
rw : f x y ∈ closure[inst_2] (closure[inst_2] u)
⊢ f x y ∈ closure[inst_2] u

Tactic:
rw [← isClosed_closure.closure_eq]

Premises used: IsClosed.closure_eq, isClosed_closure
-- 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
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
apply : ∀ (b : Y) (hb : b ∈ t), f x b ∈ closure[inst_2] u
⊢ f x y ∈ closure[inst_2] (closure[inst_2] u)

Tactic:
apply map_mem_closure (hf₁ x) hy fun b hb ↦ ?_

Premises used: map_mem_closure
-- 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
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
b : Y
hb : b ∈ t
⊢ f x b ∈ closure[inst_2] u

Tactic:
apply map_mem_closure (hf₂ b) hx fun a ha ↦ h a ha b hb

Premises used: map_mem_closure
-- 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
y : Y
s : Set X
t : Set Y
u : Set Z
hf : Continuous[instTopologicalSpaceProd, inst_2] (uncurry f)
hx : x ∈ closure[inst] s
hy : y ∈ closure[inst_1] t
h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u
⊢ (x, y) ∈ closure[instTopologicalSpaceProd] (s ×ˢ t)

Tactic:
simpa only [closure_prod_eq] using mk_mem_prod hx hy

Premises used: Set.mk_mem_prod, closure_prod_eq
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s₁ : Set X
s₂ : Set Y
h₁ : IsClosed[inst] s₁
h₂ : IsClosed[inst_1] s₂
⊢ closure[instTopologicalSpaceProd] (s₁ ×ˢ s₂) = s₁ ×ˢ s₂

Tactic:
simp only [h₁.closure_eq, h₂.closure_eq, closure_prod_eq]

Premises used: IsClosed.closure_eq, closure_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
hs : Dense s
ht : Dense t
x : X × Y
rw : x ∈ closure[inst] s ×ˢ closure[inst_1] t
⊢ x ∈ closure[instTopologicalSpaceProd] (s ×ˢ t)

Tactic:
rw [closure_prod_eq]

Premises used: closure_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
hs : Dense s
ht : Dense t
x : X × Y
⊢ x ∈ closure[inst] s ×ˢ closure[inst_1] t

Tactic:
⟨hs x.1, ht x.2⟩

Premises used: Set.Mem, setOf, Set.prod, Prod.fst, And.intro, Prod.snd
-- 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 : Dense s
ht : Dense t
x : X × Y
⊢ x ∈ closure[inst] s ×ˢ closure[inst_1] t

Tactic:
exact ⟨hs x.1, ht x.2⟩
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
Y : Type v
Z : Type u_2
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
ι : Type u_5
κ : Type u_6
f : ι → Y
g : κ → Z
hf : DenseRange f
hg : DenseRange g
⊢ DenseRange (Prod.map f g)

Tactic:
simpa only [DenseRange, prod_range_range_eq] using hf.prod hg

Premises used: DenseRange, Set.prod_range_range_eq, Dense.prod
-- 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 → Y
g : Z → W
hf : IsInducing f
hg : IsInducing g
x_1 : X × Z
x : X
z : Z
simp_rw : 𝓝 (x, z) = comap (fun (p : X × Z) ↦ (f p.1, g p.2)) (𝓝 (f x, g z))
simp_rw₁ : 𝓝 x ×ˢ 𝓝 z = comap (fun (p : X × Z) ↦ (f p.1, g p.2)) (𝓝 (f x) ×ˢ 𝓝 (g z))
simp_rw₂ : comap f (𝓝 (f x)) ×ˢ 𝓝 z = comap (fun (p : X × Z) ↦ (f p.1, g p.2)) (𝓝 (f x) ×ˢ 𝓝 (g z))
simp_rw₃ : comap f (𝓝 (f x)) ×ˢ comap g (𝓝 (g z)) = comap (fun (p : X × Z) ↦ (f p.1, g p.2)) (𝓝 (f x) ×ˢ 𝓝 (g z))
⊢ 𝓝 (x, z) = comap (Prod.map f g) (𝓝 (Prod.map f g (x, z)))

Tactic:
simp_rw [Prod.map_def, nhds_prod_eq, hf.nhds_eq_comap,
    hg.nhds_eq_comap, prod_comap_comap_eq]

Premises used: Topology.IsInducing.nhds_eq_comap, Filter.prod_comap_comap_eq, nhds_prod_eq, Prod.map_def
-- 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
x : X
f : Y → Z
simp_rw : inst_1 = induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) instTopologicalSpaceProd ↔ inst_1 = induced f inst_2
simp_rw₁ :
  inst_1 = induced (fun (x' : Y) ↦ (x, f x')) (induced Prod.fst inst ⊓ induced Prod.snd inst_2) ↔
    inst_1 = induced f inst_2
simp_rw₂ :
  inst_1 =
      induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) (induced Prod.fst inst) ⊓
        induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) (induced Prod.snd inst_2) ↔
    inst_1 = induced f inst_2
simp_rw₃ :
  inst_1 =
      induced (comp (β := X × Z) Prod.fst fun (x' : Y) ↦ (x, f x')) inst ⊓
        induced (comp (β := X × Z) Prod.snd fun (x' : Y) ↦ (x, f x')) inst_2 ↔
    inst_1 = induced f inst_2
simp_rw₄ : inst_1 = induced (fun (x_1 : Y) ↦ x) inst ⊓ induced (fun (x : Y) ↦ f x) inst_2 ↔ inst_1 = induced f inst_2
simp_rw₅ : inst_1 = ⊤ ⊓ induced (fun (x : Y) ↦ f x) inst_2 ↔ inst_1 = induced f inst_2
⊢ (IsInducing (Y := X × Z) fun (x' : Y) ↦ (x, f x')) ↔ IsInducing f

Tactic:
simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, top_inf_eq]

Premises used: induced_inf, induced_const, instTopologicalSpaceProd, induced_compose, top_inf_eq, Function.comp_def, Topology.isInducing_iff
-- 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
y : Y
f : X → Z
simp_rw : inst = induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) instTopologicalSpaceProd ↔ inst = induced f inst_2
simp_rw₁ :
  inst = induced (fun (x : X) ↦ (f x, y)) (induced Prod.fst inst_2 ⊓ induced Prod.snd inst_1) ↔ inst = induced f inst_2
simp_rw₂ :
  inst =
      induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) (induced Prod.fst inst_2) ⊓
        induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) (induced Prod.snd inst_1) ↔
    inst = induced f inst_2
simp_rw₃ :
  inst =
      induced (comp (β := Z × Y) Prod.fst fun (x : X) ↦ (f x, y)) inst_2 ⊓
        induced (comp (β := Z × Y) Prod.snd fun (x : X) ↦ (f x, y)) inst_1 ↔
    inst = induced f inst_2
simp_rw₄ : inst = induced (fun (x : X) ↦ f x) inst_2 ⊓ induced (fun (x : X) ↦ y) inst_1 ↔ inst = induced f inst_2
simp_rw₅ : inst = induced (fun (x : X) ↦ f x) inst_2 ⊓ ⊤ ↔ inst = induced f inst_2
⊢ (IsInducing (Y := Z × Y) fun (x : X) ↦ (f x, y)) ↔ IsInducing f

Tactic:
simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, inf_top_eq]

Premises used: induced_inf, induced_const, inf_top_eq, instTopologicalSpaceProd, induced_compose, Function.comp_def, Topology.isInducing_iff
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
y : Y
⊢ IsInducing (Y := X × Y) fun (x : X) ↦ (x, y)

Tactic:
.of_comp (.prodMk_left y) continuous_fst .id

Premises used: Topology.IsInducing.id, continuous_fst, Continuous.prodMk_left, Topology.IsInducing.of_comp
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
⊢ IsInducing (X := Y) (Prod.mk x)

Tactic:
.of_comp (.prodMk_right x) continuous_snd .id

Premises used: Topology.IsInducing.id, Continuous.prodMk_right, continuous_snd, Topology.IsInducing.of_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 : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
rw : ∀ (x : X × Z), 𝓝 (Prod.map f g x) ≤ map (Prod.map f g) (𝓝 x)
⊢ IsOpenMap (Prod.map f g)

Tactic:
rw [isOpenMap_iff_nhds_le]

Premises used: isOpenMap_iff_nhds_le
-- 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 → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
a : X
b : Z
rw : 𝓝 (Prod.map f g (a, b)).1 ×ˢ 𝓝 (Prod.map f g (a, b)).2 ≤ map f (𝓝 a) ×ˢ map g (𝓝 b)
⊢ 𝓝 (Prod.map f g (a, b)) ≤ map (Prod.map f g) (𝓝 (a, b))

Tactic:
rw [nhds_prod_eq, nhds_prod_eq, ← Filter.prod_map_map_eq']

Premises used: Filter.prod_map_map_eq', 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
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
a : X
b : Z
⊢ 𝓝 (Prod.map f g (a, b)).1 ×ˢ 𝓝 (Prod.map f g (a, b)).2 ≤ map f (𝓝 a) ×ˢ map g (𝓝 b)

Tactic:
Filter.prod_mono (hf.nhds_le a) (hg.nhds_le b)

Premises used: Set.Mem, Filter.prod_mono, IsOpenMap.nhds_le
-- 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 → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
a : X
b : Z
⊢ 𝓝 (Prod.map f g (a, b)).1 ×ˢ 𝓝 (Prod.map f g (a, b)).2 ≤ map f (𝓝 a) ×ˢ map g (𝓝 b)

Tactic:
exact Filter.prod_mono (hf.nhds_le a) (hg.nhds_le b)

Premises used: Filter.prod_mono, IsOpenMap.nhds_le
-- 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 → Y
g : Z → W
hf : IsOpenEmbedding f
hg : IsOpenEmbedding g
⊢ IsOpenEmbedding (Prod.map f g)

Tactic:
.of_isEmbedding_isOpenMap (hf.1.prodMap hg.1) (hf.isOpenMap.prodMap hg.isOpenMap)

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, IsOpenMap.prodMap, Topology.IsEmbedding.prodMap, Topology.IsOpenEmbedding.of_isEmbedding_isOpenMap
-- 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 → Y
g : Z → W
hf : IsClosedEmbedding f
hg : IsClosedEmbedding g
⊢ IsClosedEmbedding (Prod.map f g)

Tactic:
{ hf.isEmbedding.prodMap hg.isEmbedding with
    isClosed_range := range_prodMap ▸ hf.isClosed_range.prod hg.isClosed_range }

Premises used: Topology.IsEmbedding.prodMap, Eq.rec, Topology.IsClosedEmbedding.isEmbedding, Set.range_prodMap, IsClosed.prod, Eq.symm, Topology.IsClosedEmbedding.mk, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ IsEmbedding (Y := X × Y) fun (x : X) ↦ (x, f x)

Tactic:
.of_comp (continuous_id.prodMk hf) continuous_fst .id

Premises used: continuous_fst, Topology.IsEmbedding.id, continuous_id, Topology.IsEmbedding.of_comp, Continuous.prodMk
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
y : Y
⊢ IsEmbedding (Y := X × Y) fun (x : X) ↦ (x, y)

Tactic:
.of_comp (.prodMk_left y) continuous_fst .id

Premises used: continuous_fst, Topology.IsEmbedding.id, Topology.IsEmbedding.of_comp, Continuous.prodMk_left
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
⊢ IsEmbedding (X := Y) (Prod.mk x)

Tactic:
.of_comp (.prodMk_right x) continuous_snd .id

Premises used: Continuous.prodMk_right, continuous_snd, Topology.IsEmbedding.id, Topology.IsEmbedding.of_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 : X → Y
g : Z → W
hf : IsOpenQuotientMap f
hg : IsOpenQuotientMap g
⊢ IsOpenQuotientMap (Prod.map f g)

Tactic:
⟨.prodMap hf.1 hg.1, .prodMap hf.2 hg.2, .prodMap hf.3 hg.3⟩

Premises used: IsOpenQuotientMap.continuous, IsOpenMap.prodMap, Continuous.prodMap, Function.Surjective.prodMap, IsOpenQuotientMap.mk, IsOpenQuotientMap.surjective, IsOpenQuotientMap.isOpenMap
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
α : Type u_5
β : Type u_6
σ₁ σ₂ : TopologicalSpace α
τ₁ τ₂ : TopologicalSpace β
hσ : σ₁ ≤ σ₂
hτ : τ₁ ≤ τ₂
⊢ LE.le (α := TopologicalSpace (α × β)) instTopologicalSpaceProd instTopologicalSpaceProd

Tactic:
le_inf (inf_le_left.trans <| induced_mono hσ) (inf_le_right.trans <| induced_mono hτ)

Premises used: inf_le_right, le_inf, inf_le_left, induced_mono, LE.le.trans
-- 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
inst_2 : TopologicalSpace X'
inst_3 : TopologicalSpace Y'
h₁ : X ≃ₜ X'
h₂ : Y ≃ₜ Y'
⊢ (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm

Tactic:
rfl

Premises used: Prod.map, Homeomorph.symm, Equiv.symm, Equiv.prodCongr, rfl, Homeomorph.prodCongr
-- 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
inst_2 : TopologicalSpace X'
inst_3 : TopologicalSpace Y'
h₁ : X ≃ₜ X'
h₂ : Y ≃ₜ Y'
⊢ Eq (α := (a : X × Y) → X' × Y') (⇑(h₁.prodCongr h₂) : (a : X × Y) → X' × Y')
    (Prod.map (⇑h₁ : (a : X) → X') (⇑h₂ : (a : Y) → Y'))

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Eq (α := Y × X ≃ₜ X × Y) (Homeomorph.symm (prodComm X Y)) (prodComm Y X)

Tactic:
rfl

Premises used: Equiv.prodComm, Homeomorph.prodComm, Homeomorph.symm, Prod.swap, Equiv.symm, rfl
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Eq (α := (a : X × Y) → Y × X) (⇑(prodComm X Y) : (a : X × Y) → Y × X) Prod.swap

Tactic:
rfl

Premises used: Prod.swap, rfl
-- 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
⊢ toEquiv (prodAssoc X Y Z) = Equiv.prodAssoc X Y Z

Tactic:
rfl

Premises used: Equiv.prodAssoc, rfl
-- 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
⊢ Eq (α := (X × W) × Y × Z ≃ₜ (X × Y) × W × Z) (Homeomorph.symm (prodProdProdComm X Y W Z)) (prodProdProdComm X W Y Z)

Tactic:
rfl

Premises used: Homeomorph.prodProdProdComm, Homeomorph.symm, Equiv.prodProdProdComm, rfl
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Eq (α := (a : PUnit.{u_7 + 1} × X) → X) (⇑(punitProd X) : (a : PUnit.{u_7 + 1} × X) → X) Prod.snd

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Continuous[instTopologicalSpaceSum, inst_2] f ↔
    Continuous[inst, inst_2] (f ∘ inl) ∧ Continuous[inst_1, inst_2] (f ∘ inr)

Tactic:
(continuous_sup_dom (t₁ := TopologicalSpace.coinduced Sum.inl _)
    (t₂ := TopologicalSpace.coinduced Sum.inr _)).trans <|
    continuous_coinduced_dom.and continuous_coinduced_dom

Premises used: continuous_coinduced_dom, continuous_sup_dom, setOf, Iff.and, Iff.trans
-- 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 → Z
g : Y → Z
⊢ Continuous[instTopologicalSpaceSum, inst_2] (Sum.elim f g) ↔ Continuous[inst, inst_2] f ∧ Continuous[inst_1, inst_2] g

Tactic:
continuous_sum_dom

Premises used: continuous_sum_dom, Sum.elim
-- 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 → Z
g : Y → Z
hf : Continuous[inst, inst_2] f
hg : Continuous[inst_1, inst_2] g
⊢ Continuous[instTopologicalSpaceSum, inst_2] (Sum.elim f g)

Tactic:
continuous_sumElim.2 ⟨hf, hg⟩

Premises used: Iff.mpr, continuous_sumElim, And.intro
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Continuous[instTopologicalSpaceSum, _] isLeft

Tactic:
continuous_sum_dom.2 ⟨continuous_const, continuous_const⟩

Premises used: Iff.mpr, continuous_const, And.intro, continuous_sum_dom
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Continuous[instTopologicalSpaceSum, _] isRight

Tactic:
continuous_sum_dom.2 ⟨continuous_const, continuous_const⟩

Premises used: Iff.mpr, continuous_const, And.intro, continuous_sum_dom
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Continuous[inst, instTopologicalSpaceSum] inl

Tactic:
⟨fun _ => And.left⟩

Premises used: Continuous.mk, And.left
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Continuous[inst_1, instTopologicalSpaceSum] inr

Tactic:
⟨fun _ => And.right⟩

Premises used: Continuous.mk, And.right