-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.isQuotientMap {V : Set (Set X)} (hV : IsTopologicalBasis V)
    (h' : IsQuotientMap π) (h : IsOpenMap π) : IsTopologicalBasis (Set.image π '' V)

Proof state:
case h_nhds.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
πZ_in_U : π '' Z ⊆ U
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Tactic:
exact ⟨π '' Z, ⟨Z, Z_in_V, rfl⟩, ⟨x, x_in_Z, rfl⟩, πZ_in_U⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
⊢ IsTopologicalBasis (image π '' V)

Tactic:
apply isTopologicalBasis_of_isOpen_of_nhds

Result:
case h_open
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
⊢ ∀ u ∈ image π '' V, IsOpen u

case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
⊢ ∀ (a : Y) (u : Set Y), a ∈ u → IsOpen u → ∃ v ∈ image π '' V, a ∈ v ∧ v ⊆ u

Proof state:
case h_nhds.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Tactic:
have W_open : IsOpen W := U_open.preimage h'.continuous

Result:
case h_nhds.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Proof state:
case h_nhds.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Tactic:
let W := π ⁻¹' U

Result:
case h_nhds.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Proof state:
case h_open
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
⊢ ∀ u ∈ image π '' V, IsOpen u

Tactic:
rintro - ⟨U, U_in_V, rfl⟩

Result:
case h_open.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set X
U_in_V : U ∈ V
⊢ IsOpen (π '' U)

Proof state:
case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
y : Y
U : Set Y
y_in_U : y ∈ U
U_open : IsOpen U
⊢ ∃ v ∈ image π '' V, y ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨x, rfl⟩ := h'.surjective y

Result:
case h_nhds.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Proof state:
case h_nhds.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Tactic:
have x_in_W : x ∈ W := y_in_U

Result:
case h_nhds.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Proof state:
case h_open.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set X
U_in_V : U ∈ V
⊢ IsOpen (π '' U)

Tactic:
apply h U (hV.isOpen U_in_V)

Result:
no goals

Proof state:
case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
⊢ ∀ (a : Y) (u : Set Y), a ∈ u → IsOpen u → ∃ v ∈ image π '' V, a ∈ v ∧ v ⊆ u

Tactic:
intro y U y_in_U U_open

Result:
case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
y : Y
U : Set Y
y_in_U : y ∈ U
U_open : IsOpen U
⊢ ∃ v ∈ image π '' V, y ∈ v ∧ v ⊆ U

Proof state:
case h_nhds.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨Z, Z_in_V, x_in_Z, Z_in_W⟩ := hV.exists_subset_of_mem_open x_in_W W_open

Result:
case h_nhds.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Proof state:
case h_nhds.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Tactic:
have πZ_in_U : π '' Z ⊆ U := (Set.image_subset _ Z_in_W).trans (image_preimage_subset π U)

Result:
case h_nhds.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
πZ_in_U : π '' Z ⊆ U
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U