case refine'_1
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ (∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = u) → addOrderOf u = n

case refine'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ addOrderOf u = n ↔ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = u
refine' ⟨QuotientAddGroup.induction_on' u fun k hk => _, _⟩
case refine'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
h0 : addOrderOf ↑k • ↑k = 0
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
case refine'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
have h0 := addOrderOf_nsmul_eq_zero (k : AddCircle p)
case refine'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
case refine'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
h0 : addOrderOf ↑k • ↑k = 0
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
rw [hk, ← coe_nsmul, coe_eq_zero_iff] at h0
case refine'_2.intro
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : a • p = n • k
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
case refine'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
obtain ⟨a, ha⟩ := h0
case refine'_2.intro
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
case refine'_2.intro
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : a • p = n • k
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
have h0 : (_ : 𝕜) ≠ 0 := Nat.cast_ne_zero.2 h.ne'
case refine'_2.intro
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
case refine'_2.intro
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
rw [nsmul_eq_mul, mul_comm, ← div_eq_iff h0, ← a.ediv_add_emod' n, add_smul, add_div,
  zsmul_eq_mul, Int.cast_mul, Int.cast_ofNat, mul_assoc, ← mul_div, mul_comm _ p,
  mul_div_cancel p h0] at ha
case refine'_2.intro
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
case refine'_2.intro
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
have han : _ = a % n := Int.toNat_of_nonneg (Int.emod_nonneg _ <| by exact_mod_cast h.ne')
case he
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
⊢ ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k

case refine'_2.intro
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
case refine'_2.intro
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
have he : (↑(↑((a % n).toNat) / ↑n * p) : AddCircle p) = k
case refine'_2.intro.refine'_1
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
⊢ Int.toNat (a % ↑n) < n

case refine'_2.intro.refine'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
⊢ Nat.gcd (Int.toNat (a % ↑n)) n = 1
case refine'_2.intro
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
refine' ⟨(a % n).toNat, _, _, he⟩
case refine'_1.intro.intro.intro
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
left✝ : m < n
h₁ : Nat.gcd m n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n
case refine'_1
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ (∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = u) → addOrderOf u = n
rintro ⟨m, _, h₁, rfl⟩
no goals
case refine'_1.intro.intro.intro
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
left✝ : m < n
h₁ : Nat.gcd m n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n
exact addOrderOf_div_of_gcd_eq_one h h₁
no goals
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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
⊢ ↑n ≠ 0
exact_mod_cast h.ne'
case h.e'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
⊢ ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑(↑(a / ↑n) * p + (a % ↑n) • p / ↑n)
case he
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
⊢ ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
convert congr_arg (QuotientAddGroup.mk : 𝕜 → (AddCircle p)) ha using 1
no goals
case h.e'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
⊢ ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑(↑(a / ↑n) * p + (a % ↑n) • p / ↑n)
rw [coe_add, ← Int.cast_ofNat, han, zsmul_eq_mul, mul_div_right_comm, eq_comm, add_left_eq_self,
  ←zsmul_eq_mul, coe_zsmul, coe_period, smul_zero]
case refine'_2.intro.refine'_1
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
⊢ a % ↑n < ↑n
case refine'_2.intro.refine'_1
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
⊢ Int.toNat (a % ↑n) < n
rw [← Int.ofNat_lt, han]
no goals
case refine'_2.intro.refine'_1
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
⊢ a % ↑n < ↑n
exact Int.emod_lt_of_pos _ (Int.ofNat_lt.2 h)
case refine'_2.intro.refine'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
this :
  Nat.gcd (Int.toNat (a % ↑n)) n * addOrderOf ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) =
    addOrderOf ↑(↑(Int.toNat (a % ↑n)) / ↑n * p)
⊢ Nat.gcd (Int.toNat (a % ↑n)) n = 1
case refine'_2.intro.refine'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
⊢ Nat.gcd (Int.toNat (a % ↑n)) n = 1
have := (gcd_mul_addOrderOf_div_eq p (Int.toNat (a % ↑n)) h).trans
  ((congr_arg addOrderOf he).trans hk).symm
case refine'_2.intro.refine'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
this : Nat.gcd (Int.toNat (a % ↑n)) n = 1
⊢ Nat.gcd (Int.toNat (a % ↑n)) n = 1

case refine'_2.intro.refine'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
this : Nat.gcd (Int.toNat (a % ↑n)) n * addOrderOf ↑k = addOrderOf ↑k
⊢ 0 < addOrderOf ↑k
case refine'_2.intro.refine'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
this :
  Nat.gcd (Int.toNat (a % ↑n)) n * addOrderOf ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) =
    addOrderOf ↑(↑(Int.toNat (a % ↑n)) / ↑n * p)
⊢ Nat.gcd (Int.toNat (a % ↑n)) n = 1
rw [he, Nat.mul_left_eq_self_iff] at this
no goals
case refine'_2.intro.refine'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
this : Nat.gcd (Int.toNat (a % ↑n)) n = 1
⊢ Nat.gcd (Int.toNat (a % ↑n)) n = 1
exact this
no goals
case refine'_2.intro.refine'_2
𝕜 : Type u_1
B : Type ?u.220024
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
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 : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
this : Nat.gcd (Int.toNat (a % ↑n)) n * addOrderOf ↑k = addOrderOf ↑k
⊢ 0 < addOrderOf ↑k
rwa [hk]