case inr
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
this : ∀ {n m : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

G : Type u
A : Type v
x y : G
a b : A
n✝ m✝ : ℕ
inst✝ : LeftCancelMonoid G
n m : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
wlog hmn : m ≤ n generalizing m n
case intro
G : Type u
A : Type v
x y : G
a b : A
n m✝ : ℕ
inst✝ : LeftCancelMonoid G
m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
G : Type u
A : Type v
x y : G
a b : A
n✝ m✝ : ℕ
inst✝ : LeftCancelMonoid G
n m : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
case intro
G : Type u
A : Type v
x y : G
a b : A
n m✝ : ℕ
inst✝ : LeftCancelMonoid G
m k : ℕ
hmn : m ≤ m + k
⊢ k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]
case intro
G : Type u
A : Type v
x y : G
a b : A
n m✝ : ℕ
inst✝ : LeftCancelMonoid G
m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
rw [← mul_one (x ^ m), pow_add, mul_left_cancel_iff, pow_eq_one_iff_modEq]
no goals
case intro
G : Type u
A : Type v
x y : G
a b : A
n m✝ : ℕ
inst✝ : LeftCancelMonoid G
m k : ℕ
hmn : m ≤ m + k
⊢ k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]
exact ⟨fun h => Nat.ModEq.add_left _ h, fun h => Nat.ModEq.add_left_cancel' _ h⟩
no goals
case inr
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
this : ∀ {n m : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
rw [eq_comm, ModEq.comm, this (le_of_not_le hmn)]