awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set (↑U : Type u_3)),
    (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsOpen[instTopologicalSpaceSubtype] V
⊢ Continuous[instTopologicalSpaceSubtype, _]
    (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
      (a : (↑U : Type u_3)) → WithGeneratedByTopology X (↑U : Type u_3))
have continuous_equiv_symm : ∀ (s : Set (WithGeneratedByTopology X (↑U : Type u_3))),
  IsOpen s →
    IsOpen[instTopologicalSpaceSubtype]
      ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
          (a : (↑U : Type u_3)) → WithGeneratedByTopology X (↑U : Type u_3)) ⁻¹'
        s)
Tactic: rw [continuous_def]
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
⊢ IsGeneratedBy.{u_3, u_1, u_2} X (↑U : Type u_3)
have suffices : ∀ (V : Set (↑U : Type u_3)),
  (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
    IsOpen[instTopologicalSpaceSubtype] V
Tactic: suffices ∀ (V : Set U), (∀ a, IsOpen ((g a) ⁻¹' V)) → IsOpen V by
    constructor
    rw [continuous_def]
    exact fun _ hV ↦ this _ (fun a ↦
      ((IsGeneratedBy.equiv_symm_comp_continuous_iff X _).2 (hg a)).isOpen_preimage _ hV)
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set (↑U : Type u_3)
hV : ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ IsOpen[instTopologicalSpaceSubtype] V
have obtain : ∀ (V : Set Y) (hV : V ⊆ U)
  (hV :
    ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
      IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)),
  IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)
Tactic: obtain ⟨V, hV, rfl⟩ : ∃ (T : Set Y), T ⊆ U ∧ V = Subtype.val ⁻¹' T :=
    ⟨Subtype.val '' V, by simp, by simp⟩
Cleared hypotheses: V, hV
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV_1 : V ⊆ U
hV :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)
have refine : IsOpen[inst_1] V
Tactic: refine continuous_subtype_val.isOpen_preimage _ ?_
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV_1 : V ⊆ U
hV :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)
⊢ IsOpen[inst_1] V
have rw : ∀ ⦃i : ι⦄ (f : ContinuousMap.{u_2, u_3} (X i) Y), IsOpen[inst i] ((⇑f : (a : X i) → Y) ⁻¹' V)
Tactic: rw [IsGeneratedBy.isOpen_iff X]
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV_1 : V ⊆ U
hV :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)
i : ι
f : ContinuousMap.{u_2, u_3} (X i) Y
⊢ IsOpen[inst i] ((⇑f : (a : X i) → Y) ⁻¹' V)
have h : Eq (α := Set (X i)) ((⇑f : (a : X i) → Y) ⁻¹' V : Set (X i))
  (Subtype.val (p :=
        fun
          (x :
            X
              (Sigma.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)
                (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f))) ↦
        x ∈ (↑(W (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f)) : Set (X ⟨i, f⟩.fst))) ''
      g (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f) ⁻¹'
        Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V :
    Set
      (X
        (Sigma.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)
          (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f))))
Tactic: convert! (W ⟨i, f⟩).isOpen.isOpenMap_subtype_val _ (hV ⟨i, f⟩)
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst_3 : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst_1] F
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Closeds (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' F,
      isClosed' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑F : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    F.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
⊢ IsGeneratedBy.{u_3, u_1, u_2} X (↑F : Type u_3)
have hg : ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
  Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
Tactic: have hg (a) : Continuous (g a) := a.2.continuous.restrictPreimage
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst_3 : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst_1] F
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Closeds (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' F,
      isClosed' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑F : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    F.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set (↑F : Type u_3)),
    (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsClosed[instTopologicalSpaceSubtype] V
⊢ IsGeneratedBy.{u_3, u_1, u_2} X (↑F : Type u_3)
have continuous_equiv_symm : Continuous[instTopologicalSpaceSubtype, _]
  (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
    (a : (↑F : Type u_3)) → WithGeneratedByTopology X (↑F : Type u_3))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst_3 : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst_1] F
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Closeds (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' F,
      isClosed' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑F : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    F.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set (↑F : Type u_3)),
    (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsClosed[instTopologicalSpaceSubtype] V
⊢ Continuous[instTopologicalSpaceSubtype, _]
    (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
      (a : (↑F : Type u_3)) → WithGeneratedByTopology X (↑F : Type u_3))
have continuous_equiv_symm : ∀ (s : Set (WithGeneratedByTopology X (↑F : Type u_3))),
  IsClosed s →
    IsClosed[instTopologicalSpaceSubtype]
      ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
          (a : (↑F : Type u_3)) → WithGeneratedByTopology X (↑F : Type u_3)) ⁻¹'
        s)
Tactic: rw [continuous_iff_isClosed]
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst_3 : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst_1] F
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Closeds (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' F,
      isClosed' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑F : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    F.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
⊢ IsGeneratedBy.{u_3, u_1, u_2} X (↑F : Type u_3)
have suffices : ∀ (V : Set (↑F : Type u_3)),
  (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
    IsClosed[instTopologicalSpaceSubtype] V
Tactic: suffices ∀ (V : Set F), (∀ a, IsClosed ((g a) ⁻¹' V)) → IsClosed V by
    constructor
    rw [continuous_iff_isClosed]
    exact fun _ hV ↦ this _ (fun a ↦ IsClosed.preimage
      ((IsGeneratedBy.equiv_symm_comp_continuous_iff X _).2 (hg a)) hV)
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst_3 : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst_1] F
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Closeds (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' F,
      isClosed' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑F : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    F.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set (↑F : Type u_3)
hV : ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ IsClosed[instTopologicalSpaceSubtype] V
have obtain : ∀ (V : Set Y) (hV : V ⊆ F)
  (hV :
    ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
      IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ F) ⁻¹' V)),
  IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : Y) ↦ x ∈ F) ⁻¹' V)
Tactic: obtain ⟨V, hV, rfl⟩ : ∃ (T : Set Y), T ⊆ F ∧ V = Subtype.val ⁻¹' T :=
    ⟨Subtype.val '' V, by simp, by simp⟩
Cleared hypotheses: V, hV
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst_3 : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst_1] F
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Closeds (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' F,
      isClosed' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑F : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    F.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV_1 : V ⊆ F
hV :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ F) ⁻¹' V)
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : Y) ↦ x ∈ F) ⁻¹' V)
have refine : IsClosed[inst_1] V
Tactic: refine IsClosed.preimage continuous_subtype_val ?_
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst_3 : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst_1] F
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Closeds (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' F,
      isClosed' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑F : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    F.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV_1 : V ⊆ F
hV :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ F) ⁻¹' V)
⊢ IsClosed[inst_1] V
have rw : ∀ ⦃i : ι⦄ (f : ContinuousMap.{u_2, u_3} (X i) Y), IsClosed[inst i] ((⇑f : (a : X i) → Y) ⁻¹' V)
Tactic: rw [IsGeneratedBy.isClosed_iff X]
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst_3 : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst_1] F
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Closeds (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' F,
      isClosed' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑F : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    F.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV_1 : V ⊆ F
hV :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ F) ⁻¹' V)
i : ι
f : ContinuousMap.{u_2, u_3} (X i) Y
⊢ IsClosed[inst i] ((⇑f : (a : X i) → Y) ⁻¹' V)
have h : Eq (α := Set (X i)) ((⇑f : (a : X i) → Y) ⁻¹' V : Set (X i))
  (Subtype.val (p :=
        fun
          (x :
            X
              (Sigma.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)
                (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f))) ↦
        x ∈ (↑(W (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f)) : Set (X ⟨i, f⟩.fst))) ''
      g (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f) ⁻¹'
        Subtype.val (p := fun (x : Y) ↦ x ∈ F) ⁻¹' V :
    Set
      (X
        (Sigma.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)
          (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f))))
Tactic: convert! (W ⟨i, f⟩).isClosed.isClosedMap_subtype_val _ (hV ⟨i, f⟩)
-- Lean 4 proof step from Mathlib.Topology.Covering.AddCircle (goal)
Goal:
𝕜 : Type u_1
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : IsTopologicalRing 𝕜
p : 𝕜
inst_3 : T0Space.{u_1} (AddCircle p)
n : ℤ
hn : IsUnit.{u_1} (M := 𝕜) (↑n : 𝕜)
⊢ IsAddQuotientCoveringMap (X := AddCircle p) (fun (x : AddCircle p) ↦ n • x) ↥(AddMonoidHom.ker (zsmulAddGroupHom n))
have refine : ∀ (x : 𝕜) ⦃a₂ : 𝕜⦄, Eq.{u_1 + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ n • x) x) ((fun (x : 𝕜) ↦ n • x) a₂) → x = a₂
Tactic: refine hn.isQuotientMap_zsmul (QuotientAddGroup.mk' _) isQuotientMap_quotient_mk'
    |>.isAddQuotientCoveringMap_of_isDiscrete_ker_addMonoidHom
    (f := zsmulAddGroupHom (α := AddCircle p) n)
    (Set.Finite.isDiscrete <| finite_torsion_of_isSMulRegular_int _ _ fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Covering.AddCircle (goal)
Goal:
𝕜 : Type u_1
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : IsTopologicalRing 𝕜
p : 𝕜
inst_3 : T0Space.{u_1} (AddCircle p)
n : ℤ
hn : IsUnit.{u_1} (M := 𝕜) (↑n : 𝕜)
x : 𝕜
⊢ ∀ ⦃a₂ : 𝕜⦄, Eq.{u_1 + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ n • x) x) ((fun (x : 𝕜) ↦ n • x) a₂) → x = a₂
have simp_rw : ∀ ⦃a₂ : 𝕜⦄, (↑n : 𝕜) * x = (↑n : 𝕜) * a₂ → x = a₂
Tactic: simp_rw [zsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Covering.AddCircle (goal)
Goal:
𝕜 : Type u_1
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : IsTopologicalRing 𝕜
p : 𝕜
inst_3 : T0Space.{u_1} (AddCircle p)
n : ℕ
hn : IsUnit.{u_1} (M := 𝕜) (↑n : 𝕜)
⊢ IsAddQuotientCoveringMap (X := AddCircle p) (fun (x : AddCircle p) ↦ n • x) ↥(AddMonoidHom.ker (nsmulAddMonoidHom n))
have h : ∀ (x : AddCircle p), Eq (α := AddCircle p → AddCircle p) (HSMul.hSMul n) (HSMul.hSMul (α := ℤ) (↑n : ℤ))
Tactic: convert! isAddQuotientCoveringMap_zsmul p (n := n) (mod_cast hn)