Theorem: image_subset_closure_compl_image_compl (ExtrDisc/Gleason.lean)

State before:
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
⊢ ρ '' G ⊆ closure ((ρ '' Gᶜ)ᶜ)
Tactic:
by_cases G_empty : G = ∅
State after:
case pos
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : G = ∅
⊢ ρ '' G ⊆ closure ((ρ '' Gᶜ)ᶜ)

case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
⊢ ρ '' G ⊆ closure ((ρ '' Gᶜ)ᶜ)

State before:
case pos
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : G = ∅
⊢ ρ '' G ⊆ closure ((ρ '' Gᶜ)ᶜ)
Tactic:
simpa only [G_empty, image_empty] using empty_subset _
State after:
no goals

State before:
case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
⊢ ρ '' G ⊆ closure ((ρ '' Gᶜ)ᶜ)
Tactic:
intro a ha
State after:
case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
⊢ a ∈ closure ((ρ '' Gᶜ)ᶜ)

State before:
case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
⊢ a ∈ closure ((ρ '' Gᶜ)ᶜ)
Tactic:
rw [mem_closure_iff]
State after:
case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
⊢ ∀ (o : Set A), IsOpen o → a ∈ o → Set.Nonempty (o ∩ (ρ '' Gᶜ)ᶜ)

State before:
case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
⊢ ∀ (o : Set A), IsOpen o → a ∈ o → Set.Nonempty (o ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
intro N hN ha'
State after:
case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
N : Set A
hN : IsOpen N
ha' : a ∈ N
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)

State before:
case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
N : Set A
hN : IsOpen N
ha' : a ∈ N
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
rcases (G.mem_image ρ a).mp ha with ⟨e, he, rfl⟩
State after:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)

State before:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
have non_empty : (G ∩ ρ⁻¹' N).Nonempty := ⟨e, mem_inter he <| mem_preimage.mpr ha'⟩
State after:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)

State before:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
have is_open : IsOpen <| G ∩ ρ⁻¹' N := hG.inter <| hN.preimage ρ_cont
State after:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)

State before:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
have ne_top : ρ '' (G ∩ ρ⁻¹' N)ᶜ ≠ ⊤ := image_ne_top _ (compl_ne_univ.mpr non_empty)
                                          is_open.isClosed_compl
State after:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)

State before:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
rcases nonempty_compl.mpr ne_top with ⟨x, hx⟩
State after:
case neg.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)

State before:
case neg.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
have hx' : x ∈ (ρ '' Gᶜ)ᶜ := (compl_subset_compl.mpr <| image_subset ρ <|
                                compl_subset_compl.mpr <| G.inter_subset_left _) hx
State after:
case neg.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : x ∈ (ρ '' Gᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)

State before:
case neg.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : x ∈ (ρ '' Gᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
rcases ρ_surj x with ⟨y, rfl⟩
State after:
case neg.intro.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
y : ↑E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)

State before:
case neg.intro.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
y : ↑E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
have hy : y ∈ G ∩ ρ⁻¹' N := not_mem_compl_iff.mp <| (not_imp_not.mpr <| mem_image_of_mem ρ) <|
                              (mem_compl_iff _ _).mp hx
State after:
case neg.intro.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
y : ↑E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
hy : y ∈ G ∩ ρ ⁻¹' N
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)

State before:
case neg.intro.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
E : Set D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
y : ↑E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
hy : y ∈ G ∩ ρ ⁻¹' N
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
exact ⟨ρ y, mem_inter (mem_preimage.mp <| mem_of_mem_inter_right hy) hx'⟩
State after:
no goals