Theorem: compact_to_T2_injective (ExtrDisc/Gleason.lean)

State before:
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
⊢ Function.Injective ρ
Tactic:
intro x y h_eq_im
State after:
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
⊢ x = y

State before:
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
⊢ x = y
Tactic:
by_contra h
State after:
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
⊢ False

State before:
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
⊢ False
Tactic:
rcases t2_separation h with ⟨G₁, G₂, hG₁, hG₂, hxG₁, hyG₂, hG⟩
State after:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ False
Tactic:
have open1 : IsOpen ((ρ '' (G₁ᶜ))ᶜ)
State after:
case open1
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsOpen ((ρ '' G₁ᶜ)ᶜ)

case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ False
Tactic:
have open2 : IsOpen ((ρ '' (G₂ᶜ))ᶜ)
State after:
case open2
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ IsOpen ((ρ '' G₂ᶜ)ᶜ)

case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ False
Tactic:
have disj : Disjoint ((ρ '' (G₁ᶜ))ᶜ) ((ρ '' (G₂ᶜ))ᶜ)
State after:
case disj
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ Disjoint ((ρ '' G₁ᶜ)ᶜ) ((ρ '' G₂ᶜ)ᶜ)

case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint ((ρ '' G₁ᶜ)ᶜ) ((ρ '' G₂ᶜ)ᶜ)
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint ((ρ '' G₁ᶜ)ᶜ) ((ρ '' G₂ᶜ)ᶜ)
⊢ False
Tactic:
replace disj := disjoint_of_extremally_disconnected disj open1 open2
State after:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
⊢ False
Tactic:
have oups₁ := image_subset_closure_compl_image_compl ρ_cont ρ_surj image_ne_top hG₁
State after:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
⊢ False
Tactic:
have oups₂ := image_subset_closure_compl_image_compl ρ_cont ρ_surj image_ne_top hG₂
State after:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
⊢ False
Tactic:
have mem₁ : ρ x ∈ ρ '' G₁
State after:
case mem₁
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
⊢ ρ x ∈ ρ '' G₁

case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
⊢ False
Tactic:
have mem₂ : ρ x ∈ ρ '' G₂
State after:
case mem₂
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
⊢ ρ x ∈ ρ '' G₂

case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
mem₂ : ρ x ∈ ρ '' G₂
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
mem₂ : ρ x ∈ ρ '' G₂
⊢ False
Tactic:
have mem : ρ x ∈ (closure ((ρ '' G₁ᶜ)ᶜ)) ∩ (closure ((ρ '' G₂ᶜ)ᶜ)) := ⟨oups₁ mem₁, oups₂ mem₂⟩
State after:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
mem₂ : ρ x ∈ ρ '' G₂
mem : ρ x ∈ closure ((ρ '' G₁ᶜ)ᶜ) ∩ closure ((ρ '' G₂ᶜ)ᶜ)
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
mem₂ : ρ x ∈ ρ '' G₂
mem : ρ x ∈ closure ((ρ '' G₁ᶜ)ᶜ) ∩ closure ((ρ '' G₂ᶜ)ᶜ)
⊢ False
Tactic:
exact (disj.ne_of_mem mem.1 mem.2) rfl
State after:
no goals

State before:
case open1
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsOpen ((ρ '' G₁ᶜ)ᶜ)
Tactic:
simp only [isOpen_compl_iff]
State after:
case open1
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsClosed (ρ '' G₁ᶜ)

State before:
case open1
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsClosed (ρ '' G₁ᶜ)
Tactic:
apply IsCompact.isClosed
State after:
case open1.hs
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsCompact (ρ '' G₁ᶜ)

State before:
case open1.hs
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsCompact (ρ '' G₁ᶜ)
Tactic:
refine' IsCompact.image (IsClosed.isCompact _) ρ_cont
State after:
case open1.hs
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsClosed (G₁ᶜ)

State before:
case open1.hs
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsClosed (G₁ᶜ)
Tactic:
simpa only [isClosed_compl_iff]
State after:
no goals

State before:
case open2
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ IsOpen ((ρ '' G₂ᶜ)ᶜ)
Tactic:
simp only [isOpen_compl_iff]
State after:
case open2
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ IsClosed (ρ '' G₂ᶜ)

State before:
case open2
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ IsClosed (ρ '' G₂ᶜ)
Tactic:
apply IsCompact.isClosed
State after:
case open2.hs
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ IsCompact (ρ '' G₂ᶜ)

State before:
case open2.hs
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ IsCompact (ρ '' G₂ᶜ)
Tactic:
refine' IsCompact.image (IsClosed.isCompact _) ρ_cont
State after:
case open2.hs
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ IsClosed (G₂ᶜ)

State before:
case open2.hs
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ IsClosed (G₂ᶜ)
Tactic:
simpa only [isClosed_compl_iff]
State after:
no goals

State before:
case disj
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ Disjoint ((ρ '' G₁ᶜ)ᶜ) ((ρ '' G₂ᶜ)ᶜ)
Tactic:
rw [disjoint_compl_left_iff_subset]
State after:
case disj
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ (ρ '' G₂ᶜ)ᶜ ⊆ ρ '' G₁ᶜ

State before:
case disj
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ (ρ '' G₂ᶜ)ᶜ ⊆ ρ '' G₁ᶜ
Tactic:
refine' subset_trans (subset_image_compl ρ_surj) _
State after:
case disj
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ ρ '' G₂ᶜᶜ ⊆ ρ '' G₁ᶜ

State before:
case disj
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ ρ '' G₂ᶜᶜ ⊆ ρ '' G₁ᶜ
Tactic:
simp only [compl_compl, image_subset_iff]
State after:
case disj
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ G₂ ⊆ ρ ⁻¹' (ρ '' G₁ᶜ)

State before:
case disj
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ G₂ ⊆ ρ ⁻¹' (ρ '' G₁ᶜ)
Tactic:
refine' subset_trans _ (subset_preimage_image _ _)
State after:
case disj
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ G₂ ⊆ G₁ᶜ

State before:
case disj
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ G₂ ⊆ G₁ᶜ
Tactic:
rw [← disjoint_compl_left_iff_subset]
State after:
case disj
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ Disjoint (G₁ᶜᶜ) G₂

State before:
case disj
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ Disjoint (G₁ᶜᶜ) G₂
Tactic:
simpa only [compl_compl]
State after:
no goals

State before:
case mem₁
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
⊢ ρ x ∈ ρ '' G₁
Tactic:
exact mem_image_of_mem _ hxG₁
State after:
no goals

State before:
case mem₂
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
⊢ ρ x ∈ ρ '' G₂
Tactic:
rw [h_eq_im]
State after:
case mem₂
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
⊢ ρ y ∈ ρ '' G₂

State before:
case mem₂
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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₀ ≠ ⊤
inst✝³ : T2Space A
inst✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
⊢ ρ y ∈ ρ '' G₂
Tactic:
exact mem_image_of_mem _ hyG₂
State after:
no goals