awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
h :
  ∀ (x : (i : (↑S : Type u_1)) → α (↑i : ι)),
    Membership.mem (γ := Set ((i : (↑S : Type u_1)) → α (↑i : ι)))
        (image (α := (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
          Prod.snd
          (image (α := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
            (⇑(Homeomorph.preimageImageRestrict α S s) :
              (a : (↑(Sᶜ.restrict ⁻¹' Sᶜ.restrict '' s) : Type (max u_1 u_2))) →
                (↑(Sᶜ.restrict '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
            ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦
                (↑x : (a : ι) → α a)) ⁻¹'
              s)))
        x ↔
      x ∈ S.restrict (π := α) '' s
⊢ image (α := (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) Prod.snd
      (image (α := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
        (⇑(Homeomorph.preimageImageRestrict α S s) :
          (a : (↑(Sᶜ.restrict ⁻¹' Sᶜ.restrict '' s) : Type (max u_1 u_2))) →
            (↑(Sᶜ.restrict '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
        ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦
            (↑x : (a : ι) → α a)) ⁻¹'
          s)) =
    S.restrict (π := α) '' s

Tactic:
ext x
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
x : (i : (↑S : Type u_1)) → α (↑i : ι)
h :
  (∃ (a : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)),
      (∃ x ∈ s, Sᶜ.restrict (π := α) x = a) ∧
        ∃ a_1 ∈ s,
          ((∃ x ∈ s, Sᶜ.restrict (π := α) x = Sᶜ.restrict (π := α) a_1) ∧ Sᶜ.restrict (π := α) a_1 = a) ∧
            (fun (i : (↑S : Type u_1)) ↦ a_1 (↑i : ι)) = x) ↔
    ∃ x_1 ∈ s, S.restrict (π := α) x_1 = x
⊢ Membership.mem (γ := Set ((i : (↑S : Type u_1)) → α (↑i : ι)))
      (image (α := (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) Prod.snd
        (image (α := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
          (⇑(Homeomorph.preimageImageRestrict α S s) :
            (a : (↑(Sᶜ.restrict ⁻¹' Sᶜ.restrict '' s) : Type (max u_1 u_2))) →
              (↑(Sᶜ.restrict '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
          ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦
              (↑x : (a : ι) → α a)) ⁻¹'
            s)))
      x ↔
    x ∈ S.restrict (π := α) '' s

Tactic:
simp only [Homeomorph.preimageImageRestrict, Homeomorph.homeomorph_mk_coe, Equiv.coe_fn_mk,
    mem_image, mem_preimage, Subtype.exists, exists_and_left, Prod.exists, Prod.mk.injEq,
    exists_and_right, exists_eq_right, Subtype.mk.injEq, exists_prop]

Premises used: Homeomorph.homeomorph_mk_coe, Set.mem_image, Subtype.exists, exists_eq_right, exists_and_left, exists_and_right, exists_prop, Homeomorph.preimageImageRestrict, Prod.mk.injEq, Subtype.mk.injEq, Equiv.coe_fn_mk, Prod.exists, Set.mem_preimage
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
x : (i : (↑S : Type u_1)) → α (↑i : ι)
h :
  (∃ (a : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)),
      (∃ x ∈ s, Sᶜ.restrict (π := α) x = a) ∧
        ∃ a_1 ∈ s,
          ((∃ x ∈ s, Sᶜ.restrict (π := α) x = Sᶜ.restrict (π := α) a_1) ∧ Sᶜ.restrict (π := α) a_1 = a) ∧
            (fun (i : (↑S : Type u_1)) ↦ a_1 (↑i : ι)) = x) →
    ∃ x_1 ∈ s, S.restrict (π := α) x_1 = x
h₁ :
  (∃ x_1 ∈ s, S.restrict (π := α) x_1 = x) →
    ∃ (a : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)),
      (∃ x ∈ s, Sᶜ.restrict (π := α) x = a) ∧
        ∃ a_1 ∈ s,
          ((∃ x ∈ s, Sᶜ.restrict (π := α) x = Sᶜ.restrict (π := α) a_1) ∧ Sᶜ.restrict (π := α) a_1 = a) ∧
            (fun (i : (↑S : Type u_1)) ↦ a_1 (↑i : ι)) = x
⊢ (∃ (a : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)),
      (∃ x ∈ s, Sᶜ.restrict (π := α) x = a) ∧
        ∃ a_1 ∈ s,
          ((∃ x ∈ s, Sᶜ.restrict (π := α) x = Sᶜ.restrict (π := α) a_1) ∧ Sᶜ.restrict (π := α) a_1 = a) ∧
            (fun (i : (↑S : Type u_1)) ↦ a_1 (↑i : ι)) = x) ↔
    ∃ x_1 ∈ s, S.restrict (π := α) x_1 = x

Tactic:
constructor
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
x : (i : (↑S : Type u_1)) → α (↑i : ι)
y : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)
left : ∃ x ∈ s, Sᶜ.restrict (π := α) x = y
z : (a : ι) → α a
hz_mem : z ∈ s
left_1 : (∃ x ∈ s, Sᶜ.restrict (π := α) x = Sᶜ.restrict (π := α) z) ∧ Sᶜ.restrict (π := α) z = y
hzx : (fun (i : (↑S : Type u_1)) ↦ z (↑i : ι)) = x
⊢ ∃ x_1 ∈ s, S.restrict (π := α) x_1 = x

Tactic:
⟨z, hz_mem, hzx⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
x : (i : (↑S : Type u_1)) → α (↑i : ι)
y : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)
left : ∃ x ∈ s, Sᶜ.restrict (π := α) x = y
z : (a : ι) → α a
hz_mem : z ∈ s
left_1 : (∃ x ∈ s, Sᶜ.restrict (π := α) x = Sᶜ.restrict (π := α) z) ∧ Sᶜ.restrict (π := α) z = y
hzx : (fun (i : (↑S : Type u_1)) ↦ z (↑i : ι)) = x
⊢ ∃ x_1 ∈ s, S.restrict (π := α) x_1 = x

Tactic:
exact ⟨z, hz_mem, hzx⟩
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
x : (i : (↑S : Type u_1)) → α (↑i : ι)
z : (a : ι) → α a
hz_mem : z ∈ s
hzx : S.restrict (π := α) z = x
⊢ ∃ (a : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)),
    (∃ x ∈ s, Sᶜ.restrict (π := α) x = a) ∧
      ∃ a_1 ∈ s,
        ((∃ x ∈ s, Sᶜ.restrict (π := α) x = Sᶜ.restrict (π := α) a_1) ∧ Sᶜ.restrict (π := α) a_1 = a) ∧
          (fun (i : (↑S : Type u_1)) ↦ a_1 (↑i : ι)) = x

Tactic:
⟨Sᶜ.restrict z, mem_image_of_mem Sᶜ.restrict hz_mem, z, hz_mem,
      ⟨⟨⟨z, hz_mem, rfl⟩, rfl⟩, hzx⟩⟩

Premises used: Compl.compl, Set.mem_image_of_mem, And.intro, Exists.intro, Set.restrict, rfl
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
x : (i : (↑S : Type u_1)) → α (↑i : ι)
z : (a : ι) → α a
hz_mem : z ∈ s
hzx : S.restrict (π := α) z = x
⊢ ∃ (a : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)),
    (∃ x ∈ s, Sᶜ.restrict (π := α) x = a) ∧
      ∃ a_1 ∈ s,
        ((∃ x ∈ s, Sᶜ.restrict (π := α) x = Sᶜ.restrict (π := α) a_1) ∧ Sᶜ.restrict (π := α) a_1 = a) ∧
          (fun (i : (↑S : Type u_1)) ↦ a_1 (↑i : ι)) = x

Tactic:
exact ⟨Sᶜ.restrict z, mem_image_of_mem Sᶜ.restrict hz_mem, z, hz_mem,
      ⟨⟨⟨z, hz_mem, rfl⟩, rfl⟩, hzx⟩⟩
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
rw :
  IsClosed (X := (a : (↑S : Type u_1)) → α (↑a : ι))
    (Set.image (α := (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
      Prod.snd
      (Set.image (α := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
        (⇑(Homeomorph.preimageImageRestrict α S s) :
          (a : (↑(Sᶜ.restrict ⁻¹' Sᶜ.restrict '' s) : Type (max u_1 u_2))) →
            (↑(Sᶜ.restrict '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
        ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦
            (↑x : (a : ι) → α a)) ⁻¹'
          s)))
⊢ IsClosed (S.restrict (π := α) '' s)

Tactic:
rw [← Topology.image_snd_preimageImageRestrict]

Premises used: Topology.image_snd_preimageImageRestrict
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
⊢ CompactSpace (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))

Tactic:
have : CompactSpace (Sᶜ.restrict '' s) :=
    isCompact_iff_compactSpace.mp (hs_compact.image (Pi.continuous_restrict _))
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this : CompactSpace (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))
⊢ IsClosed (X := (a : (↑S : Type u_1)) → α (↑a : ι))
    (Set.image (α := (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
      Prod.snd
      (Set.image (α := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
        (⇑(Homeomorph.preimageImageRestrict α S s) :
          (a : (↑(Sᶜ.restrict ⁻¹' Sᶜ.restrict '' s) : Type (max u_1 u_2))) →
            (↑(Sᶜ.restrict '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
        ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦
            (↑x : (a : ι) → α a)) ⁻¹'
          s)))

Tactic:
isClosedMap_snd_of_compactSpace _ ?_

Premises used: isClosedMap_snd_of_compactSpace
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this : CompactSpace (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))
refine :
  IsClosed (X := (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((a : (↑S : Type u_1)) → α (↑a : ι)))
    (Set.image (α := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
      (⇑(Homeomorph.preimageImageRestrict α S s) :
        (a : (↑(Sᶜ.restrict ⁻¹' Sᶜ.restrict '' s) : Type (max u_1 u_2))) →
          (↑(Sᶜ.restrict '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
      ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦
          (↑x : (a : ι) → α a)) ⁻¹'
        s))
⊢ IsClosed (X := (a : (↑S : Type u_1)) → α (↑a : ι))
    (Set.image (α := (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
      Prod.snd
      (Set.image (α := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
        (⇑(Homeomorph.preimageImageRestrict α S s) :
          (a : (↑(Sᶜ.restrict ⁻¹' Sᶜ.restrict '' s) : Type (max u_1 u_2))) →
            (↑(Sᶜ.restrict '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
        ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦
            (↑x : (a : ι) → α a)) ⁻¹'
          s)))

Tactic:
refine isClosedMap_snd_of_compactSpace _ ?_

Premises used: isClosedMap_snd_of_compactSpace
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this : CompactSpace (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))
rw :
  IsClosed (X := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
    ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦ (↑x : (a : ι) → α a)) ⁻¹'
      s)
⊢ IsClosed (X := (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((a : (↑S : Type u_1)) → α (↑a : ι)))
    (Set.image (α := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
      (⇑(Homeomorph.preimageImageRestrict α S s) :
        (a : (↑(Sᶜ.restrict ⁻¹' Sᶜ.restrict '' s) : Type (max u_1 u_2))) →
          (↑(Sᶜ.restrict '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι)))
      ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦
          (↑x : (a : ι) → α a)) ⁻¹'
        s))

Tactic:
rw [Homeomorph.isClosed_image]

Premises used: Homeomorph.isClosed_image
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this : CompactSpace (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))
⊢ IsClosed (X := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
    ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦ (↑x : (a : ι) → α a)) ⁻¹'
      s)

Tactic:
hs_closed.preimage continuous_subtype_val

Premises used: continuous_subtype_val, IsClosed.preimage
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this : CompactSpace (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))
⊢ IsClosed (X := (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)))
    ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))) ↦ (↑x : (a : ι) → α a)) ⁻¹'
      s)

Tactic:
exact hs_closed.preimage continuous_subtype_val

Premises used: continuous_subtype_val, IsClosed.preimage
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
inst_1 : ∀ (i : ι), CompactSpace.{u_2} (α i)
s : Set ((a : ι) → α a)
hs : IsClosed s
⊢ Eq (α := (f : (a : ι) → α a) → (a : (↑S : Type u_1)) → α (↑a : ι)) (S.restrict (π := α))
    (Function.comp (β := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
      (⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
        (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))))

Tactic:
have : S.restrict (π := α) = Prod.fst ∘ (Homeomorph.piEquivPiSubtypeProd (· ∈ S) α) := rfl
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
inst_1 : ∀ (i : ι), CompactSpace.{u_2} (α i)
s : Set ((a : ι) → α a)
hs : IsClosed s
this :
  Eq (α := (f : (a : ι) → α a) → (a : (↑S : Type u_1)) → α (↑a : ι)) (S.restrict (π := α))
    (Function.comp (β := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
      (⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
        (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))))
rw :
  IsClosed (X := (a : (↑S : Type u_1)) → α (↑a : ι))
    (image (α := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
      ((⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
          (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) ''
        s))
⊢ IsClosed (S.restrict (π := α) '' s)

Tactic:
rw [this, image_comp]

Premises used: Set.image_comp
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
inst_1 : ∀ (i : ι), CompactSpace.{u_2} (α i)
s : Set ((a : ι) → α a)
hs : IsClosed s
this :
  Eq (α := (f : (a : ι) → α a) → (a : (↑S : Type u_1)) → α (↑a : ι)) (S.restrict (π := α))
    (Function.comp (β := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
      (⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
        (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))))
⊢ IsClosed (X := (a : (↑S : Type u_1)) → α (↑a : ι))
    (image (α := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
      ((⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
          (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) ''
        s))

Tactic:
isClosedMap_fst_of_compactSpace _ <| (Homeomorph.isClosed_image _).mpr hs

Premises used: Iff.mpr, Homeomorph.isClosed_image, isClosedMap_fst_of_compactSpace
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
inst_1 : ∀ (i : ι), CompactSpace.{u_2} (α i)
s : Set ((a : ι) → α a)
hs : IsClosed s
this :
  Eq (α := (f : (a : ι) → α a) → (a : (↑S : Type u_1)) → α (↑a : ι)) (S.restrict (π := α))
    (Function.comp (β := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
      (⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
        (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))))
⊢ IsClosed (X := (a : (↑S : Type u_1)) → α (↑a : ι))
    (image (α := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
      ((⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
          (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) ''
        s))

Tactic:
exact isClosedMap_fst_of_compactSpace _ <| (Homeomorph.isClosed_image _).mpr hs

Premises used: Iff.mpr, Homeomorph.isClosed_image, isClosedMap_fst_of_compactSpace
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
inst_1 : ∀ (i : ι), CompactSpace.{u_2} (α i)
s : Set ((a : ι) → α a)
hs : IsClosed s
have have₁ have₂ :
  ∀
    (this :
      Eq (α := (f : (a : ι) → α a) → (a : (↑S : Type u_1)) → α (↑a : ι)) (S.restrict (π := α))
        (Function.comp (β := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
          (⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
            (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))))),
    IsClosed (S.restrict (π := α) '' s)
have₃ :
  ∀
    (this :
      Eq (α := (f : (a : ι) → α a) → (a : (↑S : Type u_1)) → α (↑a : ι)) (S.restrict (π := α))
        (Function.comp (β := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
          (⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
            (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))))),
    IsClosed (X := (a : (↑S : Type u_1)) → α (↑a : ι))
      (image (α := ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) Prod.fst
        ((⇑(Homeomorph.piEquivPiSubtypeProd (fun (x : ι) ↦ x ∈ S) α) :
            (a : (i : ι) → α i) → ((i : { x : ι // x ∈ S }) → α (↑i : ι)) × ((i : { x : ι // x ∉ S }) → α (↑i : ι))) ''
          s))
⊢ IsClosed (S.restrict (π := α) '' s)

Tactic:
classical
  have : S.restrict (π := α) = Prod.fst ∘ (Homeomorph.piEquivPiSubtypeProd (· ∈ S) α) := rfl
  rw [this, image_comp]
  exact isClosedMap_fst_of_compactSpace _ <| (Homeomorph.isClosed_image _).mpr hs

Premises used: Iff.mpr, Homeomorph.isClosed_image, Set.image_comp, isClosedMap_fst_of_compactSpace
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this : IsClosed (X := (a : (↑{i} : Type u_1)) → α (↑a : ι)) (restrict (π := α) {i} '' s)
⊢ Eq (α := ((a : ι) → α a) → α (↑default : ι))
    (Function.comp (β := (t : (↑{i} : Type u_1)) → α (↑t : ι))
      (⇑(Homeomorph.piUnique fun (t : (↑{i} : Type u_1)) ↦ α (↑t : ι)) :
        (a : (t : (↑{i} : Type u_1)) → α (↑t : ι)) → α (↑default : ι))
      (restrict (π := α) {i}))
    fun (x : (j : ι) → α j) ↦ x i

Tactic:
have : Homeomorph.piUnique _ ∘ Set.restrict {i} = fun (x : Π j, α j) ↦ x i := rfl
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this_1 : IsClosed (X := (a : (↑{i} : Type u_1)) → α (↑a : ι)) (restrict (π := α) {i} '' s)
this :
  Eq (α := ((a : ι) → α a) → α (↑default : ι))
    (Function.comp (β := (t : (↑{i} : Type u_1)) → α (↑t : ι))
      (⇑(Homeomorph.piUnique fun (t : (↑{i} : Type u_1)) ↦ α (↑t : ι)) :
        (a : (t : (↑{i} : Type u_1)) → α (↑t : ι)) → α (↑default : ι))
      (restrict (π := α) {i}))
    fun (x : (j : ι) → α j) ↦ x i
rwa :
  IsClosed.{u_2} (X := α i)
    (Function.comp (β := (t : (↑{i} : Type u_1)) → α (↑t : ι))
        (⇑(Homeomorph.piUnique fun (t : (↑{i} : Type u_1)) ↦ α (↑t : ι)) :
          (a : (t : (↑{i} : Type u_1)) → α (↑t : ι)) → α (↑default : ι))
        (restrict (π := α) {i}) ''
      s)
rwa₁ :
  IsClosed.{u_2} (X := α i)
    (image (α := (t : (↑{i} : Type u_1)) → α (↑t : ι))
      (⇑(Homeomorph.piUnique fun (t : (↑{i} : Type u_1)) ↦ α (↑t : ι)) :
        (a : (t : (↑{i} : Type u_1)) → α (↑t : ι)) → α (↑default : ι))
      (restrict (π := α) {i} '' s))
rwa₂ rwa₃ rwa₄ rwa₅ : IsClosed (X := (t : (↑{i} : Type u_1)) → α (↑t : ι)) (restrict (π := α) {i} '' s)
⊢ IsClosed.{u_2} (X := α i) ((fun (x : (i : ι) → α i) ↦ x i) '' s)

Tactic:
rwa [← this, image_comp, Homeomorph.isClosed_image (Homeomorph.piUnique _)]

Premises used: Homeomorph.isClosed_image, Set.image_comp, Homeomorph.piUnique
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
suffices : IsClosed (X := (a : (↑{i} : Type u_1)) → α (↑a : ι)) (restrict (π := α) {i} '' s)
⊢ IsClosed.{u_2} (X := α i) ((fun (x : (i : ι) → α i) ↦ x i) '' s)

Tactic:
suffices IsClosed (Set.restrict {i} '' s) by
    have : Homeomorph.piUnique _ ∘ Set.restrict {i} = fun (x : Π j, α j) ↦ x i := rfl
    rwa [← this, image_comp, Homeomorph.isClosed_image (Homeomorph.piUnique _)]
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
⊢ IsClosed (X := (a : (↑{i} : Type u_1)) → α (↑a : ι)) (restrict (π := α) {i} '' s)

Tactic:
hs_compact.isClosed_image_restrict {i} hs_closed

Premises used: IsCompact.isClosed_image_restrict, Singleton.singleton
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
⊢ IsClosed (X := (a : (↑{i} : Type u_1)) → α (↑a : ι)) (restrict (π := α) {i} '' s)

Tactic:
exact hs_compact.isClosed_image_restrict {i} hs_closed

Premises used: IsCompact.isClosed_image_restrict, Singleton.singleton
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
⊢ IsLocalHomeomorphOn f s ↔ ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)

Tactic:
⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
refine_1 :
  ∀ (h : IsLocalHomeomorphOn f s) (x : X) (hx : x ∈ s), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)
refine_2 :
  ∀ (h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)) (x : X) (hx : x ∈ s),
    ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = (↑e : X → Y)
⊢ IsLocalHomeomorphOn f s ↔ ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict (π := fun (a : X) ↦ Y) f)

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩