awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hp : p ≠ 0
hq : q ≠ 0
x : 𝕜
⊢ Eq (α := AddCircle p)
    ((Homeomorph.symm (homeomorphAddCircle p q hp hq) : (a : AddCircle q) → AddCircle p) (↑x : 𝕜 ⧸ zmultiples q) :
      AddCircle p)
    ((↑(x * (q⁻¹ * p)) : HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) :
      HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, MulOpposite.unop, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p q r : 𝕜
m : ℕ
rw :
  (↑((↑m : 𝕜) * (r / q)) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
rw₁ :
  (↑(m • (r / q)) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
rw₂ rw₃ :
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
⊢ (↑((↑m : 𝕜) / q * r) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)

Tactic:
rw [mul_comm_div, ← nsmul_eq_mul, coe_nsmul]

Premises used: AddCircle.coe_nsmul, mul_comm_div, nsmul_eq_mul
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p q r : 𝕜
m : ℤ
rw :
  (↑((↑m : 𝕜) * (r / q)) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
rw₁ :
  (↑(m • (r / q)) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
rw₂ rw₃ :
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
⊢ (↑((↑m : 𝕜) / q * r) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)

Tactic:
rw [mul_comm_div, ← zsmul_eq_mul, coe_zsmul]

Premises used: zsmul_eq_mul, AddCircle.coe_zsmul, mul_comm_div
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
inst_3 : FloorRing 𝕜
x : 𝕜
⊢ (↑((equivIco p 0 : (a : AddCircle p) → (↑(Ico 0 (0 + p)) : Type u_1)) (↑x : 𝕜 ⧸ zmultiples p)) : 𝕜) =
    Int.fract (x / p) * p

Tactic:
toIcoMod_eq_fract_mul _ x

Premises used: toIcoMod_eq_fract_mul, Quotient.liftOn', Function.Periodic.lift, toIcoMod
-- 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)
inst_3 : FloorRing 𝕜
x : AddCircle p
⊢ Eq (α := AddCircle p)
    (↑(HMul.hMul (α := 𝕜) (↑0 : 𝕜)⁻¹ (↑((equivIco p 0 : (a : AddCircle p) → (↑(Ico 0 (0 + p)) : Type u_1)) x) : 𝕜)) :
      𝕜 ⧸ zmultiples p)
    0

Tactic:
simp
-- 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)
inst_3 : FloorRing 𝕜
n : ℤ
x : AddCircle p
hn : n ≠ 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬n = 0
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0

Tactic:
norm_cast
-- 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)
inst_3 : FloorRing 𝕜
n : ℤ
x : AddCircle p
hn : n ≠ 0
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0

Tactic:
replace hn : (n : 𝕜) ≠ 0 := by norm_cast
-- 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)
inst_3 : FloorRing 𝕜
n : ℤ
x : AddCircle p
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
change :
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) n
      ((QuotientAddGroup.mk' (zmultiples p) : (a : 𝕜) → 𝕜 ⧸ zmultiples p)
          (HMul.hMul (α := 𝕜) (↑n : 𝕜)⁻¹
            (↑((equivIco p 0 : (a : AddCircle p) → (↑(Ico 0 (0 + p)) : Type u_1)) x) : 𝕜)) :
        HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) =
    x
⊢ HSMul.hSMul (β := AddCircle p) n
      (↑(HMul.hMul (α := 𝕜) (↑n : 𝕜)⁻¹ (↑((equivIco p 0 : (a : AddCircle p) → (↑(Ico 0 (0 + p)) : Type u_1)) x) : 𝕜)) :
        𝕜 ⧸ zmultiples p) =
    x

Tactic:
change n • QuotientAddGroup.mk' _ ((n : 𝕜)⁻¹ * ↑(equivIco p 0 x)) = x

Premises used: Int.cast, HMul.hMul, QuotientAddGroup.mk', Inv.inv, DFunLike.coe
-- 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)
inst_3 : FloorRing 𝕜
n : ℤ
x : AddCircle p
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
rw :
  (QuotientAddGroup.mk' (zmultiples p) : (a : 𝕜) → 𝕜 ⧸ zmultiples p)
      (↑((equivIco p 0 : (a : AddCircle p) → (↑(Ico 0 (0 + p)) : Type u_1)) x) : 𝕜) =
    x
⊢ HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) n
      ((QuotientAddGroup.mk' (zmultiples p) : (a : 𝕜) → 𝕜 ⧸ zmultiples p)
          (HMul.hMul (α := 𝕜) (↑n : 𝕜)⁻¹
            (↑((equivIco p 0 : (a : AddCircle p) → (↑(Ico 0 (0 + p)) : Type u_1)) x) : 𝕜)) :
        HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) =
    x

Tactic:
rw [← map_zsmul, ← smul_mul_assoc, zsmul_eq_mul, mul_inv_cancel₀ hn, one_mul]

Premises used: zsmul_eq_mul, mul_inv_cancel₀, smul_mul_assoc, one_mul, map_zsmul
-- 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)
inst_3 : FloorRing 𝕜
n : ℤ
x : AddCircle p
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
⊢ (QuotientAddGroup.mk' (zmultiples p) : (a : 𝕜) → 𝕜 ⧸ zmultiples p)
      (↑((equivIco p 0 : (a : AddCircle p) → (↑(Ico 0 (0 + p)) : Type u_1)) x) : 𝕜) =
    x

Tactic:
(equivIco p 0).symm_apply_apply x

Premises used: AddCircle.equivIco, Equiv.symm_apply_apply, OfNat.ofNat
-- 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)
inst_3 : FloorRing 𝕜
n : ℤ
x : AddCircle p
hn : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
⊢ (QuotientAddGroup.mk' (zmultiples p) : (a : 𝕜) → 𝕜 ⧸ zmultiples p)
      (↑((equivIco p 0 : (a : AddCircle p) → (↑(Ico 0 (0 + p)) : Type u_1)) x) : 𝕜) =
    x

Tactic:
exact (equivIco p 0).symm_apply_apply x

Premises used: AddCircle.equivIco, Equiv.symm_apply_apply, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : FloorRing 𝕜
x : 𝕜
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples 1)) (↑(Int.fract x) : 𝕜 ⧸ zmultiples 1)
    (↑x : 𝕜 ⧸ zmultiples 1)

Tactic:
simp [← Int.self_sub_floor, mem_zmultiples_iff]

Premises used: AddSubgroup.mem_zmultiples_iff, Int.self_sub_floor
-- 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
rw :
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) n (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) =
      0 ∧
    ∀ m < n,
      0 < m →
        HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m
            (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) ≠
          0
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) = n

Tactic:
rw [addOrderOf_eq_iff h]

Premises used: addOrderOf_eq_iff
-- 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
⊢ LT.lt.{u_1} (α := 𝕜) 0 (↑n : 𝕜)

Tactic:
replace h : 0 < (n : 𝕜) := Nat.cast_pos.2 h
-- 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 : LT.lt.{u_1} (α := 𝕜) 0 (↑n : 𝕜)
⊢ HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) n (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) =
      0 ∧
    ∀ m < n,
      0 < m →
        HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m
            (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) ≠
          0

Tactic:
⟨?_, fun m hn h0 => ?_⟩

Premises used: And.intro
-- 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 : LT.lt.{u_1} (α := 𝕜) 0 (↑n : 𝕜)
refine_1 :
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) n (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) =
    0
refine_2 :
  ∀ (m : ℕ) (hn : m < n) (h0 : 0 < m),
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m
        (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) ≠
      0
⊢ HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) n (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) =
      0 ∧
    ∀ m < n,
      0 < m →
        HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m
            (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) ≠
          0

Tactic:
refine ⟨?_, fun m hn h0 => ?_⟩
-- 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 : LT.lt.{u_1} (α := 𝕜) 0 (↑n : 𝕜)
refine_1 :
  Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑((↑n : 𝕜) * (p / (↑n : 𝕜))) : 𝕜 ⧸ zmultiples p)
    0
⊢ HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) n (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) =
    0

Tactic:
simp only [Ne, ← coe_nsmul, nsmul_eq_mul]

Premises used: AddCircle.coe_nsmul, Ne, nsmul_eq_mul
-- 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 : LT.lt.{u_1} (α := 𝕜) 0 (↑n : 𝕜)
m : ℕ
hn : m < n
h0 : 0 < m
refine_2 :
  ¬Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑((↑m : 𝕜) * (p / (↑n : 𝕜))) : 𝕜 ⧸ zmultiples p) 0
⊢ HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) ≠
    0

Tactic:
simp only [Ne, ← coe_nsmul, nsmul_eq_mul]

Premises used: AddCircle.coe_nsmul, Ne, nsmul_eq_mul
-- 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 : LT.lt.{u_1} (α := 𝕜) 0 (↑n : 𝕜)
refine_1 : Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑p : 𝕜 ⧸ zmultiples p) 0
refine_1₁ refine_1₂ : Eq.{u_1 + 1} (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) 0 0
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑((↑n : 𝕜) * (p / (↑n : 𝕜))) : 𝕜 ⧸ zmultiples p)
    0

Tactic:
rw [mul_div_cancel₀ _ h.ne', coe_period]

Premises used: mul_div_cancel₀, LT.lt.ne', AddCircle.coe_period
-- 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 : LT.lt.{u_1} (α := 𝕜) 0 (↑n : 𝕜)
m : ℕ
hn : m < n
h0 : 0 < m
refine_2 : ¬∃ (n_1 : ℕ), n_1 • p = (↑m : 𝕜) * (p / (↑n : 𝕜))
⊢ ¬Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑((↑m : 𝕜) * (p / (↑n : 𝕜))) : 𝕜 ⧸ zmultiples p) 0

Tactic:
rw [coe_eq_zero_of_pos_iff p hp.out (mul_pos (Nat.cast_pos.2 h0) <| div_pos hp.out h)]

Premises used: Iff.mpr, Nat.cast_pos, mul_pos, AddCircle.coe_eq_zero_of_pos_iff, div_pos, Fact.out
-- 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 : LT.lt.{u_1} (α := 𝕜) 0 (↑n : 𝕜)
m : ℕ
hn : m < n
h0 : 0 < m
k : ℕ
hk : k • p = (↑m : 𝕜) * (p / (↑n : 𝕜))
⊢ n * k = m

Tactic:
rw [mul_div, eq_div_iff h.ne', nsmul_eq_mul, mul_right_comm, ← Nat.cast_mul,
    (mul_left_injective₀ hp.out.ne').eq_iff, Nat.cast_inj, mul_comm] at hk

Premises used: mul_div, mul_left_injective₀, Function.Injective.eq_iff, Nat.cast_inj, LT.lt.ne', Nat.cast_mul, mul_right_comm, mul_comm, nsmul_eq_mul, eq_div_iff, Fact.out
-- 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 : LT.lt.{u_1} (α := 𝕜) 0 (↑n : 𝕜)
m : ℕ
hn : m < n
h0 : 0 < m
k : ℕ
hk : n * k = m
⊢ False

Tactic:
(Nat.le_of_dvd h0 ⟨_, hk.symm⟩).not_gt hn

Premises used: LE.le.not_gt, Exists.intro, Eq.symm, Nat.le_of_dvd
-- 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 : LT.lt.{u_1} (α := 𝕜) 0 (↑n : 𝕜)
m : ℕ
hn : m < n
h0 : 0 < m
k : ℕ
hk : n * k = m
⊢ False

Tactic:
exact (Nat.le_of_dvd h0 ⟨_, hk.symm⟩).not_gt hn

Premises used: LE.le.not_gt, Exists.intro, Eq.symm, Nat.le_of_dvd
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
rw :
  m.gcd n *
      (addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
          (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) /
        (addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
              (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)).gcd
          m) =
    n
h :
  IsOfFinAddOrder (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)
⊢ m.gcd n *
      addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
        (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n

Tactic:
rw [natCast_div_mul_eq_nsmul, IsOfFinAddOrder.addOrderOf_nsmul]

Premises used: IsOfFinAddOrder.addOrderOf_nsmul, AddCircle.natCast_div_mul_eq_nsmul
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
rw : n.gcd m ∣ n
⊢ m.gcd n *
      (addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
          (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) /
        (addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
              (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)).gcd
          m) =
    n

Tactic:
rw [addOrderOf_period_div hn, Nat.gcd_comm, Nat.mul_div_cancel']

Premises used: AddCircle.addOrderOf_period_div, Nat.gcd_comm, Nat.mul_div_cancel'
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ n.gcd m ∣ n

Tactic:
n.gcd_dvd_left m

Premises used: Nat.gcd_dvd_left
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ n.gcd m ∣ n

Tactic:
exact n.gcd_dvd_left m

Premises used: Nat.gcd_dvd_left
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
h :
  0 < addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)
h₁ h₂ h₃ h₄ : 0 < n
⊢ IsOfFinAddOrder (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)

Tactic:
rwa [← addOrderOf_pos_iff, addOrderOf_period_div hn]

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

Tactic:
gcd_mul_addOrderOf_div_eq p m hn

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)
m n : ℕ
hn : 0 < n
h : m.gcd n = 1
h₁ :
  addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    m.gcd n *
      addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
        (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p)
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n

Tactic:
convert! gcd_mul_addOrderOf_div_eq p m hn

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)
m n : ℕ
hn : 0 < n
h : m.gcd n = 1
h₁ :
  addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    1 *
      addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
        (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p)
h₂ h₃ :
  addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p)
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    m.gcd n *
      addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
        (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p)

Tactic:
rw [h, 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)
m : ℤ
n : ℕ
hn : 0 < n
h : m.natAbs.gcd n = 1
ofNat :
  ∀ (a : ℕ) (h : (Int.ofNat a).natAbs.gcd n = 1),
    addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
        (↑(HDiv.hDiv (α := 𝕜) (↑(Int.ofNat a) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
      n
negSucc :
  ∀ (a : ℕ) (h : (Int.negSucc a).natAbs.gcd n = 1),
    addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
        (↑(HDiv.hDiv (α := 𝕜) (↑(Int.negSucc a) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
      n
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n

Tactic:
cases m
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a : ℕ
h : (Int.ofNat a).natAbs.gcd n = 1
ofNat :
  addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑a : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑(Int.ofNat a) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n

Tactic:
simp only [Int.ofNat_eq_natCast, Int.cast_natCast, Int.natAbs_natCast] at h ⊢

Premises used: Int.cast_natCast, Int.ofNat_eq_natCast, Int.natAbs_natCast
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a : ℕ
h : a.gcd n = 1
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑a : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n

Tactic:
addOrderOf_div_of_gcd_eq_one hn 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 : ℕ
hn : 0 < n
a : ℕ
h : a.gcd n = 1
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑a : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n

Tactic:
exact addOrderOf_div_of_gcd_eq_one hn 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 : ℕ
hn : 0 < n
a : ℕ
h : (Int.negSucc a).natAbs.gcd n = 1
negSucc :
  addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑(a + 1) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑(Int.negSucc a) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n

Tactic:
simp only [Int.cast_negSucc, neg_div, neg_mul, coe_neg, addOrderOf_neg]

Premises used: addOrderOf_neg, neg_div, AddCircle.coe_neg, Int.cast_negSucc, neg_mul
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a : ℕ
h : (Int.negSucc a).natAbs.gcd n = 1
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑(a + 1) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n

Tactic:
addOrderOf_div_of_gcd_eq_one hn 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 : ℕ
hn : 0 < n
a : ℕ
h : (Int.negSucc a).natAbs.gcd n = 1
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑(a + 1) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n

Tactic:
exact addOrderOf_div_of_gcd_eq_one hn 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)
q : ℚ
norm_cast : ¬q.den = 0
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑(↑q.den : ℤ) : 𝕜) 0

Tactic:
norm_cast
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ ¬q.den = 0

Tactic:
q.pos.ne.symm

Premises used: Rat.pos, Ne.symm, 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)
q : ℚ
⊢ ¬q.den = 0

Tactic:
exact q.pos.ne.symm

Premises used: Rat.pos, Ne.symm, 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)
q : ℚ
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑(↑q.den : ℤ) : 𝕜) 0

Tactic:
have : (↑(q.den : ℤ) : 𝕜) ≠ 0 := by
    norm_cast
    exact q.pos.ne.symm