awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Convenient.OpenClosed
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)
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
⊢ IsGeneratedBy.{u_3, u_1, u_2} X (↑F : Type u_3)

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)
-- Module: Mathlib.Topology.Convenient.OpenClosed
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)
⊢ Subtype.val (p := fun (x : Y) ↦ x ∈ F) '' V ⊆ F

Tactic:
simp
-- Module: Mathlib.Topology.Convenient.OpenClosed
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)
⊢ V = Subtype.val (p := fun (x : Y) ↦ x ∈ F) ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ F) '' V

Tactic:
simp
-- Module: Mathlib.Topology.Convenient.OpenClosed
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)
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)
⊢ IsClosed[instTopologicalSpaceSubtype] V

Tactic:
obtain ⟨V, hV, rfl⟩ : ∃ (T : Set Y), T ⊆ F ∧ V = Subtype.val ⁻¹' T :=
    ⟨Subtype.val '' V, by simp, by simp⟩

Premises used: Subtype.val, rfl, Set
-- Module: Mathlib.Topology.Convenient.OpenClosed
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)

Tactic:
IsClosed.preimage continuous_subtype_val ?_

Premises used: continuous_subtype_val, IsClosed.preimage
-- Module: Mathlib.Topology.Convenient.OpenClosed
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)
refine : IsClosed[inst_1] V
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : Y) ↦ x ∈ F) ⁻¹' V)

Tactic:
refine IsClosed.preimage continuous_subtype_val ?_

Premises used: continuous_subtype_val, IsClosed.preimage
-- Module: Mathlib.Topology.Convenient.OpenClosed
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)
rw : ∀ ⦃i : ι⦄ (f : ContinuousMap.{u_2, u_3} (X i) Y), IsClosed[inst i] ((⇑f : (a : X i) → Y) ⁻¹' V)
⊢ IsClosed[inst_1] V

Tactic:
rw [IsGeneratedBy.isClosed_iff X]

Premises used: Topology.IsGeneratedBy.isClosed_iff
-- Module: Mathlib.Topology.Convenient.OpenClosed
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⟩.fst]
    (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)

Tactic:
(W ⟨i, f⟩).isClosed.isClosedMap_subtype_val _ (hV ⟨i, f⟩)

Premises used: TopologicalSpace.Closeds.isClosed, IsClosed.isClosedMap_subtype_val, Sigma.mk
-- Module: Mathlib.Topology.Convenient.OpenClosed
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
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))))
⊢ IsClosed[inst i] ((⇑f : (a : X i) → Y) ⁻¹' V)

Tactic:
convert! (W ⟨i, f⟩).isClosed.isClosedMap_subtype_val _ (hV ⟨i, f⟩)

Premises used: TopologicalSpace.Closeds.isClosed, IsClosed.isClosedMap_subtype_val, Sigma.mk
-- Module: Mathlib.Topology.Convenient.OpenClosed
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
⊢ 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:
aesop
-- Module: Mathlib.Topology.Convenient.OpenClosed
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
U : Type u_4
inst_4 : TopologicalSpace U
f : U → Y
hf : IsClosedEmbedding f
⊢ IsGeneratedBy X U

Tactic:
have := hf.isClosed_range.isGeneratedBy (X := X)
  hf.toIsEmbedding.toHomeomorph.symm.isQuotientMap.isGeneratedBy

Premises used: IsClosed.isGeneratedBy, Topology.IsClosedEmbedding.toIsEmbedding, Homeomorph.symm, Topology.IsQuotientMap.isGeneratedBy, Topology.IsClosedEmbedding.isClosed_range, Topology.IsEmbedding.toHomeomorph, Homeomorph.isQuotientMap
-- Module: Mathlib.Topology.Covering.AddCircle
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : IsTopologicalAddGroup 𝕜
inst_3 : DiscreteTopology.{u_1} ↥(zmultiples p)
⊢ IsAddQuotientCoveringMap.{u_1, u_1, u_1} (E := 𝕜) (X := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
    QuotientAddGroup.mk ↥(zmultiples p)

Tactic:
isAddQuotientCoveringMap_of_comm _ DiscreteTopology.isDiscrete

Premises used: DiscreteTopology.isDiscrete, AddSubgroup.isAddQuotientCoveringMap_of_comm
-- Module: Mathlib.Topology.Covering.AddCircle
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : IsTopologicalAddGroup 𝕜
inst_3 : DiscreteTopology.{u_1} ↥(zmultiples p)
⊢ IsCoveringMap.{u_1, u_1} (E := 𝕜) (X := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
    QuotientAddGroup.mk

Tactic:
(isAddQuotientCoveringMap_coe p).isCoveringMap

Premises used: AddCircle.isAddQuotientCoveringMap_coe, IsAddQuotientCoveringMap.isCoveringMap
-- Module: Mathlib.Topology.Covering.AddCircle
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : IsTopologicalAddGroup 𝕜
inst_3 : DiscreteTopology.{u_1} ↥(zmultiples p)
⊢ IsLocalHomeomorph.{u_1, u_1} (X := 𝕜) (Y := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
    QuotientAddGroup.mk

Tactic:
(isCoveringMap_coe p).isLocalHomeomorph

Premises used: IsCoveringMap.isLocalHomeomorph, AddCircle.isCoveringMap_coe
-- Module: Mathlib.Topology.Covering.AddCircle
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))

Tactic:
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 _ ↦ ?_)

Premises used: isQuotientMap_quotient_mk', IsUnit.isQuotientMap_zsmul, QuotientAddGroup.mk', Set.Finite.isDiscrete, Topology.IsQuotientMap.isAddQuotientCoveringMap_of_isDiscrete_ker_addMonoidHom, AddCircle.finite_torsion_of_isSMulRegular_int
-- Module: Mathlib.Topology.Covering.AddCircle
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 : 𝕜)
refine : ∀ (x : 𝕜) ⦃a₂ : 𝕜⦄, Eq.{u_1 + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ n • x) x) ((fun (x : 𝕜) ↦ n • x) a₂) → x = a₂
⊢ IsAddQuotientCoveringMap (X := AddCircle p) (fun (x : AddCircle p) ↦ n • x) ↥(AddMonoidHom.ker (zsmulAddGroupHom n))

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 _ ↦ ?_)

Premises used: isQuotientMap_quotient_mk', IsUnit.isQuotientMap_zsmul, QuotientAddGroup.mk', Set.Finite.isDiscrete, Topology.IsQuotientMap.isAddQuotientCoveringMap_of_isDiscrete_ker_addMonoidHom, AddCircle.finite_torsion_of_isSMulRegular_int
-- Module: Mathlib.Topology.Covering.AddCircle
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 : 𝕜
simp_rw : ∀ ⦃a₂ : 𝕜⦄, (↑n : 𝕜) * x = (↑n : 𝕜) * a₂ → x = a₂
⊢ ∀ ⦃a₂ : 𝕜⦄, Eq.{u_1 + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ n • x) x) ((fun (x : 𝕜) ↦ n • x) a₂) → x = a₂

Tactic:
simp_rw [zsmul_eq_mul]

Premises used: zsmul_eq_mul
-- Module: Mathlib.Topology.Covering.AddCircle
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₂ : 𝕜⦄, (↑n : 𝕜) * x = (↑n : 𝕜) * a₂ → x = a₂

Tactic:
apply hn.isSMulRegular 𝕜

Premises used: IsUnit.isSMulRegular
-- Module: Mathlib.Topology.Covering.AddCircle
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) ↦ HSMul.hSMul (α := ℤ) (↑n : ℤ) x)
    ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ)))

Tactic:
isAddQuotientCoveringMap_zsmul p (n := n) (mod_cast hn)

Premises used: Int.cast_natCast, congrArg, IsUnit, cast, AddCircle.isAddQuotientCoveringMap_zsmul, Eq.symm
-- Module: Mathlib.Topology.Covering.AddCircle
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 : 𝕜)
h : ∀ (x : AddCircle p), Eq (α := AddCircle p → AddCircle p) (HSMul.hSMul n) (HSMul.hSMul (α := ℤ) (↑n : ℤ))
h₁ :
  ∀ (x : AddCircle p), Eq.{u_1 + 1} (α := AddCircle p →+ AddCircle p) (nsmulAddMonoidHom n) (zsmulAddGroupHom (↑n : ℤ))
h₂ :
  ↥(AddMonoidHom.ker (nsmulAddMonoidHom n)) = ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ))) →
    Eq.{u_1 + 1} (α := AddCircle p →+ AddCircle p) (nsmulAddMonoidHom n) (zsmulAddGroupHom (↑n : ℤ))
h₃ :
  ↥(AddMonoidHom.ker (nsmulAddMonoidHom n)) = ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ))) →
    HEq.{u_1 + 1} (α := AddGroup ↥(AddMonoidHom.ker (nsmulAddMonoidHom n)))
        (AddSubgroup.toAddGroup (AddMonoidHom.ker (nsmulAddMonoidHom n))) (β :=
        AddGroup ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ))))
        (AddSubgroup.toAddGroup (AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ)))) →
      Eq.{u_1 + 1} (α := AddCircle p →+ AddCircle p) (nsmulAddMonoidHom n) (zsmulAddGroupHom (↑n : ℤ))
⊢ IsAddQuotientCoveringMap (X := AddCircle p) (fun (x : AddCircle p) ↦ n • x) ↥(AddMonoidHom.ker (nsmulAddMonoidHom n))

Tactic:
convert! isAddQuotientCoveringMap_zsmul p (n := n) (mod_cast hn)

Premises used: AddCircle.isAddQuotientCoveringMap_zsmul
-- Module: Mathlib.Topology.Covering.AddCircle
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 : AddCircle p
h : ∀ (x : AddCircle p), n • x = HSMul.hSMul (α := ℤ) (↑n : ℤ) x
⊢ Eq (α := AddCircle p → AddCircle p) (HSMul.hSMul n) (HSMul.hSMul (α := ℤ) (↑n : ℤ))

Tactic:
ext
-- Module: Mathlib.Topology.Covering.AddCircle
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 x_1 : AddCircle p
⊢ n • x_1 = HSMul.hSMul (α := ℤ) (↑n : ℤ) x_1

Tactic:
simp
-- Module: Mathlib.Topology.Covering.AddCircle
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 : AddCircle p
h :
  ∀ (x : 𝕜),
    Eq (α := AddCircle p)
      ((AddMonoidHom.comp (nsmulAddMonoidHom n) (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) :
            (a : 𝕜) → AddCircle p)
          x :
        AddCircle p)
      ((AddMonoidHom.comp (zsmulAddGroupHom (↑n : ℤ)) (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) :
            (a : 𝕜) → AddCircle p)
          x :
        AddCircle p)
⊢ Eq.{u_1 + 1} (α := AddCircle p →+ AddCircle p) (nsmulAddMonoidHom n) (zsmulAddGroupHom (↑n : ℤ))

Tactic:
ext