awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
⊢ ¬IsCyclic (ZMod (4 * n))ˣ
have this : Nat.Coprime 4 n
Tactic: have : Nat.Coprime 4 n := (Nat.prime_two.coprime_iff_not_dvd.mpr h2n).pow_left 2
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this : Nat.Coprime 4 n
⊢ ¬IsCyclic (ZMod (4 * n))ˣ
have inr : ¬(IsCyclic (ZMod 4)ˣ ∧ IsCyclic (ZMod n)ˣ ∧ (Nat.card (ZMod 4)ˣ).Coprime (Nat.card (ZMod n)ˣ))
Tactic: rw [((Units.mapEquiv (chineseRemainder this).toMulEquiv).trans .prodUnits).isCyclic,
    Group.isCyclic_prod_iff]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
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)ˣ)
⊢ False
have this₁ : NeZero n
Tactic: have : NeZero n := ⟨hn0⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
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
⊢ False
have this₁ : Odd (φ n)
Tactic: have : Odd (φ n) := by simpa [show φ 4 = 2 from rfl] using h
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
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)
⊢ False
have this₁ : n = 1 ∨ n = 2
Tactic: rw [Nat.odd_totient_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
⊢ ¬IsCyclic (ZMod (m * n))ˣ
have x : NeZero m
Tactic: have _ : NeZero m := ⟨Nat.ne_of_odd_add hm⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
h : NeZero m
⊢ ¬IsCyclic (ZMod (m * n))ˣ
have x : NeZero n
Tactic: have _ : NeZero n := ⟨Nat.ne_of_odd_add hn⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ ¬IsCyclic (ZMod (m * n))ˣ
have rw : ¬(IsCyclic (ZMod m)ˣ ∧ IsCyclic (ZMod n)ˣ ∧ (Nat.card (ZMod m)ˣ).Coprime (Nat.card (ZMod n)ˣ))
Tactic: rw [e.isCyclic, Group.isCyclic_prod_iff]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
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)ˣ)
⊢ False
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ False
have inl : ∀ (hm : Odd (α := ℕ) 2) (hm1 : Ne (α := ℕ) 2 1) (hmn : Nat.Coprime 2 n), NeZero (R := ℕ) 2 → False
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: m, hm, hm1, hmn, h_1, e, h
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ False
have inr : ∀ (hn : Odd (α := ℕ) 2) (hn1 : Ne (α := ℕ) 2 1) (hmn : m.Coprime 2), NeZero (R := ℕ) 2 → False
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: n, hn, hn1, hmn, h_2, e, h
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
⊢ ¬IsCyclic (ZMod (m * n))ˣ
have have : NeZero m → ¬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
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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))ˣ
⊢ ¬IsCyclic (ZMod (m * n))ˣ
have have₃ : NeZero m → NeZero n → ¬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
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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))ˣ
⊢ ¬IsCyclic (ZMod (m * n))ˣ
have have₅ : NeZero m → NeZero n → ¬(IsCyclic (ZMod m)ˣ ∧ IsCyclic (ZMod n)ˣ ∧ (Nat.card (ZMod m)ˣ).Coprime (Nat.card (ZMod 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
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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)ˣ))
⊢ ¬IsCyclic (ZMod (m * n))ˣ
have have₆ : NeZero m → NeZero n → ∀ (h : (Nat.card (ZMod m)ˣ).Coprime (Nat.card (ZMod n)ˣ)), False
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
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ ¬IsCyclic (ZMod (m * n))ˣ
have have₇ : NeZero m → NeZero n → ∀ (h : m = 2 ∨ n = 2), False
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
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ ¬IsCyclic (ZMod (m * n))ˣ
have inl : NeZero n → ∀ (hm : Odd (α := ℕ) 2) (hm1 : Ne (α := ℕ) 2 1) (hmn : Nat.Coprime 2 n), NeZero (R := ℕ) 2 → False
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
Cleared hypotheses: m, hm, hm1, hmn
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ ¬IsCyclic (ZMod (m * n))ˣ
have inr : NeZero m → ∀ (hn : Odd (α := ℕ) 2) (hn1 : Ne (α := ℕ) 2 1) (hmn : m.Coprime 2), NeZero (R := ℕ) 2 → False
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
Cleared hypotheses: n, hn, hn1, hmn
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
n : ℕ
hn : Odd n
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
have hn0 : n ≠ 0
Tactic: have hn0 : n ≠ 0 := by rintro rfl; exact Nat.not_odd_zero hn
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
hn : Odd n
hn0 : n ≠ 0
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
have inl : ∀ (hn : Odd (α := ℕ) 1) (hn0 : Ne (α := ℕ) 1 0), IsCyclic (ZMod 1)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 = p ^ m
Tactic: obtain rfl | h1 := eq_or_ne n 1
Cleared hypotheses: n, hn, hn0
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
have inr : ∀ (h1 : n ≠ 1), IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
Tactic: obtain rfl | h1 := eq_or_ne n 1
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
hn : Odd (α := ℕ) 1
hn0 : Ne (α := ℕ) 1 0
⊢ IsCyclic (ZMod 1)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 = p ^ m
have inl : ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ 1 = p ^ m
Tactic: simp_rw [isCyclic_units_one, true_iff]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
hn : Odd (α := ℕ) 1
hn0 : Ne (α := ℕ) 1 0
⊢ 1 = HPow.hPow (α := ℕ) (β := ℕ) 3 0
have rw : Eq (α := ℕ) 1 1
Tactic: rw [pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
have inr : ∀ (p : ℕ) (hp : Nat.Prime p) (dvd : p ∣ n), IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
Tactic: have ⟨p, hp, dvd⟩ := n.exists_prime_and_dvd h1
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
have odd : Odd p
Tactic: have odd := hn.of_dvd_nat dvd
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
have pos : ∀ (hnp : n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)),
  IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
Tactic: by_cases hnp : n = p ^ n.factorization p
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
have neg : ∀ (hnp : ¬n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)),
  IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
Tactic: by_cases hnp : n = p ^ n.factorization p
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
have neg : ¬IsCyclic (ZMod n)ˣ
Tactic: refine iff_of_false ?_ (mt ?_ hnp)
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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)ˣ
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m
have neg₁ : (∃ (p : ℕ) (m : ℕ), Nat.Prime p ∧ Odd p ∧ n = p ^ m) → n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: refine iff_of_false ?_ (mt ?_ hnp)
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
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)ˣ
have this : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n
Tactic: have := n.ordProj_dvd p
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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 n)ˣ
have neg : ¬IsCyclic
    (ZMod
        (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) *
          (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ))))ˣ
Tactic: rw [← Nat.mul_div_cancel' this]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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 : ℕ))))ˣ
have neg : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 1
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 ..)
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ ¬IsCyclic
      (ZMod
          (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) *
            (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ))))ˣ
have neg₁ : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 1
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 ..)
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 1
have neg : ∀ (hnp : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1),
  n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: contrapose hnp
Cleared hypotheses: hnp
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
| n
have rw : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [← Nat.div_mul_cancel this, hnp, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have conv_lhs : n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: conv_lhs => rw [← Nat.div_mul_cancel this, hnp, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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 : ℕ)
⊢ n = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have neg : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) =
  HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: conv_lhs => rw [← Nat.div_mul_cancel this, hnp, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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 : ℕ)
⊢ q ^ m = HPow.hPow (β := ℕ) p (((q ^ m).factorization : (a : ℕ) → ℕ) p : ℕ)
have 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 : ℕ)
Tactic: cases (Nat.prime_dvd_prime_iff_eq hp hq).mp (hp.dvd_of_dvd_pow dvd)
Cleared hypotheses: q, hq, hn, hn0, h1, dvd, hnp
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
⊢ 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)
have 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)
Tactic: by_cases h0 : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h0 : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
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)
have 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)
Tactic: rw [h0]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
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)
have 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)
Tactic: by_cases h1 : n = 1
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h1 : n = 1
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
h0 : ¬n = 0
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)
have 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)
Tactic: rw [h1]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
h0 : ¬n = 0
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)
have 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)
Tactic: by_cases h2 : n = 2