case inl
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
hG : ∀ (g : G), g ^ 0 = 1
⊢ exponent G ∣ 0

case inr
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
⊢ exponent G ∣ n
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
⊢ exponent G ∣ n
rcases n.eq_zero_or_pos with (rfl | hpos)
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
⊢ n % exponent G = 0
case inr
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
⊢ exponent G ∣ n
apply Nat.dvd_of_mod_eq_zero
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
⊢ False
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
⊢ n % exponent G = 0
by_contra h
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
⊢ False
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
⊢ False
have h₁ := Nat.pos_of_ne_zero h
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ False
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
⊢ False
have h₂ : n % exponent G < exponent G := Nat.mod_lt _ (exponent_pos_of_exists n hpos hG)
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
h₃ : exponent G ≤ n % exponent G
⊢ False
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ False
have h₃ : exponent G ≤ n % exponent G := by
  apply exponent_min' _ h₁
  simp_rw [← pow_eq_mod_exponent]
  exact hG
no goals
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
h₃ : exponent G ≤ n % exponent G
⊢ False
linarith
no goals
case inl
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
hG : ∀ (g : G), g ^ 0 = 1
⊢ exponent G ∣ 0
exact dvd_zero _
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ (n % exponent G) = 1
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ exponent G ≤ n % exponent G
apply exponent_min' _ h₁
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ n = 1
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ (n % exponent G) = 1
simp_rw [← pow_eq_mod_exponent]
no goals
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ n = 1
exact hG