awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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)
⊢ (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
have 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
Tactic: obtain ⟨y, hy⟩ := this (n + 1)
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ (n + 1) =
    1
have 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
Tactic: rw [hy, ← pow_add, ← Nat.cast_pow]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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)
⊢ (↑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
have 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)
Tactic: rw [← pow_succ', ← pow_succ, ← pow_mul, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n : ℕ
⊢ orderOf (1 + HMul.hMul (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) (↑a : ZMod (p ^ (n + 1)))) = p ^ n
have 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))))
Tactic: convert! orderOf_one_add_mul_prime_pow hp 1 one_ne_zero _ a ha n using 1
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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))))
⊢ orderOf (1 + HMul.hMul (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) (↑a : ZMod (p ^ (n + 1)))) = p ^ n
have convert! : HAdd.hAdd (α := ℕ) 1 2 ≤ p * 1
Tactic: convert! orderOf_one_add_mul_prime_pow hp 1 one_ne_zero _ a ha n using 1
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n : ℕ
⊢ 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))))
have 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))))
Tactic: rw [pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n : ℕ
⊢ HAdd.hAdd (α := ℕ) 1 2 ≤ p * 1
have this : 2 ≤ p
Tactic: have := hp.two_le
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ orderOf (HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))) = p ^ n
have h : (↑p : ZMod (p ^ (n + 1))) = HMul.hMul (α := ZMod (p ^ (n + 1))) (↑p : ZMod (p ^ (n + 1))) (↑1 : ZMod (p ^ (n + 1)))
Tactic: convert! orderOf_one_add_mul_prime hp hp2 1 _ n
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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)))
⊢ orderOf (HAdd.hAdd (α := ZMod (p ^ (n + 1))) 1 (↑p : ZMod (p ^ (n + 1)))) = p ^ n
have convert! : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) 1
Tactic: convert! orderOf_one_add_mul_prime hp hp2 1 _ n
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
H : Dvd.dvd (α := ℤ) (↑p : ℤ) 1
⊢ False
have apply : p = 1
Tactic: apply hp.ne_one
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ IsCyclic (ZMod (p ^ n))ˣ
have x : NeZero (p ^ n)
Tactic: have _ : NeZero (p ^ n) := ⟨pow_ne_zero n hp.ne_zero⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
h : NeZero (p ^ n)
⊢ IsCyclic (ZMod (p ^ n))ˣ
have this : Fact (Nat.Prime p)
Tactic: have := Fact.mk hp
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
h : NeZero (p ^ n)
this : Fact (Nat.Prime p)
⊢ IsCyclic (ZMod (p ^ n))ˣ
have zero : NeZero (HPow.hPow (β := ℕ) p 0) → IsCyclic (ZMod (HPow.hPow (β := ℕ) p 0))ˣ
Tactic: rcases n with _ | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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))ˣ
⊢ IsCyclic (ZMod (p ^ n))ˣ
have succ : ∀ (n : ℕ), NeZero (p ^ (n + 1)) → IsCyclic (ZMod (p ^ (n + 1)))ˣ
Tactic: rcases n with _ | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
h : NeZero (p ^ (n + 1))
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
have ha_def : 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
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
have rw : (1 + p).Coprime (p ^ (n + 1))
Tactic: rw [ha_def, ← Nat.cast_one (R := ZMod _), ← Nat.cast_add, ZMod.isUnit_iff_coprime]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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 ^ (n + 1))
have H1 : (1 + p).Coprime p
Tactic: apply Nat.Coprime.pow_right
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
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)))
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
have ha : 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]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
have rw : orderOf a = p ^ n
Tactic: rw [← orderOf_injective _ Units.coeHom_injective ha.unit, Units.coeHom_apply, IsUnit.unit_spec]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
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
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
have ha' : 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
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
have succ : ∀ (c : (ZMod p)ˣ) (hc : orderOf c = Nat.card (ZMod p)ˣ), IsCyclic (ZMod (p ^ (n + 1)))ˣ
Tactic: obtain ⟨c, hc⟩ := isCyclic_iff_exists_orderOf_eq_natCard.mp (isCyclic_units_prime hp)
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
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)ˣ
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
have hc₁ : orderOf c = p - 1
Tactic: rw [Nat.card_eq_fintype_card, ZMod.card_units] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
have succ : ∀ (b : (ZMod (p ^ (n + 1)))ˣ)
  (hc : orderOf (G := (ZMod p)ˣ) ((unitsMap sorry : (a : (ZMod (p ^ n * p))ˣ) → (ZMod p)ˣ) b : (ZMod p)ˣ) = p - 1),
  IsCyclic (ZMod (p ^ (n + 1)))ˣ
Tactic: obtain ⟨(b : (ZMod (p ^ (n + 1)))ˣ), rfl⟩ :=
    ZMod.unitsMap_surjective (Dvd.intro_left (p ^ n) rfl) c
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
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
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
have this₁ : p - 1 ∣ orderOf b
Tactic: have : p - 1 ∣ orderOf b := hc ▸ orderOf_map_dvd _ b
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
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)
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
have this₁ : orderOf (b ^ k) = p - 1
Tactic: have : orderOf (b ^ k) = p - 1 := orderOf_pow_orderOf_div (orderOf_pos b).ne' this
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
have succ : ∃ (g : (ZMod (p ^ (n + 1)))ˣ), orderOf g = Nat.card (ZMod (p ^ (n + 1)))ˣ
Tactic: rw [isCyclic_iff_exists_orderOf_eq_natCard]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ ∃ (g : (ZMod (p ^ (n + 1)))ˣ), orderOf g = Nat.card (ZMod (p ^ (n + 1)))ˣ
have h : orderOf (ha.unit * b ^ k) = Nat.card (ZMod (p ^ (n + 1)))ˣ
Tactic: use ha.unit * b ^ k
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ orderOf (ha.unit * b ^ k) = Nat.card (ZMod (p ^ (n + 1)))ˣ
have h : (orderOf ha.unit).Coprime (orderOf (b ^ k))
Tactic: rw [(Commute.all _ _).orderOf_mul_eq_mul_orderOf_of_coprime, this, Nat.card_eq_fintype_card,
    ZMod.card_units_eq_totient, Nat.totient_prime_pow_succ hp, ← ha']
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ (orderOf ha.unit).Coprime (orderOf (b ^ k))
have h : (p ^ n).Coprime (p - 1)
Tactic: rw [ha', this]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ (p ^ n).Coprime (p - 1)
have h : p.Coprime (p - 1)
Tactic: apply Nat.Coprime.pow_left
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ p.Coprime (p - 1)
have h : p.Coprime (Nat.succ 0)
Tactic: rw [Nat.coprime_self_sub_right hp.pos]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n_1 n : ℕ
⊢ IsCyclic (ZMod (HPow.hPow (α := ℕ) 2 (n + 3)))ˣ ↔ n + 3 ≤ 2
have simp : ¬IsCyclic (ZMod (HPow.hPow (α := ℕ) 2 (n + 3)))ˣ
Tactic: simp only [Nat.reduceLeDiff, iff_false]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n_1 n : ℕ
H : IsCyclic (ZMod (HPow.hPow (α := ℕ) 2 (n + 3)))ˣ
⊢ False
have apply : IsCyclic (ZMod 8)ˣ
Tactic: apply not_isCyclic_units_eight
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
n_1 n : ℕ
H : IsCyclic (ZMod (HPow.hPow (α := ℕ) 2 (n + 3)))ˣ
⊢ IsCyclic (ZMod 8)ˣ
have h : HPow.hPow (α := ℕ) (β := ℕ) 2 3 ∣ HPow.hPow (α := ℕ) 2 (n + 3)
Tactic: have h : 2 ^ 3 ∣ 2 ^ (n + 3) := pow_dvd_pow _ (by lia)
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
a : ℤ
ha : Odd a
n : ℕ
⊢ orderOf (1 + HMul.hMul (α := ZMod (HPow.hPow (α := ℕ) 2 (n + 2))) 4 (↑a : ZMod (2 ^ (n + 2)))) =
    HPow.hPow (α := ℕ) 2 n
have h : orderOf (1 + HMul.hMul (α := ZMod (HPow.hPow (α := ℕ) 2 (n + 2))) 4 (↑a : ZMod (2 ^ (n + 2)))) =
  orderOf
    (1 +
      HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (n + 2))) (β := ℕ) (↑2 : ZMod (2 ^ (n + 2))) 2 *
        (↑a : ZMod (2 ^ (n + 2))))
Tactic: convert! orderOf_one_add_mul_prime_pow Nat.prime_two 2 two_ne_zero le_rfl a ?_ n using 1
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
a : ℤ
ha : Odd a
n : ℕ
h :
  orderOf (1 + HMul.hMul (α := ZMod (HPow.hPow (α := ℕ) 2 (n + 2))) 4 (↑a : ZMod (2 ^ (n + 2)))) =
    orderOf
      (1 +
        HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (n + 2))) (β := ℕ) (↑2 : ZMod (2 ^ (n + 2))) 2 *
          (↑a : ZMod (2 ^ (n + 2))))
⊢ orderOf (1 + HMul.hMul (α := ZMod (HPow.hPow (α := ℕ) 2 (n + 2))) 4 (↑a : ZMod (2 ^ (n + 2)))) =
    HPow.hPow (α := ℕ) 2 n
have convert! : ¬(↑2 : ℤ) ∣ a
Tactic: convert! orderOf_one_add_mul_prime_pow Nat.prime_two 2 two_ne_zero le_rfl a ?_ n using 1
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
a : ℤ
ha : Odd a
n : ℕ
⊢ ¬(↑2 : ℤ) ∣ a
have rwa : ∀ (ha : ¬Even a) (n : ℕ), ¬(↑2 : ℤ) ∣ a
Tactic: rwa [← Int.not_even_iff_odd, even_iff_two_dvd] at ha
Cleared hypotheses: ha, n
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
a : ℤ
ha : Odd a
n : ℕ
rwa : ∀ (ha : ¬Even a) (n : ℕ), ¬(↑2 : ℤ) ∣ a
⊢ ¬(↑2 : ℤ) ∣ a
have rwa₁ : ∀ (ha : ¬2 ∣ a) (n : ℕ), ¬(↑2 : ℤ) ∣ a
Tactic: rwa [← Int.not_even_iff_odd, even_iff_two_dvd] at ha
Cleared hypotheses: ha, n
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
⊢ orderOf (G := ZMod (HPow.hPow (α := ℕ) 2 (n + 2))) 5 = HPow.hPow (α := ℕ) 2 n
have h : 5 = 1 + HMul.hMul (α := ZMod (HPow.hPow (α := ℕ) 2 (n + 2))) 4 (↑1 : ZMod (2 ^ (n + 2)))
Tactic: convert! orderOf_one_add_four_mul 1 (by simp) n
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1
have inl : IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 0))ˣ ↔ Eq (α := ℕ) 0 0 ∨ Eq (α := ℕ) 0 1
Tactic: obtain rfl | hn0 := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
inl : IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 0))ˣ ↔ Eq (α := ℕ) 0 0 ∨ Eq (α := ℕ) 0 1
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1
have inr : ∀ (hn0 : n ≠ 0), IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1
Tactic: obtain rfl | hn0 := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
hn0 : n ≠ 0
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1
have inr : ∀ (hn0 : Ne (α := ℕ) 1 0), IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 1))ˣ ↔ Eq (α := ℕ) 1 0 ∨ Eq (α := ℕ) 1 1
Tactic: obtain rfl | hn1 := eq_or_ne n 1
Cleared hypotheses: n, hn0
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
hn0 : n ≠ 0
inr : ∀ (hn0 : Ne (α := ℕ) 1 0), IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 1))ˣ ↔ Eq (α := ℕ) 1 0 ∨ Eq (α := ℕ) 1 1
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1
have inr₁ : ∀ (hn1 : n ≠ 1), IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1
Tactic: obtain rfl | hn1 := eq_or_ne n 1
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1
have inr : ¬IsCyclic (ZMod (4 * n))ˣ
Tactic: refine iff_of_false ?_ (by simp [hn0, hn1])
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ ¬IsCyclic (ZMod (4 * n))ˣ
have inr : ∀ (n : ℕ) (hn0 : 2 * n ≠ 0) (hn1 : 2 * n ≠ 1), ¬IsCyclic (ZMod (4 * (2 * n)))ˣ
Tactic: obtain ⟨n, rfl⟩ | h2n := em (2 ∣ n)
Cleared hypotheses: n, hn0, hn1
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
inr : ∀ (n : ℕ) (hn0 : 2 * n ≠ 0) (hn1 : 2 * n ≠ 1), ¬IsCyclic (ZMod (4 * (2 * n)))ˣ
⊢ ¬IsCyclic (ZMod (4 * n))ˣ
have inr₁ : ∀ (h2n : ¬2 ∣ n), ¬IsCyclic (ZMod (4 * n))ˣ
Tactic: obtain ⟨n, rfl⟩ | h2n := em (2 ∣ n)
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
⊢ ¬IsCyclic (ZMod (4 * (2 * n)))ˣ
have inr : ¬IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 2 * n))ˣ
Tactic: rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
⊢ ¬IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 2 * n))ˣ
have this : NeZero n
Tactic: have : NeZero n := ⟨by simpa using hn0⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
this : NeZero n
⊢ ¬IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 2 * n))ˣ
have inr : IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 2 * n))ˣ → IsCyclic (ZMod 8)ˣ
Tactic: refine mt (fun _ ↦ ?_) not_isCyclic_units_eight