-- Mathlib/Topology/ExtremallyDisconnected.lean
theorem CompactT2.ExtremallyDisconnected.projective [ExtremallyDisconnected A]
    [CompactSpace A] [T2Space A] : CompactT2.Projective A

Proof state:
case intro.intro.intro
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ
⊢ ∃ h, Continuous h ∧ f ∘ h = φ

Tactic:
let ρ : E → A := E.restrict π₁

Result:
case intro.intro.intro
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ
ρ : ↑E → A := E.restrict π₁
⊢ ∃ h, Continuous h ∧ f ∘ h = φ

Proof state:
case intro.intro.intro
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ
ρ : ↑E → A := E.restrict π₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
⊢ ∃ h, Continuous h ∧ f ∘ h = φ

Tactic:
let π₂ : D → B := Prod.snd ∘ Subtype.val

Result:
case intro.intro.intro
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ
ρ : ↑E → A := E.restrict π₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
π₂ : ↑D → B := Prod.snd ∘ Subtype.val
⊢ ∃ h, Continuous h ∧ f ∘ h = φ

Proof state:
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
⊢ ∃ h, Continuous h ∧ f ∘ h = φ

Tactic:
have π₁_surj : π₁.Surjective := fun a => ⟨⟨⟨a, _⟩, (f_surj <| φ a).choose_spec.symm⟩, rfl⟩

Result:
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
⊢ ∃ h, Continuous h ∧ f ∘ h = φ

Proof state:
case intro.intro.intro
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ
ρ : ↑E → A := E.restrict π₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
⊢ ∃ h, Continuous h ∧ f ∘ h = φ

Tactic:
let ρ' := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min

Result:
case intro.intro.intro
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ
ρ : ↑E → A := E.restrict π₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
⊢ ∃ h, Continuous h ∧ f ∘ h = φ

Proof state:
case intro.intro.intro
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ
ρ : ↑E → A := E.restrict π₁
⊢ ∃ h, Continuous h ∧ f ∘ h = φ

Tactic:
have ρ_cont : Continuous ρ := π₁_cont.continuousOn.restrict

Result:
case intro.intro.intro
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
π₁ : ↑D → A := Prod.fst ∘ Subtype.val
π₁_cont : Continuous π₁
π₁_surj : Surjective π₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : π₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ
ρ : ↑E → A := E.restrict π₁
ρ_cont : Continuous ρ
⊢ ∃ h, Continuous h ∧ f ∘ h = φ