-- Mathlib/Topology/LocalAtTarget.lean
theorem isOpenMap_iff_restrictPreimage :
    IsOpenMap f ↔ ∀ i, IsOpenMap ((U i).1.restrictPreimage f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)

Tactic:
refine ⟨fun h i ↦ h.restrictPreimage _, fun H s hs ↦ ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen s
⊢ IsOpen (f '' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen s
⊢ IsOpen (f '' s)

Tactic:
rw [hU.isOpen_iff_coe_preimage]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen s
⊢ ∀ (i : ι), IsOpen (Subtype.val ⁻¹' (f '' s))

Proof state:
case h.e'_3.h.h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
x : β
hx : x ∈ U i
⊢ (∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x

Tactic:
exact ⟨fun ⟨a, b, c⟩ ↦ ⟨a, b, c.symm ▸ hx, c⟩, by tauto⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen s
i : ι
⊢ IsOpen (Subtype.val ⁻¹' (f '' s))

Tactic:
convert H i _ (hs.preimage continuous_subtype_val)

Result:
case h.e'_3.h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
⊢ Subtype.val ⁻¹' (f '' s) = (U i).carrier.restrictPreimage f '' (Subtype.val ⁻¹' s)

Proof state:
case h.e'_3.h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
⊢ Subtype.val ⁻¹' (f '' s) = (U i).carrier.restrictPreimage f '' (Subtype.val ⁻¹' s)

Tactic:
ext ⟨x, hx⟩

Result:
case h.e'_3.h.h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
x : β
hx : x ∈ U i
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' (f '' s) ↔ ⟨x, hx⟩ ∈ (U i).carrier.restrictPreimage f '' (Subtype.val ⁻¹' s)

Proof state:
case h.e'_3.h.h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
x : β
hx : x ∈ U i
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' (f '' s) ↔ ⟨x, hx⟩ ∈ (U i).carrier.restrictPreimage f '' (Subtype.val ⁻¹' s)

Tactic:
suffices (∃ y, y ∈ s ∧ f y = x) ↔ ∃ y, y ∈ s ∧ f y ∈ U i ∧ f y = x by simpa [← Subtype.coe_inj]

Result:
case h.e'_3.h.h.mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
x : β
hx : x ∈ U i
⊢ (∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
x : β
hx : x ∈ U i
this : (∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' (f '' s) ↔ ⟨x, hx⟩ ∈ (U i).carrier.restrictPreimage f '' (Subtype.val ⁻¹' s)

Tactic:
simpa [← Subtype.coe_inj]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
x : β
hx : x ∈ U i
⊢ (∃ y ∈ s, f y ∈ U i ∧ f y = x) → ∃ y ∈ s, f y = x

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen s
⊢ ∀ (i : ι), IsOpen (Subtype.val ⁻¹' (f '' s))

Tactic:
intro i

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen s
i : ι
⊢ IsOpen (Subtype.val ⁻¹' (f '' s))