case inr
M : Type u_1
N : Type ?u.1819153
G : Type ?u.1819156
R : Type ?u.1819159
S : Type ?u.1819162
F : Type ?u.1819165
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
this : ∀ ⦃i j : ℕ⦄, i < k → j < k → ζ ^ i = ζ ^ j → i ≤ j → i = j
hij : ¬i ≤ j
⊢ i = j

M : Type u_1
N : Type ?u.1819153
G : Type ?u.1819156
R : Type ?u.1819159
S : Type ?u.1819162
F : Type ?u.1819165
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ i = j
M : Type u_1
N : Type ?u.1819153
G : Type ?u.1819156
R : Type ?u.1819159
S : Type ?u.1819162
F : Type ?u.1819165
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
⊢ i = j
wlog hij : i ≤ j generalizing i j
M : Type u_1
N : Type ?u.1819153
G : Type ?u.1819156
R : Type ?u.1819159
S : Type ?u.1819162
F : Type ?u.1819165
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ j ≤ i
M : Type u_1
N : Type ?u.1819153
G : Type ?u.1819156
R : Type ?u.1819159
S : Type ?u.1819162
F : Type ?u.1819165
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ i = j
apply le_antisymm hij
M : Type u_1
N : Type ?u.1819153
G : Type ?u.1819156
R : Type ?u.1819159
S : Type ?u.1819162
F : Type ?u.1819165
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ j - i = 0
M : Type u_1
N : Type ?u.1819153
G : Type ?u.1819156
R : Type ?u.1819159
S : Type ?u.1819162
F : Type ?u.1819165
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ j ≤ i
rw [← tsub_eq_zero_iff_le]
M : Type u_1
N : Type ?u.1819153
G : Type ?u.1819156
R : Type ?u.1819159
S : Type ?u.1819162
F : Type ?u.1819165
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ k ∣ j - i
M : Type u_1
N : Type ?u.1819153
G : Type ?u.1819156
R : Type ?u.1819159
S : Type ?u.1819162
F : Type ?u.1819165
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ j - i = 0
apply Nat.eq_zero_of_dvd_of_lt _ (lt_of_le_of_lt tsub_le_self hj)
case a
M : Type u_1
N : Type ?u.1819153
G : Type ?u.1819156
R : Type ?u.1819159
S : Type ?u.1819162
F : Type ?u.1819165
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ ζ ^ (j - i) = 1
M : Type u_1
N : Type ?u.1819153
G : Type ?u.1819156
R : Type ?u.1819159
S : Type ?u.1819162
F : Type ?u.1819165
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ k ∣ j - i
apply h.dvd_of_pow_eq_one
no goals
case a
M : Type u_1
N : Type ?u.1819153
G : Type ?u.1819156
R : Type ?u.1819159
S : Type ?u.1819162
F : Type ?u.1819165
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ ζ ^ (j - i) = 1
rw [← ((h.isUnit (lt_of_le_of_lt (Nat.zero_le _) hi)).pow i).mul_left_inj, ← pow_add,
  tsub_add_cancel_of_le hij, H, one_mul]
no goals
case inr
M : Type u_1
N : Type ?u.1819153
G : Type ?u.1819156
R : Type ?u.1819159
S : Type ?u.1819162
F : Type ?u.1819165
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
this : ∀ ⦃i j : ℕ⦄, i < k → j < k → ζ ^ i = ζ ^ j → i ≤ j → i = j
hij : ¬i ≤ j
⊢ i = j
exact (this hj hi H.symm (le_of_not_le hij)).symm