awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W Z : (↑(irreducibleComponents Y) : Type u_2)
⊢ LE.le.{u_1} (α := (↑(irreducibleComponents X) : Type u_1))
      (({
              toFun := fun (W : (↑(irreducibleComponents Y) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Set X) ↦ x ∈ irreducibleComponents X) (f ⁻¹' (↑W : Set Y)) ⋯,
              invFun := fun (W : (↑(irreducibleComponents X) : Type u_1)) ↦
                Subtype.mk (p := fun (x : Set Y) ↦ x ∈ irreducibleComponents Y) (f '' (↑W : Set X)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(irreducibleComponents Y) : Type u_2)) → (↑(irreducibleComponents X) : Type u_1))
          W :
        (↑(irreducibleComponents X) : Type u_1))
      (({
              toFun := fun (W : (↑(irreducibleComponents Y) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Set X) ↦ x ∈ irreducibleComponents X) (f ⁻¹' (↑W : Set Y)) ⋯,
              invFun := fun (W : (↑(irreducibleComponents X) : Type u_1)) ↦
                Subtype.mk (p := fun (x : Set Y) ↦ x ∈ irreducibleComponents Y) (f '' (↑W : Set X)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(irreducibleComponents Y) : Type u_2)) → (↑(irreducibleComponents X) : Type u_1))
          Z :
        (↑(irreducibleComponents X) : Type u_1)) ↔
    W ≤ Z
have refine : ∀
  (H :
    LE.le.{u_1} (α := (↑(irreducibleComponents X) : Type u_1))
      (({
              toFun := fun (W : (↑(irreducibleComponents Y) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Set X) ↦ x ∈ irreducibleComponents X) (f ⁻¹' (↑W : Set Y)) sorry,
              invFun := fun (W : (↑(irreducibleComponents X) : Type u_1)) ↦
                Subtype.mk (p := fun (x : Set Y) ↦ x ∈ irreducibleComponents Y) (f '' (↑W : Set X)) sorry,
              left_inv := sorry, right_inv := sorry } :
            (a : (↑(irreducibleComponents Y) : Type u_2)) → (↑(irreducibleComponents X) : Type u_1))
          W :
        (↑(irreducibleComponents X) : Type u_1))
      (({
              toFun := fun (W : (↑(irreducibleComponents Y) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Set X) ↦ x ∈ irreducibleComponents X) (f ⁻¹' (↑W : Set Y)) sorry,
              invFun := fun (W : (↑(irreducibleComponents X) : Type u_1)) ↦
                Subtype.mk (p := fun (x : Set Y) ↦ x ∈ irreducibleComponents Y) (f '' (↑W : Set X)) sorry,
              left_inv := sorry, right_inv := sorry } :
            (a : (↑(irreducibleComponents Y) : Type u_2)) → (↑(irreducibleComponents X) : Type u_1))
          Z :
        (↑(irreducibleComponents X) : Type u_1))),
  W ≤ Z
Tactic: refine ⟨fun H ↦ ?_, Set.preimage_mono⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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
⊢ x = y
have obtain : ∀ (U : Set X) (hU : IsOpen[inst] U) (hUx : U ∩ s = {x}), x = y
Tactic: obtain ⟨U, hU, hUx⟩ := isDiscrete_iff_forall_exists_isOpen.mp hs x hxs
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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}
⊢ x = y
have obtain : ∀ (V : Set X) (hV : IsOpen[inst] V) (hVy : V ∩ s = {y}), x = y
Tactic: obtain ⟨V, hV, hVy⟩ := isDiscrete_iff_forall_exists_isOpen.mp hs y hys
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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}
⊢ x = y
have obtain : ∀ (z : X) (hz : z ∈ s ∩ (U ∩ V)), x = y
Tactic: obtain ⟨z, hz⟩ := hs' _ _ hU hV ⟨x, by grind⟩ ⟨y, by grind⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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.{u_2} (X := Y) univ
have rw : IsPreirreducible (f '' univ)
Tactic: rw [← hf.range_eq, ← Set.image_univ]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
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.{u_2} (X := Y) univ
have rw : IsPreirreducible (f '' univ)
Tactic: rw [← hf.range_eq, ← Set.image_univ]
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (hypothesis)
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)
⊢ reorderRestrictProd (α := α) S s p (↑j : ι) = p.2 j
have hj : (↑j : ι) ∈ S
Tactic: have hj : ↑j ∈ S := j.prop
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (hypothesis)
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)
⊢ reorderRestrictProd (α := α) S s p (↑j : ι) = (↑p.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) j
have hj : (↑j : ι) ∉ S
Tactic: have hj : ↑j ∉ S := j.prop
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
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 : ι))
⊢ Sᶜ.restrict (π := α) (reorderRestrictProd (α := α) S s p) = (↑p.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι))
have h : ∀ (x : (↑Sᶜ : Type u_1)),
  Sᶜ.restrict (π := α) (reorderRestrictProd (α := α) S s p) x = (↑p.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] (reorderRestrictProd (α := α) S s)
have 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
Tactic: refine continuous_pi fun j ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
j : ι
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
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)
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
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 : ι))
⊢ reorderRestrictProd (α := α) S s p ∈ Sᶜ.restrict (π := α) ⁻¹' Sᶜ.restrict (π := α) '' s
have 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
Tactic: obtain ⟨y, hy_mem_s, hy_eq⟩ := p.1.2
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
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))
⊢ 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)
have 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)) sorry,
        fun (i : (↑S : Type u_1)) ↦ (↑x : (a : ι) → α a) (↑i : ι))
      x_1 =
    (↑x : (a : ι) → α a) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
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))
⊢ (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
have 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) sorry)
            ((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)) sorry,
                    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: ext
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
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 : ι))
⊢ (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
have 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)) sorry,
                    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) sorry)
                p)).1 :
        (a : (↑Sᶜ : Type u_1)) → α (↑a : ι))
      x =
    (↑p.1 : (a : (↑Sᶜ : Type u_1)) → α (↑a : ι)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
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
⊢ (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
have 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)) sorry,
                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) sorry)
            p)).2
      x =
    p.2 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
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, 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 : ι))
have 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 : ι)
Tactic: refine (Continuous.subtype_mk (by fun_prop) _).prodMk ?_
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
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))) (i : (↑S : Type u_1)) ↦
    (↑x : (a : ι) → α a) (↑i : ι)
have 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 : ι)
Tactic: rw [continuous_pi_iff]
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α 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)) =
    S.restrict (π := α) '' s
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
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
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst : (i : ι) → TopologicalSpace (α i)
x : (i : (↑S : Type u_1)) → α (↑i : ι)
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.IsClosedRestrict (goal)
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
⊢ IsClosed (S.restrict (π := α) '' s)
have 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)))
Tactic: rw [← Topology.image_snd_preimageImageRestrict]