-- Mathlib/Topology/Constructions.lean
theorem isClosedMap_sum {f : X ⊕ Y → Z} :
    IsClosedMap f ↔ (IsClosedMap fun a => f (.inl a)) ∧ IsClosedMap fun b => f (.inr b)

Proof state:
case mpr
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
⊢ ((IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)) → IsClosedMap f

Tactic:
rintro h Z hZ

Result:
case mpr
X : Type u
Y : Type v
Z✝ : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed Z
⊢ IsClosed (f '' Z)

Proof state:
case mpr
X : Type u
Y : Type v
Z✝ : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed (inl ⁻¹' Z) ∧ IsClosed (inr ⁻¹' Z)
⊢ IsClosed (f '' Z)

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

Result:
case h.e'_3
X : Type u
Y : Type v
Z✝ : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed (inl ⁻¹' Z) ∧ IsClosed (inr ⁻¹' Z)
⊢ f '' Z = (fun a => f (inl a)) '' (inl ⁻¹' Z) ∪ (fun b => f (inr b)) '' (inr ⁻¹' Z)

Proof state:
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
⊢ IsClosedMap f ↔ (IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)

Tactic:
constructor

Result:
case mp
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
⊢ IsClosedMap f → (IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)

case mpr
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
⊢ ((IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)) → IsClosedMap f

Proof state:
case mp
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
h : IsClosedMap f
⊢ (IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)

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

Result:
no goals

Proof state:
case mpr
X : Type u
Y : Type v
Z✝ : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed Z
⊢ IsClosed (f '' Z)

Tactic:
rw [isClosed_sum_iff] at hZ

Result:
case mpr
X : Type u
Y : Type v
Z✝ : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed (inl ⁻¹' Z) ∧ IsClosed (inr ⁻¹' Z)
⊢ IsClosed (f '' Z)

Proof state:
case h.e'_3
X : Type u
Y : Type v
Z✝ : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed (inl ⁻¹' Z) ∧ IsClosed (inr ⁻¹' Z)
⊢ f '' Z = (fun a => f (inl a)) '' (inl ⁻¹' Z) ∪ (fun b => f (inr b)) '' (inr ⁻¹' Z)

Tactic:
ext

Result:
case h.e'_3.h
X : Type u
Y : Type v
Z✝ : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed (inl ⁻¹' Z) ∧ IsClosed (inr ⁻¹' Z)
x✝ : Z✝
⊢ x✝ ∈ f '' Z ↔ x✝ ∈ (fun a => f (inl a)) '' (inl ⁻¹' Z) ∪ (fun b => f (inr b)) '' (inr ⁻¹' Z)

Proof state:
case h.e'_3.h
X : Type u
Y : Type v
Z✝ : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z✝
f : X ⊕ Y → Z✝
h : (IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed (inl ⁻¹' Z) ∧ IsClosed (inr ⁻¹' Z)
x✝ : Z✝
⊢ x✝ ∈ f '' Z ↔ x✝ ∈ (fun a => f (inl a)) '' (inl ⁻¹' Z) ∪ (fun b => f (inr b)) '' (inr ⁻¹' Z)

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

Result:
no goals

Proof state:
case mp
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
⊢ IsClosedMap f → (IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)

Tactic:
intro h

Result:
case mp
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
h : IsClosedMap f
⊢ (IsClosedMap fun a => f (inl a)) ∧ IsClosedMap fun b => f (inr b)