awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p x y : 𝕜
⊢ (↑(x - y) : 𝕜 ⧸ zmultiples p) =
    HSub.hSub (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
      (↑y : 𝕜 ⧸ zmultiples p)

Tactic:
rfl

Premises used: Quotient.map₂, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p x : 𝕜
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑(-x) : 𝕜 ⧸ zmultiples p)
    (-(↑x : 𝕜 ⧸ zmultiples p))

Tactic:
rfl

Premises used: Quot.map, Quotient.map', rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
⊢ Eq.{u_1 + 1} (α := AddCircle p) (↑0 : 𝕜 ⧸ zmultiples p) 0

Tactic:
rfl

Premises used: AddAction.orbitRel, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p x : 𝕜
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) 0 ↔ ∃ (n : ℤ), n • p = x

Tactic:
simp [AddSubgroup.mem_zmultiples_iff]

Premises used: AddSubgroup.mem_zmultiples_iff
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑p : 𝕜 ⧸ zmultiples p) 0

Tactic:
(QuotientAddGroup.eq_zero_iff p).2 <| mem_zmultiples p

Premises used: Iff.mpr, AddSubgroup.mem_zmultiples, QuotientAddGroup.eq_zero_iff
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p x : 𝕜
rw :
  HAdd.hAdd (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
      (↑p : 𝕜 ⧸ zmultiples p) =
    (↑x : 𝕜 ⧸ zmultiples p)
rw₁ :
  (↑p : 𝕜 ⧸ zmultiples p) =
    HSub.hSub (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
      (↑x : 𝕜 ⧸ zmultiples p)
rw₂ : Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑p : 𝕜 ⧸ zmultiples p) 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) 0 0
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑(x + p) : 𝕜 ⧸ zmultiples p)
    (↑x : 𝕜 ⧸ zmultiples p)

Tactic:
rw [coe_add, ← eq_sub_iff_add_eq', sub_self, coe_period]

Premises used: eq_sub_iff_add_eq', sub_self, AddCircle.coe_period, AddCircle.coe_add
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : TopologicalSpace 𝕜
⊢ Continuous[inst_1, QuotientAddGroup.instTopologicalSpace (zmultiples p)]
    (⇑(QuotientAddGroup.mk' (zmultiples p)) : (a : 𝕜) → 𝕜 ⧸ zmultiples p)

Tactic:
continuous_coinduced_rng

Premises used: Quotient.mk', continuous_coinduced_rng
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
x : (↑{x : AddCircle p | n • x = 0} : Type u_1)
obtain :
  ∀ (x : AddCircle p) (hx : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x),
    ∃ (k : Fin n) (y : 𝕜),
      (↑y : 𝕜 ⧸ zmultiples p) =
          (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
                Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) x hx) :
            AddCircle p) ∧
        n • y = (↑k : ℕ) • p
⊢ ∃ (k : Fin n) (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑k : ℕ) • p

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
x : AddCircle p
hx : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x
obtain :
  ∀ (y : 𝕜) (hx : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)),
    ∃ (k : Fin n) (y_1 : 𝕜),
      (↑y_1 : 𝕜 ⧸ zmultiples p) =
          (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
                Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) (↑y : 𝕜 ⧸ zmultiples p) hx) :
            AddCircle p) ∧
        n • y_1 = (↑k : ℕ) • p
⊢ ∃ (k : Fin n) (y : 𝕜),
    (↑y : 𝕜 ⧸ zmultiples p) =
        (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) x hx) :
          AddCircle p) ∧
      n • y = (↑k : ℕ) • p

Tactic:
obtain ⟨y, rfl⟩ := mk_surjective x

Premises used: QuotientAddGroup.mk_surjective, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
⊢ Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)

Tactic:
rw [Set.mem_setOf, ← mk_nsmul, eq_zero_iff] at hx

Premises used: Set.mem_setOf, QuotientAddGroup.mk_nsmul, QuotientAddGroup.eq_zero_iff
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx_1 : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
hx : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
have :
  ∀ (m' : ℤ) (hm : (fun (x : ℤ) ↦ x • p) m' = n • y),
    ∃ (k : Fin n) (y_1 : 𝕜),
      (↑y_1 : 𝕜 ⧸ zmultiples p) =
          (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
                Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) (↑y : 𝕜 ⧸ zmultiples p) hx_1) :
            AddCircle p) ∧
        n • y_1 = (↑k : ℕ) • p
⊢ ∃ (k : Fin n) (y_1 : 𝕜),
    (↑y_1 : 𝕜 ⧸ zmultiples p) =
        (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) (↑y : 𝕜 ⧸ zmultiples p) hx_1) :
          AddCircle p) ∧
      n • y_1 = (↑k : ℕ) • p

Tactic:
have ⟨m', hm⟩ := hx
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx_1 : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
hx : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
m' : ℤ
hm : (fun (x : ℤ) ↦ x • p) m' = n • y
⊢ NeZero n

Tactic:
have : NeZero n := ⟨h0⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx_1 : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
hx : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
m' : ℤ
hm : (fun (x : ℤ) ↦ x • p) m' = n • y
this : NeZero n
⊢ (fun (x : ℤ) ↦ x • p)
      (HMul.hMul (α := ℤ) ((Int.divModEquiv n : (a : ℤ) → ℤ × Fin n) m').1 (↑n : ℤ) +
        (↑(↑((Int.divModEquiv n : (a : ℤ) → ℤ × Fin n) m').2 : ℕ) : ℤ)) =
    n • y

Tactic:
rw [← (Int.divModEquiv n).symm_apply_apply m', Int.divModEquiv_symm_apply] at hm

Premises used: Equiv.symm_apply_apply, Int.divModEquiv, Int.divModEquiv_symm_apply
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx_1 : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
hx : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
m' : ℤ
this : NeZero n
hm :
  (fun (x : ℤ) ↦ x • p)
      (HMul.hMul (α := ℤ) ((Int.divModEquiv n : (a : ℤ) → ℤ × Fin n) m').1 (↑n : ℤ) +
        (↑(↑((Int.divModEquiv n : (a : ℤ) → ℤ × Fin n) m').2 : ℕ) : ℤ)) =
    n • y
⊢ let m : ℤ × Fin n := (Int.divModEquiv n : (a : ℤ) → ℤ × Fin n) m';
  (fun (x : ℤ) ↦ x • p) (m.1 * (↑n : ℤ) + (↑(↑m.2 : ℕ) : ℤ)) = n • y

Tactic:
set m := m'.divModEquiv n

Premises used: Int.divModEquiv, DFunLike.coe
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx_1 : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
hx : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n : (a : ℤ) → ℤ × Fin n) m'
hm : (fun (x : ℤ) ↦ x • p) (m.1 * (↑n : ℤ) + (↑(↑m.2 : ℕ) : ℤ)) = n • y
h :
  (↑(y - m.1 • p) : 𝕜 ⧸ zmultiples p) =
      (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
            Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) (↑y : 𝕜 ⧸ zmultiples p) hx_1) :
        AddCircle p) ∧
    n • (y - m.1 • p) = (↑m.2 : ℕ) • p
⊢ ∃ (k : Fin n) (y_1 : 𝕜),
    (↑y_1 : 𝕜 ⧸ zmultiples p) =
        (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) (↑y : 𝕜 ⧸ zmultiples p) hx_1) :
          AddCircle p) ∧
      n • y_1 = (↑k : ℕ) • p

Tactic:
use m.2, y - m.1 • p

Premises used: Prod.fst, Prod.snd
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx_1 : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
hx : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n : (a : ℤ) → ℤ × Fin n) m'
hm : (fun (x : ℤ) ↦ x • p) (m.1 * (↑n : ℤ) + (↑(↑m.2 : ℕ) : ℤ)) = n • y
h : True ∧ n • (y - m.1 • p) = (↑m.2 : ℕ) • p
⊢ (↑(y - m.1 • p) : 𝕜 ⧸ zmultiples p) =
      (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
            Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) (↑y : 𝕜 ⧸ zmultiples p) hx_1) :
        AddCircle p) ∧
    n • (y - m.1 • p) = (↑m.2 : ℕ) • p

Tactic:
simp_rw [mk_sub, mk_zsmul, sub_eq_self, coe_period, smul_zero]

Premises used: smul_zero, sub_eq_self, QuotientAddGroup.mk_sub, QuotientAddGroup.mk_zsmul, AddCircle.coe_period
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx_1 : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
hx : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n : (a : ℤ) → ℤ × Fin n) m'
hm : (fun (x : ℤ) ↦ x • p) (m.1 * (↑n : ℤ) + (↑(↑m.2 : ℕ) : ℤ)) = n • y
h : True ∧ (fun (x : ℤ) ↦ x • p) ((↑(↑m.2 : ℕ) : ℤ) + m.1 * (↑n : ℤ)) = (↑m.2 : ℕ) • p + n • m.1 • p
⊢ True ∧ n • (y - m.1 • p) = (↑m.2 : ℕ) • p

Tactic:
rw [smul_sub, sub_eq_iff_eq_add, ← hm, add_comm]

Premises used: add_comm, smul_sub, sub_eq_iff_eq_add
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx_1 : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
hx : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n : (a : ℤ) → ℤ × Fin n) m'
hm : (fun (x : ℤ) ↦ x • p) (m.1 * (↑n : ℤ) + (↑(↑m.2 : ℕ) : ℤ)) = n • y
⊢ True ∧ (fun (x : ℤ) ↦ x • p) ((↑(↑m.2 : ℕ) : ℤ) + m.1 * (↑n : ℤ)) = (↑m.2 : ℕ) • p + n • m.1 • p

Tactic:
simp [add_smul, mul_comm, mul_smul]

Premises used: add_smul, mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
⊢ ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (k : Fin n) (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑k : ℕ) • p

Tactic:
have (x : {x : AddCircle p | n • x = 0}) : ∃ (k : Fin n) (y : 𝕜), y = x.1 ∧ n • y = k.1 • p := by
    obtain ⟨x, hx⟩ := x
    obtain ⟨y, rfl⟩ := mk_surjective x
    rw [Set.mem_setOf, ← mk_nsmul, eq_zero_iff] at hx
    have ⟨m', hm⟩ := hx
    have : NeZero n := ⟨h0⟩
    rw [← (Int.divModEquiv n).symm_apply_apply m', Int.divModEquiv_symm_apply] at hm
    set m := m'.divModEquiv n
    use m.2, y - m.1 • p
    simp_rw [mk_sub, mk_zsmul, sub_eq_self, coe_period, smul_zero]
    rw [smul_sub, sub_eq_iff_eq_add, ← hm, add_comm]
    simp [add_smul, mul_comm, mul_smul]
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
this :
  ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (k : Fin n) (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑k : ℕ) • p
choose :
  ∀ (f : (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)) → Fin n)
    (hf :
      ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
        ∃ (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑(f x) : ℕ) • p),
    encard.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0} ≤ (↑n : ℕ∞)
⊢ encard.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0} ≤ (↑n : ℕ∞)

Tactic:
choose f hf using this
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)) → Fin n
hf :
  ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑(f x) : ℕ) • p
⊢ ENat.card (Fin n) ≤ (↑n : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)) → Fin n
hf :
  ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑(f x) : ℕ) • p
refine :
  ∀ (x x' : (↑{x : AddCircle p | n • x = 0} : Type u_1)) (eq : f x = f x'), (↑x : AddCircle p) = (↑x' : AddCircle p)
⊢ encard.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0} ≤ (↑n : ℕ∞)

Tactic:
refine (ENat.card_le_card_of_injective (f := f) fun x x' eq ↦ Subtype.ext ?_).trans (by simp)

Premises used: ENat.card_le_card_of_injective, LE.le.trans, Subtype.ext
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)) → Fin n
hf :
  ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑(f x) : ℕ) • p
x x' : (↑{x : AddCircle p | n • x = 0} : Type u_1)
eq : f x = f x'
have :
  ∀ (y : 𝕜) (hyx : (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p)) (hy : n • y = (↑(f x) : ℕ) • p),
    (↑x : AddCircle p) = (↑x' : AddCircle p)
⊢ (↑x : AddCircle p) = (↑x' : AddCircle p)

Tactic:
have ⟨y, hyx, hy⟩ := hf x
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)) → Fin n
hf :
  ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑(f x) : ℕ) • p
x x' : (↑{x : AddCircle p | n • x = 0} : Type u_1)
eq : f x = f x'
y : 𝕜
hyx : (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p)
hy : n • y = (↑(f x) : ℕ) • p
have :
  ∀ (y' : 𝕜) (hyx' : (↑y' : 𝕜 ⧸ zmultiples p) = (↑x' : AddCircle p)) (hy' : n • y' = (↑(f x') : ℕ) • p),
    (↑x : AddCircle p) = (↑x' : AddCircle p)
⊢ (↑x : AddCircle p) = (↑x' : AddCircle p)

Tactic:
have ⟨y', hyx', hy'⟩ := hf x'
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)) → Fin n
hf :
  ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑(f x) : ℕ) • p
x x' : (↑{x : AddCircle p | n • x = 0} : Type u_1)
eq : f x = f x'
y : 𝕜
hyx : (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p)
hy : n • y = (↑(f x) : ℕ) • p
y' : 𝕜
hyx' : (↑y' : 𝕜 ⧸ zmultiples p) = (↑x' : AddCircle p)
hy' : n • y' = (↑(f x') : ℕ) • p
rw :
  ∀ (y' : 𝕜) (hy : y = y') (hyx' : (↑y' : 𝕜 ⧸ zmultiples p) = (↑x' : AddCircle p)) (hy' : n • y' = (↑(f x') : ℕ) • p),
    (↑x : AddCircle p) = (↑x' : AddCircle p)
⊢ (↑x : AddCircle p) = (↑x' : AddCircle p)

Tactic:
rw [eq, ← hy', hn.eq_iff] at hy

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)) → Fin n
hf :
  ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑(f x) : ℕ) • p
x x' : (↑{x : AddCircle p | n • x = 0} : Type u_1)
eq : f x = f x'
y : 𝕜
hyx : (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p)
y' : 𝕜
hy : y = y'
hyx' : (↑y' : 𝕜 ⧸ zmultiples p) = (↑x' : AddCircle p)
hy' : n • y' = (↑(f x') : ℕ) • p
rw : (↑y : 𝕜 ⧸ zmultiples p) = (↑x' : AddCircle p)
rw₁ : (↑y' : 𝕜 ⧸ zmultiples p) = (↑x' : AddCircle p)
rw₂ rw₃ : (↑x' : AddCircle p) = (↑x' : AddCircle p)
⊢ (↑x : AddCircle p) = (↑x' : AddCircle p)

Tactic:
rw [← hyx, hy, hyx']
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
hn : IsSMulRegular 𝕜 n
⊢ Nontrivial 𝕜

Tactic:
nontriviality 𝕜
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
hn : IsSMulRegular 𝕜 n
h : Nontrivial 𝕜
inl :
  ∀ (hn : IsSMulRegular (R := ℕ) 𝕜 0),
    Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | HSMul.hSMul (α := ℕ) 0 x = 0}
inr : ∀ (h0 : n ≠ 0), Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0}
⊢ Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0}

Tactic:
obtain rfl | h0 := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
h : Nontrivial 𝕜
hn : IsSMulRegular (R := ℕ) 𝕜 0
⊢ Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | HSMul.hSMul (α := ℕ) 0 x = 0}

Tactic:
hn.not_zero.elim

Premises used: False.elim, IsSMulRegular.not_zero
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
hn : IsSMulRegular 𝕜 n
h : Nontrivial 𝕜
h0 : n ≠ 0
⊢ Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0}

Tactic:
ENat.card_lt_top.mp <|
    (card_torsion_le_of_isSMulRegular p n h0 hn).trans_lt <| ENat.coe_lt_top n

Premises used: AddCircle.card_torsion_le_of_isSMulRegular, ENat.card_lt_top, Set.Finite, Iff.mp, LE.le.trans_lt, ENat.coe_lt_top
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
h : Nontrivial 𝕜
hn : IsSMulRegular (R := ℕ) 𝕜 0
⊢ Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | HSMul.hSMul (α := ℕ) 0 x = 0}

Tactic:
exacts [hn.not_zero.elim, ENat.card_lt_top.mp <|
    (card_torsion_le_of_isSMulRegular p n h0 hn).trans_lt <| ENat.coe_lt_top n]

Premises used: ENat.card_lt_top, False.elim, IsSMulRegular.not_zero, Iff.mp
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℤ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
⊢ encard.{u_1} (α := AddCircle p) {x : AddCircle p | n.natAbs • x = 0} ≤ (↑n.natAbs : ℕ∞)

Tactic:
card_torsion_le_of_isSMulRegular p _ (Int.natAbs_ne_zero.mpr h0)
      (IsSMulRegular.natAbs_iff.mpr hn)

Premises used: Iff.mpr, AddCircle.card_torsion_le_of_isSMulRegular, IsSMulRegular.natAbs_iff, Int.natAbs_ne_zero
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℤ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
h :
  encard.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0} =
    encard.{u_1} (α := AddCircle p) {x : AddCircle p | n.natAbs • x = 0}
⊢ encard.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0} ≤ (↑n.natAbs : ℕ∞)

Tactic:
convert!
    card_torsion_le_of_isSMulRegular p _ (Int.natAbs_ne_zero.mpr h0)
      (IsSMulRegular.natAbs_iff.mpr hn) using 1

Premises used: Iff.mpr, AddCircle.card_torsion_le_of_isSMulRegular, IsSMulRegular.natAbs_iff, Int.natAbs_ne_zero
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℤ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
⊢ encard.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0} =
    encard.{u_1} (α := AddCircle p) {x : AddCircle p | n.natAbs • x = 0}

Tactic:
simp
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℤ
hn : IsSMulRegular 𝕜 n
⊢ Nontrivial 𝕜

Tactic:
nontriviality 𝕜
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℤ
hn : IsSMulRegular 𝕜 n
h : Nontrivial 𝕜
inl :
  ∀ (hn : IsSMulRegular (R := ℤ) 𝕜 0),
    Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | HSMul.hSMul (α := ℤ) 0 x = 0}
inr : ∀ (h0 : n ≠ 0), Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0}
⊢ Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0}

Tactic:
obtain rfl | h0 := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
h : Nontrivial 𝕜
hn : IsSMulRegular (R := ℤ) 𝕜 0
⊢ Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | HSMul.hSMul (α := ℤ) 0 x = 0}

Tactic:
hn.not_zero.elim

Premises used: False.elim, IsSMulRegular.not_zero
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℤ
hn : IsSMulRegular 𝕜 n
h : Nontrivial 𝕜
h0 : n ≠ 0
⊢ Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0}

Tactic:
ENat.card_lt_top.mp <|
    (card_torsion_le_of_isSMulRegular_int p n h0 hn).trans_lt <| ENat.coe_lt_top _

Premises used: ENat.card_lt_top, Set.Finite, AddCircle.card_torsion_le_of_isSMulRegular_int, Iff.mp, LE.le.trans_lt, ENat.coe_lt_top
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
h : Nontrivial 𝕜
hn : IsSMulRegular (R := ℤ) 𝕜 0
⊢ Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | HSMul.hSMul (α := ℤ) 0 x = 0}

Tactic:
exacts [hn.not_zero.elim, ENat.card_lt_top.mp <|
    (card_torsion_le_of_isSMulRegular_int p n h0 hn).trans_lt <| ENat.coe_lt_top _]

Premises used: ENat.card_lt_top, False.elim, IsSMulRegular.not_zero, Iff.mp, ENat.coe_lt_top
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
n : ℕ
hn : 0 < n
x : 𝕜
⊢ n • x = 0 → x = 0

Tactic:
simp [hn.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
n : ℕ
hn : 0 < n
⊢ Set.Finite.{u_1} (α := AddCircle p) {u : AddCircle p | addOrderOf u = n}

Tactic:
(finite_torsion p hn).subset fun _ h ↦ ((addOrderOf_eq_iff hn).mp h).1

Premises used: Set.Finite.subset, And.left, addOrderOf_eq_iff, Iff.mp, AddCircle.finite_torsion
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
rw : (∃ (n : ℤ), n • p = x) ↔ ∃ (n : ℕ), n • p = x
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) 0 ↔ ∃ (n : ℕ), n • p = x

Tactic:
rw [coe_eq_zero_iff]

Premises used: AddCircle.coe_eq_zero_iff
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
mp : (∃ (n : ℤ), n • p = x) → ∃ (n : ℕ), n • p = x
mpr : (∃ (n : ℕ), n • p = x) → ∃ (n : ℤ), n • p = x
⊢ (∃ (n : ℤ), n • p = x) ↔ ∃ (n : ℕ), n • p = x

Tactic:
constructor
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
contrapose! : ∀ (hx : n ≤ 0), n • p ≤ 0
⊢ 0 < n

Tactic:
contrapose! hx
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : n ≤ 0
⊢ n • p ≤ 0

Tactic:
simpa only [← neg_nonneg, ← zsmul_neg, zsmul_neg'] using zsmul_nonneg hp.le (neg_nonneg.2 hx)

Premises used: zsmul_neg, Iff.mpr, LT.lt.le, neg_nonneg, zsmul_nonneg, zsmul_neg'