awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x_1 : 𝕜
⊢ Eq (α := AddCircle p)
    ((AddMonoidHom.comp (nsmulAddMonoidHom n) (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) : (a : 𝕜) → AddCircle p)
        x_1 :
      AddCircle p)
    ((AddMonoidHom.comp (zsmulAddGroupHom (↑n : ℤ)) (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) :
          (a : 𝕜) → AddCircle p)
        x_1 :
      AddCircle p)

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 : 𝕜)
e_6 : ↥(AddMonoidHom.ker (nsmulAddMonoidHom n)) = ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ)))
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
-- 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 : 𝕜)
e_6 : ↥(AddMonoidHom.ker (nsmulAddMonoidHom n)) = ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ)))
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)

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 : 𝕜)
e_6 : ↥(AddMonoidHom.ker (nsmulAddMonoidHom n)) = ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ)))
e_7 :
  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 : ℤ))))
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
-- 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 : 𝕜)
e_6 : ↥(AddMonoidHom.ker (nsmulAddMonoidHom n)) = ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ)))
e_7 :
  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 : ℤ))))
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)

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)
inst_4 : Algebra ℚ 𝕜
n : ℤ
inst_5 : NeZero n
⊢ IsUnit (M := 𝕜) ((algebraMap ℚ 𝕜 : (a : ℚ) → 𝕜) (↑n : ℚ) : 𝕜)

Tactic:
(Int.cast_ne_zero.mpr <| NeZero.ne n).isUnit.map (algebraMap ℚ 𝕜)

Premises used: Algebra.algebraMap, Ne.isUnit, Rat, IsUnit.map
-- 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)
inst_4 : Algebra ℚ 𝕜
n : ℤ
inst_5 : NeZero n
h : Eq (α := 𝕜) ((↑n : 𝕜) : 𝕜) ((algebraMap ℚ 𝕜 : (a : ℚ) → 𝕜) (↑n : ℚ) : 𝕜)
⊢ IsUnit.{u_1} (M := 𝕜) (↑n : 𝕜)

Tactic:
convert! (Int.cast_ne_zero.mpr <| NeZero.ne n).isUnit.map (algebraMap ℚ 𝕜)

Premises used: Algebra.algebraMap, Ne.isUnit, Rat, IsUnit.map
-- 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)
inst_4 : Algebra ℚ 𝕜
n : ℤ
inst_5 : NeZero n
⊢ Eq (α := 𝕜) ((↑n : 𝕜) : 𝕜) ((algebraMap ℚ 𝕜 : (a : ℚ) → 𝕜) (↑n : ℚ) : 𝕜)

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)
inst_4 : Algebra ℚ 𝕜
n : ℕ
inst_5 : NeZero n
⊢ IsUnit (M := 𝕜) ((algebraMap ℚ 𝕜 : (a : ℚ) → 𝕜) (↑n : ℚ) : 𝕜)

Tactic:
(Nat.cast_ne_zero.mpr <| NeZero.ne n).isUnit.map (algebraMap ℚ 𝕜)

Premises used: Algebra.algebraMap, Ne.isUnit, Rat, IsUnit.map
-- 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)
inst_4 : Algebra ℚ 𝕜
n : ℕ
inst_5 : NeZero n
h : Eq (α := 𝕜) ((↑n : 𝕜) : 𝕜) ((algebraMap ℚ 𝕜 : (a : ℚ) → 𝕜) (↑n : ℚ) : 𝕜)
⊢ IsUnit.{u_1} (M := 𝕜) (↑n : 𝕜)

Tactic:
convert! (Nat.cast_ne_zero.mpr <| NeZero.ne n).isUnit.map (algebraMap ℚ 𝕜)

Premises used: Algebra.algebraMap, Ne.isUnit, Rat, IsUnit.map
-- 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)
inst_4 : Algebra ℚ 𝕜
n : ℕ
inst_5 : NeZero n
⊢ Eq (α := 𝕜) ((↑n : 𝕜) : 𝕜) ((algebraMap ℚ 𝕜 : (a : ℚ) → 𝕜) (↑n : ℚ) : 𝕜)

Tactic:
simp
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
h : IsEvenlyCovered f x I
choose :
  DiscreteTopology I →
    (U : Set X) →
      (hxU : x ∈ U) →
        (hU : IsOpen[inst_1] U) →
          (hfU : IsOpen[inst] (f ⁻¹' U)) →
            (H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I) →
              (hH :
                  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
                    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)) →
                Homeomorph.{u_3, u_1} I (↑(f ⁻¹' {x}) : Type u_1)
⊢ Homeomorph.{u_3, u_1} I (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
choose _ U hxU hU hfU H hH using h
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
i : I
⊢ (↑((H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1)) (Subtype.mk (p := fun (x : X) ↦ x ∈ U) x hxU, i)) :
      E) ∈
    f ⁻¹' {x}

Tactic:
simp [← hH]
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
e : (↑(f ⁻¹' {x}) : Type u_1)
rwa : f (↑e : E) ∈ U
rwa₁ rwa₂ rwa₃ rwa₄ : x ∈ U
⊢ (↑e : E) ∈ f ⁻¹' U

Tactic:
rwa [Set.mem_preimage, (e.2 : f e = x)]

Premises used: Set.mem_preimage, Subtype.property
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
x_1 : I
⊢ (fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦
        (((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
              (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) (↑e : E) ⋯)).2 :
          I))
      ((fun (i : I) ↦
          Subtype.mk (p := fun (x_2 : E) ↦ x_2 ∈ f ⁻¹' {x})
            (↑((H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1))
                  (Subtype.mk (p := fun (x : X) ↦ x ∈ U) x hxU, i)) :
              E)
            ⋯)
        x_1) =
    x_1

Tactic:
simp
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
e : (↑(f ⁻¹' {x}) : Type u_1)
⊢ Eq.{u_2 + 1} (α := X)
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
            (Set.inclusion (s := f ⁻¹' {x}) (t := f ⁻¹' U) ⋯
              ((fun (i : I) ↦
                  Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ f ⁻¹' {x})
                    (↑((H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1))
                          (Subtype.mk (p := fun (x : X) ↦ x ∈ U) x hxU, i)) :
                      E)
                    ⋯)
                ((fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦
                    (((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                          (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) (↑e : E) ⋯)).2 :
                      I))
                  e)))).1 :
      X)
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
            (Set.inclusion (s := f ⁻¹' {x}) (t := f ⁻¹' U) ⋯ e)).1 :
      X)

Tactic:
simpa [hH] using e.2.symm

Premises used: Eq.symm, Subtype.property
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
e : (↑(f ⁻¹' {x}) : Type u_1)
⊢ Eq.{u_3 + 1} (α := I)
    ((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
        (Set.inclusion (s := f ⁻¹' {x}) (t := f ⁻¹' U) ⋯
          ((fun (i : I) ↦
              Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ f ⁻¹' {x})
                (↑((H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1))
                      (Subtype.mk (p := fun (x : X) ↦ x ∈ U) x hxU, i)) :
                  E)
                ⋯)
            ((fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦
                (((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                      (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) (↑e : E) ⋯)).2 :
                  I))
              e)))).2
    ((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) (Set.inclusion (s := f ⁻¹' {x}) (t := f ⁻¹' U) ⋯ e)).2

Tactic:
simp
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
⊢ Continuous[inst_2, instTopologicalSpaceSubtype] fun (i : I) ↦
    Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ f ⁻¹' {x})
      (↑((H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1))
            (Subtype.mk (p := fun (x : X) ↦ x ∈ U) x hxU, i)) :
        E)
      ⋯

Tactic:
fun_prop
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
⊢ Continuous[instTopologicalSpaceSubtype, inst_2] fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦
    ((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) (↑e : E) ⋯)).2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
⊢ Homeomorph.{u_3, u_1} I (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
exact
  { toFun i := ⟨H.symm (⟨x, hxU⟩, i), by simp [← hH]⟩
    invFun e := (H ⟨e, by rwa [Set.mem_preimage, (e.2 : f e = x)]⟩).2
    left_inv _ := by simp
    right_inv e := Set.inclusion_injective (Set.preimage_mono (Set.singleton_subset_iff.mpr hxU)) <|
      H.injective <| Prod.ext (Subtype.ext <| by simpa [hH] using e.2.symm) (by simp)
    continuous_toFun := by fun_prop
    continuous_invFun := by fun_prop }
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
h : IsEvenlyCovered f x I
⊢ DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
have := h.1; h.fiberHomeomorph.discreteTopology

Premises used: IsEvenlyCovered.fiberHomeomorph, And.left, Homeomorph.discreteTopology
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
inst_3 : Nonempty I
h : IsEvenlyCovered f x I
choose :
  DiscreteTopology I →
    (U : Set X) →
      (hxU : x ∈ U) →
        (hU : IsOpen[inst_1] U) →
          (hfU : IsOpen[inst] (f ⁻¹' U)) →
            (H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I) →
              (hH :
                  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
                    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)) →
                Trivialization I f
⊢ Trivialization I f

Tactic:
choose _ U hxU hU hfU H hH using h
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
inst_3 : Nonempty I
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
e : E
he : f e ∈ U
⊢ (if he : f e ∈ U then
      ((↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e he)).1 :
          X),
        ((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e he)).2)
    else (x, Classical.arbitrary I)) ∈
    SProd.sprod (β := Set I) U Set.univ

Tactic:
simp [he]
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
inst_3 : Nonempty I
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
e : E
he : f e ∈ U
⊢ (↑((H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1))
          (if hx :
                (if he : f e ∈ U then
                      ((↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                                (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e he)).1 :
                          X),
                        ((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e he)).2)
                    else (x, Classical.arbitrary I)).1 ∈
                  U then
              Subtype.mk (p := fun (x : X) ↦ x ∈ U)
                (if he : f e ∈ U then
                    ((↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                              (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e he)).1 :
                        X),
                      ((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                          (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e he)).2)
                  else (x, Classical.arbitrary I)).1
                hx
            else Subtype.mk (p := fun (x : X) ↦ x ∈ U) x hxU,
            (if he : f e ∈ U then
                ((↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                          (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e he)).1 :
                    X),
                  ((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                      (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e he)).2)
              else (x, Classical.arbitrary I)).2)) :
      E) =
    e

Tactic:
simp [he]
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
inst_3 : Nonempty I
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
xi : X × I
hx : xi.1 ∈ U
⊢ (if he :
        f
            (↑((H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1))
                  (if hx : xi.1 ∈ U then Subtype.mk (p := fun (x : X) ↦ x ∈ U) xi.1 hx
                    else Subtype.mk (p := fun (x : X) ↦ x ∈ U) x hxU,
                    xi.2)) :
              E) ∈
          U then
      ((↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U)
                  (↑((H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1))
                        (if hx : xi.1 ∈ U then Subtype.mk (p := fun (x : X) ↦ x ∈ U) xi.1 hx
                          else Subtype.mk (p := fun (x : X) ↦ x ∈ U) x hxU,
                          xi.2)) :
                    E)
                  he)).1 :
          X),
        ((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U)
              (↑((H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1))
                    (if hx : xi.1 ∈ U then Subtype.mk (p := fun (x : X) ↦ x ∈ U) xi.1 hx
                      else Subtype.mk (p := fun (x : X) ↦ x ∈ U) x hxU,
                      xi.2)) :
                E)
              he)).2)
    else (x, Classical.arbitrary I)) =
    xi

Tactic:
simpa [hx] using fun h ↦ (h (H.symm _).2).elim
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
inst_3 : Nonempty I
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
x_1 : (↑(f ⁻¹' U) : Type u_1)
e : E
he : f e ∈ U
⊢ Eq (α := X × I)
    (Function.comp (α := (↑(f ⁻¹' U) : Type u_1)) (β := Prod.{u_2, u_3} { x : X // x ∈ U } I)
      (Prod.map (Subtype.val (p := fun (x : X) ↦ x ∈ U)) id) (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e he))
    ((f ⁻¹' U).restrict («π» := fun (a : E) ↦ X × I)
      (fun (e : E) ↦
        if he : f e ∈ U then
          ((↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                    (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e he)).1 :
              X),
            ((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e he)).2)
        else (x, Classical.arbitrary I))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e he))

Tactic:
simp [Prod.map, he]

Premises used: Prod.map
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
inst_3 : Nonempty I
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd]
    fun (ui : (↑(SProd.sprod (β := Set I) U Set.univ) : Type (max u_2 u_3))) ↦
    (Subtype.mk (p := fun (x : X) ↦ x ∈ U) (↑ui : X × I).1 ⋯, (↑ui : X × I).2)

Tactic:
fun_prop