-- Mathlib/FieldTheory/Finite/Basic.lean
theorem ZMod.eq_one_or_isUnit_sub_one {n p k : ℕ} [Fact p.Prime] (hn : n = p ^ k) (a : ZMod n)
    (ha : (orderOf a).Coprime n) : a = 1 ∨ IsUnit (a - 1)

Proof state:
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
⊢ a = 1 ∨ IsUnit (a - 1)

Tactic:
rcases eq_or_ne n 0 with rfl | hn0

Result:
case inl
p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : 0 = p ^ k
a : ZMod 0
ha : (orderOf a).Coprime 0
⊢ a = 1 ∨ IsUnit (a - 1)

case inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
hn0 : n ≠ 0
⊢ a = 1 ∨ IsUnit (a - 1)

Proof state:
case inr.inr.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
h : ¬IsUnit (↑a - 1)
⊢ orderOf ↑a ∣ n

Tactic:
rw [orderOf_dvd_iff_pow_eq_one, ← Nat.cast_pow, ← Nat.cast_one, ZMod.eq_iff_modEq_nat, hn]

Result:
case inr.inr.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
h : ¬IsUnit (↑a - 1)
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Proof state:
case inr.inr.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
⊢ ¬IsUnit (↑a - 1) → orderOf ↑a = 1

Tactic:
refine fun h ↦ ha.eq_one_of_dvd ?_

Result:
case inr.inr.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
h : ¬IsUnit (↑a - 1)
⊢ orderOf ↑a ∣ n

Proof state:
case inr.inr.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬(a - 1).Coprime (p ^ k)
ha0 : 1 ≤ a
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Tactic:
obtain ⟨b, hb⟩ := not_imp_comm.mp (Nat.Prime.coprime_pow_of_not_dvd Fact.out) h

Result:
case inr.inr.intro.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬(a - 1).Coprime (p ^ k)
ha0 : 1 ≤ a
b : ℕ
hb : a - 1 = p * b
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Proof state:
case inr.inr.intro.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬(a - 1).Coprime (p ^ k)
ha0 : 1 ≤ a
b : ℕ
hb : a = 1 + p * b
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Tactic:
exact hb ▸ pow_pow_modEq_one p k b

Result:
no goals

Proof state:
case inr.inr.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
⊢ ↑a = 1 ∨ IsUnit (↑a - 1)

Tactic:
rw [← orderOf_eq_one_iff, or_iff_not_imp_right]

Result:
case inr.inr.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
⊢ ¬IsUnit (↑a - 1) → orderOf ↑a = 1

Proof state:
case inr.inr.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
h : ¬IsUnit (↑a - 1)
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Tactic:
replace ha0 : 1 ≤ a := by
  contrapose! ha0
  rw [Nat.lt_one_iff.mp ha0, Nat.cast_zero]

Result:
case inr.inr.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬IsUnit (↑a - 1)
ha0 : 1 ≤ a
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Proof state:
case inl
p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : 0 = p ^ k
a : ZMod 0
ha : (orderOf a).Coprime 0
⊢ a = 1 ∨ IsUnit (a - 1)

Tactic:
exact Or.inl (orderOf_eq_one_iff.mp ((orderOf a).coprime_zero_right.mp ha))

Result:
no goals

Proof state:
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬IsUnit (↑a - 1)
ha0 : a < 1
⊢ ↑a = 0

Tactic:
rw [Nat.lt_one_iff.mp ha0, Nat.cast_zero]

Result:
no goals

Proof state:
case inr.inr.intro.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬(a - 1).Coprime (p ^ k)
ha0 : 1 ≤ a
b : ℕ
hb : a - 1 = p * b
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Tactic:
rw [tsub_eq_iff_eq_add_of_le ha0, add_comm] at hb

Result:
case inr.inr.intro.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬(a - 1).Coprime (p ^ k)
ha0 : 1 ≤ a
b : ℕ
hb : a = 1 + p * b
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Proof state:
case inr.inl
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
ha : (orderOf 0).Coprime n
⊢ 0 = 1 ∨ IsUnit (0 - 1)

Tactic:
exact Or.inr (zero_sub (1 : ZMod n) ▸ isUnit_neg_one)

Result:
no goals

Proof state:
case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
hn0 : n ≠ 0
ha0 : a ≠ 0
⊢ a = 1 ∨ IsUnit (a - 1)

Tactic:
have : NeZero n := ⟨hn0⟩

Result:
case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
hn0 : n ≠ 0
ha0 : a ≠ 0
this : NeZero n
⊢ a = 1 ∨ IsUnit (a - 1)

Proof state:
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
h : ¬IsUnit (↑a - 1)
⊢ 1 ≤ a

Tactic:
contrapose! ha0

Result:
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬IsUnit (↑a - 1)
ha0 : a < 1
⊢ ↑a = 0

Proof state:
case inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
hn0 : n ≠ 0
⊢ a = 1 ∨ IsUnit (a - 1)

Tactic:
rcases eq_or_ne a 0 with rfl | ha0

Result:
case inr.inl
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
ha : (orderOf 0).Coprime n
⊢ 0 = 1 ∨ IsUnit (0 - 1)

case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
hn0 : n ≠ 0
ha0 : a ≠ 0
⊢ a = 1 ∨ IsUnit (a - 1)

Proof state:
case inr.inr.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬IsUnit (↑a - 1)
ha0 : 1 ≤ a
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Tactic:
rw [← Nat.cast_one, ← Nat.cast_sub ha0, ZMod.isUnit_iff_coprime, hn] at h

Result:
case inr.inr.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬(a - 1).Coprime (p ^ k)
ha0 : 1 ≤ a
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Proof state:
case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
hn0 : n ≠ 0
ha0 : a ≠ 0
this : NeZero n
⊢ a = 1 ∨ IsUnit (a - 1)

Tactic:
obtain ⟨a, rfl⟩ := ZMod.natCast_zmod_surjective a

Result:
case inr.inr.intro
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
⊢ ↑a = 1 ∨ IsUnit (↑a - 1)