awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
U : Set X
hU : IsOpen[inst] U
hUx : U ∩ s = {x}
V : Set X
hV : IsOpen[inst] V
hVy : V ∩ s = {y}
z : X
hz : z ∈ s ∩ (U ∩ V)
⊢ z ∈ U ∩ s

Tactic:
grind
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
U : Set X
hU : IsOpen[inst] U
hUx : U ∩ s = {x}
V : Set X
hV : IsOpen[inst] V
hVy : V ∩ s = {y}
z : X
hz : z ∈ s ∩ (U ∩ V)
⊢ z ∈ V ∩ s

Tactic:
grind
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
U : Set X
hU : IsOpen[inst] U
hUx : U ∩ s = {x}
V : Set X
hV : IsOpen[inst] V
hVy : V ∩ s = {y}
z : X
hz : z ∈ s ∩ (U ∩ V)
⊢ x = y

Tactic:
exact (hUx.le (by grind)).symm.trans (b := z) (hVy.le (by grind))

Premises used: Eq.le, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst, inst_1] f
hf : Surjective f
inst_2 : PreirreducibleSpace X
rw : IsPreirreducible (f '' univ)
⊢ IsPreirreducible.{u_2} (X := Y) univ

Tactic:
rw [← hf.range_eq, ← Set.image_univ]

Premises used: Set.image_univ, Function.Surjective.range_eq
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst, inst_1] f
hf : Surjective f
inst_2 : PreirreducibleSpace X
⊢ IsPreirreducible (f '' univ)

Tactic:
(PreirreducibleSpace.isPreirreducible_univ).image _ hfc.continuousOn

Premises used: Continuous.continuousOn, IsPreirreducible.image, PreirreducibleSpace.isPreirreducible_univ
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst, inst_1] f
hf : Surjective f
inst_2 : PreirreducibleSpace X
⊢ IsPreirreducible (f '' univ)

Tactic:
exact (PreirreducibleSpace.isPreirreducible_univ).image _ hfc.continuousOn

Premises used: Continuous.continuousOn, IsPreirreducible.image, PreirreducibleSpace.isPreirreducible_univ
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst, inst_1] f
hf : Surjective f
inst_2 : IrreducibleSpace X
rw : IsPreirreducible (f '' univ)
⊢ IsPreirreducible.{u_2} (X := Y) univ

Tactic:
rw [← hf.range_eq, ← Set.image_univ]

Premises used: Set.image_univ, Function.Surjective.range_eq
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst, inst_1] f
hf : Surjective f
inst_2 : IrreducibleSpace X
⊢ IsPreirreducible (f '' univ)

Tactic:
(PreirreducibleSpace.isPreirreducible_univ).image _ hfc.continuousOn

Premises used: Continuous.continuousOn, IsPreirreducible.image, PreirreducibleSpace.isPreirreducible_univ
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst, inst_1] f
hf : Surjective f
inst_2 : IrreducibleSpace X
⊢ IsPreirreducible (f '' univ)

Tactic:
exact (PreirreducibleSpace.isPreirreducible_univ).image _ hfc.continuousOn

Premises used: Continuous.continuousOn, IsPreirreducible.image, PreirreducibleSpace.isPreirreducible_univ
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ₜ Y
⊢ IrreducibleSpace X ↔ IrreducibleSpace Y

Tactic:
⟨fun _ ↦ e.surjective.irreducibleSpace e.continuous,
    fun _ ↦ e.symm.surjective.irreducibleSpace e.symm.continuous⟩

Premises used: Homeomorph.continuous, Function.Surjective.irreducibleSpace, Homeomorph.symm, Iff.intro, Homeomorph.surjective
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))
j : (↑S : Type u_1)
⊢ (↑j : ι) ∈ S

Tactic:
have hj : ↑j ∈ S := j.prop
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))
j : (↑S : Type u_1)
hj : (↑j : ι) ∈ S
⊢ reorderRestrictProd (α := α) S s p (↑j : ι) = p.2 j

Tactic:
simp [reorderRestrictProd, hj]

Premises used: Topology.reorderRestrictProd
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))
j : (↑Sᶜ : Type u_1)
⊢ (↑j : ι) ∉ S

Tactic:
have hj : ↑j ∉ S := j.prop
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))
j : (↑Sᶜ : Type u_1)
hj : (↑j : ι) ∉ S
⊢ reorderRestrictProd (α := α) S s p (↑j : ι) = (↑p.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) j

Tactic:
simp [reorderRestrictProd, hj]

Premises used: Topology.reorderRestrictProd
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))
h :
  ∀ (x : (↑Sᶜ : Type u_1)),
    Sᶜ.restrict (π := α) (reorderRestrictProd (α := α) S s p) x = (↑p.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) x
⊢ Sᶜ.restrict (π := α) (reorderRestrictProd (α := α) S s p) = (↑p.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι))

Tactic:
ext
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))
x : (↑Sᶜ : Type u_1)
⊢ Sᶜ.restrict (π := α) (reorderRestrictProd (α := α) S s p) x = (↑p.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) x

Tactic:
simp
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] (reorderRestrictProd (α := α) S s)

Tactic:
continuous_pi fun j ↦ ?_

Premises used: continuous_pi
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
refine :
  ∀ (j : ι),
    Continuous[instTopologicalSpaceProd, inst j]
      fun (a : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
      reorderRestrictProd (α := α) S s a j
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] (reorderRestrictProd (α := α) S s)

Tactic:
refine continuous_pi fun j ↦ ?_

Premises used: continuous_pi
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
j : ι
pos :
  ∀ (h : j ∈ S),
    Continuous[instTopologicalSpaceProd, inst j]
      fun (a : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
      a.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ S) j h)
neg :
  ∀ (h : j ∉ S),
    Continuous[instTopologicalSpaceProd, inst j]
      fun (a : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
      (↑a.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ Sᶜ) j h)
⊢ Continuous[instTopologicalSpaceProd, inst j]
    fun (a : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
    if h : j ∈ S then a.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ S) j h)
    else (↑a.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ Sᶜ) j h)

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
j : ι
h : j ∈ S
⊢ Continuous[instTopologicalSpaceProd, inst j]
    fun (a : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
    a.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ S) j h)

Tactic:
fun_prop
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
j : ι
h : j ∉ S
⊢ Continuous[instTopologicalSpaceProd, inst j]
    fun (a : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
    (↑a.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ Sᶜ) j h)

Tactic:
((continuous_apply _).comp continuous_subtype_val).comp continuous_fst

Premises used: continuous_subtype_val, Continuous.comp, continuous_fst, continuous_apply
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
j : ι
h : j ∉ S
⊢ Continuous[instTopologicalSpaceProd, inst j]
    fun (a : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
    (↑a.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ Sᶜ) j h)

Tactic:
exact ((continuous_apply _).comp continuous_subtype_val).comp continuous_fst

Premises used: continuous_subtype_val, Continuous.comp, continuous_fst, continuous_apply
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))
obtain :
  ∀ (y : (a : ι) → α a) (hy_mem_s : y ∈ s)
    (hy_eq : Sᶜ.restrict (π := α) y = (↑p.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι))),
    reorderRestrictProd (α := α) S s p ∈ Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s
⊢ reorderRestrictProd (α := α) S s p ∈ Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s

Tactic:
obtain ⟨y, hy_mem_s, hy_eq⟩ := p.1.2

Premises used: Prod.fst, Subtype.property
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))
y : (a : ι) → α a
hy_mem_s : y ∈ s
hy_eq : Sᶜ.restrict (π := α) y = (↑p.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι))
⊢ reorderRestrictProd (α := α) S s p ∈ Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s

Tactic:
⟨y, hy_mem_s, hy_eq.trans (restrict_compl_reorderRestrictProd p).symm⟩

Premises used: Set.Mem, setOf, Set.preimage, And.intro, Exists.intro, Set.image, Eq.symm, Topology.restrict_compl_reorderRestrictProd, Eq.trans
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2)) × ((i : (↑S : Type u_1)) → α (↑i : ι))
y : (a : ι) → α a
hy_mem_s : y ∈ s
hy_eq : Sᶜ.restrict (π := α) y = (↑p.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι))
⊢ reorderRestrictProd (α := α) S s p ∈ Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s

Tactic:
exact ⟨y, hy_mem_s, hy_eq.trans (restrict_compl_reorderRestrictProd p).symm⟩
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))
h :
  ∀ (x_1 : ι),
    reorderRestrictProd (α := α) S s
        (Subtype.mk (p := fun (x : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) ↦ x ∈ Sᶜ.restrict (π := α) '' s)
            (Sᶜ.restrict (π := α) (↑x : (a : ι) → α a)) ⋯,
          fun (i : (↑S : Type u_1)) ↦ (↑x : (a : ι) → α a) (↑i : ι))
        x_1 =
      (↑x : (a : ι) → α a) x_1
⊢ reorderRestrictProd (α := α) S s
      (Subtype.mk (p := fun (x : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) ↦ x ∈ Sᶜ.restrict (π := α) '' s)
          (Sᶜ.restrict (π := α) (↑x : (a : ι) → α a)) ⋯,
        fun (i : (↑S : Type u_1)) ↦ (↑x : (a : ι) → α a) (↑i : ι)) =
    (↑x : (a : ι) → α a)

Tactic:
ext
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_2))
x_1 : ι
⊢ reorderRestrictProd (α := α) S s
      (Subtype.mk (p := fun (x : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) ↦ x ∈ Sᶜ.restrict (π := α) '' s)
          (Sᶜ.restrict (π := α) (↑x : (a : ι) → α a)) ⋯,
        fun (i : (↑S : Type u_1)) ↦ (↑x : (a : ι) → α a) (↑i : ι))
      x_1 =
    (↑x : (a : ι) → α a) x_1

Tactic:
simp [reorderRestrictProd]

Premises used: Topology.reorderRestrictProd
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α_1 : ι → Type u_2
s_1 : Set ((i : ι) → α_1 i)
i : ι
S_1 : Set ι
α : ι → Type u_3
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))
a :
  ∀ (x_1 : ι),
    (↑((fun (p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
                Subtype.mk (p := fun (x : (a : ι) → α a) ↦ x ∈ Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s)
                  (reorderRestrictProd (α := α) S s p) ⋯)
              ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) ↦
                  ((Subtype.mk (p := fun (x : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) ↦ x ∈ Sᶜ.restrict (π := α) '' s)
                        (Sᶜ.restrict (π := α) (↑x : (a : ι) → α a)) ⋯,
                      fun (i : (↑S : Type u_1)) ↦ (↑x : (a : ι) → α a) (↑i : ι)) :
                    (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))))
                x)) :
          (a : ι) → α a)
        x_1 =
      (↑x : (a : ι) → α a) x_1
⊢ (fun (p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
        Subtype.mk (p := fun (x : (a : ι) → α a) ↦ x ∈ Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s)
          (reorderRestrictProd (α := α) S s p) ⋯)
      ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) ↦
          ((Subtype.mk (p := fun (x : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) ↦ x ∈ Sᶜ.restrict (π := α) '' s)
                (Sᶜ.restrict (π := α) (↑x : (a : ι) → α a)) ⋯,
              fun (i : (↑S : Type u_1)) ↦ (↑x : (a : ι) → α a) (↑i : ι)) :
            (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α_1 : ι → Type u_2
s_1 : Set ((i : ι) → α_1 i)
i : ι
S_1 : Set ι
α : ι → Type u_3
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))
x_1 : ι
⊢ (↑((fun (p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
              Subtype.mk (p := fun (x : (a : ι) → α a) ↦ x ∈ Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s)
                (reorderRestrictProd (α := α) S s p) ⋯)
            ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) ↦
                ((Subtype.mk (p := fun (x : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) ↦ x ∈ Sᶜ.restrict (π := α) '' s)
                      (Sᶜ.restrict (π := α) (↑x : (a : ι) → α a)) ⋯,
                    fun (i : (↑S : Type u_1)) ↦ (↑x : (a : ι) → α a) (↑i : ι)) :
                  (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))))
              x)) :
        (a : ι) → α a)
      x_1 =
    (↑x : (a : ι) → α a) x_1

Tactic:
simp
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α_1 : ι → Type u_2
s_1 : Set ((i : ι) → α_1 i)
i : ι
S_1 : Set ι
α : ι → Type u_3
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))
fst :
  ∀ (x : (↑Sᶜ : Type u_1)),
    (↑((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) ↦
                  ((Subtype.mk (p := fun (x : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) ↦ x ∈ Sᶜ.restrict (π := α) '' s)
                        (Sᶜ.restrict (π := α) (↑x : (a : ι) → α a)) ⋯,
                      fun (i : (↑S : Type u_1)) ↦ (↑x : (a : ι) → α a) (↑i : ι)) :
                    (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))))
                ((fun (p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
                    Subtype.mk (p := fun (x : (a : ι) → α a) ↦ x ∈ Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s)
                      (reorderRestrictProd (α := α) S s p) ⋯)
                  p)).1 :
          (a : (↑Sᶜ : Type u_1)) → α (↑a : ι))
        x =
      (↑p.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) x
snd :
  ∀ (x : (↑S : Type u_1)),
    ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) ↦
              ((Subtype.mk (p := fun (x : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) ↦ x ∈ Sᶜ.restrict (π := α) '' s)
                    (Sᶜ.restrict (π := α) (↑x : (a : ι) → α a)) ⋯,
                  fun (i : (↑S : Type u_1)) ↦ (↑x : (a : ι) → α a) (↑i : ι)) :
                (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))))
            ((fun (p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
                Subtype.mk (p := fun (x : (a : ι) → α a) ↦ x ∈ Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s)
                  (reorderRestrictProd (α := α) S s p) ⋯)
              p)).2
        x =
      p.2 x
⊢ (fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) ↦
        ((Subtype.mk (p := fun (x : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) ↦ x ∈ Sᶜ.restrict (π := α) '' s)
              (Sᶜ.restrict (π := α) (↑x : (a : ι) → α a)) ⋯,
            fun (i : (↑S : Type u_1)) ↦ (↑x : (a : ι) → α a) (↑i : ι)) :
          (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))))
      ((fun (p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
          Subtype.mk (p := fun (x : (a : ι) → α a) ↦ x ∈ Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s)
            (reorderRestrictProd (α := α) S s p) ⋯)
        p) =
    p

Tactic:
ext
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α_1 : ι → Type u_2
s_1 : Set ((i : ι) → α_1 i)
i : ι
S_1 : Set ι
α : ι → Type u_3
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))
x : (↑Sᶜ : Type u_1)
⊢ (↑((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) ↦
                ((Subtype.mk (p := fun (x : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) ↦ x ∈ Sᶜ.restrict (π := α) '' s)
                      (Sᶜ.restrict (π := α) (↑x : (a : ι) → α a)) ⋯,
                    fun (i : (↑S : Type u_1)) ↦ (↑x : (a : ι) → α a) (↑i : ι)) :
                  (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))))
              ((fun (p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
                  Subtype.mk (p := fun (x : (a : ι) → α a) ↦ x ∈ Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s)
                    (reorderRestrictProd (α := α) S s p) ⋯)
                p)).1 :
        (a : (↑Sᶜ : Type u_1)) → α (↑a : ι))
      x =
    (↑p.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) x

Tactic:
simp
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α_1 : ι → Type u_2
s_1 : Set ((i : ι) → α_1 i)
i : ι
S_1 : Set ι
α : ι → Type u_3
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))
x : (↑S : Type u_1)
⊢ ((fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) ↦
            ((Subtype.mk (p := fun (x : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) ↦ x ∈ Sᶜ.restrict (π := α) '' s)
                  (Sᶜ.restrict (π := α) (↑x : (a : ι) → α a)) ⋯,
                fun (i : (↑S : Type u_1)) ↦ (↑x : (a : ι) → α a) (↑i : ι)) :
              (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))))
          ((fun (p : (↑(Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3)) × ((i : (↑S : Type u_1)) → α (↑i : ι))) ↦
              Subtype.mk (p := fun (x : (a : ι) → α a) ↦ x ∈ Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s)
                (reorderRestrictProd (α := α) S s p) ⋯)
            p)).2
      x =
    p.2 x

Tactic:
simp
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α_1 : ι → Type u_2
s_1 : Set ((i : ι) → α_1 i)
i : ι
S_1 : Set ι
α : ι → Type u_3
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
⊢ Continuous[instTopologicalSpaceSubtype, Pi.topologicalSpace]
    fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) ↦
    Sᶜ.restrict (π := α) (↑x : (a : ι) → α a)

Tactic:
fun_prop
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α_1 : ι → Type u_2
s_1 : Set ((i : ι) → α_1 i)
i : ι
S_1 : Set ι
α : ι → Type u_3
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
refine :
  Continuous[instTopologicalSpaceSubtype, Pi.topologicalSpace]
    fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) (i : (↑S : Type u_1)) ↦
    (↑x : (a : ι) → α a) (↑i : ι)
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd]
    fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) ↦
    (Subtype.mk (p := fun (x : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) ↦ x ∈ Sᶜ.restrict (π := α) '' s)
        (Sᶜ.restrict (π := α) (↑x : (a : ι) → α a)) ⋯,
      fun (i : (↑S : Type u_1)) ↦ (↑x : (a : ι) → α a) (↑i : ι))

Tactic:
refine (Continuous.subtype_mk (by fun_prop) _).prodMk ?_

Premises used: Continuous.subtype_mk, Continuous.prodMk
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α_1 : ι → Type u_2
s_1 : Set ((i : ι) → α_1 i)
i : ι
S_1 : Set ι
α : ι → Type u_3
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
rw :
  ∀ (i : (↑S : Type u_1)),
    Continuous[instTopologicalSpaceSubtype, inst (↑i : ι)]
      fun (a : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) ↦
      (↑a : (a : ι) → α a) (↑i : ι)
⊢ Continuous[instTopologicalSpaceSubtype, Pi.topologicalSpace]
    fun (x : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) (i : (↑S : Type u_1)) ↦
    (↑x : (a : ι) → α a) (↑i : ι)

Tactic:
rw [continuous_pi_iff]

Premises used: continuous_pi_iff
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α_1 : ι → Type u_2
s_1 : Set ((i : ι) → α_1 i)
i : ι
S_1 : Set ι
α : ι → Type u_3
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
⊢ ∀ (i : (↑S : Type u_1)),
    Continuous[instTopologicalSpaceSubtype, inst (↑i : ι)]
      fun (a : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) ↦
      (↑a : (a : ι) → α a) (↑i : ι)

Tactic:
fun _ ↦ (continuous_apply _).comp continuous_subtype_val

Premises used: continuous_subtype_val, Continuous.comp, continuous_apply, Subtype.val
-- Module: Mathlib.Topology.IsClosedRestrict
Goal:
ι : Type u_1
α_1 : ι → Type u_2
s_1 : Set ((i : ι) → α_1 i)
i : ι
S_1 : Set ι
α : ι → Type u_3
inst : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
⊢ ∀ (i : (↑S : Type u_1)),
    Continuous[instTopologicalSpaceSubtype, inst (↑i : ι)]
      fun (a : (↑(Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s) : Type (max u_1 u_3))) ↦
      (↑a : (a : ι) → α a) (↑i : ι)

Tactic:
exact fun _ ↦ (continuous_apply _).comp continuous_subtype_val

Premises used: continuous_subtype_val, Continuous.comp, continuous_apply