n : ℕ
ζ : ℂ
h : ∃ i, i < n ∧ ∃ x, Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n)) = ζ
hn : n ≠ 0
⊢ ∃ i, Complex.arg ζ = ↑i / ↑n * (2 * Real.pi) ∧ IsCoprime i ↑n ∧ Int.natAbs i < n
n : ℕ
ζ : ℂ
h : IsPrimitiveRoot ζ n
hn : n ≠ 0
⊢ ∃ i, Complex.arg ζ = ↑i / ↑n * (2 * Real.pi) ∧ IsCoprime i ↑n ∧ Int.natAbs i < n
rw [Complex.isPrimitiveRoot_iff _ _ hn] at h
case intro.intro.intro
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ ∃ i_1,
    Complex.arg (Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n))) = ↑i_1 / ↑n * (2 * Real.pi) ∧
      IsCoprime i_1 ↑n ∧ Int.natAbs i_1 < n
n : ℕ
ζ : ℂ
h : ∃ i, i < n ∧ ∃ x, Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n)) = ζ
hn : n ≠ 0
⊢ ∃ i, Complex.arg ζ = ↑i / ↑n * (2 * Real.pi) ∧ IsCoprime i ↑n ∧ Int.natAbs i < n
obtain ⟨i, h, hin, rfl⟩ := h
case intro.intro.intro
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ ∃ i_1,
    Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
        ↑i_1 / ↑n * (2 * Real.pi) ∧
      IsCoprime i_1 ↑n ∧ Int.natAbs i_1 < n
case intro.intro.intro
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ ∃ i_1,
    Complex.arg (Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n))) = ↑i_1 / ↑n * (2 * Real.pi) ∧
      IsCoprime i_1 ↑n ∧ Int.natAbs i_1 < n
rw [mul_comm, ← mul_assoc, Complex.exp_mul_I]
case intro.intro.intro.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
    ↑(if i * 2 ≤ n then ↑i else ↑i - ↑n) / ↑n * (2 * Real.pi)

case intro.intro.intro.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ IsCoprime (if i * 2 ≤ n then ↑i else ↑i - ↑n) ↑n

case intro.intro.intro.refine'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Int.natAbs (if i * 2 ≤ n then ↑i else ↑i - ↑n) < n
case intro.intro.intro
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ ∃ i_1,
    Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
        ↑i_1 / ↑n * (2 * Real.pi) ∧
      IsCoprime i_1 ↑n ∧ Int.natAbs i_1 < n
refine' ⟨if i * 2 ≤ n then i else i - n, _, _, _⟩
case intro.intro.intro.refine'_1.inl
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
    ↑↑i / ↑n * (2 * Real.pi)

case intro.intro.intro.refine'_1.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
    ↑(↑i - ↑n) / ↑n * (2 * Real.pi)
case intro.intro.intro.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
    ↑(if i * 2 ≤ n then ↑i else ↑i - ↑n) / ↑n * (2 * Real.pi)
split_ifs with h₂
case intro.intro.intro.refine'_1.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Complex.arg
      (Complex.cos (↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi) +
        Complex.sin (↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi) * Complex.I) =
    ↑(↑i - ↑n) / ↑n * (2 * Real.pi)
case intro.intro.intro.refine'_1.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
    ↑(↑i - ↑n) / ↑n * (2 * Real.pi)
rw [← Complex.cos_sub_two_pi, ← Complex.sin_sub_two_pi]
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi = ↑(↑(↑i - ↑n) / ↑n * (2 * Real.pi))

case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi = ↑(↑(↑i - ↑n) / ↑n * (2 * Real.pi))

case intro.intro.intro.refine'_1.inr.convert_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑(↑i - ↑n) / ↑n * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) Real.pi
case intro.intro.intro.refine'_1.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Complex.arg
      (Complex.cos (↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi) +
        Complex.sin (↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi) * Complex.I) =
    ↑(↑i - ↑n) / ↑n * (2 * Real.pi)
convert Complex.arg_cos_add_sin_mul_I _
case intro.intro.intro.refine'_1.inr.convert_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ -Real.pi < (↑i - ↑n) * (2 * Real.pi) / ↑n ∧ (↑i - ↑n) * (2 * Real.pi) / ↑n ≤ Real.pi
case intro.intro.intro.refine'_1.inr.convert_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑(↑i - ↑n) / ↑n * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) Real.pi
field_simp [hn]
case intro.intro.intro.refine'_1.inr.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ -Real.pi < (↑i - ↑n) * (2 * Real.pi) / ↑n

case intro.intro.intro.refine'_1.inr.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ (↑i - ↑n) * (2 * Real.pi) / ↑n ≤ 0
case intro.intro.intro.refine'_1.inr.convert_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ -Real.pi < (↑i - ↑n) * (2 * Real.pi) / ↑n ∧ (↑i - ↑n) * (2 * Real.pi) / ↑n ≤ Real.pi
refine' ⟨_, le_trans _ Real.pi_pos.le⟩
case intro.intro.intro.refine'_1.inr.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ -Real.pi < (↑i - ↑n) * (2 * Real.pi) / ↑n
case intro.intro.intro.refine'_1.inr.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ -Real.pi < (↑i - ↑n) * (2 * Real.pi) / ↑n

case intro.intro.intro.refine'_1.inr.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ (↑i - ↑n) * (2 * Real.pi) / ↑n ≤ 0
on_goal 2 =>
  rw [mul_div_assoc]
  exact mul_nonpos_of_nonpos_of_nonneg (sub_nonpos.mpr <| by exact_mod_cast h.le)
    (div_nonneg (by simp [Real.pi_pos.le]) <| by simp)
case intro.intro.intro.refine'_1.inr.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n * (2 - 1) < ↑i * 2

case intro.intro.intro.refine'_1.inr.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ 0 < ↑n
case intro.intro.intro.refine'_1.inr.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ -Real.pi < (↑i - ↑n) * (2 * Real.pi) / ↑n
rw [← mul_rotate', mul_div_assoc, neg_lt, ← mul_neg, mul_lt_iff_lt_one_right Real.pi_pos, ←
  neg_div, ← neg_mul, neg_sub, div_lt_iff, one_mul, sub_mul, sub_lt_comm, ← mul_sub_one]
case intro.intro.intro.refine'_1.inr.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n < ↑i * 2

case intro.intro.intro.refine'_1.inr.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ 0 < ↑n
case intro.intro.intro.refine'_1.inr.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n * (2 - 1) < ↑i * 2

case intro.intro.intro.refine'_1.inr.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ 0 < ↑n
norm_num
case intro.intro.intro.refine'_1.inr.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ 0 < ↑n
case intro.intro.intro.refine'_1.inr.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n < ↑i * 2

case intro.intro.intro.refine'_1.inr.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ 0 < ↑n
exact_mod_cast not_le.mp h₂
case intro.intro.intro.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
⊢ IsCoprime (if i * 2 ≤ n then ↑i else ↑i - ↑n) ↑n
case intro.intro.intro.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ IsCoprime (if i * 2 ≤ n then ↑i else ↑i - ↑n) ↑n
replace hin := Nat.isCoprime_iff_coprime.mpr hin
case intro.intro.intro.refine'_2.inl
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : i * 2 ≤ n
⊢ IsCoprime ↑i ↑n

case intro.intro.intro.refine'_2.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ IsCoprime (↑i - ↑n) ↑n
case intro.intro.intro.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
⊢ IsCoprime (if i * 2 ≤ n then ↑i else ↑i - ↑n) ↑n
split_ifs
no goals
case intro.intro.intro.refine'_2.inl
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : i * 2 ≤ n
⊢ IsCoprime ↑i ↑n
exact hin
case h.e'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ ↑i - ↑n = ↑i + ↑n * -1
case intro.intro.intro.refine'_2.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ IsCoprime (↑i - ↑n) ↑n
convert hin.add_mul_left_left (-1) using 1
no goals
case h.e'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ ↑i - ↑n = ↑i + ↑n * -1
rw [mul_neg_one, sub_eq_add_neg]
case intro.intro.intro.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
⊢ IsCoprime (if i * 2 ≤ n then ↑i else ↑i - ↑n) ↑n
case intro.intro.intro.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ IsCoprime (if i * 2 ≤ n then ↑i else ↑i - ↑n) ↑n
replace hin := Nat.isCoprime_iff_coprime.mpr hin
case intro.intro.intro.refine'_2.inl
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : i * 2 ≤ n
⊢ IsCoprime ↑i ↑n

case intro.intro.intro.refine'_2.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ IsCoprime (↑i - ↑n) ↑n
case intro.intro.intro.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
⊢ IsCoprime (if i * 2 ≤ n then ↑i else ↑i - ↑n) ↑n
split_ifs
no goals
case intro.intro.intro.refine'_2.inl
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : i * 2 ≤ n
⊢ IsCoprime ↑i ↑n
exact hin
case h.e'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ ↑i - ↑n = ↑i + ↑n * -1
case intro.intro.intro.refine'_2.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ IsCoprime (↑i - ↑n) ↑n
convert hin.add_mul_left_left (-1) using 1
no goals
case h.e'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : IsCoprime ↑i ↑n
h✝ : ¬i * 2 ≤ n
⊢ ↑i - ↑n = ↑i + ↑n * -1
rw [mul_neg_one, sub_eq_add_neg]
case intro.intro.intro.refine'_3.inl
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ Int.natAbs ↑i < n

case intro.intro.intro.refine'_3.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Int.natAbs (↑i - ↑n) < n
case intro.intro.intro.refine'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Int.natAbs (if i * 2 ≤ n then ↑i else ↑i - ↑n) < n
split_ifs with h₂
case intro.intro.intro.refine'_3.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Int.natAbs (↑i - ↑n) = n - i
case intro.intro.intro.refine'_3.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Int.natAbs (↑i - ↑n) < n
suffices (i - n : ℤ).natAbs = n - i by
  rw [this]
  apply tsub_lt_self hn.bot_lt
  contrapose! h₂
  rw [Nat.eq_zero_of_le_zero h₂, MulZeroClass.zero_mul]
  exact zero_le _
case intro.intro.intro.refine'_3.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n - ↑i = ↑(n - i) ∨ ↑n - ↑i = -↑(n - i)
case intro.intro.intro.refine'_3.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Int.natAbs (↑i - ↑n) = n - i
rw [← Int.natAbs_neg, neg_sub, Int.natAbs_eq_iff]
no goals
case intro.intro.intro.refine'_3.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n - ↑i = ↑(n - i) ∨ ↑n - ↑i = -↑(n - i)
exact Or.inl (Int.ofNat_sub h.le).symm
no goals
case intro.intro.intro.refine'_3.inl
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ Int.natAbs ↑i < n
exact_mod_cast h
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
this : Int.natAbs (↑i - ↑n) = n - i
⊢ n - i < n
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
this : Int.natAbs (↑i - ↑n) = n - i
⊢ Int.natAbs (↑i - ↑n) < n
rw [this]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
this : Int.natAbs (↑i - ↑n) = n - i
⊢ 0 < i
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
this : Int.natAbs (↑i - ↑n) = n - i
⊢ n - i < n
apply tsub_lt_self hn.bot_lt
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
this : Int.natAbs (↑i - ↑n) = n - i
h₂ : i ≤ 0
⊢ i * 2 ≤ n
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
this : Int.natAbs (↑i - ↑n) = n - i
⊢ 0 < i
contrapose! h₂
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
this : Int.natAbs (↑i - ↑n) = n - i
h₂ : i ≤ 0
⊢ 0 ≤ n
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
this : Int.natAbs (↑i - ↑n) = n - i
h₂ : i ≤ 0
⊢ i * 2 ≤ n
rw [Nat.eq_zero_of_le_zero h₂, MulZeroClass.zero_mul]
no goals
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
this : Int.natAbs (↑i - ↑n) = n - i
h₂ : i ≤ 0
⊢ 0 ≤ n
exact zero_le _
case intro.intro.intro.refine'_3.inl
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ Int.natAbs ↑i < n

case intro.intro.intro.refine'_3.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Int.natAbs (↑i - ↑n) < n
case intro.intro.intro.refine'_3
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
⊢ Int.natAbs (if i * 2 ≤ n then ↑i else ↑i - ↑n) < n
split_ifs with h₂
case intro.intro.intro.refine'_3.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Int.natAbs (↑i - ↑n) = n - i
case intro.intro.intro.refine'_3.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Int.natAbs (↑i - ↑n) < n
suffices (i - n : ℤ).natAbs = n - i by
  rw [this]
  apply tsub_lt_self hn.bot_lt
  contrapose! h₂
  rw [Nat.eq_zero_of_le_zero h₂, MulZeroClass.zero_mul]
  exact zero_le _
case intro.intro.intro.refine'_3.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n - ↑i = ↑(n - i) ∨ ↑n - ↑i = -↑(n - i)
case intro.intro.intro.refine'_3.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ Int.natAbs (↑i - ↑n) = n - i
rw [← Int.natAbs_neg, neg_sub, Int.natAbs_eq_iff]
no goals
case intro.intro.intro.refine'_3.inr
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n - ↑i = ↑(n - i) ∨ ↑n - ↑i = -↑(n - i)
exact Or.inl (Int.ofNat_sub h.le).symm
no goals
case intro.intro.intro.refine'_3.inl
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ Int.natAbs ↑i < n
exact_mod_cast h
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
this : Int.natAbs (↑i - ↑n) = n - i
⊢ n - i < n
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
this : Int.natAbs (↑i - ↑n) = n - i
⊢ Int.natAbs (↑i - ↑n) < n
rw [this]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
this : Int.natAbs (↑i - ↑n) = n - i
⊢ 0 < i
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
this : Int.natAbs (↑i - ↑n) = n - i
⊢ n - i < n
apply tsub_lt_self hn.bot_lt
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
this : Int.natAbs (↑i - ↑n) = n - i
h₂ : i ≤ 0
⊢ i * 2 ≤ n
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
this : Int.natAbs (↑i - ↑n) = n - i
⊢ 0 < i
contrapose! h₂
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
this : Int.natAbs (↑i - ↑n) = n - i
h₂ : i ≤ 0
⊢ 0 ≤ n
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
this : Int.natAbs (↑i - ↑n) = n - i
h₂ : i ≤ 0
⊢ i * 2 ≤ n
rw [Nat.eq_zero_of_le_zero h₂, MulZeroClass.zero_mul]
no goals
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
this : Int.natAbs (↑i - ↑n) = n - i
h₂ : i ≤ 0
⊢ 0 ≤ n
exact zero_le _
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑(↑↑i / ↑n * (2 * Real.pi))

case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑(↑↑i / ↑n * (2 * Real.pi))

case intro.intro.intro.refine'_1.inl.convert_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑↑i / ↑n * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) Real.pi
case intro.intro.intro.refine'_1.inl
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ Complex.arg (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I) =
    ↑↑i / ↑n * (2 * Real.pi)
convert Complex.arg_cos_add_sin_mul_I _
case intro.intro.intro.refine'_1.inl.convert_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ -Real.pi < ↑i * (2 * Real.pi) / ↑n ∧ ↑i * (2 * Real.pi) / ↑n ≤ Real.pi
case intro.intro.intro.refine'_1.inl.convert_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑↑i / ↑n * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) Real.pi
field_simp [hn]
case intro.intro.intro.refine'_1.inl.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ -0 ≤ ↑i * (2 * Real.pi) / ↑n

case intro.intro.intro.refine'_1.inl.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i * (2 * Real.pi) / ↑n ≤ Real.pi
case intro.intro.intro.refine'_1.inl.convert_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ -Real.pi < ↑i * (2 * Real.pi) / ↑n ∧ ↑i * (2 * Real.pi) / ↑n ≤ Real.pi
refine' ⟨(neg_lt_neg Real.pi_pos).trans_le _, _⟩
case intro.intro.intro.refine'_1.inl.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ Real.pi * (↑i * 2 / ↑n) ≤ Real.pi
case intro.intro.intro.refine'_1.inl.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i * (2 * Real.pi) / ↑n ≤ Real.pi
rw [← mul_rotate', mul_div_assoc]
case intro.intro.intro.refine'_1.inl.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n * 1
⊢ Real.pi * (↑i * 2 / ↑n) ≤ Real.pi
case intro.intro.intro.refine'_1.inl.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ Real.pi * (↑i * 2 / ↑n) ≤ Real.pi
rw [← mul_one n] at h₂
no goals
case intro.intro.intro.refine'_1.inl.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n * 1
⊢ Real.pi * (↑i * 2 / ↑n) ≤ Real.pi
exact mul_le_of_le_one_right Real.pi_pos.le
  ((div_le_iff' <| by exact_mod_cast pos_of_gt h).mpr <| by exact_mod_cast h₂)
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑i / ↑n * (2 * ↑Real.pi)
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑(↑↑i / ↑n * (2 * Real.pi))
push_cast
no goals
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑i / ↑n * (2 * ↑Real.pi)
rfl
case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑i / ↑n * (2 * ↑Real.pi)
case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑(↑↑i / ↑n * (2 * Real.pi))
push_cast
no goals
case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) = ↑i / ↑n * (2 * ↑Real.pi)
rfl
case intro.intro.intro.refine'_1.inl.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ 0 ≤ ↑i * (2 * Real.pi) / ↑n
case intro.intro.intro.refine'_1.inl.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ -0 ≤ ↑i * (2 * Real.pi) / ↑n
rw [neg_zero]
no goals
case intro.intro.intro.refine'_1.inl.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ 0 ≤ ↑i * (2 * Real.pi) / ↑n
exact mul_nonneg (mul_nonneg i.cast_nonneg <| by simp [Real.pi_pos.le])
  (by rw [inv_nonneg]; simp only [Nat.cast_nonneg])
no goals
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ 0 ≤ 2 * Real.pi
simp [Real.pi_pos.le]
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ 0 ≤ ↑n
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ 0 ≤ (↑n)⁻¹
rw [inv_nonneg]
no goals
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n
⊢ 0 ≤ ↑n
simp only [Nat.cast_nonneg]
no goals
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n * 1
⊢ 0 < ↑n
exact_mod_cast pos_of_gt h
no goals
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : i * 2 ≤ n * 1
⊢ ↑i * 2 ≤ ↑n * 1
exact_mod_cast h₂
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi = (↑i - ↑n) / ↑n * (2 * ↑Real.pi)
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi = ↑(↑(↑i - ↑n) / ↑n * (2 * Real.pi))
push_cast
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n ≠ 0
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi = (↑i - ↑n) / ↑n * (2 * ↑Real.pi)
rw [← sub_one_mul, sub_div, div_self]
no goals
case h.e'_2.h.e'_1.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n ≠ 0
exact_mod_cast hn
case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi = (↑i - ↑n) / ↑n * (2 * ↑Real.pi)
case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi = ↑(↑(↑i - ↑n) / ↑n * (2 * Real.pi))
push_cast
case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n ≠ 0
case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi = (↑i - ↑n) / ↑n * (2 * ↑Real.pi)
rw [← sub_one_mul, sub_div, div_self]
no goals
case h.e'_2.h.e'_1.h.e'_6.h.e'_5.h.e'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑n ≠ 0
exact_mod_cast hn
case intro.intro.intro.refine'_1.inr.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ (↑i - ↑n) * (2 * Real.pi / ↑n) ≤ 0
case intro.intro.intro.refine'_1.inr.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ (↑i - ↑n) * (2 * Real.pi) / ↑n ≤ 0
rw [mul_div_assoc]
no goals
case intro.intro.intro.refine'_1.inr.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ (↑i - ↑n) * (2 * Real.pi / ↑n) ≤ 0
exact mul_nonpos_of_nonpos_of_nonneg (sub_nonpos.mpr <| by exact_mod_cast h.le)
  (div_nonneg (by simp [Real.pi_pos.le]) <| by simp)
no goals
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i ≤ ↑n
exact_mod_cast h.le
no goals
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ 0 ≤ 2 * Real.pi
simp [Real.pi_pos.le]
no goals
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ 0 ≤ ↑n
simp
case intro.intro.intro.refine'_1.inr.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ (↑i - ↑n) * (2 * Real.pi / ↑n) ≤ 0
case intro.intro.intro.refine'_1.inr.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ (↑i - ↑n) * (2 * Real.pi) / ↑n ≤ 0
rw [mul_div_assoc]
no goals
case intro.intro.intro.refine'_1.inr.convert_2.refine'_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ (↑i - ↑n) * (2 * Real.pi / ↑n) ≤ 0
exact mul_nonpos_of_nonpos_of_nonneg (sub_nonpos.mpr <| by exact_mod_cast h.le)
  (div_nonneg (by simp [Real.pi_pos.le]) <| by simp)
no goals
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ ↑i ≤ ↑n
exact_mod_cast h.le
no goals
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ 0 ≤ 2 * Real.pi
simp [Real.pi_pos.le]
no goals
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ 0 ≤ ↑n
simp
no goals
case intro.intro.intro.refine'_1.inr.convert_2.refine'_1
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : Nat.coprime i n
h₂ : ¬i * 2 ≤ n
⊢ 0 < ↑n
exact Nat.cast_pos.mpr hn.bot_lt