awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous[_, inst] f → IsOpen (f ⁻¹' s)
K : Set X
hK : IsCompact K
this : CompactSpace.{u} (↑K : Type u)
⊢ IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)

Tactic:
exact hs K Subtype.val continuous_subtype_val

Premises used: continuous_subtype_val, Set.Elem, Subtype.val
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] (f : K → X),
        Continuous[_, inst] f → IsOpen (f ⁻¹' s)) →
      IsOpen[inst] s
⊢ CompactlyCoherentSpace X

Tactic:
of_isOpen fun A hA ↦ h A fun K _ _ f hf ↦ ?_

Premises used: CompactlyCoherentSpace.of_isOpen
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] (f : K → X),
        Continuous[_, inst] f → IsOpen (f ⁻¹' s)) →
      IsOpen[inst] s
refine :
  ∀ (A : Set X) (hA : ∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ A)) (K : Type u)
    (x : TopologicalSpace K), CompactSpace K → ∀ (f : K → X) (hf : Continuous[_, inst] f), IsOpen (f ⁻¹' A)
⊢ CompactlyCoherentSpace X

Tactic:
refine of_isOpen fun A hA ↦ h A fun K _ _ f hf ↦ ?_

Premises used: CompactlyCoherentSpace.of_isOpen
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] (f : K → X),
        Continuous[_, inst] f → IsOpen (f ⁻¹' s)) →
      IsOpen[inst] s
A : Set X
hA : ∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ A)
K : Type u
x : TopologicalSpace K
h_1 : CompactSpace K
f : K → X
hf : Continuous[x, inst] f
⊢ IsOpen[instTopologicalSpaceSubtype] (range f ↓∩ A)

Tactic:
specialize hA (range f) (isCompact_range hf)

Premises used: isCompact_range, Set.range
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] (f : K → X),
        Continuous[_, inst] f → IsOpen (f ⁻¹' s)) →
      IsOpen[inst] s
A : Set X
K : Type u
x : TopologicalSpace K
h_1 : CompactSpace K
f : K → X
hf : Continuous[x, inst] f
hA : IsOpen[instTopologicalSpaceSubtype] (range f ↓∩ A)
⊢ IsOpen[x] (codRestrict f (range f) ⋯ ⁻¹' range f ↓∩ A)

Tactic:
have := hA.preimage (hf.codRestrict mem_range_self)
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] (f : K → X),
        Continuous[_, inst] f → IsOpen (f ⁻¹' s)) →
      IsOpen[inst] s
A : Set X
K : Type u
x : TopologicalSpace K
h_1 : CompactSpace K
f : K → X
hf : Continuous[x, inst] f
hA : IsOpen[instTopologicalSpaceSubtype] (range f ↓∩ A)
this : IsOpen[x] (codRestrict f (range f) ⋯ ⁻¹' range f ↓∩ A)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : IsOpen[x] (Subtype.val (p := fun (x : X) ↦ x ∈ range f) ∘ codRestrict f (range f) ⋯ ⁻¹' A)),
    IsOpen[x] (f ⁻¹' A)
⊢ IsOpen[x] (f ⁻¹' A)

Tactic:
rwa [← preimage_comp] at this

Premises used: Set.preimage_comp
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
⊢ CompactCoherentification.map f ∘ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) =
    (⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f

Tactic:
rfl
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set (𝐤X)
simp_rw :
  (∀ (i : Set X) (i_1 : IsCompact i),
      IsOpen[TopologicalSpace.coinduced Subtype.val
            { IsOpen := instTopologicalSpace._aux_1 i, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }]
        ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' A)) ↔
    ∀ (K : Set X),
      IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' A)
⊢ IsOpen[instTopologicalSpace] A ↔
    ∀ (K : Set X),
      IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' A)

Tactic:
simp_rw [isOpen_coinduced, isOpen_iSup_iff]

Premises used: isOpen_iSup_iff, isOpen_coinduced
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set (𝐤X)
⊢ (∀ (i : Set X) (i_1 : IsCompact i),
      IsOpen[TopologicalSpace.coinduced Subtype.val
            { IsOpen := instTopologicalSpace._aux_1 i, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }]
        ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' A)) ↔
    ∀ (K : Set X),
      IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' A)

Tactic:
rfl
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set (𝐤X)
simp_rw :
  (∀ (i : Set X) (i_1 : IsCompact i),
      IsClosed[TopologicalSpace.coinduced (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)
            (TopologicalSpace.coinduced Subtype.val
              { IsOpen := instTopologicalSpace._aux_1 i, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ })]
        A) ↔
    ∀ (K : Set X),
      IsCompact K →
        IsClosed[TopologicalSpace.coinduced (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)
              (TopologicalSpace.coinduced Subtype.val instTopologicalSpaceSubtype)]
          A
⊢ IsClosed[instTopologicalSpace] A ↔
    ∀ (K : Set X),
      IsCompact K → IsClosed[instTopologicalSpaceSubtype] (K ↓∩ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' A)

Tactic:
simp_rw [isClosed_coinduced, isClosed_iSup_iff, ← isClosed_coinduced]

Premises used: isClosed_iSup_iff, isClosed_coinduced
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set (𝐤X)
⊢ (∀ (i : Set X) (i_1 : IsCompact i),
      IsClosed[TopologicalSpace.coinduced (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)
            (TopologicalSpace.coinduced Subtype.val
              { IsOpen := instTopologicalSpace._aux_1 i, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ })]
        A) ↔
    ∀ (K : Set X),
      IsCompact K →
        IsClosed[TopologicalSpace.coinduced (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)
              (TopologicalSpace.coinduced Subtype.val instTopologicalSpaceSubtype)]
          A

Tactic:
rfl
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : 𝐤X → Y
simp_rw :
  (∀ (i : Set X) (i_1 : IsCompact i),
      Continuous[{ IsOpen := instTopologicalSpace._aux_1 i, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ },
          inst_1]
        ((f ∘ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)) ∘ Subtype.val (p := i))) ↔
    ∀ (K : Set X),
      IsCompact K →
        Continuous[instTopologicalSpaceSubtype, inst_1]
          (K.restrict (π := fun (a : X) ↦ Y) (f ∘ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)))
⊢ Continuous[instTopologicalSpace, inst_1] f ↔
    ∀ (K : Set X), IsCompact K → ContinuousOn (f ∘ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)) K

Tactic:
simp_rw [continuous_coinduced_dom, continuous_iSup_dom, continuous_coinduced_dom,
    continuousOn_iff_continuous_restrict]

Premises used: continuous_coinduced_dom, continuous_iSup_dom, continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : 𝐤X → Y
⊢ (∀ (i : Set X) (i_1 : IsCompact i),
      Continuous[{ IsOpen := instTopologicalSpace._aux_1 i, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ },
          inst_1]
        ((f ∘ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)) ∘ Subtype.val (p := i))) ↔
    ∀ (K : Set X),
      IsCompact K →
        Continuous[instTopologicalSpaceSubtype, inst_1]
          (K.restrict (π := fun (a : X) ↦ Y) (f ∘ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)))

Tactic:
rfl
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
rw :
  ∀ (K : Set X),
    IsCompact K →
      ContinuousOn (Y := X)
        (Function.comp (β := 𝐤X) (⇑(CompactCoherentification.mk X).symm : (a : 𝐤X) → X)
          (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X))
        K
⊢ Continuous[instTopologicalSpace, inst] (⇑(CompactCoherentification.mk X).symm : (a : 𝐤X) → X)

Tactic:
rw [continuous_dom_iff]

Premises used: CompactCoherentification.continuous_dom_iff
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ ∀ (K : Set X),
    IsCompact K →
      ContinuousOn (Y := X)
        (Function.comp (β := 𝐤X) (⇑(CompactCoherentification.mk X).symm : (a : 𝐤X) → X)
          (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X))
        K

Tactic:
fun _ _ ↦ continuousOn_id

Premises used: continuousOn_id
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ ∀ (K : Set X),
    IsCompact K →
      ContinuousOn (Y := X)
        (Function.comp (β := 𝐤X) (⇑(CompactCoherentification.mk X).symm : (a : 𝐤X) → X)
          (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X))
        K

Tactic:
exact fun _ _ ↦ continuousOn_id

Premises used: continuousOn_id
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ Continuous[instTopologicalSpace, inst_1] (f ∘ (⇑(CompactCoherentification.mk X).symm : (a : 𝐤X) → X))

Tactic:
hf.comp continuous_mk_symm

Premises used: CompactCoherentification.continuous_mk_symm, Continuous.comp
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
hA : IsOpen[inst] A
rw : ∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ A)
⊢ IsOpen[instTopologicalSpace] ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) '' A)

Tactic:
rw [isOpen_iff, Equiv.preimage_image]

Premises used: CompactCoherentification.isOpen_iff, Equiv.preimage_image
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
hA : IsOpen[inst] A
K : Set X
hK : IsCompact K
⊢ IsOpen[instTopologicalSpaceSubtype] (K ↓∩ A)

Tactic:
hA.preimage_val

Premises used: IsOpen.preimage_val
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
hA : IsOpen[inst] A
K : Set X
hK : IsCompact K
⊢ IsOpen[instTopologicalSpaceSubtype] (K ↓∩ A)

Tactic:
exact hA.preimage_val

Premises used: IsOpen.preimage_val
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set X
hK : IsCompact K
rw :
  Continuous[instTopologicalSpaceSubtype, instTopologicalSpace]
    (K.restrict (π := fun (a : X) ↦ 𝐤X) (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X))
⊢ ContinuousOn (Y := 𝐤X) (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) K

Tactic:
rw [continuousOn_iff_continuous_restrict]

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set X
hK : IsCompact K
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpace]
    (K.restrict (π := fun (a : X) ↦ 𝐤X) (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X))

Tactic:
⟨fun U hU ↦ isOpen_iff.mp hU K hK⟩

Premises used: Continuous.mk, CompactCoherentification.isOpen_iff, Iff.mp
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set X
hK : IsCompact K
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpace]
    (K.restrict (π := fun (a : X) ↦ 𝐤X) (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X))

Tactic:
exact ⟨fun U hU ↦ isOpen_iff.mp hU K hK⟩
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → 𝐤Y
K : Set X
hK : IsCompact K
⊢ ContinuousOn f K ↔ ContinuousOn (Y := Y) ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f) K

Tactic:
⟨fun H ↦ continuous_mk_symm.comp_continuousOn H, fun H ↦ ?_⟩

Premises used: Continuous.comp_continuousOn, CompactCoherentification.continuous_mk_symm, Iff.intro
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → 𝐤Y
K : Set X
hK : IsCompact K
refine : ∀ (H : ContinuousOn (Y := Y) ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f) K), ContinuousOn f K
⊢ ContinuousOn f K ↔ ContinuousOn (Y := Y) ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f) K

Tactic:
refine ⟨fun H ↦ continuous_mk_symm.comp_continuousOn H, fun H ↦ ?_⟩
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → 𝐤Y
K : Set X
hK : IsCompact K
H : ContinuousOn (Y := Y) ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f) K
⊢ ContinuousOn f K

Tactic:
continuousOn_isCompact_mk (hK.image_of_continuousOn H) |>.comp H (mapsTo_image f K)

Premises used: CompactCoherentification.continuousOn_isCompact_mk, Set.mapsTo_image, ContinuousOn.comp, IsCompact.image_of_continuousOn
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → 𝐤Y
K : Set X
hK : IsCompact K
H : ContinuousOn (Y := Y) ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f) K
⊢ ContinuousOn f K

Tactic:
exact continuousOn_isCompact_mk (hK.image_of_continuousOn H) |>.comp H (mapsTo_image f K)

Premises used: CompactCoherentification.continuousOn_isCompact_mk, Set.mapsTo_image, ContinuousOn.comp, IsCompact.image_of_continuousOn
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactlyCoherentSpace X
rw :
  ∀ (s : Set X),
    Membership.mem (γ := Set (Set X)) {K : Set X | IsCompact K} s →
      ContinuousOn (Y := 𝐤X) (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) s
⊢ Continuous[inst, instTopologicalSpace] (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)

Tactic:
rw [CompactlyCoherentSpace.isCoherentWith.continuous_iff]

Premises used: Topology.IsCoherentWith.continuous_iff, CompactlyCoherentSpace.isCoherentWith
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactlyCoherentSpace X
⊢ ∀ (s : Set X),
    Membership.mem (γ := Set (Set X)) {K : Set X | IsCompact K} s →
      ContinuousOn (Y := 𝐤X) (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) s

Tactic:
fun K hK ↦ continuousOn_isCompact_mk hK

Premises used: CompactCoherentification.continuousOn_isCompact_mk
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactlyCoherentSpace X
⊢ ∀ (s : Set X),
    Membership.mem (γ := Set (Set X)) {K : Set X | IsCompact K} s →
      ContinuousOn (Y := 𝐤X) (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) s

Tactic:
exact fun K hK ↦ continuousOn_isCompact_mk hK

Premises used: CompactCoherentification.continuousOn_isCompact_mk
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → 𝐤Y
inst_2 : CompactSpace X
rw : ContinuousOn f univ ↔ Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f)
rw₁ :
  ContinuousOn (Y := Y) ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f) univ ↔
    Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f)
rw₂ rw₃ :
  Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f) ↔
    Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f)
⊢ Continuous[inst, instTopologicalSpace] f ↔
    Continuous[inst, inst_1] ((⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y) ∘ f)

Tactic:
rw [← continuousOn_univ, continuousOn_rng_of_isCompact isCompact_univ, continuousOn_univ]

Premises used: CompactCoherentification.continuousOn_rng_of_isCompact, isCompact_univ, continuousOn_univ
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : ∀ (K : Set X), IsCompact K → ContinuousOn f K
simp_rw : ∀ (K : Set X), IsCompact K → ContinuousOn (Y := 𝐤Y) ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f) K
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (CompactCoherentification.map f)

Tactic:
simp_rw [continuous_dom_iff, CompactCoherentification.map_comp_mk]

Premises used: CompactCoherentification.map_comp_mk, CompactCoherentification.continuous_dom_iff
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : ∀ (K : Set X), IsCompact K → ContinuousOn f K
⊢ ∀ (K : Set X), IsCompact K → ContinuousOn (Y := 𝐤Y) ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f) K

Tactic:
fun K hK ↦ continuousOn_rng_of_isCompact hK |>.mpr <| hf K hK

Premises used: Iff.mpr, CompactCoherentification.continuousOn_rng_of_isCompact
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : ∀ (K : Set X), IsCompact K → ContinuousOn f K
⊢ ∀ (K : Set X), IsCompact K → ContinuousOn (Y := 𝐤Y) ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f) K

Tactic:
exact fun K hK ↦ continuousOn_rng_of_isCompact hK |>.mpr <| hf K hK

Premises used: Iff.mpr, CompactCoherentification.continuousOn_rng_of_isCompact
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
hf₁ : ∀ (K : Set X), IsCompact K → ContinuousOn f K
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (CompactCoherentification.map f)

Tactic:
apply continuous_map_of_continuousOn

Premises used: CompactCoherentification.continuous_map_of_continuousOn
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
K : Set X
h : IsCompact K
⊢ ContinuousOn f K

Tactic:
hf.continuousOn

Premises used: Continuous.continuousOn
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
K : Set X
h : IsCompact K
⊢ ContinuousOn f K

Tactic:
exact hf.continuousOn

Premises used: Continuous.continuousOn
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
f : X → Y
rw :
  Continuous[inst, inst_1]
      (Function.comp (β := 𝐤Y) (⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y)
        ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f)) ↔
    Continuous[inst, inst_1] f
rw₁ :
  Continuous[inst, inst_1]
      (Function.comp (β := 𝐤Y) (⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y)
          (⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘
        f) ↔
    Continuous[inst, inst_1] f
rw₂ : Continuous[inst, inst_1] (id ∘ f) ↔ Continuous[inst, inst_1] f
rw₃ rw₄ : Continuous[inst, inst_1] f ↔ Continuous[inst, inst_1] f
⊢ Continuous[inst, instTopologicalSpace] ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f) ↔
    Continuous[inst, inst_1] f

Tactic:
rw [continuous_rng_of_compactSpace, ← Function.comp_assoc, Equiv.symm_comp_self, Function.id_comp]

Premises used: Equiv.symm_comp_self, CompactCoherentification.continuous_rng_of_compactSpace, Function.comp_assoc, Function.id_comp
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
A : Set X
hA : IsCompact A
f : X → Y
simp_rw :
  Continuous[instTopologicalSpaceSubtype, instTopologicalSpace]
      (A.restrict (π := fun (a : X) ↦ 𝐤Y) ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f)) ↔
    Continuous[instTopologicalSpaceSubtype, inst_1] (A.restrict (π := fun (a : X) ↦ Y) f)
⊢ ContinuousOn (Y := 𝐤Y) ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f) A ↔ ContinuousOn f A

Tactic:
simp_rw [continuousOn_iff_continuous_restrict]

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
A : Set X
hA : IsCompact A
f : X → Y
this : CompactSpace.{u_1} (↑A : Type u_1) := ⋯
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpace]
      (A.restrict (π := fun (a : X) ↦ 𝐤Y) ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f)) ↔
    Continuous[instTopologicalSpaceSubtype, inst_1] (A.restrict (π := fun (a : X) ↦ Y) f)

Tactic:
continuous_mk_comp_iff_of_compactSpace

Premises used: CompactCoherentification.continuous_mk_comp_iff_of_compactSpace, Set.restrict
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
A : Set X
hA : IsCompact A
f : X → Y
this : CompactSpace.{u_1} (↑A : Type u_1) := ⋯
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpace]
      (A.restrict (π := fun (a : X) ↦ 𝐤Y) ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f)) ↔
    Continuous[instTopologicalSpaceSubtype, inst_1] (A.restrict (π := fun (a : X) ↦ Y) f)

Tactic:
exact continuous_mk_comp_iff_of_compactSpace

Premises used: CompactCoherentification.continuous_mk_comp_iff_of_compactSpace
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set (𝐤X)
mp : IsCompact K → IsCompact (X := X) ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' K)
mpr : IsCompact (X := X) ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' K) → IsCompact K
⊢ IsCompact K ↔ IsCompact (X := X) ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' K)

Tactic:
constructor
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set (𝐤X)
hK : IsCompact K
⊢ IsCompact (X := X) ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' K)

Tactic:
Equiv.image_symm_eq_preimage _ _ ▸ hK.image continuous_mk_symm

Premises used: CompactCoherentification.continuous_mk_symm, Eq.rec, IsCompact.image, Equiv.image_symm_eq_preimage
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set (𝐤X)
hK : IsCompact K
⊢ IsCompact (X := X) ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' K)

Tactic:
exact Equiv.image_symm_eq_preimage _ _ ▸ hK.image continuous_mk_symm
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set (𝐤X)
hK : IsCompact (X := X) ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' K)
⊢ IsCompact K

Tactic:
exact Equiv.image_preimage _ _ ▸ hK.image_of_continuousOn <| continuousOn_isCompact_mk hK

Premises used: CompactCoherentification.continuousOn_isCompact_mk