-- Mathlib/Topology/Instances/AddCircle.lean
theorem addOrderOf_eq_pos_iff {u : AddCircle p} {n : ℕ} (h : 0 < n) :
    addOrderOf u = n ↔ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(a % ↑n).toNat = a % ↑n
⊢ ↑(↑(a % ↑n).toNat / ↑n * p) = ↑k

Tactic:
convert congr_arg (QuotientAddGroup.mk : 𝕜 → (AddCircle p)) ha using 1

Result:
case h.e'_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(a % ↑n).toNat = a % ↑n
⊢ ↑(↑(a % ↑n).toNat / ↑n * p) = ↑(↑(a / ↑n) * p + (a % ↑n) • p / ↑n)

Proof state:
case refine_2.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(a % ↑n).toNat = a % ↑n
he : ↑(↑(a % ↑n).toNat / ↑n * p) = ↑k
⊢ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k

Tactic:
refine ⟨(a % n).toNat, ?_, ?_, he⟩

Result:
case refine_2.intro.refine_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(a % ↑n).toNat = a % ↑n
he : ↑(↑(a % ↑n).toNat / ↑n * p) = ↑k
⊢ (a % ↑n).toNat < n

case refine_2.intro.refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(a % ↑n).toNat = a % ↑n
he : ↑(↑(a % ↑n).toNat / ↑n * p) = ↑k
⊢ (a % ↑n).toNat.gcd n = 1

Proof state:
case refine_2.intro.refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(a % ↑n).toNat = a % ↑n
he : ↑(↑(a % ↑n).toNat / ↑n * p) = ↑k
this : (a % ↑n).toNat.gcd n * addOrderOf ↑(↑(a % ↑n).toNat / ↑n * p) = addOrderOf ↑(↑(a % ↑n).toNat / ↑n * p)
⊢ (a % ↑n).toNat.gcd n = 1

Tactic:
rw [he, Nat.mul_left_eq_self_iff] at this

Result:
case refine_2.intro.refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(a % ↑n).toNat = a % ↑n
he : ↑(↑(a % ↑n).toNat / ↑n * p) = ↑k
this : (a % ↑n).toNat.gcd n = 1
⊢ (a % ↑n).toNat.gcd n = 1

case refine_2.intro.refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(a % ↑n).toNat = a % ↑n
he : ↑(↑(a % ↑n).toNat / ↑n * p) = ↑k
this : (a % ↑n).toNat.gcd n * addOrderOf ↑k = addOrderOf ↑k
⊢ 0 < addOrderOf ↑k

Proof state:
case refine_2.intro.refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(a % ↑n).toNat = a % ↑n
he : ↑(↑(a % ↑n).toNat / ↑n * p) = ↑k
this : (a % ↑n).toNat.gcd n = 1
⊢ (a % ↑n).toNat.gcd n = 1

Tactic:
exact this

Result:
no goals

Proof state:
case refine_2.intro.refine_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(a % ↑n).toNat = a % ↑n
he : ↑(↑(a % ↑n).toNat / ↑n * p) = ↑k
⊢ (a % ↑n).toNat < n

Tactic:
rw [← Int.ofNat_lt, han]

Result:
case refine_2.intro.refine_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(a % ↑n).toNat = a % ↑n
he : ↑(↑(a % ↑n).toNat / ↑n * p) = ↑k
⊢ a % ↑n < ↑n

Proof state:
case refine_2.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(a % ↑n).toNat = a % ↑n
⊢ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k

Tactic:
have he : (↑(↑((a % n).toNat) / ↑n * p) : AddCircle p) = k := by
  convert congr_arg (QuotientAddGroup.mk : 𝕜 → (AddCircle p)) ha using 1
  rw [coe_add, ← Int.cast_natCast, han, zsmul_eq_mul, mul_div_right_comm, eq_comm,
    add_left_eq_self, ← zsmul_eq_mul, coe_zsmul, coe_period, smul_zero]

Result:
case refine_2.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(a % ↑n).toNat = a % ↑n
he : ↑(↑(a % ↑n).toNat / ↑n * p) = ↑k
⊢ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k

Proof state:
case refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
h0 : ∃ n_1, n_1 • p = n • k
⊢ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k

Tactic:
obtain ⟨a, ha⟩ := h0

Result:
case refine_2.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : a • p = n • k
⊢ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k

Proof state:
case refine_2.intro.refine_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(a % ↑n).toNat = a % ↑n
he : ↑(↑(a % ↑n).toNat / ↑n * p) = ↑k
⊢ a % ↑n < ↑n

Tactic:
exact Int.emod_lt_of_pos _ (Int.ofNat_lt.2 h)

Result:
no goals

Proof state:
case refine_2.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : a • p = n • k
⊢ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k

Tactic:
have h0 : (_ : 𝕜) ≠ 0 := Nat.cast_ne_zero.2 h.ne'

Result:
case refine_2.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : a • p = n • k
h0 : ↑n ≠ 0
⊢ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k

Proof state:
case refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
h0 : addOrderOf ↑k • ↑k = 0
⊢ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k

Tactic:
rw [hk, ← coe_nsmul, coe_eq_zero_iff] at h0

Result:
case refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
h0 : ∃ n_1, n_1 • p = n • k
⊢ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k

Proof state:
case refine_1.intro.intro.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
left✝ : m < n
h₁ : m.gcd n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n

Tactic:
exact addOrderOf_div_of_gcd_eq_one h h₁

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u) → addOrderOf u = n

Tactic:
rintro ⟨m, _, h₁, rfl⟩

Result:
case refine_1.intro.intro.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
left✝ : m < n
h₁ : m.gcd n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n