awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ)
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n

Tactic:
have := n.ordProj_dvd p
-- 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 : ℕ)
this : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n
neg :
  ¬IsCyclic
      (ZMod
          (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) *
            (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ))))ˣ
⊢ ¬IsCyclic (ZMod n)ˣ

Tactic:
rw [← Nat.mul_div_cancel' this]

Premises used: Nat.mul_div_cancel'
-- 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 : ℕ)
this : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n
⊢ ¬IsCyclic
      (ZMod
          (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) *
            (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ))))ˣ

Tactic:
not_isCyclic_units_of_mul_coprime _ _ (hn.of_dvd_nat this) ?_
      (hn.of_dvd_nat (Nat.div_dvd_of_dvd this)) ?_ ((Nat.coprime_ordCompl hp hn0).pow_left ..)

Premises used: ZMod.not_isCyclic_units_of_mul_coprime, Nat.Coprime.pow_left, Odd.of_dvd_nat, Nat.coprime_ordCompl, Nat.div_dvd_of_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
hnp : ¬n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
this : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n
neg : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 1
neg₁ : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 1
⊢ ¬IsCyclic
      (ZMod
          (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) *
            (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ))))ˣ

Tactic:
refine not_isCyclic_units_of_mul_coprime _ _ (hn.of_dvd_nat this) ?_
      (hn.of_dvd_nat (Nat.div_dvd_of_dvd this)) ?_ ((Nat.coprime_ordCompl hp hn0).pow_left ..)

Premises used: ZMod.not_isCyclic_units_of_mul_coprime, Nat.Coprime.pow_left, Odd.of_dvd_nat, Nat.coprime_ordCompl, Nat.div_dvd_of_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
hnp : ¬n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
this : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 1

Tactic:
simpa [(hp.factorization_pos_of_dvd hn0 dvd).ne'] using hp.ne_one

Premises used: Nat.Prime.factorization_pos_of_dvd, LT.lt.ne', Nat.Prime.ne_one
-- 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 : ℕ)
this : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n
neg :
  ∀ (hnp : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1),
    n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 1

Tactic:
contrapose hnp
-- 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
this : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n
hnp : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
rw : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
| n

Tactic:
rw [← Nat.div_mul_cancel this, hnp, one_mul]

Premises used: Nat.div_mul_cancel, one_mul
-- 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
this : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n
hnp : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
conv_lhs : n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
neg :
  HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
conv_lhs => rw [← Nat.div_mul_cancel this, hnp, one_mul]

Premises used: Nat.div_mul_cancel, one_mul
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
odd : Odd p
q m : ℕ
hq : Nat.Prime q
hn : Odd (q ^ m)
hn0 : q ^ m ≠ 0
h1 : q ^ m ≠ 1
dvd : p ∣ q ^ m
hnp : ¬q ^ m = HPow.hPow (β := ℕ) p (((q ^ m).factorization : (a : ℕ) → ℕ) p : ℕ)
neg :
  ∀ (hq : Nat.Prime p) (hn : Odd (p ^ m)) (hn0 : p ^ m ≠ 0) (h1 : p ^ m ≠ 1) (dvd : p ∣ p ^ m)
    (hnp : ¬p ^ m = HPow.hPow (β := ℕ) p (((p ^ m).factorization : (a : ℕ) → ℕ) p : ℕ)),
    p ^ m = HPow.hPow (β := ℕ) p (((p ^ m).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ q ^ m = HPow.hPow (β := ℕ) p (((q ^ m).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
cases (Nat.prime_dvd_prime_iff_eq hp hq).mp (hp.dvd_of_dvd_pow dvd)

Premises used: Nat.Prime.dvd_of_dvd_pow, Nat.prime_dvd_prime_iff_eq, Iff.mp
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
odd : Odd p
m : ℕ
hq : Nat.Prime p
hn : Odd (p ^ m)
hn0 : p ^ m ≠ 0
h1 : p ^ m ≠ 1
dvd : p ∣ p ^ m
hnp : ¬p ^ m = HPow.hPow (β := ℕ) p (((p ^ m).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ p ^ m = HPow.hPow (β := ℕ) p (((p ^ m).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp [hp.factorization_self] at hnp

Premises used: Nat.Prime.factorization_self
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
pos :
  ∀ (h0 : n = 0),
    IsCyclic (ZMod n)ˣ ↔
      n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
neg :
  ∀ (h0 : ¬n = 0),
    IsCyclic (ZMod n)ˣ ↔
      n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
⊢ IsCyclic (ZMod n)ˣ ↔
    n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
by_cases h0 : n = 0
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : n = 0
pos :
  IsCyclic (ZMod 0)ˣ ↔
    Eq (α := ℕ) 0 0 ∨
      Eq (α := ℕ) 0 1 ∨
        Eq (α := ℕ) 0 2 ∨ Eq (α := ℕ) 0 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (0 = p ^ m ∨ 0 = 2 * p ^ m)
⊢ IsCyclic (ZMod n)ˣ ↔
    n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
rw [h0]
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : n = 0
⊢ IsCyclic (ZMod 0)ˣ ↔
    Eq (α := ℕ) 0 0 ∨
      Eq (α := ℕ) 0 1 ∨
        Eq (α := ℕ) 0 2 ∨ Eq (α := ℕ) 0 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (0 = p ^ m ∨ 0 = 2 * p ^ m)

Tactic:
simp [isCyclic_units_zero]

Premises used: ZMod.isCyclic_units_zero
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
pos :
  ∀ (h1 : n = 1),
    IsCyclic (ZMod n)ˣ ↔
      n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
neg :
  ∀ (h1 : ¬n = 1),
    IsCyclic (ZMod n)ˣ ↔
      n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
⊢ IsCyclic (ZMod n)ˣ ↔
    n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
by_cases h1 : n = 1
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
h1 : n = 1
pos :
  IsCyclic (ZMod 1)ˣ ↔
    Eq (α := ℕ) 1 0 ∨
      Eq (α := ℕ) 1 1 ∨
        Eq (α := ℕ) 1 2 ∨ Eq (α := ℕ) 1 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (1 = p ^ m ∨ 1 = 2 * p ^ m)
⊢ IsCyclic (ZMod n)ˣ ↔
    n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
rw [h1]
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ IsCyclic (ZMod 1)ˣ ↔
    Eq (α := ℕ) 1 0 ∨
      Eq (α := ℕ) 1 1 ∨
        Eq (α := ℕ) 1 2 ∨ Eq (α := ℕ) 1 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (1 = p ^ m ∨ 1 = 2 * p ^ m)

Tactic:
simp [isCyclic_units_one]

Premises used: ZMod.isCyclic_units_one
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
pos :
  ∀ (h2 : n = 2),
    IsCyclic (ZMod n)ˣ ↔
      n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
neg :
  ∀ (h2 : ¬n = 2),
    IsCyclic (ZMod n)ˣ ↔
      n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
⊢ IsCyclic (ZMod n)ˣ ↔
    n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
by_cases h2 : n = 2
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : n = 2
pos :
  IsCyclic (ZMod 2)ˣ ↔
    Eq (α := ℕ) 2 0 ∨
      Eq (α := ℕ) 2 1 ∨
        Eq (α := ℕ) 2 2 ∨ Eq (α := ℕ) 2 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (2 = p ^ m ∨ 2 = 2 * p ^ m)
⊢ IsCyclic (ZMod n)ˣ ↔
    n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
rw [h2]
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : n = 2
⊢ IsCyclic (ZMod 2)ˣ ↔
    Eq (α := ℕ) 2 0 ∨
      Eq (α := ℕ) 2 1 ∨
        Eq (α := ℕ) 2 2 ∨ Eq (α := ℕ) 2 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (2 = p ^ m ∨ 2 = 2 * p ^ m)

Tactic:
simp [isCyclic_units_two]

Premises used: ZMod.isCyclic_units_two
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
pos :
  ∀ (h4 : n = 4),
    IsCyclic (ZMod n)ˣ ↔
      n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
neg :
  ∀ (h4 : ¬n = 4),
    IsCyclic (ZMod n)ˣ ↔
      n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
⊢ IsCyclic (ZMod n)ˣ ↔
    n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
by_cases h4 : n = 4
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : n = 4
pos :
  IsCyclic (ZMod 4)ˣ ↔
    Eq (α := ℕ) 4 0 ∨
      Eq (α := ℕ) 4 1 ∨
        Eq (α := ℕ) 4 2 ∨ Eq (α := ℕ) 4 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (4 = p ^ m ∨ 4 = 2 * p ^ m)
⊢ IsCyclic (ZMod n)ˣ ↔
    n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
rw [h4]
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : n = 4
⊢ IsCyclic (ZMod 4)ˣ ↔
    Eq (α := ℕ) 4 0 ∨
      Eq (α := ℕ) 4 1 ∨
        Eq (α := ℕ) 4 2 ∨ Eq (α := ℕ) 4 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (4 = p ^ m ∨ 4 = 2 * p ^ m)

Tactic:
simp [isCyclic_units_four]

Premises used: ZMod.isCyclic_units_four
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
neg :
  IsCyclic (ZMod n)ˣ ↔
    (∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = x ^ x_1) ∨
      ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = 2 * x ^ x_1
⊢ IsCyclic (ZMod n)ˣ ↔
    n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
simp only [h0, h1, h2, h4, false_or, and_or_left, exists_or]

Premises used: and_or_left, exists_or, false_or
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
neg :
  ∀ (hn : Odd n),
    IsCyclic (ZMod n)ˣ ↔
      (∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = x ^ x_1) ∨
        ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = 2 * x ^ x_1
neg₁ :
  ∀ (hn : Even n),
    IsCyclic (ZMod n)ˣ ↔
      (∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = x ^ x_1) ∨
        ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = 2 * x ^ x_1
⊢ IsCyclic (ZMod n)ˣ ↔
    (∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = x ^ x_1) ∨
      ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = 2 * x ^ x_1

Tactic:
rcases (n.even_or_odd).symm with hn | hn

Premises used: Or.symm, Nat.even_or_odd
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
neg :
  (∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m) ↔
    ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = x ^ x_1
neg₁ : ¬∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = 2 * x ^ x_1
⊢ IsCyclic (ZMod n)ˣ ↔
    (∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = x ^ x_1) ∨
      ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = 2 * x ^ x_1

Tactic:
rw [isCyclic_units_iff_of_odd hn, or_iff_left]

Premises used: ZMod.isCyclic_units_iff_of_odd, or_iff_left
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
neg : ∀ (p m : ℕ), n = p ^ m ↔ 1 ≤ m ∧ n = p ^ m
⊢ (∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m) ↔
    ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = x ^ x_1

Tactic:
congr! with p m
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
p m : ℕ
neg : n = p ^ m → 1 ≤ m
⊢ n = p ^ m ↔ 1 ≤ m ∧ n = p ^ m

Tactic:
rw [and_iff_right_of_imp]

Premises used: and_iff_right_of_imp
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p m : ℕ
h0 : ¬p ^ m = 0
h1 : ¬p ^ m = 1
h2 : ¬p ^ m = 2
h4 : ¬p ^ m = 4
hn : Odd (p ^ m)
neg : ∀ (h1 : m < 1), p ^ m = 1
⊢ 1 ≤ m

Tactic:
contrapose! h1
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p m : ℕ
h0 : ¬p ^ m = 0
h2 : ¬p ^ m = 2
h4 : ¬p ^ m = 4
hn : Odd (p ^ m)
h1 : m < 1
neg :
  ∀ (h0 : ¬HPow.hPow (β := ℕ) p 0 = 0) (h2 : ¬HPow.hPow (β := ℕ) p 0 = 2) (h4 : ¬HPow.hPow (β := ℕ) p 0 = 4)
    (hn : Odd (HPow.hPow (β := ℕ) p 0)) (h1 : LT.lt (α := ℕ) 0 1), HPow.hPow (β := ℕ) p 0 = 1
⊢ p ^ m = 1

Tactic:
cases Nat.lt_one_iff.mp h1

Premises used: Nat.lt_one_iff, Iff.mp
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
h0 : ¬HPow.hPow (β := ℕ) p 0 = 0
h2 : ¬HPow.hPow (β := ℕ) p 0 = 2
h4 : ¬HPow.hPow (β := ℕ) p 0 = 4
hn : Odd (HPow.hPow (β := ℕ) p 0)
h1 : LT.lt (α := ℕ) 0 1
⊢ HPow.hPow (β := ℕ) p 0 = 1

Tactic:
apply pow_zero

Premises used: pow_zero
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p m : ℕ
h0 : ¬2 * p ^ m = 0
h1 : ¬2 * p ^ m = 1
h2 : ¬2 * p ^ m = 2
h4 : ¬2 * p ^ m = 4
hn : Odd (2 * p ^ m)
⊢ False

Tactic:
simp [← Nat.not_even_iff_odd] at hn

Premises used: Nat.not_even_iff_odd
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Even n
neg :
  ∀ (n : ℕ) (h0 : ¬2 * n = 0) (h1 : ¬2 * n = 1) (h2 : ¬2 * n = 2) (h4 : ¬2 * n = 4) (hn : Even (2 * n)),
    IsCyclic (ZMod (2 * n))ˣ ↔
      (∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1) ∨
        ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1
⊢ IsCyclic (ZMod n)ˣ ↔
    (∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = x ^ x_1) ∨
      ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = 2 * x ^ x_1

Tactic:
obtain ⟨n, rfl⟩ := hn.two_dvd

Premises used: Even.two_dvd, rfl
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn : Even (2 * n)
neg :
  ∀ (hn : Odd n),
    IsCyclic (ZMod (2 * n))ˣ ↔
      (∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1) ∨
        ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1
neg₁ :
  ∀ (hn : Even n),
    IsCyclic (ZMod (2 * n))ˣ ↔
      (∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1) ∨
        ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1
⊢ IsCyclic (ZMod (2 * n))ˣ ↔
    (∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1) ∨
      ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1

Tactic:
rcases (n.even_or_odd).symm with hn | hn

Premises used: Or.symm, Nat.even_or_odd
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn_1 : Even (2 * n)
hn : Odd n
neg :
  (∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m) ↔
    ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1
neg₁ : ¬∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1
⊢ IsCyclic (ZMod (2 * n))ˣ ↔
    (∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1) ∨
      ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1

Tactic:
rw [isCyclic_units_two_mul_iff_of_odd _ hn, isCyclic_units_iff_of_odd hn, or_iff_right]

Premises used: ZMod.isCyclic_units_iff_of_odd, ZMod.isCyclic_units_two_mul_iff_of_odd, or_iff_right
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn_1 : Even (2 * n)
hn : Odd n
neg : ∀ (p m : ℕ), n = p ^ m ↔ 1 ≤ m ∧ 2 * n = 2 * p ^ m
⊢ (∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m) ↔
    ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1

Tactic:
congr! with p m
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn_1 : Even (2 * n)
hn : Odd n
p m : ℕ
neg : n = p ^ m → 1 ≤ m
⊢ n = p ^ m ↔ 1 ≤ m ∧ 2 * n = 2 * p ^ m

Tactic:
rw [Nat.mul_left_cancel_iff zero_lt_two, and_iff_right_of_imp]

Premises used: Nat.mul_left_cancel_iff, zero_lt_two, and_iff_right_of_imp
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p m : ℕ
h0 : ¬2 * p ^ m = 0
h1 : ¬2 * p ^ m = 1
h2 : ¬2 * p ^ m = 2
h4 : ¬2 * p ^ m = 4
hn_1 : Even (2 * p ^ m)
hn : Odd (p ^ m)
neg : ∀ (h2 : m < 1), 2 * p ^ m = 2
⊢ 1 ≤ m

Tactic:
contrapose! h2
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p m : ℕ
h0 : ¬2 * p ^ m = 0
h1 : ¬2 * p ^ m = 1
h4 : ¬2 * p ^ m = 4
hn_1 : Even (2 * p ^ m)
hn : Odd (p ^ m)
h2 : m < 1
neg :
  ∀ (h0 : ¬2 * HPow.hPow (β := ℕ) p 0 = 0) (h1 : ¬2 * HPow.hPow (β := ℕ) p 0 = 1) (h4 : ¬2 * HPow.hPow (β := ℕ) p 0 = 4)
    (hn : Even (2 * HPow.hPow (β := ℕ) p 0)) (hn : Odd (HPow.hPow (β := ℕ) p 0)) (h2 : LT.lt (α := ℕ) 0 1),
    2 * HPow.hPow (β := ℕ) p 0 = 2
⊢ 2 * p ^ m = 2

Tactic:
cases Nat.lt_one_iff.mp h2

Premises used: Nat.lt_one_iff, Iff.mp
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
h0 : ¬2 * HPow.hPow (β := ℕ) p 0 = 0
h1 : ¬2 * HPow.hPow (β := ℕ) p 0 = 1
h4 : ¬2 * HPow.hPow (β := ℕ) p 0 = 4
hn_1 : Even (2 * HPow.hPow (β := ℕ) p 0)
hn : Odd (HPow.hPow (β := ℕ) p 0)
h2 : LT.lt (α := ℕ) 0 1
neg : HMul.hMul (α := ℕ) 2 1 = 2
neg₁ neg₂ : Eq (α := ℕ) 2 2
⊢ 2 * HPow.hPow (β := ℕ) p 0 = 2

Tactic:
rw [pow_zero, mul_one]

Premises used: pow_zero, mul_one
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn_1 : Even (2 * n)
hn : Odd n
p m : ℕ
odd : Odd p
eq : 2 * n = p ^ m
⊢ Odd (2 * n)

Tactic:
have := eq ▸ odd.pow
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn_1 : Even (2 * n)
hn : Odd n
p m : ℕ
odd : Odd p
eq : 2 * n = p ^ m
this : Odd (2 * n)
⊢ False

Tactic:
simp [← Nat.not_even_iff_odd] at this

Premises used: Nat.not_even_iff_odd
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn_1 : Even (2 * n)
hn : Even n
neg :
  ∀ (n : ℕ) (h0 : ¬2 * (2 * n) = 0) (h1 : ¬2 * (2 * n) = 1) (h2 : ¬2 * (2 * n) = 2) (h4 : ¬2 * (2 * n) = 4)
    (hn : Even (2 * (2 * n))) (hn : Even (2 * n)),
    IsCyclic (ZMod (2 * (2 * n)))ˣ ↔
      (∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * (2 * n) = x ^ x_1) ∨
        ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * (2 * n) = 2 * x ^ x_1
⊢ IsCyclic (ZMod (2 * n))ˣ ↔
    (∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1) ∨
      ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1

Tactic:
obtain ⟨n, rfl⟩ := hn.two_dvd

Premises used: Even.two_dvd, rfl
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬2 * (2 * n) = 0
h1 : ¬2 * (2 * n) = 1
h2 : ¬2 * (2 * n) = 2
h4 : ¬2 * (2 * n) = 4
hn_1 : Even (2 * (2 * n))
hn : Even (2 * n)
neg : ¬IsCyclic (ZMod (2 * (2 * n)))ˣ
neg₁ :
  ¬((∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * (2 * n) = x ^ x_1) ∨
      ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * (2 * n) = 2 * x ^ x_1)
⊢ IsCyclic (ZMod (2 * (2 * n)))ˣ ↔
    (∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * (2 * n) = x ^ x_1) ∨
      ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * (2 * n) = 2 * x ^ x_1

Tactic:
apply iff_of_false

Premises used: iff_of_false
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬2 * (2 * n) = 0
h1 : ¬2 * (2 * n) = 1
h2 : ¬2 * (2 * n) = 2
h4 : ¬2 * (2 * n) = 4
hn_1 : Even (2 * (2 * n))
hn : Even (2 * n)
neg : ¬(n = 0 ∨ n = 1)
⊢ ¬IsCyclic (ZMod (2 * (2 * n)))ˣ

Tactic:
rw [← mul_assoc, show 2 * 2 = 4 from rfl, isCyclic_units_four_mul_iff]

Premises used: mul_assoc, ZMod.isCyclic_units_four_mul_iff, rfl
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬2 * (2 * n) = 0
h1 : ¬2 * (2 * n) = 1
h2 : ¬2 * (2 * n) = 2
h4 : ¬2 * (2 * n) = 4
hn_1 : Even (2 * (2 * n))
hn : Even (2 * n)
⊢ ¬(n = 0 ∨ n = 1)

Tactic:
lia
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
n : ℕ
h0 : ¬2 * (2 * n) = 0
h1 : ¬2 * (2 * n) = 1
h2 : ¬2 * (2 * n) = 2
h4 : ¬2 * (2 * n) = 4
hn_1 : Even (2 * (2 * n))
hn : Even (2 * n)
⊢ ¬((∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * (2 * n) = x ^ x_1) ∨
      ∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * (2 * n) = 2 * x ^ x_1)

Tactic:
grind
-- Module: Mathlib.RingTheory.ZMod
Goal:
n : ℕ
h :
  ∀ (x : ℤ),
    Membership.mem (γ := Ideal ℤ) (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (ZMod n))) x ↔
      Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑n : ℤ)}) x
⊢ Eq (α := Ideal ℤ) (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (ZMod n))) (Ideal.span {(↑n : ℤ)})

Tactic:
ext
-- Module: Mathlib.RingTheory.ZMod
Goal:
n : ℕ
x : ℤ
h : Membership.mem (γ := Ideal ℤ) (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (ZMod n))) x ↔ (↑n : ℤ) ∣ x
h₁ : Eq (α := ZMod n) ((Int.castRingHom (ZMod n) : (a : ℤ) → ZMod n) x : ZMod n) (0 : ZMod n) ↔ (↑n : ℤ) ∣ x
h₂ : Eq (α := ZMod n) ((fun (x : ℤ) ↦ ((↑x : ZMod n) : ZMod n)) x) 0 ↔ (↑n : ℤ) ∣ x
h₃ h₄ : (↑n : ℤ) ∣ x ↔ (↑n : ℤ) ∣ x
⊢ Membership.mem (γ := Ideal ℤ) (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (ZMod n))) x ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑n : ℤ)}) x

Tactic:
rw [Ideal.mem_span_singleton, RingHom.mem_ker, Int.coe_castRingHom,
    ZMod.intCast_zmod_eq_zero_iff_dvd]

Premises used: Int.coe_castRingHom, RingHom.mem_ker, ZMod.intCast_zmod_eq_zero_iff_dvd, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.ZMod
Goal:
n : ℕ
R : Type u_1
inst : Ring R
f g : R →+* ZMod n
h : Eq (α := Ideal R) (RingHom.ker f) (RingHom.ker g)
⊢ RingHom.comp
      (((f.liftOfRightInverse cast ⋯ :
            { g : R →+* ZMod n // LE.le (α := Ideal R) (RingHom.ker f) (RingHom.ker g) } ≃ (ZMod n →+* ZMod n)) :
          (a : { g : R →+* ZMod n // RingHom.ker f ≤ RingHom.ker g }) → ZMod n →+* ZMod n)
        (Subtype.mk (p := fun (g : R →+* ZMod n) ↦ LE.le (α := Ideal R) (RingHom.ker f) (RingHom.ker g)) g ⋯))
      f =
    (↑(Subtype.mk (p := fun (g : R →+* ZMod n) ↦ LE.le (α := Ideal R) (RingHom.ker f) (RingHom.ker g)) g ⋯) :
      R →+* ZMod n)

Tactic:
have := f.liftOfRightInverse_comp _ (ZMod.ringHom_rightInverse f) ⟨g, le_of_eq h⟩