awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
p : 𝕜[X]
x : 𝕜
hx :
  Membership.mem (γ := Set 𝕜)
    (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ eval x p)
      ((fun (x : 𝕜) ↦ eval x p) '' {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) p) = 0})ᶜ)
    x
⊢ Eq.{u_1 + 1} (α := 𝕜 → 𝕜)
    (↑(HasStrictFDerivAt.toOpenPartialHomeomorph fun (x : 𝕜) ↦ eval x p (f' :=
            (ContinuousLinearEquiv.unitsEquivAut 𝕜 : (a : 𝕜ˣ) → 𝕜 ≃L[𝕜] 𝕜)
              (Units.mk0 (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)) ⋯))
            ⋯ :
          OpenPartialHomeomorph 𝕜 𝕜) :
      𝕜 → 𝕜)
    fun (x : 𝕜) ↦ eval x p

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
p : 𝕜[X]
refine :
  ∀ (x : 𝕜)
    (hx :
      Membership.mem (γ := Set 𝕜)
        ((fun (x : 𝕜) ↦ eval x p) '' {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) p) = 0})ᶜ x),
    Set.Finite (α := 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ eval x p) {x})
⊢ IsCoveringMapOn (X := 𝕜) (fun (x : 𝕜) ↦ eval x p)
    ((fun (x : 𝕜) ↦ eval x p) '' {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) p) = 0})ᶜ

Tactic:
refine p.isClosedMap_eval.isCoveringMapOn_of_openPartialHomeomorph (fun x hx ↦ ?_)
    fun x hx ↦ ⟨_, ((p.hasStrictDerivAt x).hasStrictFDerivAt_equiv
      fun h ↦ hx ⟨x, h, rfl⟩).mem_toOpenPartialHomeomorph_source, by simp⟩
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
p : 𝕜[X]
x : 𝕜
hx :
  Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) p) = 0})ᶜ x
inl :
  ∀
    (hx :
      Membership.mem (γ := Set 𝕜)
        ((fun (x_1 : 𝕜) ↦ eval x_1 ((C : (a : 𝕜) → 𝕜[X]) x)) ''
            {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) x)) = 0})ᶜ
        x),
    Set.Finite (α := 𝕜) (Set.preimage (β := 𝕜) (fun (x_1 : 𝕜) ↦ eval x_1 ((C : (a : 𝕜) → 𝕜[X]) x)) {x})
inr : ∀ (ne : p ≠ (C : (a : 𝕜) → 𝕜[X]) x), Set.Finite (α := 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ eval x p) {x})
⊢ Set.Finite (α := 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ eval x p) {x})

Tactic:
obtain rfl | ne := eq_or_ne p (C x)

Premises used: Polynomial.C, eq_or_ne, DFunLike.coe, rfl
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
x : 𝕜
hx :
  Membership.mem (γ := Set 𝕜)
    ((fun (x_1 : 𝕜) ↦ eval x_1 ((C : (a : 𝕜) → 𝕜[X]) x)) ''
        {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) x)) = 0})ᶜ
    x
⊢ Set.Finite (α := 𝕜) (Set.preimage (β := 𝕜) (fun (x_1 : 𝕜) ↦ eval x_1 ((C : (a : 𝕜) → 𝕜[X]) x)) {x})

Tactic:
simp at hx
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
p : 𝕜[X]
x : 𝕜
hx :
  Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) p) = 0})ᶜ x
ne : p ≠ (C : (a : 𝕜) → 𝕜[X]) x
⊢ Set.Finite (α := 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ eval x p) {x})

Tactic:
simpa only [preimage_eval_singleton ne] using rootSet_finite ..

Premises used: Polynomial.rootSet_finite, Polynomial.preimage_eval_singleton
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
⊢ IsCoveringMapOn (X := 𝕜) (fun (x : 𝕜) ↦ eval x (HPow.hPow (α := 𝕜[X]) X n)) {0}ᶜ

Tactic:
(X ^ n).isCoveringMapOn_eval.mono fun x' h ↦ _

Premises used: Polynomial.isCoveringMapOn_eval, HPow.hPow, IsCoveringMapOn.mono, Polynomial.X
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
h : ∀ (x : 𝕜), x ^ n = eval x (HPow.hPow (α := 𝕜[X]) X n)
convert_2 : ProperSpace 𝕜
convert_5 :
  ∀ (x' : 𝕜) (h : Membership.mem (γ := Set 𝕜) {0}ᶜ x'),
    Membership.mem (γ := Set 𝕜)
      ((fun (x : 𝕜) ↦ eval x (HPow.hPow (α := 𝕜[X]) X n)) ''
          {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) (HPow.hPow (α := 𝕜[X]) X n)) = 0})ᶜ
      x'
⊢ IsCoveringMapOn (X := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ

Tactic:
convert! (X ^ n).isCoveringMapOn_eval.mono fun x' h ↦ _ with x

Premises used: Polynomial.isCoveringMapOn_eval, HPow.hPow, IsCoveringMapOn.mono, Polynomial.X
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
x : 𝕜
⊢ x ^ n = eval x (HPow.hPow (α := 𝕜[X]) X n)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
⊢ ProperSpace 𝕜

Tactic:
assumption
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
x' : 𝕜
h : Membership.mem (γ := Set 𝕜) {0}ᶜ x'
⊢ n ≠ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
x' : 𝕜
h : Membership.mem (γ := Set 𝕜) {0}ᶜ x'
⊢ Membership.mem (γ := Set 𝕜)
    ((fun (x : 𝕜) ↦ eval x (HPow.hPow (α := 𝕜[X]) X n)) ''
        {k : 𝕜 | eval k ((derivative : (a : 𝕜[X]) → 𝕜[X]) (HPow.hPow (α := 𝕜[X]) X n)) = 0})ᶜ
    x'

Tactic:
simpa [derivative_X_pow, hn, show n ≠ 0 by aesop] using fun _ ↦ Ne.symm h

Premises used: Ne.symm, Polynomial.derivative_X_pow
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
⊢ IsCoveringMap (E := (↑{x : 𝕜 | x ≠ 0} : Type u_1)) (X := (↑{0}ᶜ : Type u_1))
    (Function.comp (β := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
      (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
      (⇑(Homeomorph.setCongr (s := {x : 𝕜 | x ≠ 0}) (t := Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) ⋯) :
        (a : (↑{x : 𝕜 | x ≠ 0} : Type u_1)) → (↑((fun (x : 𝕜) ↦ x ^ n) ⁻¹' {0}ᶜ) : Type u_1)))

Tactic:
(isCoveringMapOn_npow n hn).isCoveringMap_restrictPreimage.comp_homeomorph
      (.setCongr (s := {x | x ≠ 0}) _)

Premises used: IsCoveringMap.comp_homeomorph, IsCoveringMapOn.isCoveringMap_restrictPreimage, isCoveringMapOn_npow, Homeomorph.setCongr
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
n₁ : Eq (α := Set 𝕜) {x : 𝕜 | x ≠ 0} (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ)
⊢ IsCoveringMap (X := { x : 𝕜 // x ≠ 0 }) fun (x : { x : 𝕜 // x ≠ 0 }) ↦
    Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) ((↑x : 𝕜) ^ n) ⋯

Tactic:
convert!
    (isCoveringMapOn_npow n hn).isCoveringMap_restrictPreimage.comp_homeomorph
      (.setCongr (s := {x | x ≠ 0}) _) using 1

Premises used: IsCoveringMap.comp_homeomorph, IsCoveringMapOn.isCoveringMap_restrictPreimage, isCoveringMapOn_npow, Homeomorph.setCongr
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
h :
  ∀ (x : 𝕜),
    Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ≠ 0} x ↔
      Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x
⊢ Eq (α := Set 𝕜) {x : 𝕜 | x ≠ 0} (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ)

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
x : 𝕜
⊢ n ≠ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
x : 𝕜
⊢ Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ≠ 0} x ↔
    Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x

Tactic:
simp [show n ≠ 0 by aesop]
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℤ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
inl :
  ∀ (n : ℕ) (hn : Ne.{u_1 + 1} (α := 𝕜) (↑(↑n : ℤ) : 𝕜) 0),
    IsCoveringMap (X := { x : 𝕜 // x ≠ 0 }) fun (x : { x : 𝕜 // x ≠ 0 }) ↦
      Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) (HPow.hPow (β := ℤ) (↑x : 𝕜) (↑n : ℤ)) ⋯
inr :
  ∀ (n : ℕ) (hn : Ne.{u_1 + 1} (α := 𝕜) (↑(-(↑n : ℤ)) : 𝕜) 0),
    IsCoveringMap (X := { x : 𝕜 // x ≠ 0 }) fun (x : { x : 𝕜 // x ≠ 0 }) ↦
      Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) (HPow.hPow (β := ℤ) (↑x : 𝕜) (-(↑n : ℤ))) ⋯
⊢ IsCoveringMap (X := { x : 𝕜 // x ≠ 0 }) fun (x : { x : 𝕜 // x ≠ 0 }) ↦
    Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) ((↑x : 𝕜) ^ n) ⋯

Tactic:
obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑(↑n : ℤ) : 𝕜) 0
⊢ IsCoveringMap (X := { x : 𝕜 // x ≠ 0 }) fun (x : { x : 𝕜 // x ≠ 0 }) ↦
    Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) ((↑x : 𝕜) ^ n) ⋯

Tactic:
isCoveringMap_npow n _

Premises used: isCoveringMap_npow
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑(↑n : ℤ) : 𝕜) 0
h : ∀ (x : { x : 𝕜 // x ≠ 0 }), HPow.hPow (β := ℤ) (↑x : 𝕜) (↑n : ℤ) = (↑x : 𝕜) ^ n
inl : ProperSpace 𝕜
inl₁ : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
⊢ IsCoveringMap (X := { x : 𝕜 // x ≠ 0 }) fun (x : { x : 𝕜 // x ≠ 0 }) ↦
    Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) (HPow.hPow (β := ℤ) (↑x : 𝕜) (↑n : ℤ)) ⋯

Tactic:
convert! isCoveringMap_npow n _

Premises used: isCoveringMap_npow
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑(↑n : ℤ) : 𝕜) 0
x : { x : 𝕜 // x ≠ 0 }
⊢ HPow.hPow (β := ℤ) (↑x : 𝕜) (↑n : ℤ) = (↑x : 𝕜) ^ n

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑(↑n : ℤ) : 𝕜) 0
⊢ ProperSpace 𝕜

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑(↑n : ℤ) : 𝕜) 0
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑(-(↑n : ℤ)) : 𝕜) 0
⊢ IsCoveringMap (E := { g : 𝕜 // g ≠ 0 }) (X := { x : 𝕜 // x ≠ 0 })
    ((fun (x : { x : 𝕜 // x ≠ 0 }) ↦ Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) ((↑x : 𝕜) ^ n) ⋯) ∘
      (⇑(Homeomorph.inv₀ 𝕜) : (a : { g : 𝕜 // g ≠ 0 }) → { x : 𝕜 // x ≠ 0 }))

Tactic:
(isCoveringMap_npow n _).comp_homeomorph (.inv₀ 𝕜)

Premises used: IsCoveringMap.comp_homeomorph, Homeomorph.inv₀, isCoveringMap_npow
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑(-(↑n : ℤ)) : 𝕜) 0
h :
  ∀ (x : { x : 𝕜 // x ≠ 0 }),
    HPow.hPow (β := ℤ) (↑x : 𝕜) (-(↑n : ℤ)) =
      (↑(((fun (x : { x : 𝕜 // x ≠ 0 }) ↦ Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) ((↑x : 𝕜) ^ n) ⋯) ∘
              (⇑(Homeomorph.inv₀ 𝕜) : (a : { g : 𝕜 // g ≠ 0 }) → { x : 𝕜 // x ≠ 0 }))
            x) :
        𝕜)
inr : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
⊢ IsCoveringMap (X := { x : 𝕜 // x ≠ 0 }) fun (x : { x : 𝕜 // x ≠ 0 }) ↦
    Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) (HPow.hPow (β := ℤ) (↑x : 𝕜) (-(↑n : ℤ))) ⋯

Tactic:
convert! (isCoveringMap_npow n _).comp_homeomorph (.inv₀ 𝕜)

Premises used: IsCoveringMap.comp_homeomorph, Homeomorph.inv₀, isCoveringMap_npow
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑(-(↑n : ℤ)) : 𝕜) 0
x : { x : 𝕜 // x ≠ 0 }
⊢ HPow.hPow (β := ℤ) (↑x : 𝕜) (-(↑n : ℤ)) =
    (↑(((fun (x : { x : 𝕜 // x ≠ 0 }) ↦ Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) ((↑x : 𝕜) ^ n) ⋯) ∘
            (⇑(Homeomorph.inv₀ 𝕜) : (a : { g : 𝕜 // g ≠ 0 }) → { x : 𝕜 // x ≠ 0 }))
          x) :
      𝕜)

Tactic:
simp [Homeomorph.inv₀]

Premises used: Homeomorph.inv₀
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑(-(↑n : ℤ)) : 𝕜) 0
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0

Tactic:
simpa using hn
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℤ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
x : 𝕜
⊢ n ≠ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℤ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
⊢ ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0

Tactic:
have (x : 𝕜) : x ^ n = 0 ↔ x = 0 := zpow_eq_zero_iff (by aesop)
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℤ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}ᶜ

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℤ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
refine_1 :
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ)
refine_2 :
  IsCoveringMap (E := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
    (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
⊢ IsCoveringMapOn (X := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ

Tactic:
refine .of_isCoveringMap_restrictPreimage _ (by simp) ?_ ?_
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℤ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}ᶜ

Tactic:
isClosed_singleton (x := (0 : 𝕜)).isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℤ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
h : Eq (α := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) {0}ᶜ
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ)

Tactic:
convert! isClosed_singleton (x := (0 : 𝕜)).isOpen_compl using 1

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℤ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
h :
  ∀ (x : 𝕜),
    Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x ↔
      Membership.mem (γ := Set 𝕜) {0}ᶜ x
⊢ Eq (α := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) {0}ᶜ

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℤ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
x : 𝕜
⊢ Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x ↔ Membership.mem (γ := Set 𝕜) {0}ᶜ x

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℤ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ IsCoveringMap.{u_1, u_1} (E :=
    { x : 𝕜 // Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x }) (X :=
    { x : 𝕜 // x ≠ 0 })
    ((fun (x : { x : 𝕜 // x ≠ 0 }) ↦ Subtype.mk (p := fun (x : 𝕜) ↦ x ≠ 0) ((↑x : 𝕜) ^ n) ⋯) ∘
      (⇑(Homeomorph.ofEqSubtypes (p := fun (x : 𝕜) ↦
            Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x) (q := fun (x : 𝕜) ↦ x ≠ 0)
            ⋯) :
        (a : { x : 𝕜 // x ∈ (fun (x : 𝕜) ↦ x ^ n) ⁻¹' {0}ᶜ }) → { x : 𝕜 // x ≠ 0 }))

Tactic:
(isCoveringMap_zpow n hn).comp_homeomorph (.ofEqSubtypes _)

Premises used: IsCoveringMap.comp_homeomorph, isCoveringMap_zpow, Homeomorph.ofEqSubtypes
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℤ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
refine_2 :
  Eq.{u_1 + 1} (α := 𝕜 → Prop)
    (fun (x : 𝕜) ↦ Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x) fun (x : 𝕜) ↦ x ≠ 0
⊢ IsCoveringMap (E := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
    (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)

Tactic:
convert! (isCoveringMap_zpow n hn).comp_homeomorph (.ofEqSubtypes _) using 1

Premises used: IsCoveringMap.comp_homeomorph, isCoveringMap_zpow, Homeomorph.ofEqSubtypes
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℤ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
refine_2 : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x ↔ x ≠ 0
⊢ Eq.{u_1 + 1} (α := 𝕜 → Prop)
    (fun (x : 𝕜) ↦ Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x) fun (x : 𝕜) ↦ x ≠ 0

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℤ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
x : 𝕜
⊢ Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x ↔ x ≠ 0

Tactic:
simpa using (this _).not

Premises used: Iff.not
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
rw : IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) ↥(rootsOfUnity n 𝕜 : Subgroup 𝕜ˣ)
⊢ IsQuotientCoveringMap (X := 𝕜ˣ) (fun (x : 𝕜ˣ) ↦ x ^ n) ↥(MonoidHom.ker (M := 𝕜ˣ) (powMonoidHom n))

Tactic:
rw [← rootsOfUnity_eq_ker]

Premises used: rootsOfUnity_eq_ker
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
⊢ n ≠ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
⊢ NeZero n

Tactic:
have : NeZero n := ⟨by aesop⟩
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
this : NeZero n
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
this : NeZero n
⊢ IsQuotientMap (X := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
    (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)

Tactic:
have := ((isClosedMap_pow 𝕜 n).restrictPreimage {0}ᶜ).isQuotientMap
    (by fun_prop) (.restrictPreimage _ surj)
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
this_1 : NeZero n
this :
  IsQuotientMap (X := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
    (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g : 𝕜 // g ≠ 0 } := unitsHomeomorphNeZero
⊢ IsQuotientMap (X := 𝕜ˣ) (Y := 𝕜ˣ)
    (Function.comp (β := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
      ((⇑e.symm : (a : { g : 𝕜 // g ≠ 0 }) → 𝕜ˣ) ∘ Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
      (⇑(e.trans
            (Homeomorph.ofEqSubtypes (p := fun (g : 𝕜) ↦ g ≠ 0) (q := fun (x : 𝕜) ↦
              Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x) ⋯)) :
        (a : 𝕜ˣ) → { x : 𝕜 // x ∈ (fun (x : 𝕜) ↦ x ^ n) ⁻¹' {0}ᶜ }))

Tactic:
(e.symm.isQuotientMap.comp this).comp (e.trans (.ofEqSubtypes _)).isQuotientMap

Premises used: Topology.IsQuotientMap.comp, Homeomorph.symm, Homeomorph.trans, Homeomorph.ofEqSubtypes, Homeomorph.isQuotientMap
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
this_1 : NeZero n
this :
  IsQuotientMap (X := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
    (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g : 𝕜 // g ≠ 0 } := unitsHomeomorphNeZero
h :
  ∀ (x : 𝕜ˣ),
    x ^ n =
      Function.comp (β := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
        ((⇑e.symm : (a : { g : 𝕜 // g ≠ 0 }) → 𝕜ˣ) ∘ Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
        (⇑(e.trans
              (Homeomorph.ofEqSubtypes (p := fun (g : 𝕜) ↦ g ≠ 0) (q := fun (x : 𝕜) ↦
                Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x) ⋯)) :
          (a : 𝕜ˣ) → { x : 𝕜 // x ∈ (fun (x : 𝕜) ↦ x ^ n) ⁻¹' {0}ᶜ })
        x
convert! :
  Eq.{u_1 + 1} (α := 𝕜 → Prop) (fun (g : 𝕜) ↦ g ≠ 0) fun (x : 𝕜) ↦
    Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x
⊢ IsQuotientMap (Y := 𝕜ˣ) fun (x : 𝕜ˣ) ↦ x ^ n

Tactic:
convert! (e.symm.isQuotientMap.comp this).comp (e.trans (.ofEqSubtypes _)).isQuotientMap

Premises used: Topology.IsQuotientMap.comp, Homeomorph.symm, Homeomorph.trans, Homeomorph.ofEqSubtypes, Homeomorph.isQuotientMap
-- Module: Mathlib.Analysis.Complex.CoveringMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
n : ℕ
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
surj : Function.Surjective (β := 𝕜) fun (x : 𝕜) ↦ x ^ n
this_1 : NeZero n
this :
  IsQuotientMap (X := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
    (Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g : 𝕜 // g ≠ 0 } := unitsHomeomorphNeZero
x : 𝕜ˣ
⊢ x ^ n =
    Function.comp (β := (↑(Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) : Type u_1))
      ((⇑e.symm : (a : { g : 𝕜 // g ≠ 0 }) → 𝕜ˣ) ∘ Set.restrictPreimage {0}ᶜ fun (x : 𝕜) ↦ x ^ n)
      (⇑(e.trans
            (Homeomorph.ofEqSubtypes (p := fun (g : 𝕜) ↦ g ≠ 0) (q := fun (x : 𝕜) ↦
              Membership.mem (γ := Set 𝕜) (Set.preimage (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) {0}ᶜ) x) ⋯)) :
        (a : 𝕜ˣ) → { x : 𝕜 // x ∈ (fun (x : 𝕜) ↦ x ^ n) ⁻¹' {0}ᶜ })
      x

Tactic:
(e.left_inv _).symm

Premises used: Function.invFun, Homeomorph.toEquiv, dite, Eq.symm, Equiv.left_inv