case pos
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : coprime n (orderOf x)
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x

case neg
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : coprime n (orderOf x)
h0 : ¬orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : coprime n (orderOf x)
⊢ ∃ m, (x ^ n) ^ m = x
by_cases h0 : orderOf x = 0
case pos
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : coprime n (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x

case neg
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : coprime n (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x
case neg
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : coprime n (orderOf x)
h0 : ¬orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x
by_cases h1 : orderOf x = 1
case neg.intro
G : Type u
A : Type v
x y : G
a b : A
n m✝ : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h✝ : coprime n (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x
case neg
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : coprime n (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x
obtain ⟨m, h⟩ := exists_mul_emod_eq_one_of_coprime h (one_lt_iff_ne_zero_and_ne_one.mpr ⟨h0, h1⟩)
no goals
case neg.intro
G : Type u
A : Type v
x y : G
a b : A
n m✝ : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h✝ : coprime n (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x
exact ⟨m, by rw [← pow_mul, pow_eq_mod_orderOf, h, pow_one]⟩
case pos
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : n = 1
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x
case pos
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : coprime n (orderOf x)
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x
rw [h0, coprime_zero_right] at h
no goals
case pos
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : n = 1
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x
exact ⟨1, by rw [h, pow_one, pow_one]⟩
no goals
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : n = 1
h0 : orderOf x = 0
⊢ (x ^ n) ^ 1 = x
rw [h, pow_one, pow_one]
no goals
case pos
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : coprime n (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x
exact ⟨0, by rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]⟩
no goals
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : coprime n (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ (x ^ n) ^ 0 = x
rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]
no goals
G : Type u
A : Type v
x y : G
a b : A
n m✝ : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h✝ : coprime n (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ (x ^ n) ^ m = x
rw [← pow_mul, pow_eq_mod_orderOf, h, pow_one]