awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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)
⊢ 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 : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
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)
have 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)
Tactic: rw [h2]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
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)
have 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)
Tactic: by_cases h4 : n = 4
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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)
⊢ 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 : ∀ (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)
Tactic: by_cases h4 : n = 4
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
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)
have 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)
Tactic: rw [h4]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
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)
have 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
Tactic: simp only [h0, h1, h2, h4, false_or, and_or_left, exists_or]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
⊢ 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
have 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
Tactic: rcases (n.even_or_odd).symm with hn | hn
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ 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
have 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
Tactic: rcases (n.even_or_odd).symm with hn | hn
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
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
have 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
Tactic: rw [isCyclic_units_iff_of_odd hn, or_iff_left]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ 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
have neg₁ : ¬∃ (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]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
⊢ (∃ (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
have neg : ∀ (p m : ℕ), n = p ^ m ↔ 1 ≤ m ∧ n = p ^ m
Tactic: congr! with p m
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
p m : ℕ
⊢ n = p ^ m ↔ 1 ≤ m ∧ n = p ^ m
have neg : n = p ^ m → 1 ≤ m
Tactic: rw [and_iff_right_of_imp]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p m : ℕ
h0 : ¬p ^ m = 0
h1 : ¬p ^ m = 1
h2 : ¬p ^ m = 2
h4 : ¬p ^ m = 4
hn : Odd (p ^ m)
⊢ 1 ≤ m
have neg : ∀ (h1 : m < 1), p ^ m = 1
Tactic: contrapose! h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p m : ℕ
h0 : ¬p ^ m = 0
h2 : ¬p ^ m = 2
h4 : ¬p ^ m = 4
hn : Odd (p ^ m)
h1 : m < 1
⊢ p ^ m = 1
have 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
Tactic: cases Nat.lt_one_iff.mp h1
Cleared hypotheses: m, h0, h2, h4, hn, h1
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
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
have 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
Tactic: obtain ⟨n, rfl⟩ := hn.two_dvd
Cleared hypotheses: n, h0, h1, h2, h4, hn
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
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
have 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
Tactic: rcases (n.even_or_odd).symm with hn | hn
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ 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
have 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
Tactic: rcases (n.even_or_odd).symm with hn | hn
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ 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
have 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
Tactic: rw [isCyclic_units_two_mul_iff_of_odd _ hn, isCyclic_units_iff_of_odd hn, or_iff_right]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ 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
have neg₁ : ¬∃ (x : ℕ) (x_1 : ℕ), Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1
Tactic: rw [isCyclic_units_two_mul_iff_of_odd _ hn, isCyclic_units_iff_of_odd hn, or_iff_right]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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 : ℕ), 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
have neg : ∀ (p m : ℕ), n = p ^ m ↔ 1 ≤ m ∧ 2 * n = 2 * p ^ m
Tactic: congr! with p m
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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 : ℕ
⊢ n = p ^ m ↔ 1 ≤ m ∧ 2 * n = 2 * p ^ m
have neg : n = p ^ m → 1 ≤ m
Tactic: rw [Nat.mul_left_cancel_iff zero_lt_two, and_iff_right_of_imp]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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)
⊢ 1 ≤ m
have neg : ∀ (h2 : m < 1), 2 * p ^ m = 2
Tactic: contrapose! h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ 2 * p ^ m = 2
have 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
Tactic: cases Nat.lt_one_iff.mp h2
Cleared hypotheses: m, h0, h1, h4, hn_1, hn, h2
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ 2 * HPow.hPow (β := ℕ) p 0 = 2
have neg : HMul.hMul (α := ℕ) 2 1 = 2
Tactic: rw [pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ 2 * HPow.hPow (β := ℕ) p 0 = 2
have neg₁ : Eq (α := ℕ) 2 2
Tactic: rw [pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
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
⊢ False
have this : Odd (2 * n)
Tactic: have := eq ▸ odd.pow
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨n, rfl⟩ := hn.two_dvd
Cleared hypotheses: n, h0, h1, h2, h4, hn_1, hn
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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)
⊢ 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
have neg : ¬IsCyclic (ZMod (2 * (2 * n)))ˣ
Tactic: apply iff_of_false
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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)))ˣ
⊢ 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
have 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)
Tactic: apply iff_of_false
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
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)
⊢ ¬IsCyclic (ZMod (2 * (2 * n)))ˣ
have neg : ¬(n = 0 ∨ n = 1)
Tactic: rw [← mul_assoc, show 2 * 2 = 4 from rfl, isCyclic_units_four_mul_iff]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
Goal:
n : ℕ
⊢ Eq (α := Ideal ℤ) (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (ZMod n))) (Ideal.span {(↑n : ℤ)})
have h : ∀ (x : ℤ),
  Membership.mem (γ := Ideal ℤ) (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (ZMod n))) x ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑n : ℤ)}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
Goal:
n : ℕ
x : ℤ
⊢ Membership.mem (γ := Ideal ℤ) (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (ZMod n))) x ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑n : ℤ)}) x
have h : Membership.mem (γ := Ideal ℤ) (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (ZMod n))) x ↔ (↑n : ℤ) ∣ x
Tactic: rw [Ideal.mem_span_singleton, RingHom.mem_ker, Int.coe_castRingHom,
    ZMod.intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
Goal:
n : ℕ
x : ℤ
h : Membership.mem (γ := Ideal ℤ) (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (ZMod n))) x ↔ (↑n : ℤ) ∣ x
⊢ Membership.mem (γ := Ideal ℤ) (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (ZMod n))) x ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑n : ℤ)}) x
have h₁ : Eq (α := ZMod n) ((Int.castRingHom (ZMod n) : (a : ℤ) → ZMod n) x : ZMod n) (0 : ZMod n) ↔ (↑n : ℤ) ∣ x
Tactic: rw [Ideal.mem_span_singleton, RingHom.mem_ker, Int.coe_castRingHom,
    ZMod.intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
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
⊢ Membership.mem (γ := Ideal ℤ) (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (ZMod n))) x ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑n : ℤ)}) x
have h₂ : Eq (α := ZMod n) ((fun (x : ℤ) ↦ ((↑x : ZMod n) : ZMod n)) x) 0 ↔ (↑n : ℤ) ∣ x
Tactic: rw [Ideal.mem_span_singleton, RingHom.mem_ker, Int.coe_castRingHom,
    ZMod.intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
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
⊢ Membership.mem (γ := Ideal ℤ) (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (ZMod n))) x ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑n : ℤ)}) x
have h₃ : (↑n : ℤ) ∣ x ↔ (↑n : ℤ) ∣ x
Tactic: rw [Ideal.mem_span_singleton, RingHom.mem_ker, Int.coe_castRingHom,
    ZMod.intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (hypothesis)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
f g : R →+* ZMod n
h : Eq (α := Ideal R) (RingHom.ker f) (RingHom.ker g)
⊢ f = g
have this : RingHom.comp
    (((f.liftOfRightInverse cast sorry :
          { 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 sorry))
    f =
  (↑(Subtype.mk (p := fun (g : R →+* ZMod n) ↦ LE.le (α := Ideal R) (RingHom.ker f) (RingHom.ker g)) g sorry) :
    R →+* ZMod n)
Tactic: have := f.liftOfRightInverse_comp _ (ZMod.ringHom_rightInverse f) ⟨g, le_of_eq h⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (hypothesis)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
f g : R →+* ZMod n
h : Eq (α := Ideal R) (RingHom.ker f) (RingHom.ker g)
this :
  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)
⊢ f = g
have this₁ : RingHom.comp
    (((f.liftOfRightInverse cast sorry :
          { 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 sorry))
    f =
  g
Tactic: rw [Subtype.coe_mk] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
f g : R →+* ZMod n
h : Eq (α := Ideal R) (RingHom.ker f) (RingHom.ker g)
this :
  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 =
    g
⊢ f = g
have rw : f =
  RingHom.comp
    (((f.liftOfRightInverse cast sorry :
          { 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 sorry))
    f
Tactic: rw [← this, RingHom.ext_zmod (f.liftOfRightInverse _ _ ⟨g, _⟩) _, RingHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
f g : R →+* ZMod n
h : Eq (α := Ideal R) (RingHom.ker f) (RingHom.ker g)
this :
  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 =
    g
rw :
  f =
    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
⊢ f = g
have rw₁ : f = RingHom.comp (RingHom.id (ZMod n)) f
Tactic: rw [← this, RingHom.ext_zmod (f.liftOfRightInverse _ _ ⟨g, _⟩) _, RingHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
f g : R →+* ZMod n
h : Eq (α := Ideal R) (RingHom.ker f) (RingHom.ker g)
this :
  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 =
    g
rw :
  f =
    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
rw₁ : f = RingHom.comp (RingHom.id (ZMod n)) f
⊢ f = g
have rw₂ : ZMod n →+* ZMod n
Tactic: rw [← this, RingHom.ext_zmod (f.liftOfRightInverse _ _ ⟨g, _⟩) _, RingHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
f g : R →+* ZMod n
h : Eq (α := Ideal R) (RingHom.ker f) (RingHom.ker g)
this :
  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 =
    g
rw :
  f =
    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
rw₁ : f = RingHom.comp (RingHom.id (ZMod n)) f
rw₂ : ZMod n →+* ZMod n
⊢ f = g
have rw₃ : f = f
Tactic: rw [← this, RingHom.ext_zmod (f.liftOfRightInverse _ _ ⟨g, _⟩) _, RingHom.id_comp]