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
⊢ Continuous[instTopologicalSpaceSum, instTopologicalSpaceSum] Sum.swap

Tactic:
Continuous.sumElim continuous_inr continuous_inl

Premises used: Sum.swap, continuous_inl, continuous_inr, Continuous.sumElim
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set (X ⊕ Y)
⊢ IsOpen[instTopologicalSpaceSum] s ↔ IsOpen[inst] (inl ⁻¹' s) ∧ IsOpen[inst_1] (inr ⁻¹' s)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter, IsOpen
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set (X ⊕ Y)
⊢ IsClosed[instTopologicalSpaceSum] s ↔ IsClosed[inst] (inl ⁻¹' s) ∧ IsClosed[inst_1] (inr ⁻¹' s)

Tactic:
simp only [← isOpen_compl_iff, isOpen_sum_iff, preimage_compl]

Premises used: isOpen_sum_iff, Set.preimage_compl, isOpen_compl_iff
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
u : Set X
hu : IsOpen[inst] u
⊢ IsOpen[instTopologicalSpaceSum] (inl '' u)

Tactic:
simpa [isOpen_sum_iff, preimage_image_eq u Sum.inl_injective]

Premises used: isOpen_sum_iff, Sum.inl_injective, Set.preimage_image_eq
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
u : Set Y
hu : IsOpen[inst_1] u
⊢ IsOpen[instTopologicalSpaceSum] (inr '' u)

Tactic:
simpa [isOpen_sum_iff, preimage_image_eq u Sum.inr_injective]

Premises used: isOpen_sum_iff, Sum.inr_injective, Set.preimage_image_eq
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
u : Set X
hu : IsClosed[inst] u
⊢ IsClosed[instTopologicalSpaceSum] (inl '' u)

Tactic:
simpa [isClosed_sum_iff, preimage_image_eq u Sum.inl_injective]

Premises used: Sum.inl_injective, Set.preimage_image_eq, isClosed_sum_iff
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
u : Set Y
hu : IsClosed[inst_1] u
⊢ IsClosed[instTopologicalSpaceSum] (inr '' u)

Tactic:
simpa [isClosed_sum_iff, preimage_image_eq u Sum.inr_injective]

Premises used: Sum.inr_injective, Set.preimage_image_eq, isClosed_sum_iff
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsOpenEmbedding (X := X) (Y := X ⊕ Y) inl

Tactic:
.of_continuous_injective_isOpenMap continuous_inl inl_injective isOpenMap_inl

Premises used: continuous_inl, Sum.inl_injective, Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap, isOpenMap_inl
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsOpenEmbedding (X := Y) (Y := X ⊕ Y) inr

Tactic:
.of_continuous_injective_isOpenMap continuous_inr inr_injective isOpenMap_inr

Premises used: Sum.inr_injective, continuous_inr, Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap, isOpenMap_inr
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsEmbedding (X := X) (Y := X ⊕ Y) inl

Tactic:
IsOpenEmbedding.inl.1

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.inl
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsEmbedding (X := Y) (Y := X ⊕ Y) inr

Tactic:
IsOpenEmbedding.inr.1

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.inr
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsOpen[instTopologicalSpaceSum] (range inl)

Tactic:
IsOpenEmbedding.inl.2

Premises used: Topology.IsOpenEmbedding.isOpen_range, Topology.IsOpenEmbedding.inl
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsOpen[instTopologicalSpaceSum] (range inr)

Tactic:
IsOpenEmbedding.inr.2

Premises used: Topology.IsOpenEmbedding.inr, Topology.IsOpenEmbedding.isOpen_range
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
rw : IsOpen[instTopologicalSpaceSum] (range inr)
⊢ IsClosed[instTopologicalSpaceSum] (range inl)

Tactic:
rw [← isOpen_compl_iff, compl_range_inl]

Premises used: Set.compl_range_inl, isOpen_compl_iff
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsOpen[instTopologicalSpaceSum] (range inr)

Tactic:
isOpen_range_inr

Premises used: isOpen_range_inr
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsOpen[instTopologicalSpaceSum] (range inr)

Tactic:
exact isOpen_range_inr

Premises used: isOpen_range_inr
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
rw : IsOpen[instTopologicalSpaceSum] (range inl)
⊢ IsClosed[instTopologicalSpaceSum] (range inr)

Tactic:
rw [← isOpen_compl_iff, compl_range_inr]

Premises used: Set.compl_range_inr, isOpen_compl_iff
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsOpen[instTopologicalSpaceSum] (range inl)

Tactic:
isOpen_range_inl

Premises used: isOpen_range_inl
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsOpen[instTopologicalSpaceSum] (range inl)

Tactic:
exact isOpen_range_inl

Premises used: isOpen_range_inl
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsClosedEmbedding (X := X) (Y := X ⊕ Y) Sum.inl

Tactic:
⟨.inl, isClosed_range_inl⟩

Premises used: Topology.IsEmbedding.inl, isClosed_range_inl, Topology.IsClosedEmbedding.mk
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsClosedEmbedding (X := Y) (Y := X ⊕ Y) Sum.inr

Tactic:
⟨.inr, isClosed_range_inr⟩

Premises used: isClosed_range_inr, Topology.IsClosedEmbedding.mk, Topology.IsEmbedding.inr
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
⊢ Eq (α := Filter (X ⊕ Y)) (𝓝 (inl x)) (map inl (𝓝 x))

Tactic:
(IsOpenEmbedding.inl.map_nhds_eq _).symm

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, Topology.IsOpenEmbedding.inl, Eq.symm
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
y : Y
⊢ Eq (α := Filter (X ⊕ Y)) (𝓝 (inr y)) (map inr (𝓝 y))

Tactic:
(IsOpenEmbedding.inr.map_nhds_eq _).symm

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, Topology.IsOpenEmbedding.inr, Eq.symm
-- 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 W
inst_3 : TopologicalSpace Z
f : X → Y
g : Z → W
⊢ Continuous[instTopologicalSpaceSum, instTopologicalSpaceSum] (Sum.map f g) ↔
    Continuous[inst, inst_1] f ∧ Continuous[inst_3, inst_2] g

Tactic:
continuous_sumElim.trans <|
    IsEmbedding.inl.continuous_iff.symm.and IsEmbedding.inr.continuous_iff.symm

Premises used: Topology.IsEmbedding.inl, continuous_sumElim, Sum.map, Iff.and, Iff.trans, Topology.IsEmbedding.continuous_iff, Iff.symm, Topology.IsEmbedding.inr
-- 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 W
inst_3 : TopologicalSpace Z
f : X → Y
g : Z → W
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_3, inst_2] g
⊢ Continuous[instTopologicalSpaceSum, instTopologicalSpaceSum] (Sum.map f g)

Tactic:
continuous_sumMap.2 ⟨hf, hg⟩

Premises used: Iff.mpr, continuous_sumMap, And.intro
-- 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
⊢ IsOpenMap f ↔
    (IsOpenMap.{u, u_2} (Y := Z) fun (a : X) ↦ f (inl a)) ∧ IsOpenMap.{v, u_2} (Y := Z) fun (b : Y) ↦ f (inr b)

Tactic:
simp only [isOpenMap_iff_nhds_le, Sum.forall, nhds_inl, nhds_inr, Filter.map_map, comp_def]

Premises used: isOpenMap_iff_nhds_le, Filter.map_map, nhds_inl, nhds_inr, Function.comp_def, Sum.forall
-- 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 W
inst_3 : TopologicalSpace Z
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
⊢ IsOpenMap (Sum.map f g)

Tactic:
isOpenMap_sum.2 ⟨isOpenMap_inl.comp hf, isOpenMap_inr.comp hg⟩

Premises used: Iff.mpr, IsOpenMap.comp, isOpenMap_sum, isOpenMap_inl, And.intro, isOpenMap_inr
-- 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
⊢ IsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g

Tactic:
simp only [isOpenMap_sum, elim_inl, elim_inr]

Premises used: Sum.elim_inr, isOpenMap_sum, Sum.elim_inl
-- 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 : IsOpenMap f
hg : IsOpenMap g
⊢ IsOpenMap (Sum.elim f g)

Tactic:
isOpenMap_sumElim.2 ⟨hf, hg⟩

Premises used: Iff.mpr, And.intro, isOpenMap_sumElim
-- 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 : IsOpenEmbedding f
hg : IsOpenEmbedding g
h : Injective (Sum.elim f g)
rw :
  ∀ (hf : Continuous[inst, inst_2] f ∧ Injective f ∧ IsOpenMap f)
    (hg : Continuous[inst_1, inst_2] g ∧ Injective g ∧ IsOpenMap g) (h : Injective (Sum.elim f g)),
    Continuous[instTopologicalSpaceSum, inst_2] (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsOpenMap (Sum.elim f g)
⊢ IsOpenEmbedding (Sum.elim f g)

Tactic:
rw [isOpenEmbedding_iff_continuous_injective_isOpenMap] at hf hg ⊢

Premises used: Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap
-- 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 ∧ Injective f ∧ IsOpenMap f
hg : Continuous[inst_1, inst_2] g ∧ Injective g ∧ IsOpenMap g
h : Injective (Sum.elim f g)
⊢ Continuous[instTopologicalSpaceSum, inst_2] (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsOpenMap (Sum.elim f g)

Tactic:
⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩

Premises used: And.right, And.left, And.intro, Continuous.sumElim, IsOpenMap.sumElim
-- 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 ∧ Injective f ∧ IsOpenMap f
hg : Continuous[inst_1, inst_2] g ∧ Injective g ∧ IsOpenMap g
h : Injective (Sum.elim f g)
⊢ Continuous[instTopologicalSpaceSum, inst_2] (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsOpenMap (Sum.elim f g)

Tactic:
exact ⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩
-- 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
mp :
  IsClosedMap f →
    (IsClosedMap.{u, u_2} (Y := Z) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z) fun (b : Y) ↦ f (inr b)
mpr :
  ((IsClosedMap.{u, u_2} (Y := Z) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z) fun (b : Y) ↦ f (inr b)) →
    IsClosedMap f
⊢ IsClosedMap f ↔
    (IsClosedMap.{u, u_2} (Y := Z) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z) fun (b : Y) ↦ f (inr b)

Tactic:
constructor
-- 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
h : IsClosedMap f
⊢ (IsClosedMap.{u, u_2} (Y := Z) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z) fun (b : Y) ↦ f (inr b)

Tactic:
⟨h.comp IsClosedEmbedding.inl.isClosedMap, h.comp IsClosedEmbedding.inr.isClosedMap⟩

Premises used: Topology.IsClosedEmbedding.isClosedMap, Topology.IsClosedEmbedding.inr, Topology.IsClosedEmbedding.inl, And.intro, IsClosedMap.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
h : IsClosedMap f
⊢ (IsClosedMap.{u, u_2} (Y := Z) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z) fun (b : Y) ↦ f (inr b)

Tactic:
exact ⟨h.comp IsClosedEmbedding.inl.isClosedMap, h.comp IsClosedEmbedding.inr.isClosedMap⟩
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z_1 : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z_1
f : X ⊕ Y → Z_1
h : (IsClosedMap.{u, u_2} (Y := Z_1) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z_1) fun (b : Y) ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[instTopologicalSpaceSum] Z
⊢ IsClosed[inst] (inl ⁻¹' Z) ∧ IsClosed[inst_1] (inr ⁻¹' Z)

Tactic:
rw [isClosed_sum_iff] at hZ

Premises used: isClosed_sum_iff
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z_1 : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z_1
f : X ⊕ Y → Z_1
h : (IsClosedMap.{u, u_2} (Y := Z_1) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z_1) fun (b : Y) ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[inst] (inl ⁻¹' Z) ∧ IsClosed[inst_1] (inr ⁻¹' Z)
⊢ IsClosed[inst_2] ((fun (a : X) ↦ f (inl a)) '' inl ⁻¹' Z ∪ (fun (b : Y) ↦ f (inr b)) '' inr ⁻¹' Z)

Tactic:
(h.1 _ hZ.1).union (h.2 _ hZ.2)

Premises used: IsClosed.union, And.right, And.left
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z_1 : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z_1
f : X ⊕ Y → Z_1
h : (IsClosedMap.{u, u_2} (Y := Z_1) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z_1) fun (b : Y) ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[inst] (inl ⁻¹' Z) ∧ IsClosed[inst_1] (inr ⁻¹' Z)
h₁ : f '' Z = (fun (a : X) ↦ f (inl a)) '' inl ⁻¹' Z ∪ (fun (b : Y) ↦ f (inr b)) '' inr ⁻¹' Z
⊢ IsClosed[inst_2] (f '' Z)

Tactic:
convert! (h.1 _ hZ.1).union (h.2 _ hZ.2)

Premises used: IsClosed.union, And.right, And.left
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z_1 : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z_1
f : X ⊕ Y → Z_1
h : (IsClosedMap.{u, u_2} (Y := Z_1) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z_1) fun (b : Y) ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[inst] (inl ⁻¹' Z) ∧ IsClosed[inst_1] (inr ⁻¹' Z)
h₁ :
  ∀ (x : Z_1),
    x ∈ f '' Z ↔
      Membership.mem (γ := Set Z_1) ((fun (a : X) ↦ f (inl a)) '' inl ⁻¹' Z ∪ (fun (b : Y) ↦ f (inr b)) '' inr ⁻¹' Z) x
⊢ f '' Z = (fun (a : X) ↦ f (inl a)) '' inl ⁻¹' Z ∪ (fun (b : Y) ↦ f (inr b)) '' inr ⁻¹' Z

Tactic:
ext
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z_1 : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z_1
f : X ⊕ Y → Z_1
h : (IsClosedMap.{u, u_2} (Y := Z_1) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z_1) fun (b : Y) ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[inst] (inl ⁻¹' Z) ∧ IsClosed[inst_1] (inr ⁻¹' Z)
x : Z_1
⊢ x ∈ f '' Z ↔
    Membership.mem (γ := Set Z_1) ((fun (a : X) ↦ f (inl a)) '' inl ⁻¹' Z ∪ (fun (b : Y) ↦ f (inr b)) '' inr ⁻¹' Z) x

Tactic:
simp only [mem_image, Sum.exists, mem_union, mem_preimage]

Premises used: Set.mem_union, Set.mem_image, Sum.exists, Set.mem_preimage
-- 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 W
inst_3 : TopologicalSpace Z
f : X → Y
g : Z → W
hf : IsClosedMap f
hg : IsClosedMap g
⊢ IsClosedMap (Sum.map f g)

Tactic:
isClosedMap_sum.2 ⟨isClosedMap_inl.comp hf, isClosedMap_inr.comp hg⟩

Premises used: Iff.mpr, isClosedMap_inr, isClosedMap_inl, And.intro, IsClosedMap.comp, isClosedMap_sum
-- 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
⊢ IsClosedMap (Sum.elim f g) ↔ IsClosedMap f ∧ IsClosedMap g

Tactic:
simp only [isClosedMap_sum, Sum.elim_inl, Sum.elim_inr]

Premises used: Sum.elim_inr, Sum.elim_inl, isClosedMap_sum
-- 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 : IsClosedMap f
hg : IsClosedMap g
⊢ IsClosedMap (Sum.elim f g)

Tactic:
isClosedMap_sumElim.2 ⟨hf, hg⟩

Premises used: Iff.mpr, isClosedMap_sumElim, And.intro
-- 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 : IsClosedEmbedding f
hg : IsClosedEmbedding g
h : Injective (Sum.elim f g)
rw :
  ∀ (hf : Continuous[inst, inst_2] f ∧ Injective f ∧ IsClosedMap f)
    (hg : Continuous[inst_1, inst_2] g ∧ Injective g ∧ IsClosedMap g) (h : Injective (Sum.elim f g)),
    Continuous[instTopologicalSpaceSum, inst_2] (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsClosedMap (Sum.elim f g)
⊢ IsClosedEmbedding (Sum.elim f g)

Tactic:
rw [IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap] at hf hg ⊢

Premises used: Topology.IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap
-- 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 ∧ Injective f ∧ IsClosedMap f
hg : Continuous[inst_1, inst_2] g ∧ Injective g ∧ IsClosedMap g
h : Injective (Sum.elim f g)
⊢ Continuous[instTopologicalSpaceSum, inst_2] (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsClosedMap (Sum.elim f g)

Tactic:
⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩

Premises used: IsClosedMap.sumElim, And.right, And.left, And.intro, Continuous.sumElim
-- 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 ∧ Injective f ∧ IsClosedMap f
hg : Continuous[inst_1, inst_2] g ∧ Injective g ∧ IsClosedMap g
h : Injective (Sum.elim f g)
⊢ Continuous[instTopologicalSpaceSum, inst_2] (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsClosedMap (Sum.elim f g)

Tactic:
exact ⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩
-- 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₁.sumCongr h₂).symm = h₁.symm.sumCongr h₂.symm

Tactic:
rfl

Premises used: Sum.map, Equiv.sumCongr, Homeomorph.symm, Equiv.symm, Homeomorph.sumCongr, rfl, Sum.elim
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
H :
  ∀ (i : X ⊕ Y),
    Eq (α := X ⊕ Y) ((sumCongr (Homeomorph.refl X) (Homeomorph.refl Y) : (a : X ⊕ Y) → X ⊕ Y) i : X ⊕ Y)
      ((Homeomorph.refl (X ⊕ Y) : (a : X ⊕ Y) → X ⊕ Y) i : X ⊕ Y)
⊢ Eq (α := X ⊕ Y ≃ₜ X ⊕ Y) (sumCongr (Homeomorph.refl X) (Homeomorph.refl Y)) (Homeomorph.refl (X ⊕ Y))

Tactic:
ext i
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
i : X ⊕ Y
H :
  ∀ (val : X),
    Eq (α := X ⊕ Y) ((sumCongr (Homeomorph.refl X) (Homeomorph.refl Y) : (a : X ⊕ Y) → X ⊕ Y) (inl val) : X ⊕ Y)
      ((Homeomorph.refl (X ⊕ Y) : (a : X ⊕ Y) → X ⊕ Y) (inl val) : X ⊕ Y)
H₁ :
  ∀ (val : Y),
    Eq (α := X ⊕ Y) ((sumCongr (Homeomorph.refl X) (Homeomorph.refl Y) : (a : X ⊕ Y) → X ⊕ Y) (inr val) : X ⊕ Y)
      ((Homeomorph.refl (X ⊕ Y) : (a : X ⊕ Y) → X ⊕ Y) (inr val) : X ⊕ Y)
⊢ Eq (α := X ⊕ Y) ((sumCongr (Homeomorph.refl X) (Homeomorph.refl Y) : (a : X ⊕ Y) → X ⊕ Y) i : X ⊕ Y)
    ((Homeomorph.refl (X ⊕ Y) : (a : X ⊕ Y) → X ⊕ Y) i : X ⊕ Y)

Tactic:
cases i
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
val : X
⊢ Eq (α := X ⊕ Y) ((sumCongr (Homeomorph.refl X) (Homeomorph.refl Y) : (a : X ⊕ Y) → X ⊕ Y) (inl val) : X ⊕ Y)
    ((Homeomorph.refl (X ⊕ Y) : (a : X ⊕ Y) → X ⊕ Y) (inl val) : X ⊕ Y)

Tactic:
rfl
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
val : Y
⊢ Eq (α := X ⊕ Y) ((sumCongr (Homeomorph.refl X) (Homeomorph.refl Y) : (a : X ⊕ Y) → X ⊕ Y) (inr val) : X ⊕ Y)
    ((Homeomorph.refl (X ⊕ Y) : (a : X ⊕ Y) → X ⊕ Y) (inr val) : X ⊕ Y)

Tactic:
rfl
-- 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'
X'' : Type u_7
Y'' : Type u_8
inst_4 : TopologicalSpace X''
inst_5 : TopologicalSpace Y''
h₁ : X ≃ₜ X'
h₂ : Y ≃ₜ Y'
h₃ : X' ≃ₜ X''
h₄ : Y' ≃ₜ Y''
H :
  ∀ (i : X ⊕ Y),
    Eq (α := X'' ⊕ Y'') (((h₁.sumCongr h₂).trans (h₃.sumCongr h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') i : X'' ⊕ Y'')
      (((h₁.trans h₃).sumCongr (h₂.trans h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') i : X'' ⊕ Y'')
⊢ (h₁.sumCongr h₂).trans (h₃.sumCongr h₄) = (h₁.trans h₃).sumCongr (h₂.trans h₄)

Tactic:
ext i
-- 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'
X'' : Type u_7
Y'' : Type u_8
inst_4 : TopologicalSpace X''
inst_5 : TopologicalSpace Y''
h₁ : X ≃ₜ X'
h₂ : Y ≃ₜ Y'
h₃ : X' ≃ₜ X''
h₄ : Y' ≃ₜ Y''
i : X ⊕ Y
H :
  ∀ (val : X),
    Eq (α := X'' ⊕ Y'') (((h₁.sumCongr h₂).trans (h₃.sumCongr h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') (inl val) : X'' ⊕ Y'')
      (((h₁.trans h₃).sumCongr (h₂.trans h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') (inl val) : X'' ⊕ Y'')
H₁ :
  ∀ (val : Y),
    Eq (α := X'' ⊕ Y'') (((h₁.sumCongr h₂).trans (h₃.sumCongr h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') (inr val) : X'' ⊕ Y'')
      (((h₁.trans h₃).sumCongr (h₂.trans h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') (inr val) : X'' ⊕ Y'')
⊢ Eq (α := X'' ⊕ Y'') (((h₁.sumCongr h₂).trans (h₃.sumCongr h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') i : X'' ⊕ Y'')
    (((h₁.trans h₃).sumCongr (h₂.trans h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') i : X'' ⊕ Y'')

Tactic:
cases i
-- 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'
X'' : Type u_7
Y'' : Type u_8
inst_4 : TopologicalSpace X''
inst_5 : TopologicalSpace Y''
h₁ : X ≃ₜ X'
h₂ : Y ≃ₜ Y'
h₃ : X' ≃ₜ X''
h₄ : Y' ≃ₜ Y''
val : X
⊢ Eq (α := X'' ⊕ Y'') (((h₁.sumCongr h₂).trans (h₃.sumCongr h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') (inl val) : X'' ⊕ Y'')
    (((h₁.trans h₃).sumCongr (h₂.trans h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') (inl val) : X'' ⊕ Y'')

Tactic:
rfl