awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
y : ZMod (p ^ (n + 1 + m))
hy :
  (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ n =
    1 +
      HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) n *
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
        ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
⊢ Ne (α := ℤ) (↑(p ^ (n + m)) : ℤ) 0

Tactic:
simp [hp.ne_zero]

Premises used: Nat.Prime.ne_zero
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
y : ZMod (p ^ (n + 1 + m))
hy :
  (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ n =
    1 +
      HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) n *
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
        ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
refine_2 :
  ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(↑(p ^ (n + m)) : ℤ) : ZMod (p ^ (n + 1 + m)))
        (↑a : ZMod (p ^ (n + 1 + m))) =
      0
refine_2₁ : ¬Eq (α := ZMod (p ^ (n + 1 + m))) (↑((↑(p ^ (n + m)) : ℤ) * a) : ZMod (p ^ (n + 1 + m))) 0
refine_2₂ : ¬(↑(p ^ (n + 1 + m)) : ℤ) ∣ (↑(p ^ (n + m)) : ℤ) * a
refine_2₃ : ¬(↑(p ^ (n + m + 1)) : ℤ) ∣ (↑(p ^ (n + m)) : ℤ) * a
refine_2₄ : ¬(↑(p ^ (n + m) * p) : ℤ) ∣ (↑(p ^ (n + m)) : ℤ) * a
refine_2₅ : ¬HMul.hMul (α := ℤ) (↑(p ^ (n + m)) : ℤ) (↑p : ℤ) ∣ (↑(p ^ (n + m)) : ℤ) * a
refine_2₆ refine_2₇ refine_2₈ refine_2₉ : ¬(↑p : ℤ) ∣ a
⊢ ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(p ^ (n + m)) : ZMod (p ^ (n + 1 + m))) (↑a : ZMod (p ^ (n + 1 + m))) = 0

Tactic:
rwa [← Int.cast_natCast, ← Int.cast_mul, ZMod.intCast_zmod_eq_zero_iff_dvd, add_right_comm,
          pow_succ, Nat.cast_mul, Int.mul_dvd_mul_iff_left (by simp [hp.ne_zero])]

Premises used: Int.cast_natCast, pow_succ, add_right_comm, ZMod.intCast_zmod_eq_zero_iff_dvd, Int.cast_mul, Nat.cast_mul, Int.mul_dvd_mul_iff_left
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
refine_2 :
  ∀ (y : ZMod (p ^ (n + 1 + m)))
    (hy :
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ (n + 1) =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) (n + 1) *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)),
    (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
        p ^ (n + 1) =
      1
⊢ (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ (n + 1) =
    1

Tactic:
obtain ⟨y, hy⟩ := this (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
y : ZMod (p ^ (n + 1 + m))
hy :
  (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ (n + 1) =
    1 +
      HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) (n + 1) *
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
        ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
refine_2 :
  1 +
      (↑(p ^ (n + 1 + m)) : ZMod (p ^ (n + 1 + m))) *
        ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y) =
    1
⊢ (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ (n + 1) =
    1

Tactic:
rw [hy, ← pow_add, ← Nat.cast_pow]

Premises used: pow_add, Nat.cast_pow
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
y : ZMod (p ^ (n + 1 + m))
hy :
  (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ (n + 1) =
    1 +
      HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) (n + 1) *
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
        ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
⊢ 1 +
      (↑(p ^ (n + 1 + m)) : ZMod (p ^ (n + 1 + m))) *
        ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y) =
    1

Tactic:
simp
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this : Fact (Nat.Prime p)
refine_1 :
  HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) (m + 1 + 1) ∣
    HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) (p * m)
⊢ (↑p : ZMod (p ^ (n + 1 + m))) * HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
      (↑p : ZMod (p ^ (n + 1 + m))) ∣
    HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m ^ p

Tactic:
rw [← pow_succ', ← pow_succ, ← pow_mul, mul_comm]

Premises used: pow_succ, pow_mul, mul_comm, pow_succ'
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this : Fact (Nat.Prime p)
⊢ HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) (m + 1 + 1) ∣
    HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) (p * m)

Tactic:
pow_dvd_pow _ hpm

Premises used: pow_dvd_pow
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this : Fact (Nat.Prime p)
⊢ HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) (m + 1 + 1) ∣
    HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) (p * m)

Tactic:
exact pow_dvd_pow _ hpm

Premises used: pow_dvd_pow
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n : ℕ
⊢ orderOf (1 + HPow.hPow (α := ZMod (p ^ (n + m))) (↑p : ZMod (p ^ (n + m))) m * (↑a : ZMod (p ^ (n + m)))) = p ^ n

Tactic:
match n with
  | 0 => rw [← Nat.cast_pow, zero_add m, ZMod.natCast_self]; simp
  | n + 1 =>
    have := Fact.mk hp
    have := exists_one_add_mul_pow_prime_pow_eq
      (R := ZMod (p ^ (n + 1 + m))) (u := p ^ m) (v := p) hp (dvd_pow_self _ hm0) ?_ a
    · apply orderOf_eq_prime_pow
      · obtain ⟨y, hy⟩ := this n
        rw [hy, ← pow_add, add_eq_left, mul_add, ← mul_assoc, ← pow_succ]
        simp_rw [add_right_comm n _ 1, ← Nat.cast_pow, ZMod.natCast_self, zero_mul, add_zero]
        rwa [← Int.cast_natCast, ← Int.cast_mul, ZMod.intCast_zmod_eq_zero_iff_dvd, add_right_comm,
          pow_succ, Nat.cast_mul, Int.mul_dvd_mul_iff_left (by simp [hp.ne_zero])]
      · obtain ⟨y, hy⟩ := this (n + 1)
        rw [hy, ← pow_add, ← Nat.cast_pow]
        simp
    · rw [← pow_succ', ← pow_succ, ← pow_mul, mul_comm]
      exact pow_dvd_pow _ hpm
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n : ℕ
⊢ orderOf (1 + HPow.hPow (α := ZMod (p ^ (n + 1))) (β := ℕ) (↑p : ZMod (p ^ (n + 1))) 1 * (↑a : ZMod (p ^ (n + 1)))) =
    p ^ n

Tactic:
orderOf_one_add_mul_prime_pow hp 1 one_ne_zero _ a ha n

Premises used: ZMod.orderOf_one_add_mul_prime_pow, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n : ℕ
h :
  orderOf (1 + HMul.hMul (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) (↑a : ZMod (p ^ (n + 1)))) =
    orderOf (1 + HPow.hPow (α := ZMod (p ^ (n + 1))) (β := ℕ) (↑p : ZMod (p ^ (n + 1))) 1 * (↑a : ZMod (p ^ (n + 1))))
convert! : HAdd.hAdd (α := ℕ) 1 2 ≤ p * 1
⊢ orderOf (1 + HMul.hMul (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) (↑a : ZMod (p ^ (n + 1)))) = p ^ n

Tactic:
convert! orderOf_one_add_mul_prime_pow hp 1 one_ne_zero _ a ha n using 1

Premises used: ZMod.orderOf_one_add_mul_prime_pow, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n : ℕ
h h₁ :
  orderOf (1 + HMul.hMul (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) (↑a : ZMod (p ^ (n + 1)))) =
    orderOf (1 + HMul.hMul (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) (↑a : ZMod (p ^ (n + 1))))
⊢ orderOf (1 + HMul.hMul (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) (↑a : ZMod (p ^ (n + 1)))) =
    orderOf (1 + HPow.hPow (α := ZMod (p ^ (n + 1))) (β := ℕ) (↑p : ZMod (p ^ (n + 1))) 1 * (↑a : ZMod (p ^ (n + 1))))

Tactic:
rw [pow_one]

Premises used: pow_one
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n : ℕ
⊢ 2 ≤ p

Tactic:
have := hp.two_le
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n : ℕ
this : 2 ≤ p
⊢ HAdd.hAdd (α := ℕ) 1 2 ≤ p * 1

Tactic:
lia
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ orderOf (1 + HMul.hMul (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) (↑1 : ZMod (p ^ (n + 1)))) = p ^ n

Tactic:
orderOf_one_add_mul_prime hp hp2 1 _ n

Premises used: ZMod.orderOf_one_add_mul_prime, OfNat.ofNat
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
h : (↑p : ZMod (p ^ (n + 1))) = HMul.hMul (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) (↑1 : ZMod (p ^ (n + 1)))
convert! : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) 1
⊢ orderOf (HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))) = p ^ n

Tactic:
convert! orderOf_one_add_mul_prime hp hp2 1 _ n

Premises used: ZMod.orderOf_one_add_mul_prime, OfNat.ofNat
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ (↑p : ZMod (p ^ (n + 1))) = HMul.hMul (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) (↑1 : ZMod (p ^ (n + 1)))

Tactic:
simp
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
H : Dvd.dvd (α := ℤ) (↑p : ℤ) 1
apply : p = 1
⊢ False

Tactic:
apply hp.ne_one

Premises used: Nat.Prime.ne_one
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
H : Dvd.dvd (α := ℤ) (↑p : ℤ) 1
⊢ p = 1

Tactic:
simpa using Int.eq_one_of_dvd_one (Int.natCast_nonneg p) H

Premises used: Int.eq_one_of_dvd_one, Int.natCast_nonneg
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ NeZero (p ^ n)

Tactic:
have _ : NeZero (p ^ n) := ⟨pow_ne_zero n hp.ne_zero⟩
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
h : NeZero (p ^ n)
⊢ Fact (Nat.Prime p)

Tactic:
have := Fact.mk hp
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
h : NeZero (p ^ n)
this : Fact (Nat.Prime p)
zero : NeZero (HPow.hPow (β := ℕ) p 0) → IsCyclic (ZMod (HPow.hPow (β := ℕ) p 0))ˣ
succ : ∀ (n : ℕ), NeZero (p ^ (n + 1)) → IsCyclic (ZMod (p ^ (n + 1)))ˣ
⊢ IsCyclic (ZMod (p ^ n))ˣ

Tactic:
rcases n with _ | n
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
h : NeZero (HPow.hPow (β := ℕ) p 0)
⊢ IsCyclic (ZMod 1)ˣ

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
⊢ let a := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)));
  a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))

Tactic:
set a := (1 + p : ZMod (p ^ (n + 1))) with ha_def

Premises used: Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
rw : (1 + p).Coprime (p ^ (n + 1))
⊢ IsUnit a

Tactic:
rw [ha_def, ← Nat.cast_one (R := ZMod _), ← Nat.cast_add, ZMod.isUnit_iff_coprime]

Premises used: ZMod.isUnit_iff_coprime, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
H1 : (1 + p).Coprime p
⊢ (1 + p).Coprime (p ^ (n + 1))

Tactic:
apply Nat.Coprime.pow_right

Premises used: Nat.Coprime.pow_right
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
⊢ (1 + p).Coprime p

Tactic:
simp only [Nat.coprime_add_self_left, Nat.coprime_one_left_eq_true]

Premises used: Nat.coprime_add_self_left, Nat.coprime_one_left_eq_true
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
⊢ IsUnit a

Tactic:
have ha : IsUnit a := by
    rw [ha_def, ← Nat.cast_one (R := ZMod _), ← Nat.cast_add, ZMod.isUnit_iff_coprime]
    apply Nat.Coprime.pow_right
    simp only [Nat.coprime_add_self_left, Nat.coprime_one_left_eq_true]
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha : IsUnit a
rw : orderOf a = p ^ n
⊢ orderOf ha.unit = p ^ n

Tactic:
rw [← orderOf_injective _ Units.coeHom_injective ha.unit, Units.coeHom_apply, IsUnit.unit_spec]

Premises used: Units.coeHom_apply, IsUnit.unit, IsUnit.unit_spec, orderOf_injective, Units.coeHom_injective
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha : IsUnit a
⊢ orderOf a = p ^ n

Tactic:
orderOf_one_add_prime hp hp2 n

Premises used: ZMod.orderOf_one_add_prime
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha : IsUnit a
⊢ orderOf a = p ^ n

Tactic:
exact orderOf_one_add_prime hp hp2 n

Premises used: ZMod.orderOf_one_add_prime
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha : IsUnit a
⊢ orderOf ha.unit = p ^ n

Tactic:
have ha' : orderOf ha.unit = p ^ n := by
    rw [← orderOf_injective _ Units.coeHom_injective ha.unit, Units.coeHom_apply, IsUnit.unit_spec]
    exact orderOf_one_add_prime hp hp2 n
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha : IsUnit a
ha' : orderOf ha.unit = p ^ n
succ : ∀ (c : (ZMod p)ˣ) (hc : orderOf c = Nat.card (ZMod p)ˣ), IsCyclic (ZMod (p ^ (n + 1)))ˣ
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ

Tactic:
obtain ⟨c, hc⟩ := isCyclic_iff_exists_orderOf_eq_natCard.mp (isCyclic_units_prime hp)

Premises used: isCyclic_iff_exists_orderOf_eq_natCard, Iff.mp, ZMod.isCyclic_units_prime
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha : IsUnit a
ha' : orderOf ha.unit = p ^ n
c : (ZMod p)ˣ
hc : orderOf c = Nat.card (ZMod p)ˣ
⊢ orderOf c = p - 1

Tactic:
rw [Nat.card_eq_fintype_card, ZMod.card_units] at hc

Premises used: ZMod.card_units, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha : IsUnit a
ha' : orderOf ha.unit = p ^ n
c : (ZMod p)ˣ
hc : orderOf c = p - 1
succ :
  ∀ (b : (ZMod (p ^ (n + 1)))ˣ)
    (hc : orderOf (G := (ZMod p)ˣ) ((unitsMap ⋯ : (a : (ZMod (p ^ n * p))ˣ) → (ZMod p)ˣ) b : (ZMod p)ˣ) = p - 1),
    IsCyclic (ZMod (p ^ (n + 1)))ˣ
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ

Tactic:
obtain ⟨(b : (ZMod (p ^ (n + 1)))ˣ), rfl⟩ :=
    ZMod.unitsMap_surjective (Dvd.intro_left (p ^ n) rfl) c

Premises used: ZMod.unitsMap_surjective, Dvd.intro_left, ZMod, HPow.hPow, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha : IsUnit a
ha' : orderOf ha.unit = p ^ n
b : (ZMod (p ^ (n + 1)))ˣ
hc : orderOf (G := (ZMod p)ˣ) ((unitsMap ⋯ : (a : (ZMod (p ^ n * p))ˣ) → (ZMod p)ˣ) b : (ZMod p)ˣ) = p - 1
⊢ p - 1 ∣ orderOf b

Tactic:
have : p - 1 ∣ orderOf b := hc ▸ orderOf_map_dvd _ b
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this_1 : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha : IsUnit a
ha' : orderOf ha.unit = p ^ n
b : (ZMod (p ^ (n + 1)))ˣ
hc : orderOf (G := (ZMod p)ˣ) ((unitsMap ⋯ : (a : (ZMod (p ^ n * p))ˣ) → (ZMod p)ˣ) b : (ZMod p)ˣ) = p - 1
this : p - 1 ∣ orderOf b
k : ℕ := orderOf b / (p - 1)
⊢ orderOf (b ^ k) = p - 1

Tactic:
have : orderOf (b ^ k) = p - 1 := orderOf_pow_orderOf_div (orderOf_pos b).ne' this
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this_1 : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha : IsUnit a
ha' : orderOf ha.unit = p ^ n
b : (ZMod (p ^ (n + 1)))ˣ
hc : orderOf (G := (ZMod p)ˣ) ((unitsMap ⋯ : (a : (ZMod (p ^ n * p))ˣ) → (ZMod p)ˣ) b : (ZMod p)ˣ) = p - 1
this_2 : p - 1 ∣ orderOf b
k : ℕ := orderOf b / (p - 1)
this : orderOf (b ^ k) = p - 1
succ : ∃ (g : (ZMod (p ^ (n + 1)))ˣ), orderOf g = Nat.card (ZMod (p ^ (n + 1)))ˣ
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ

Tactic:
rw [isCyclic_iff_exists_orderOf_eq_natCard]

Premises used: isCyclic_iff_exists_orderOf_eq_natCard
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this_1 : Fact (Nat.Prime p)
n : ℕ
h_1 : NeZero (p ^ (n + 1))
a : ZMod (p ^ (n + 1)) := HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha_def : a = HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))
ha : IsUnit a
ha' : orderOf ha.unit = p ^ n
b : (ZMod (p ^ (n + 1)))ˣ
hc : orderOf (G := (ZMod p)ˣ) ((unitsMap ⋯ : (a : (ZMod (p ^ n * p))ˣ) → (ZMod p)ˣ) b : (ZMod p)ˣ) = p - 1
this_2 : p - 1 ∣ orderOf b
k : ℕ := orderOf b / (p - 1)
this : orderOf (b ^ k) = p - 1
h : orderOf (ha.unit * b ^ k) = Nat.card (ZMod (p ^ (n + 1)))ˣ
⊢ ∃ (g : (ZMod (p ^ (n + 1)))ˣ), orderOf g = Nat.card (ZMod (p ^ (n + 1)))ˣ

Tactic:
use ha.unit * b ^ k

Premises used: IsUnit.unit