awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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)
⊢ (↑((↑m : 𝕜) / q * r) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
have 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)
Tactic: rw [mul_comm_div, ← nsmul_eq_mul, coe_nsmul]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p q r : 𝕜
m : ℤ
⊢ (↑((↑m : 𝕜) / q * r) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
have rw : (↑((↑m : 𝕜) * (r / q)) : 𝕜 ⧸ 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]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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)
⊢ (↑((↑m : 𝕜) / q * r) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
have rw₁ : (↑(m • (r / q)) : 𝕜 ⧸ 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]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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)
⊢ (↑((↑m : 𝕜) / q * r) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
have 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)
Tactic: rw [mul_comm_div, ← zsmul_eq_mul, coe_zsmul]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
have norm_cast : ¬n = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (hypothesis)
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
⊢ 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
have hn₁ : Ne.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0
Tactic: replace hn : (n : 𝕜) ≠ 0 := by norm_cast
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ 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
have 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
Tactic: change n • QuotientAddGroup.mk' _ ((n : 𝕜)⁻¹ * ↑(equivIco p 0 x)) = x
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ 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
have rw : (QuotientAddGroup.mk' (zmultiples p) : (a : 𝕜) → 𝕜 ⧸ zmultiples p)
    (↑((equivIco p 0 : (a : AddCircle p) → (↑(Ico 0 (0 + p)) : Type u_1)) x) : 𝕜) =
  x
Tactic: rw [← map_zsmul, ← smul_mul_assoc, zsmul_eq_mul, mul_inv_cancel₀ hn, one_mul]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) = n
have 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
Tactic: rw [addOrderOf_eq_iff h]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 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
have h₁ : LT.lt.{u_1} (α := 𝕜) 0 (↑n : 𝕜)
Tactic: replace h : 0 < (n : 𝕜) := Nat.cast_pos.2 h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
have refine_1 : HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) n (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) = 0
Tactic: refine ⟨?_, fun m hn h0 => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ 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
have refine_2 : ∀ (m : ℕ) (hn : m < n) (h0 : 0 < m),
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) ≠
    0
Tactic: refine ⟨?_, fun m hn h0 => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
have refine_1 : Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑((↑n : 𝕜) * (p / (↑n : 𝕜))) : 𝕜 ⧸ zmultiples p) 0
Tactic: simp only [Ne, ← coe_nsmul, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) ≠
    0
have refine_2 : ¬Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑((↑m : 𝕜) * (p / (↑n : 𝕜))) : 𝕜 ⧸ zmultiples p)
    0
Tactic: simp only [Ne, ← coe_nsmul, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕜)
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑((↑n : 𝕜) * (p / (↑n : 𝕜))) : 𝕜 ⧸ zmultiples p)
    0
have refine_1 : Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑p : 𝕜 ⧸ zmultiples p) 0
Tactic: rw [mul_div_cancel₀ _ h.ne', coe_period]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑((↑n : 𝕜) * (p / (↑n : 𝕜))) : 𝕜 ⧸ zmultiples p)
    0
have refine_1₁ : Eq.{u_1 + 1} (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) 0 0
Tactic: rw [mul_div_cancel₀ _ h.ne', coe_period]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ ¬Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑((↑m : 𝕜) * (p / (↑n : 𝕜))) : 𝕜 ⧸ zmultiples p) 0
have refine_2 : ¬∃ (n_1 : ℕ), n_1 • p = (↑m : 𝕜) * (p / (↑n : 𝕜))
Tactic: rw [coe_eq_zero_of_pos_iff p hp.out (mul_pos (Nat.cast_pos.2 h0) <| div_pos hp.out h)]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (hypothesis)
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 : 𝕜))
⊢ False
have hk₁ : 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
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ m.gcd n *
      addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
        (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n
have 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
Tactic: rw [natCast_div_mul_eq_nsmul, IsOfFinAddOrder.addOrderOf_nsmul]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ m.gcd n *
      addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
        (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n
have h : IsOfFinAddOrder (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)
Tactic: rw [natCast_div_mul_eq_nsmul, IsOfFinAddOrder.addOrderOf_nsmul]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < 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
have rw : n.gcd m ∣ n
Tactic: rw [addOrderOf_period_div hn, Nat.gcd_comm, Nat.mul_div_cancel']
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ IsOfFinAddOrder (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)
have h : 0 < addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)
Tactic: rwa [← addOrderOf_pos_iff, addOrderOf_period_div hn]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n
have 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)
Tactic: convert! gcd_mul_addOrderOf_div_eq p m hn
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ 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)
have 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)
Tactic: rw [h, one_mul]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: rw [h, one_mul]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n
have 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
Tactic: cases m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n
have 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
Tactic: cases m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
      (↑(HDiv.hDiv (α := 𝕜) (↑(Int.ofNat a) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n
have ofNat : addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
    (↑(HDiv.hDiv (α := 𝕜) (↑a : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
  n
Tactic: simp only [Int.ofNat_eq_natCast, Int.cast_natCast, Int.natAbs_natCast] at h ⊢
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 (α := 𝕜) (↑(Int.negSucc a) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    n
have negSucc : addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))
    (↑(HDiv.hDiv (α := 𝕜) (↑(a + 1) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
  n
Tactic: simp only [Int.cast_negSucc, neg_div, neg_mul, coe_neg, addOrderOf_neg]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
have norm_cast : ¬q.den = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑((↑q : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    q.den
have this : Ne.{u_1 + 1} (α := 𝕜) (↑(↑q.den : ℤ) : 𝕜) 0
Tactic: have : (↑(q.den : ℤ) : 𝕜) ≠ 0 := by
    norm_cast
    exact q.pos.ne.symm
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑((↑q : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    q.den
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑((↑q : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    q.den
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ addOrderOf (G := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑((↑q : 𝕜) * p) : 𝕜 ⧸ zmultiples p) =
    q.den
have 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
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]