awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
inst_2 : ExtremallyDisconnected A
inst_3 : T2Space A
inst_4 : T2Space E
inst_5 : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
disj' : Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ
disj'' : Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ)
hx₁' : ρ x₁ ∈ closure (ρ '' G₁ᶜ)ᶜ
⊢ ρ x₂ ∈ closure (ρ '' G₂ᶜ)ᶜ

Tactic:
have hx₂' := image_subset_closure_compl_image_compl_of_isOpen ρ_cont ρ_surj zorn_subset G₂_open <|
    mem_image_of_mem ρ hx₂
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
inst_2 : ExtremallyDisconnected A
inst_3 : T2Space A
inst_4 : T2Space E
inst_5 : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
disj' : Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ
disj'' : Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ)
hx₁' : ρ x₁ ∈ closure (ρ '' G₁ᶜ)ᶜ
hx₂' : ρ x₂ ∈ closure (ρ '' G₂ᶜ)ᶜ
⊢ False

Tactic:
disj''.ne_of_mem hx₁' hx₂' hρx

Premises used: Disjoint.ne_of_mem
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A E : Type u
inst : TopologicalSpace A
inst_1 : TopologicalSpace E
inst_2 : ExtremallyDisconnected A
inst_3 : T2Space A
inst_4 : T2Space E
inst_5 : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
disj' : Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ
disj'' : Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ)
hx₁' : ρ x₁ ∈ closure (ρ '' G₁ᶜ)ᶜ
hx₂' : ρ x₂ ∈ closure (ρ '' G₂ᶜ)ᶜ
⊢ False

Tactic:
exact disj''.ne_of_mem hx₁' hx₂' hρx

Premises used: Disjoint.ne_of_mem
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
_ :
  ∀ [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] [CompactSpace B] [T2Space B] [CompactSpace C]
    [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ (h : A → B), Continuous h ∧ g ∘ h = f
⊢ ∀ [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] [CompactSpace B] [T2Space B] [CompactSpace C]
    [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ (h : A → B), Continuous h ∧ g ∘ h = f

Tactic:
_
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
_ :
  ∀ [inst_5 : TopologicalSpace C] [CompactSpace B] [T2Space B] [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ (h : A → B), Continuous h ∧ g ∘ h = f
⊢ ∀ [inst_5 : TopologicalSpace C] [CompactSpace B] [T2Space B] [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ (h : A → B), Continuous h ∧ g ∘ h = f

Tactic:
_
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
_ :
  ∀ [CompactSpace B] [T2Space B] [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ (h : A → B), Continuous h ∧ g ∘ h = f
⊢ ∀ [CompactSpace B] [T2Space B] [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ (h : A → B), Continuous h ∧ g ∘ h = f

Tactic:
_
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
_ :
  ∀ [T2Space B] [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ (h : A → B), Continuous h ∧ g ∘ h = f
⊢ ∀ [T2Space B] [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ (h : A → B), Continuous h ∧ g ∘ h = f

Tactic:
_
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
_ :
  ∀ [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ (h : A → B), Continuous h ∧ g ∘ h = f
⊢ ∀ [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ (h : A → B), Continuous h ∧ g ∘ h = f

Tactic:
_
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
_ :
  ∀ [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ (h : A → B), Continuous h ∧ g ∘ h = f
⊢ ∀ [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ (h : A → B), Continuous h ∧ g ∘ h = f

Tactic:
_
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
⊢ CompactSpace.{u} (↑D : Type u)

Tactic:
have D_comp : CompactSpace D := isCompact_iff_compactSpace.mp
    (isClosed_eq (φ_cont.comp continuous_fst) (f_cont.comp continuous_snd)).isCompact
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
⊢ Continuous X₁

Tactic:
have X₁_cont : Continuous X₁ := continuous_fst.comp continuous_subtype_val
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
⊢ Surjective X₁

Tactic:
have X₁_surj : X₁.Surjective := fun a => ⟨⟨⟨a, _⟩, (f_surj <| φ a).choose_spec.symm⟩, rfl⟩
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
rcases :
  ∀ (E : Set (↑D : Type u)),
    CompactSpace.{u} (↑E : Type u) →
      ∀ (E_onto : X₁ '' E = univ)
        (E_min :
          ∀ (E₀ : Set (↑E : Type u)),
            E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ),
        ∃ (h : A → B), Continuous h ∧ f ∘ h = φ
⊢ ∃ (h : A → B), Continuous h ∧ f ∘ h = φ

Tactic:
rcases exists_compact_surjective_zorn_subset X₁_cont X₁_surj with ⟨E, _, E_onto, E_min⟩

Premises used: exists_compact_surjective_zorn_subset
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
⊢ Continuous ρ

Tactic:
have ρ_cont : Continuous ρ := X₁_cont.continuousOn.restrict
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
a : A
rcases : ∀ (d : (↑D : Type u)) (hd : d ∈ E), ∃ (a : (↑E : Type u)), ρ a = X₁ d
⊢ ∃ (a_1 : (↑E : Type u)), ρ a_1 = a

Tactic:
rcases (E_onto ▸ mem_univ a : a ∈ X₁ '' E) with ⟨d, ⟨hd, rfl⟩⟩

Premises used: Eq.rec, Set.mem_univ, Eq.symm, rfl
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
d : (↑D : Type u)
hd : d ∈ E
⊢ ∃ (a : (↑E : Type u)), ρ a = X₁ d

Tactic:
⟨⟨d, hd⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
d : (↑D : Type u)
hd : d ∈ E
⊢ ∃ (a : (↑E : Type u)), ρ a = X₁ d

Tactic:
exact ⟨⟨d, hd⟩, rfl⟩
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
⊢ Surjective ρ

Tactic:
have ρ_surj : ρ.Surjective := fun a => by
    rcases (E_onto ▸ mem_univ a : a ∈ X₁ '' E) with ⟨d, ⟨hd, rfl⟩⟩; exact ⟨⟨d, hd⟩, rfl⟩
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
⊢ Continuous X₂

Tactic:
have X₂_cont : Continuous X₂ := continuous_snd.comp continuous_subtype_val
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
⊢ ∃ (h : A → B), Continuous h ∧ f ∘ h = φ

Tactic:
⟨E.restrict X₂ ∘ ρ'.symm, ⟨X₂_cont.continuousOn.restrict.comp ρ'.symm.continuous, ?_⟩⟩

Premises used: Continuous.continuousOn, Homeomorph.continuous, Continuous.comp, Function.comp, Homeomorph.symm, And.intro, ContinuousOn.restrict, Exists.intro, Set.restrict, DFunLike.coe
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
refine : f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
⊢ ∃ (h : A → B), Continuous h ∧ f ∘ h = φ

Tactic:
refine ⟨E.restrict X₂ ∘ ρ'.symm, ⟨X₂_cont.continuousOn.restrict.comp ρ'.symm.continuous, ?_⟩⟩
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
this : f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ = φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)
rw : (f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂) ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
rw₁ : comp (β := (↑E : Type u)) (φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)) (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
rw₂ : φ ∘ comp (β := (↑E : Type u)) (⇑ρ' : (a : (↑E : Type u)) → A) (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
rw₃ : φ ∘ id = φ
rw₄ rw₅ : φ = φ
⊢ f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ

Tactic:
rw [← comp_assoc, this, comp_assoc, Homeomorph.self_comp_symm, comp_id]

Premises used: Function.comp_id, Homeomorph.self_comp_symm, Function.comp_assoc
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
suffices : f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ = φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)
⊢ f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ

Tactic:
suffices f ∘ E.restrict X₂ = φ ∘ ρ' by
    rw [← comp_assoc, this, comp_assoc, Homeomorph.self_comp_symm, comp_id]
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
h :
  ∀ (x : (↑E : Type u)),
    (f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂) x = (φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)) x
⊢ f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ = φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)

Tactic:
ext x