awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
q : ℚ
this : Ne.{u_1 + 1} (α := 𝕜) (↑(↑q.den : ℤ) : 𝕜) 0
rw :
  addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑((↑(Rat.divInt q.num (↑q.den : ℤ)) : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    (Rat.divInt q.num (↑q.den : ℤ)).den
rw₁ :
  addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑q.num : 𝕜) (↑(↑q.den : ℤ) : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    (Rat.divInt q.num (↑q.den : ℤ)).den
rw₂ :
  addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑q.num : 𝕜) (↑q.den : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    (Rat.divInt q.num (↑q.den : ℤ)).den
rw₃ :
  addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑q.num : 𝕜) (↑q.den : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    q.den
rw₄ rw₅ : q.den = q.den
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑((↑q : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    q.den

Tactic:
rw [← q.num_divInt_den, Rat.cast_divInt_of_ne_zero _ this, Int.cast_natCast, Rat.num_divInt_den,
    addOrderOf_div_of_gcd_eq_one' q.pos q.reduced]

Premises used: Int.cast_natCast, Rat.reduced, Rat.pos, Rat.num_divInt_den, AddCircle.addOrderOf_div_of_gcd_eq_one', Rat.cast_divInt_of_ne_zero
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ n • u = 0 ↔ ∃ m < n, (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = u

Tactic:
⟨QuotientAddGroup.induction_on u fun k hk ↦ ?_, ?_⟩

Premises used: Iff.intro, QuotientAddGroup.induction_on
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
refine_1 : (∃ m < n, (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = u) → n • u = 0
refine_2 :
  ∀ (k : 𝕜) (hk : HSMul.hSMul (β := AddCircle p) n (↑k : 𝕜 ⧸ zmultiples p) = 0),
    ∃ m < n,
      Eq (α := AddCircle p) (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) (↑k : 𝕜 ⧸ zmultiples p)
⊢ n • u = 0 ↔ ∃ m < n, (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = u

Tactic:
refine ⟨QuotientAddGroup.induction_on u fun k hk ↦ ?_, ?_⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
refine_1 : (∃ m < n, (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = u) → addOrderOf u ∣ n
⊢ (∃ m < n, (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = u) → n • u = 0

Tactic:
rw [← addOrderOf_dvd_iff_nsmul_eq_zero]

Premises used: addOrderOf_dvd_iff_nsmul_eq_zero
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
refine_1 : n = addOrderOf (G := AddCircle p) (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) * m.gcd n
refine_1₁ : ℕ
⊢ addOrderOf (G := AddCircle p) (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) ∣ n

Tactic:
constructor
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
⊢ m.gcd n * addOrderOf (G := AddCircle p) (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = n

Tactic:
gcd_mul_addOrderOf_div_eq p m h

Premises used: AddCircle.gcd_mul_addOrderOf_div_eq
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : HSMul.hSMul (β := AddCircle p) n (↑k : 𝕜 ⧸ zmultiples p) = 0
⊢ ∃ (n_1 : ℤ), n_1 • p = n • k

Tactic:
rw [← coe_nsmul, coe_eq_zero_iff] at hk

Premises used: AddCircle.coe_eq_zero_iff, AddCircle.coe_nsmul
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : ∃ (n_1 : ℤ), n_1 • p = n • k
refine_2 :
  ∀ (a : ℤ) (ha : a • p = n • k),
    ∃ m < n,
      Eq (α := AddCircle p) (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) (↑k : 𝕜 ⧸ zmultiples p)
⊢ ∃ m < n,
    Eq (α := AddCircle p) (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) (↑k : 𝕜 ⧸ zmultiples p)

Tactic:
obtain ⟨a, ha⟩ := hk
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : a • p = n • k
⊢ ∃ m < n,
    Eq (α := AddCircle p) (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) (↑k : 𝕜 ⧸ zmultiples p)

Tactic:
⟨a.natMod n, Int.natMod_lt h.ne', ?_⟩

Premises used: Int.natMod_lt, Nat.cast, LT.lt.ne', And.intro, Exists.intro, Int.natMod
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : a • p = n • k
refine_2 :
  Eq (α := AddCircle p) (↑(HDiv.hDiv (α := 𝕜) (↑(a.natMod (↑n : ℤ)) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p)
    (↑k : 𝕜 ⧸ zmultiples p)
⊢ ∃ m < n,
    Eq (α := AddCircle p) (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) (↑k : 𝕜 ⧸ zmultiples p)

Tactic:
refine ⟨a.natMod n, Int.natMod_lt h.ne', ?_⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : a • p = n • k
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0

Tactic:
have h0 : (n : 𝕜) ≠ 0 := Nat.cast_ne_zero.2 h.ne'
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : a • p = n • k
h0 : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
⊢ (↑(a / (↑n : ℤ)) : 𝕜) * p + (a % (↑n : ℤ)) • p / (↑n : 𝕜) = k

Tactic:
rw [nsmul_eq_mul, mul_comm, ← div_eq_iff h0, ← a.ediv_mul_add_emod n, add_smul, add_div,
    zsmul_eq_mul, Int.cast_mul, Int.cast_natCast, mul_assoc, ← mul_div, mul_comm _ p,
    mul_div_cancel_right₀ p h0] at ha

Premises used: mul_div, Int.cast_natCast, zsmul_eq_mul, mul_assoc, Nat.cast, mul_div_cancel_right₀, Int.cast_mul, div_eq_iff, Int.ediv_mul_add_emod, add_smul, mul_comm, nsmul_eq_mul, add_div
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : a • p = n • k
h0 : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
ha₁ : (↑(a / (↑n : ℤ)) : 𝕜) * p + (a % (↑n : ℤ)) • p / (↑n : 𝕜) = k
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0

Tactic:
rw [nsmul_eq_mul, mul_comm, ← div_eq_iff h0, ← a.ediv_mul_add_emod n, add_smul, add_div,
    zsmul_eq_mul, Int.cast_mul, Int.cast_natCast, mul_assoc, ← mul_div, mul_comm _ p,
    mul_div_cancel_right₀ p h0] at ha

Premises used: mul_div, Int.cast_natCast, zsmul_eq_mul, mul_assoc, Nat.cast, mul_div_cancel_right₀, Int.cast_mul, div_eq_iff, Int.ediv_mul_add_emod, add_smul, mul_comm, nsmul_eq_mul, add_div
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : (↑(a / (↑n : ℤ)) : 𝕜) * p + (a % (↑n : ℤ)) • p / (↑n : 𝕜) = k
h0 : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
refine_2 : 0 ≤ a % (↑n : ℤ)
⊢ Eq (α := AddCircle p) (↑(HDiv.hDiv (α := 𝕜) (↑(a.natMod (↑n : ℤ)) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p)
    (↑k : 𝕜 ⧸ zmultiples p)

Tactic:
rw [← ha, coe_add, ← Int.cast_natCast, Int.natMod, Int.toNat_of_nonneg, zsmul_eq_mul,
    mul_div_right_comm, eq_comm, add_eq_right, ← zsmul_eq_mul, coe_zsmul, coe_period, smul_zero]

Premises used: Int.cast_natCast, zsmul_eq_mul, AddCircle.coe_zsmul, Int.toNat_of_nonneg, smul_zero, eq_comm, mul_div_right_comm, add_eq_right, AddCircle.coe_period, AddCircle.coe_add, Int.natMod
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : (↑(a / (↑n : ℤ)) : 𝕜) * p + (a % (↑n : ℤ)) • p / (↑n : 𝕜) = k
h0 : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
⊢ Ne (α := ℤ) (↑n : ℤ) 0

Tactic:
exact_mod_cast h.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : (↑(a / (↑n : ℤ)) : 𝕜) * p + (a % (↑n : ℤ)) • p / (↑n : 𝕜) = k
h0 : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
⊢ 0 ≤ a % (↑n : ℤ)

Tactic:
exact Int.emod_nonneg _ (by exact_mod_cast h.ne')

Premises used: Int.emod_nonneg
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ addOrderOf u = n ↔ ∃ m < n, m.gcd n = 1 ∧ (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = u

Tactic:
⟨QuotientAddGroup.induction_on u ?_, ?_⟩

Premises used: Iff.intro, QuotientAddGroup.induction_on
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
refine_1 :
  (∃ m < n, m.gcd n = 1 ∧ (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = u) → addOrderOf u = n
refine_2 :
  ∀ (z : 𝕜),
    addOrderOf (G := AddCircle p) (↑z : 𝕜 ⧸ zmultiples p) = n →
      ∃ m < n,
        m.gcd n = 1 ∧
          Eq (α := AddCircle p) (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) (↑z : 𝕜 ⧸ zmultiples p)
⊢ addOrderOf u = n ↔ ∃ m < n, m.gcd n = 1 ∧ (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = u

Tactic:
refine ⟨QuotientAddGroup.induction_on u ?_, ?_⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
h₁ : m.gcd n = 1
⊢ addOrderOf (G := AddCircle p) (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = n

Tactic:
addOrderOf_div_of_gcd_eq_one h h₁

Premises used: AddCircle.addOrderOf_div_of_gcd_eq_one
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
h₁ : m.gcd n = 1
⊢ addOrderOf (G := AddCircle p) (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = n

Tactic:
exact addOrderOf_div_of_gcd_eq_one h h₁

Premises used: AddCircle.addOrderOf_div_of_gcd_eq_one
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
refine_2 :
  ∀ (m : ℕ) (hm : m < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p))
    (hk :
      Eq (α := AddCircle p)
        (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) : 𝕜) * p) :
          𝕜 ⧸ zmultiples p)
        (↑k : 𝕜 ⧸ zmultiples p)),
    ∃ m < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p),
      m.gcd (addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) = 1 ∧
        Eq (α := AddCircle p)
          (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) : 𝕜) * p) :
            𝕜 ⧸ zmultiples p)
          (↑k : 𝕜 ⧸ zmultiples p)
⊢ ∃ m < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p),
    m.gcd (addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) = 1 ∧
      Eq (α := AddCircle p)
        (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) : 𝕜) * p) :
          𝕜 ⧸ zmultiples p)
        (↑k : 𝕜 ⧸ zmultiples p)

Tactic:
obtain ⟨m, hm, hk⟩ := (AddCircle.nsmul_eq_zero_iff h).mp
    (addOrderOf_nsmul_eq_zero (k : AddCircle p))

Premises used: QuotientAddGroup.mk, addOrderOf_nsmul_eq_zero, Iff.mp, AddCircle.nsmul_eq_zero_iff
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
m : ℕ
hm : m < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
hk :
  Eq (α := AddCircle p)
    (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) : 𝕜) * p) :
      𝕜 ⧸ zmultiples p)
    (↑k : 𝕜 ⧸ zmultiples p)
⊢ ∃ m < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p),
    m.gcd (addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) = 1 ∧
      Eq (α := AddCircle p)
        (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) : 𝕜) * p) :
          𝕜 ⧸ zmultiples p)
        (↑k : 𝕜 ⧸ zmultiples p)

Tactic:
⟨m, hm, mul_right_cancel₀ h.ne' ?_, hk⟩

Premises used: LT.lt.ne', And.intro, Exists.intro, mul_right_cancel₀
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
m : ℕ
hm : m < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
hk :
  Eq (α := AddCircle p)
    (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) : 𝕜) * p) :
      𝕜 ⧸ zmultiples p)
    (↑k : 𝕜 ⧸ zmultiples p)
refine_2 :
  m.gcd (addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) *
      addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p) =
    1 * addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
⊢ ∃ m < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p),
    m.gcd (addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) = 1 ∧
      Eq (α := AddCircle p)
        (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) : 𝕜) * p) :
          𝕜 ⧸ zmultiples p)
        (↑k : 𝕜 ⧸ zmultiples p)

Tactic:
refine ⟨m, hm, mul_right_cancel₀ h.ne' ?_, hk⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
m : ℕ
hm : m < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
hk :
  Eq (α := AddCircle p)
    (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) : 𝕜) * p) :
      𝕜 ⧸ zmultiples p)
    (↑k : 𝕜 ⧸ zmultiples p)
⊢ m.gcd (addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) *
      addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
        (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) : 𝕜) * p) :
          𝕜 ⧸ zmultiples p) =
    addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)

Tactic:
gcd_mul_addOrderOf_div_eq p m h

Premises used: AddCircle.gcd_mul_addOrderOf_div_eq
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
m : ℕ
hm : m < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
hk :
  Eq (α := AddCircle p)
    (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) : 𝕜) * p) :
      𝕜 ⧸ zmultiples p)
    (↑k : 𝕜 ⧸ zmultiples p)
h₁ :
  m.gcd (addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) *
      addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p) =
    m.gcd (addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) *
      addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
        (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) : 𝕜) * p) :
          𝕜 ⧸ zmultiples p)
h₂ : 1 * addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p) = addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
⊢ m.gcd (addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) *
      addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p) =
    1 * addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)

Tactic:
convert! gcd_mul_addOrderOf_div_eq p m h using 1

Premises used: AddCircle.gcd_mul_addOrderOf_div_eq
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
m : ℕ
hm : m < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
hk :
  Eq (α := AddCircle p)
    (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) : 𝕜) * p) :
      𝕜 ⧸ zmultiples p)
    (↑k : 𝕜 ⧸ zmultiples p)
h₁ h₂ :
  m.gcd (addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) *
      addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p) =
    m.gcd (addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) *
      addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑k : 𝕜 ⧸ zmultiples p)
⊢ m.gcd (addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) *
      addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p) =
    m.gcd (addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) *
      addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
        (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) : 𝕜) * p) :
          𝕜 ⧸ zmultiples p)

Tactic:
rw [hk]
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
m : ℕ
hm : m < addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)
hk :
  Eq (α := AddCircle p)
    (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)) : 𝕜) * p) :
      𝕜 ⧸ zmultiples p)
    (↑k : 𝕜 ⧸ zmultiples p)
⊢ 1 * addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p) = addOrderOf (G := AddCircle p) (↑k : 𝕜 ⧸ zmultiples p)

Tactic:
apply one_mul

Premises used: one_mul
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
h : IsOfFinAddOrder u
⊢ ∃ (m : ℕ),
    m.gcd (addOrderOf u) = 1 ∧
      m < addOrderOf u ∧ (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑(addOrderOf u) : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = u

Tactic:
let ⟨m, hl, hg, he⟩ := (addOrderOf_eq_pos_iff h.addOrderOf_pos).1 rfl
  ⟨m, hg, hl, he⟩

Premises used: Nat.gcd, HMul.hMul, IsOfFinAddOrder.addOrderOf_pos, addOrderOf, Exists, QuotientAddGroup.mk, HDiv.hDiv, Nat.cast, And, And.intro, LT.lt, _private.0.AddCircle.exists_gcd_eq_one_of_isOfFinAddOrder.match_1, Exists.intro, Iff.mp, AddCircle.addOrderOf_eq_pos_iff, OfNat.ofNat, Eq, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
a : 𝕜
simp :
  (∀ (x : ℤ), ¬x = 0 → ∀ (x_1 : ℤ), ¬p * (↑x_1 : 𝕜) = a * (↑x : 𝕜)) ↔
    ∀ (a_1 b : ℤ), ¬b = 0 → ¬p * (↑a_1 : 𝕜) = a * (↑b : 𝕜)
⊢ ¬IsOfFinAddOrder (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) ↔
    ∀ (q : ℚ), (↑q : 𝕜) ≠ a / p

Tactic:
simp +contextual [← QuotientAddGroup.mk_zsmul, mul_comm (Int.cast _), mem_zmultiples_iff,
    eq_div_iff (Fact.out : 0 < p).ne', isOfFinAddOrder_iff_zsmul_eq_zero, Rat.forall, div_eq_iff,
    div_mul_eq_mul_div]

Premises used: Int.cast, div_mul_eq_mul_div, AddSubgroup.mem_zmultiples_iff, LT.lt.ne', div_eq_iff, QuotientAddGroup.mk_zsmul, mul_comm, isOfFinAddOrder_iff_zsmul_eq_zero, eq_div_iff, Fact.out, Rat.forall
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
a : 𝕜
⊢ (∀ (x : ℤ), ¬x = 0 → ∀ (x_1 : ℤ), ¬p * (↑x_1 : 𝕜) = a * (↑x : 𝕜)) ↔
    ∀ (a_1 b : ℤ), ¬b = 0 → ¬p * (↑a_1 : 𝕜) = a * (↑b : 𝕜)

Tactic:
grind
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
a : 𝕜
⊢ IsOfFinAddOrder (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) ↔
    ∃ (q : ℚ), (↑q : 𝕜) = a / p

Tactic:
simpa using not_isOfFinAddOrder_iff_forall_rat_ne_div.not_right

Premises used: AddCircle.not_isOfFinAddOrder_iff_forall_rat_ne_div, Iff.not_right
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
⊢ Bijective.{1, u_1 + 1} (β := (↑{u : AddCircle p | addOrderOf u = n} : Type u_1))
    fun (m : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)) ↦
    Subtype.mk (p := fun (x : AddCircle p) ↦
      Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x)
      (↑(HDiv.hDiv (α := 𝕜) (↑(↑m : ℕ) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) ⋯

Tactic:
⟨fun m₁ m₂ h => Subtype.ext ?_, fun u => ?_⟩

Premises used: And.intro, Function.Bijective, Subtype.ext
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
refine_1 :
  ∀ (m₁ m₂ : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type))
    (h :
      Eq.{u_1 + 1} (α := (↑{u : AddCircle p | addOrderOf u = n} : Type u_1))
        ((fun (m : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)) ↦
            (Subtype.mk (p := fun (x : AddCircle p) ↦
                Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x)
                (↑(HDiv.hDiv (α := 𝕜) (↑(↑m : ℕ) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) ⋯ :
              { x : AddCircle p // Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x }))
          m₁)
        ((fun (m : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)) ↦
            (Subtype.mk (p := fun (x : AddCircle p) ↦
                Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x)
                (↑(HDiv.hDiv (α := 𝕜) (↑(↑m : ℕ) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) ⋯ :
              { x : AddCircle p // Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x }))
          m₂)),
    (↑m₁ : ℕ) = (↑m₂ : ℕ)
refine_2 :
  ∀ (u : (↑{u : AddCircle p | addOrderOf u = n} : Type u_1)),
    ∃ (a : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)),
      (fun (m : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)) ↦
            (Subtype.mk (p := fun (x : AddCircle p) ↦
                Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x)
                (↑(HDiv.hDiv (α := 𝕜) (↑(↑m : ℕ) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) ⋯ :
              { x : AddCircle p // Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x }))
          a =
        u
⊢ Bijective.{1, u_1 + 1} (β := (↑{u : AddCircle p | addOrderOf u = n} : Type u_1))
    fun (m : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)) ↦
    Subtype.mk (p := fun (x : AddCircle p) ↦
      Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x)
      (↑(HDiv.hDiv (α := 𝕜) (↑(↑m : ℕ) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) ⋯

Tactic:
refine ⟨fun m₁ m₂ h => Subtype.ext ?_, fun u => ?_⟩