Theorem: exists_image_ne_top
Proof state before:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.12569
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✝³ : CompactSpace A
inst✝² : T2Space B
inst✝¹ : CompactSpace B
inst✝ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
this : CompactSpace ↑(D' φ f)
S : Set (Set ↑(D' φ f)) := {E | CompactSpace ↑E ∧ π₁ φ f '' E = univ}
Ch : Set (Set ↑(D' φ f))
h : Ch ⊆ S
hCh : IsChain (fun x x_1 => x ⊆ x_1) Ch
M : Set ↑(D' φ f) := ⋂₀ Ch
h₂ : Nonempty ↑Ch
x : A
x✝ : x ∈ univ
Z : ↑Ch → Set ↑(D' φ f) := fun X => ↑X ∩ π₁ φ f ⁻¹' {x}
assumps : ∀ (i : ↑Ch), Set.Nonempty (Z i) ∧ IsCompact (Z i) ∧ IsClosed (Z i)
⊢ Directed (fun x x_1 => x ⊇ x_1) ((fun X => X ∩ π₁ φ f ⁻¹' {x}) ∘ fun X => ↑X)
Tactic:
refine' Directed.mono_comp _ _ _
Proof state after:
case refine'_1
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.12569
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✝³ : CompactSpace A
inst✝² : T2Space B
inst✝¹ : CompactSpace B
inst✝ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
this : CompactSpace ↑(D' φ f)
S : Set (Set ↑(D' φ f)) := {E | CompactSpace ↑E ∧ π₁ φ f '' E = univ}
Ch : Set (Set ↑(D' φ f))
h : Ch ⊆ S
hCh : IsChain (fun x x_1 => x ⊆ x_1) Ch
M : Set ↑(D' φ f) := ⋂₀ Ch
h₂ : Nonempty ↑Ch
x : A
x✝ : x ∈ univ
Z : ↑Ch → Set ↑(D' φ f) := fun X => ↑X ∩ π₁ φ f ⁻¹' {x}
assumps : ∀ (i : ↑Ch), Set.Nonempty (Z i) ∧ IsCompact (Z i) ∧ IsClosed (Z i)
⊢ Set ↑(D' φ f) → Set ↑(D' φ f) → Prop

case refine'_2
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.12569
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✝³ : CompactSpace A
inst✝² : T2Space B
inst✝¹ : CompactSpace B
inst✝ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
this : CompactSpace ↑(D' φ f)
S : Set (Set ↑(D' φ f)) := {E | CompactSpace ↑E ∧ π₁ φ f '' E = univ}
Ch : Set (Set ↑(D' φ f))
h : Ch ⊆ S
hCh : IsChain (fun x x_1 => x ⊆ x_1) Ch
M : Set ↑(D' φ f) := ⋂₀ Ch
h₂ : Nonempty ↑Ch
x : A
x✝ : x ∈ univ
Z : ↑Ch → Set ↑(D' φ f) := fun X => ↑X ∩ π₁ φ f ⁻¹' {x}
assumps : ∀ (i : ↑Ch), Set.Nonempty (Z i) ∧ IsCompact (Z i) ∧ IsClosed (Z i)
⊢ ∀ ⦃x_1 y : Set ↑(D' φ f)⦄, ?refine'_1 x_1 y → x_1 ∩ π₁ φ f ⁻¹' {x} ⊇ y ∩ π₁ φ f ⁻¹' {x}

case refine'_3
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.12569
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✝³ : CompactSpace A
inst✝² : T2Space B
inst✝¹ : CompactSpace B
inst✝ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
this : CompactSpace ↑(D' φ f)
S : Set (Set ↑(D' φ f)) := {E | CompactSpace ↑E ∧ π₁ φ f '' E = univ}
Ch : Set (Set ↑(D' φ f))
h : Ch ⊆ S
hCh : IsChain (fun x x_1 => x ⊆ x_1) Ch
M : Set ↑(D' φ f) := ⋂₀ Ch
h₂ : Nonempty ↑Ch
x : A
x✝ : x ∈ univ
Z : ↑Ch → Set ↑(D' φ f) := fun X => ↑X ∩ π₁ φ f ⁻¹' {x}
assumps : ∀ (i : ↑Ch), Set.Nonempty (Z i) ∧ IsCompact (Z i) ∧ IsClosed (Z i)
⊢ Directed ?refine'_1 fun X => ↑X