awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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).Coprime (orderOf (b ^ k))
⊢ orderOf (ha.unit * b ^ k) = Nat.card (ZMod (p ^ (n + 1)))ˣ

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']

Premises used: ZMod.card_units_eq_totient, Commute.orderOf_mul_eq_mul_orderOf_of_coprime, Nat.totient_prime_pow_succ, Nat.card_eq_fintype_card
-- 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 : (p ^ n).Coprime (p - 1)
⊢ (orderOf ha.unit).Coprime (orderOf (b ^ k))

Tactic:
rw [ha', this]
-- 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 : p.Coprime (p - 1)
⊢ (p ^ n).Coprime (p - 1)

Tactic:
apply Nat.Coprime.pow_left

Premises used: Nat.Coprime.pow_left
-- 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 : p.Coprime (Nat.succ 0)
⊢ p.Coprime (p - 1)

Tactic:
rw [Nat.coprime_self_sub_right hp.pos]

Premises used: Nat.coprime_self_sub_right, Nat.Prime.pos
-- 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
⊢ p.Coprime (Nat.succ 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
⊢ IsCyclic (ZMod (HPow.hPow (α := ℕ) (β := ℕ) 2 0))ˣ ↔ LE.le (α := ℕ) 0 2

Tactic:
simp [isCyclic_units_one]

Premises used: ZMod.isCyclic_units_one
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
⊢ IsCyclic (ZMod (HPow.hPow (α := ℕ) (β := ℕ) 2 1))ˣ ↔ LE.le (α := ℕ) 1 2

Tactic:
simp [isCyclic_units_prime Nat.prime_two]

Premises used: Nat.prime_two, ZMod.isCyclic_units_prime
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
⊢ IsCyclic (ZMod (HPow.hPow (α := ℕ) (β := ℕ) 2 2))ˣ ↔ LE.le (α := ℕ) 2 2

Tactic:
simp [isCyclic_units_four]

Premises used: ZMod.isCyclic_units_four
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n_1 n : ℕ
simp : ¬IsCyclic (ZMod (HPow.hPow (α := ℕ) 2 (n + 3)))ˣ
⊢ IsCyclic (ZMod (HPow.hPow (α := ℕ) 2 (n + 3)))ˣ ↔ n + 3 ≤ 2

Tactic:
simp only [Nat.reduceLeDiff, iff_false]

Premises used: iff_false, Nat.reduceLeDiff
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n_1 n : ℕ
H : IsCyclic (ZMod (HPow.hPow (α := ℕ) 2 (n + 3)))ˣ
apply : IsCyclic (ZMod 8)ˣ
⊢ False

Tactic:
apply not_isCyclic_units_eight

Premises used: ZMod.not_isCyclic_units_eight
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n_1 n : ℕ
H : IsCyclic (ZMod (HPow.hPow (α := ℕ) 2 (n + 3)))ˣ
⊢ 3 ≤ n + 3

Tactic:
lia
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n_1 n : ℕ
H : IsCyclic (ZMod (HPow.hPow (α := ℕ) 2 (n + 3)))ˣ
⊢ HPow.hPow (α := ℕ) (β := ℕ) 2 3 ∣ HPow.hPow (α := ℕ) 2 (n + 3)

Tactic:
have h : 2 ^ 3 ∣ 2 ^ (n + 3) := pow_dvd_pow _ (by lia)
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n_1 n : ℕ
H : IsCyclic (ZMod (HPow.hPow (α := ℕ) 2 (n + 3)))ˣ
h : HPow.hPow (α := ℕ) (β := ℕ) 2 3 ∣ HPow.hPow (α := ℕ) 2 (n + 3)
⊢ IsCyclic (ZMod 8)ˣ

Tactic:
isCyclic_of_surjective _ (unitsMap_surjective h)

Premises used: isCyclic_of_surjective, ZMod.unitsMap_surjective
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n_1 n : ℕ
H : IsCyclic (ZMod (HPow.hPow (α := ℕ) 2 (n + 3)))ˣ
h : HPow.hPow (α := ℕ) (β := ℕ) 2 3 ∣ HPow.hPow (α := ℕ) 2 (n + 3)
⊢ IsCyclic (ZMod 8)ˣ

Tactic:
exact isCyclic_of_surjective _ (unitsMap_surjective h)

Premises used: isCyclic_of_surjective, ZMod.unitsMap_surjective
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
⊢ IsCyclic (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ ↔ n ≤ 2

Tactic:
match n with
  | 0 => simp [isCyclic_units_one]
  | 1 => simp [isCyclic_units_prime Nat.prime_two]
  | 2 => simp [isCyclic_units_four]
  | n + 3 =>
    simp only [Nat.reduceLeDiff, iff_false]
    intro H
    apply not_isCyclic_units_eight
    have h : 2 ^ 3 ∣ 2 ^ (n + 3) := pow_dvd_pow _ (by lia)
    exact isCyclic_of_surjective _ (unitsMap_surjective h)
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
a : ℤ
ha : Odd a
n : ℕ
⊢ orderOf
      (1 +
        HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (n + 2))) (β := ℕ) (↑2 : ZMod (2 ^ (n + 2))) 2 *
          (↑a : ZMod (2 ^ (n + 2)))) =
    HPow.hPow (α := ℕ) 2 n

Tactic:
orderOf_one_add_mul_prime_pow Nat.prime_two 2 two_ne_zero le_rfl a ?_ n

Premises used: le_rfl, Nat.prime_two, two_ne_zero, ZMod.orderOf_one_add_mul_prime_pow, OfNat.ofNat
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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))))
convert! : ¬(↑2 : ℤ) ∣ a
⊢ orderOf (1 + HMul.hMul (α := ZMod (HPow.hPow (α := ℕ) 2 (n + 2))) 4 (↑a : ZMod (2 ^ (n + 2)))) =
    HPow.hPow (α := ℕ) 2 n

Tactic:
convert! orderOf_one_add_mul_prime_pow Nat.prime_two 2 two_ne_zero le_rfl a ?_ n using 1

Premises used: le_rfl, Nat.prime_two, two_ne_zero, ZMod.orderOf_one_add_mul_prime_pow, OfNat.ofNat
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
a : ℤ
ha : Odd a
n : ℕ
⊢ 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:
norm_num
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
a : ℤ
ha : Odd a
n : ℕ
rwa : ∀ (ha : ¬Even a) (n : ℕ), ¬(↑2 : ℤ) ∣ a
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (ha : ¬2 ∣ a) (n : ℕ), ¬(↑2 : ℤ) ∣ a
⊢ ¬(↑2 : ℤ) ∣ a

Tactic:
rwa [← Int.not_even_iff_odd, even_iff_two_dvd] at ha

Premises used: Int.not_even_iff_odd, even_iff_two_dvd
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
⊢ Odd (α := ℤ) 1

Tactic:
simp
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h : 5 = 1 + HMul.hMul (α := ZMod (HPow.hPow (α := ℕ) 2 (n + 2))) 4 (↑1 : ZMod (2 ^ (n + 2)))
⊢ orderOf (G := ZMod (HPow.hPow (α := ℕ) 2 (n + 2))) 5 = HPow.hPow (α := ℕ) 2 n

Tactic:
convert! orderOf_one_add_four_mul 1 (by simp) n

Premises used: ZMod.orderOf_one_add_four_mul, OfNat.ofNat
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
⊢ 5 = 1 + HMul.hMul (α := ZMod (HPow.hPow (α := ℕ) 2 (n + 2))) 4 (↑1 : ZMod (2 ^ (n + 2)))

Tactic:
norm_num
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
inl : IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 0))ˣ ↔ Eq (α := ℕ) 0 0 ∨ Eq (α := ℕ) 0 1
inr : ∀ (hn0 : n ≠ 0), IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1

Tactic:
obtain rfl | hn0 := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
⊢ IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 0))ˣ ↔ Eq (α := ℕ) 0 0 ∨ Eq (α := ℕ) 0 1

Tactic:
simp [isCyclic_units_zero]

Premises used: ZMod.isCyclic_units_zero
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : n ≠ 0
inr : ∀ (hn0 : Ne (α := ℕ) 1 0), IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 1))ˣ ↔ Eq (α := ℕ) 1 0 ∨ Eq (α := ℕ) 1 1
inr₁ : ∀ (hn1 : n ≠ 1), IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1

Tactic:
obtain rfl | hn1 := eq_or_ne n 1

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
hn0 : Ne (α := ℕ) 1 0
⊢ IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 1))ˣ ↔ Eq (α := ℕ) 1 0 ∨ Eq (α := ℕ) 1 1

Tactic:
simp [isCyclic_units_four]

Premises used: ZMod.isCyclic_units_four
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ ¬(n = 0 ∨ n = 1)

Tactic:
simp [hn0, hn1]
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
inr : ¬IsCyclic (ZMod (4 * n))ˣ
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1

Tactic:
refine iff_of_false ?_ (by simp [hn0, hn1])

Premises used: iff_of_false
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
inr : ∀ (n : ℕ) (hn0 : 2 * n ≠ 0) (hn1 : 2 * n ≠ 1), ¬IsCyclic (ZMod (4 * (2 * n)))ˣ
inr₁ : ∀ (h2n : ¬2 ∣ n), ¬IsCyclic (ZMod (4 * n))ˣ
⊢ ¬IsCyclic (ZMod (4 * n))ˣ

Tactic:
obtain ⟨n, rfl⟩ | h2n := em (2 ∣ n)

Premises used: Dvd.dvd, em, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
inr : ¬IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 2 * n))ˣ
⊢ ¬IsCyclic (ZMod (4 * (2 * n)))ˣ

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
⊢ n ≠ 0

Tactic:
simpa using hn0
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
⊢ NeZero n

Tactic:
have : NeZero n := ⟨by simpa using hn0⟩
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
this : NeZero n
⊢ ¬IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 2 * n))ˣ

Tactic:
mt (fun _ ↦ ?_) not_isCyclic_units_eight

Premises used: mt, ZMod.not_isCyclic_units_eight
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
this : NeZero n
inr : IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 2 * n))ˣ → IsCyclic (ZMod 8)ˣ
⊢ ¬IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 2 * n))ˣ

Tactic:
refine mt (fun _ ↦ ?_) not_isCyclic_units_eight

Premises used: mt, ZMod.not_isCyclic_units_eight
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
this : NeZero n
h : IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 2 * n))ˣ
⊢ IsCyclic (ZMod 8)ˣ

Tactic:
isCyclic_of_surjective _ (ZMod.unitsMap_surjective (m := 4 * 2 * n) (dvd_mul_right 8 _))

Premises used: isCyclic_of_surjective, ZMod.unitsMap_surjective, dvd_mul_right, OfNat.ofNat
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
this : NeZero n
h : IsCyclic (ZMod (HMul.hMul (α := ℕ) 4 2 * n))ˣ
⊢ IsCyclic (ZMod 8)ˣ

Tactic:
exact isCyclic_of_surjective _ (ZMod.unitsMap_surjective (m := 4 * 2 * n) (dvd_mul_right 8 _))

Premises used: isCyclic_of_surjective, ZMod.unitsMap_surjective, dvd_mul_right, OfNat.ofNat
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
⊢ Nat.Coprime 4 n

Tactic:
have : Nat.Coprime 4 n := (Nat.prime_two.coprime_iff_not_dvd.mpr h2n).pow_left 2
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this : Nat.Coprime 4 n
inr : ¬(IsCyclic (ZMod 4)ˣ ∧ IsCyclic (ZMod n)ˣ ∧ (Nat.card (ZMod 4)ˣ).Coprime (Nat.card (ZMod n)ˣ))
⊢ ¬IsCyclic (ZMod (4 * n))ˣ

Tactic:
rw [((Units.mapEquiv (chineseRemainder this).toMulEquiv).trans .prodUnits).isCyclic,
    Group.isCyclic_prod_iff]

Premises used: RingEquiv.toMulEquiv, MulEquiv.trans, ZMod.chineseRemainder, Units.mapEquiv, Group.isCyclic_prod_iff, MulEquiv.prodUnits, MulEquiv.isCyclic
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this : Nat.Coprime 4 n
h : (Nat.card (ZMod 4)ˣ).Coprime (Nat.card (ZMod n)ˣ)
⊢ NeZero n

Tactic:
have : NeZero n := ⟨hn0⟩
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this_1 : Nat.Coprime 4 n
h : (Nat.card (ZMod 4)ˣ).Coprime (Nat.card (ZMod n)ˣ)
this : NeZero n
⊢ Odd (φ n)

Tactic:
simpa [show φ 4 = 2 from rfl] using h

Premises used: rfl
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this_1 : Nat.Coprime 4 n
h : (Nat.card (ZMod 4)ˣ).Coprime (Nat.card (ZMod n)ˣ)
this : NeZero n
⊢ Odd (φ n)

Tactic:
have : Odd (φ n) := by simpa [show φ 4 = 2 from rfl] using h
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this_1 : Nat.Coprime 4 n
h : (Nat.card (ZMod 4)ˣ).Coprime (Nat.card (ZMod n)ˣ)
this_2 : NeZero n
this : Odd (φ n)
⊢ n = 1 ∨ n = 2

Tactic:
rw [Nat.odd_totient_iff] at this

Premises used: Nat.odd_totient_iff
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this_1 : Nat.Coprime 4 n
h : (Nat.card (ZMod 4)ˣ).Coprime (Nat.card (ZMod n)ˣ)
this_2 : NeZero n
this : n = 1 ∨ n = 2
⊢ False

Tactic:
lia
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn : Odd n
⊢ IsCyclic (ZMod (2 * n))ˣ ↔ IsCyclic (ZMod n)ˣ

Tactic:
simp [((Units.mapEquiv (chineseRemainder <| Nat.coprime_two_left.mpr hn).toMulEquiv).trans
    .prodUnits).isCyclic, Group.isCyclic_prod_iff, isCyclic_units_two]

Premises used: Iff.mpr, RingEquiv.toMulEquiv, MulEquiv.trans, ZMod.chineseRemainder, Nat.coprime_two_left, Units.mapEquiv, ZMod.isCyclic_units_two, Group.isCyclic_prod_iff, MulEquiv.prodUnits, MulEquiv.isCyclic
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
⊢ NeZero m

Tactic:
have _ : NeZero m := ⟨Nat.ne_of_odd_add hm⟩
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
h : NeZero m
⊢ NeZero n

Tactic:
have _ : NeZero n := ⟨Nat.ne_of_odd_add hn⟩
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
h : NeZero m
h_1 : NeZero n
e : (ZMod (m * n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
rw : ¬(IsCyclic (ZMod m)ˣ ∧ IsCyclic (ZMod n)ˣ ∧ (Nat.card (ZMod m)ˣ).Coprime (Nat.card (ZMod n)ˣ))
⊢ ¬IsCyclic (ZMod (m * n))ˣ

Tactic:
rw [e.isCyclic, Group.isCyclic_prod_iff]

Premises used: Group.isCyclic_prod_iff, MulEquiv.isCyclic
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
h_1 : NeZero m
h_2 : NeZero n
e : (ZMod (m * n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
h : (Nat.card (ZMod m)ˣ).Coprime (Nat.card (ZMod n)ˣ)
⊢ m = 2 ∨ n = 2

Tactic:
simp_rw [Nat.card_eq_fintype_card, card_units_eq_totient,
    Nat.totient_coprime_totient_iff, hm1, hn1, false_or] at h

Premises used: Nat.totient_coprime_totient_iff, ZMod.card_units_eq_totient, false_or, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
h_1 : NeZero m
h_2 : NeZero n
e : (ZMod (m * n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
h : m = 2 ∨ n = 2
inl : ∀ (hm : Odd (α := ℕ) 2) (hm1 : Ne (α := ℕ) 2 1) (hmn : Nat.Coprime 2 n), NeZero (R := ℕ) 2 → False
inr : ∀ (hn : Odd (α := ℕ) 2) (hn1 : Ne (α := ℕ) 2 1) (hmn : m.Coprime 2), NeZero (R := ℕ) 2 → False
⊢ False

Tactic:
rcases h with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn : Odd n
hn1 : n ≠ 1
h : NeZero n
hm : Odd (α := ℕ) 2
hm1 : Ne (α := ℕ) 2 1
hmn : Nat.Coprime 2 n
h_1 : NeZero (R := ℕ) 2
e : (ZMod (2 * n))ˣ ≃* (ZMod 2)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
⊢ False

Tactic:
simp [← Nat.not_even_iff_odd] at hm

Premises used: Nat.not_even_iff_odd
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
m : ℕ
hm : Odd m
hm1 : m ≠ 1
h : NeZero m
hn : Odd (α := ℕ) 2
hn1 : Ne (α := ℕ) 2 1
hmn : m.Coprime 2
h_1 : NeZero (R := ℕ) 2
e : (ZMod (m * 2))ˣ ≃* (ZMod m)ˣ × (ZMod 2)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
⊢ False

Tactic:
simp [← Nat.not_even_iff_odd] at hn

Premises used: Nat.not_even_iff_odd
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
have have₁ have₂ : NeZero m → ¬IsCyclic (ZMod (m * n))ˣ
have₃ have₄ : NeZero m → NeZero n → ¬IsCyclic (ZMod (m * n))ˣ
have₅ :
  NeZero m → NeZero n → ¬(IsCyclic (ZMod m)ˣ ∧ IsCyclic (ZMod n)ˣ ∧ (Nat.card (ZMod m)ˣ).Coprime (Nat.card (ZMod n)ˣ))
have₆ : NeZero m → NeZero n → ∀ (h : (Nat.card (ZMod m)ˣ).Coprime (Nat.card (ZMod n)ˣ)), False
have₇ : NeZero m → NeZero n → ∀ (h : m = 2 ∨ n = 2), False
inl : NeZero n → ∀ (hm : Odd (α := ℕ) 2) (hm1 : Ne (α := ℕ) 2 1) (hmn : Nat.Coprime 2 n), NeZero (R := ℕ) 2 → False
inr inr₁ : NeZero m → ∀ (hn : Odd (α := ℕ) 2) (hn1 : Ne (α := ℕ) 2 1) (hmn : m.Coprime 2), NeZero (R := ℕ) 2 → False
⊢ ¬IsCyclic (ZMod (m * n))ˣ

Tactic:
classical
  have _ : NeZero m := ⟨Nat.ne_of_odd_add hm⟩
  have _ : NeZero n := ⟨Nat.ne_of_odd_add hn⟩
  let e := (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans .prodUnits
  rw [e.isCyclic, Group.isCyclic_prod_iff]
  rintro ⟨-, -, h⟩
  simp_rw [Nat.card_eq_fintype_card, card_units_eq_totient,
    Nat.totient_coprime_totient_iff, hm1, hn1, false_or] at h
  rcases h with (rfl | rfl)
  · simp [← Nat.not_even_iff_odd] at hm
  · simp [← Nat.not_even_iff_odd] at hn

Premises used: Nat.totient_coprime_totient_iff, ZMod.card_units_eq_totient, Nat.not_even_iff_odd, false_or, Group.isCyclic_prod_iff, rfl, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
hn : Odd (α := ℕ) 0
⊢ False

Tactic:
Nat.not_odd_zero hn

Premises used: Nat.not_odd_zero
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
hn : Odd (α := ℕ) 0
⊢ False

Tactic:
exact Nat.not_odd_zero hn

Premises used: Nat.not_odd_zero
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn : Odd n
⊢ n ≠ 0

Tactic:
have hn0 : n ≠ 0 := by rintro rfl; exact Nat.not_odd_zero hn
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn : Odd n
hn0 : n ≠ 0
inl :
  ∀ (hn : Odd (α := ℕ) 1) (hn0 : Ne (α := ℕ) 1 0),
    IsCyclic (ZMod 1)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 = p ^ m
inr : ∀ (h1 : n ≠ 1), IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m

Tactic:
obtain rfl | h1 := eq_or_ne n 1

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
hn : Odd (α := ℕ) 1
hn0 : Ne (α := ℕ) 1 0
inl : ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 = p ^ m
⊢ IsCyclic (ZMod 1)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 = p ^ m

Tactic:
simp_rw [isCyclic_units_one, true_iff]

Premises used: ZMod.isCyclic_units_one, true_iff
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
hn : Odd (α := ℕ) 1
hn0 : Ne (α := ℕ) 1 0
⊢ Odd (α := ℕ) 3

Tactic:
simp [Nat.odd_iff]

Premises used: Nat.odd_iff
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
hn : Odd (α := ℕ) 1
hn0 : Ne (α := ℕ) 1 0
rw rw₁ : Eq (α := ℕ) 1 1
⊢ 1 = HPow.hPow (α := ℕ) (β := ℕ) 3 0

Tactic:
rw [pow_zero]

Premises used: pow_zero
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
hn : Odd (α := ℕ) 1
hn0 : Ne (α := ℕ) 1 0
⊢ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 = p ^ m

Tactic:
exact ⟨3, 0, Nat.prime_three, by simp [Nat.odd_iff], by rw [pow_zero]⟩
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
inr :
  ∀ (p : ℕ) (hp : Nat.Prime p) (dvd : p ∣ n), IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m

Tactic:
have ⟨p, hp, dvd⟩ := n.exists_prime_and_dvd h1
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
⊢ Odd p

Tactic:
have odd := hn.of_dvd_nat dvd
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
pos :
  ∀ (hnp : n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)),
    IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
neg :
  ∀ (hnp : ¬n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)),
    IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m

Tactic:
by_cases hnp : n = p ^ n.factorization p

Premises used: DFunLike.coe, Nat.factorization
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m

Tactic:
hnp ▸ iff_of_true (isCyclic_units_of_prime_pow p hp (odd.ne_two_of_dvd_nat dvd_rfl) _)
      ⟨p, _, hp, odd, rfl⟩

Premises used: Odd.ne_two_of_dvd_nat, Eq.rec, ZMod.isCyclic_units_of_prime_pow, iff_of_true, And.intro, Exists.intro, dvd_rfl, Eq.symm, rfl
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m

Tactic:
exact hnp ▸ iff_of_true (isCyclic_units_of_prime_pow p hp (odd.ne_two_of_dvd_nat dvd_rfl) _)
      ⟨p, _, hp, odd, rfl⟩
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m

Tactic:
iff_of_false ?_ (mt ?_ hnp)

Premises used: mt, iff_of_false
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
neg : ¬IsCyclic (ZMod n)ˣ
neg₁ :
  (∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m) →
    n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m

Tactic:
refine iff_of_false ?_ (mt ?_ hnp)

Premises used: mt, iff_of_false