case intro
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
⊢ orderOf x = n
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
⊢ orderOf x = n
cases' exists_eq_mul_right_of_dvd (orderOf_dvd_of_pow_eq_one hx) with a ha
case intro
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
⊢ a = 1
case intro
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
⊢ orderOf x = n
suffices a = 1 by simp [this, ha]
case intro
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
⊢ False
case intro
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
⊢ a = 1
by_contra h
case intro
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ False
case intro
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
⊢ False
have a_min_fac_dvd_p_sub_one : a.minFac ∣ n := by
  obtain ⟨b, hb⟩ : ∃ b : ℕ, a = b * a.minFac := exists_eq_mul_left_of_dvd a.minFac_dvd
  rw [hb, ← mul_assoc] at ha
  exact Dvd.intro_left (orderOf x * b) ha.symm
case intro
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ x ^ (n / minFac a) = 1
case intro
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ False
refine' hd a.minFac (Nat.minFac_prime h) a_min_fac_dvd_p_sub_one _
case intro
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ minFac a ∣ a

G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ IsOfFinOrder x
case intro
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ x ^ (n / minFac a) = 1
rw [← orderOf_dvd_iff_pow_eq_one, Nat.dvd_div_iff a_min_fac_dvd_p_sub_one, ha, mul_comm,
  Nat.mul_dvd_mul_iff_left (orderOf_pos' _)]
no goals
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
this : a = 1
⊢ orderOf x = n
simp [this, ha]
case intro
G : Type u
A : Type v
x y : G
a✝ b✝ : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
b : ℕ
hb : a = b * minFac a
⊢ minFac a ∣ n
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
⊢ minFac a ∣ n
obtain ⟨b, hb⟩ : ∃ b : ℕ, a = b * a.minFac := exists_eq_mul_left_of_dvd a.minFac_dvd
case intro
G : Type u
A : Type v
x y : G
a✝ b✝ : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
h : ¬a = 1
b : ℕ
ha : n = orderOf x * b * minFac a
hb : a = b * minFac a
⊢ minFac a ∣ n
case intro
G : Type u
A : Type v
x y : G
a✝ b✝ : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
b : ℕ
hb : a = b * minFac a
⊢ minFac a ∣ n
rw [hb, ← mul_assoc] at ha
no goals
case intro
G : Type u
A : Type v
x y : G
a✝ b✝ : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
h : ¬a = 1
b : ℕ
ha : n = orderOf x * b * minFac a
hb : a = b * minFac a
⊢ minFac a ∣ n
exact Dvd.intro_left (orderOf x * b) ha.symm
no goals
case intro
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ minFac a ∣ a
exact Nat.minFac_dvd a
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ ∃ n, 0 < n ∧ x ^ n = 1
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ IsOfFinOrder x
rw [isOfFinOrder_iff_pow_eq_one]
no goals
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ ∃ n, 0 < n ∧ x ^ n = 1
exact Exists.intro n (id ⟨hn, hx⟩)