-- Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
/-- Let `f : X → Y`. Suppose that to prove that `f` is continuous, it suffices to show that
for every compact Hausdorff space `K` and every continuous map `g : K → X`, `f ∘ g` is continuous.
Then `X` is compactly generated. -/
lemma uCompactlyGeneratedSpace_of_continuous_maps [t : TopologicalSpace X]
    (h : ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
      (∀ (S : CompHaus.{u}) (g : C(S, X)), Continuous (f ∘ g)) → Continuous f) :
        UCompactlyGeneratedSpace.{u} X where
  le_compactlyGenerated

Proof state:
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
⊢ t ≤ compactlyGenerated X

Tactic:
suffices Continuous[t, compactlyGenerated.{u} X] (id : X → X) by
  rwa [← continuous_id_iff_le]

Result:
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
⊢ Continuous id

Proof state:
case a
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
S : CompHaus
g : C(↑S.toTop, X)
f : (i : (T : CompHaus) × C(↑T.toTop, X)) × ↑i.fst.toTop → X :=
  fun x =>
    match x with
    | ⟨⟨fst, i⟩, s⟩ => i s
⊢ Continuous (id ∘ ⇑g)

Tactic:
suffices ∀ (i : (T : CompHaus.{u}) × C(T, X)),
  Continuous[inferInstance, compactlyGenerated X] (fun (a : i.fst) ↦ f ⟨i, a⟩) from this ⟨S, g⟩

Result:
case a
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
S : CompHaus
g : C(↑S.toTop, X)
f : (i : (T : CompHaus) × C(↑T.toTop, X)) × ↑i.fst.toTop → X :=
  fun x =>
    match x with
    | ⟨⟨fst, i⟩, s⟩ => i s
⊢ ∀ (i : (T : CompHaus) × C(↑T.toTop, X)), Continuous fun a => f ⟨i, a⟩

Proof state:
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
⊢ Continuous id

Tactic:
apply h (tY := compactlyGenerated.{u} X)

Result:
case a
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
⊢ ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (id ∘ ⇑g)

Proof state:
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
this : Continuous id
⊢ t ≤ compactlyGenerated X

Tactic:
rwa [← continuous_id_iff_le]

Result:
no goals

Proof state:
case a
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
⊢ ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (id ∘ ⇑g)

Tactic:
intro S g

Result:
case a
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
S : CompHaus
g : C(↑S.toTop, X)
⊢ Continuous (id ∘ ⇑g)

Proof state:
case a
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
S : CompHaus
g : C(↑S.toTop, X)
f : (i : (T : CompHaus) × C(↑T.toTop, X)) × ↑i.fst.toTop → X :=
  fun x =>
    match x with
    | ⟨⟨fst, i⟩, s⟩ => i s
⊢ ∀ (i : (T : CompHaus) × C(↑T.toTop, X)), Continuous fun a => f ⟨i, a⟩

Tactic:
rw [← @continuous_sigma_iff]

Result:
case a
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
S : CompHaus
g : C(↑S.toTop, X)
f : (i : (T : CompHaus) × C(↑T.toTop, X)) × ↑i.fst.toTop → X :=
  fun x =>
    match x with
    | ⟨⟨fst, i⟩, s⟩ => i s
⊢ Continuous f

Proof state:
case a
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
S : CompHaus
g : C(↑S.toTop, X)
⊢ Continuous (id ∘ ⇑g)

Tactic:
let f : (Σ (i : (T : CompHaus.{u}) × C(T, X)), i.fst) → X := fun ⟨⟨_, i⟩, s⟩ ↦ i s

Result:
case a
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
S : CompHaus
g : C(↑S.toTop, X)
f : (i : (T : CompHaus) × C(↑T.toTop, X)) × ↑i.fst.toTop → X :=
  fun x =>
    match x with
    | ⟨⟨fst, i⟩, s⟩ => i s
⊢ Continuous (id ∘ ⇑g)

Proof state:
case a
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
S : CompHaus
g : C(↑S.toTop, X)
f : (i : (T : CompHaus) × C(↑T.toTop, X)) × ↑i.fst.toTop → X :=
  fun x =>
    match x with
    | ⟨⟨fst, i⟩, s⟩ => i s
⊢ Continuous f

Tactic:
apply continuous_coinduced_rng

Result:
no goals