awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ inv_fun (to_fun x) = x
have dsimp : (if m * n = 0 then
    if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x.cast)
    else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x.cast)
  else (↑(↑(Nat.chineseRemainder h (val (n := m) x.cast.1) (val (n := n) x.cast.2)) : ℕ) : ZMod (m * n))) =
  x
Tactic: dsimp only [to_fun, inv_fun, ZMod.castHom_apply]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
x : ZMod (m * n)
| x
have rw : (↑x.val : ZMod (m * n))
Tactic: rw [← ZMod.natCast_zmod_val x]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ (if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x.cast)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x.cast)
    else (↑(↑(Nat.chineseRemainder h (val (n := m) x.cast.1) (val (n := n) x.cast.2)) : ℕ) : ZMod (m * n))) =
    x
have conv_rhs : Eq (α := ZMod (m * n))
  (if m * n = 0 then
    if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x.cast)
    else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x.cast)
  else (↑(↑(Nat.chineseRemainder h (val (n := m) x.cast.1) (val (n := n) x.cast.2)) : ℕ) : ZMod (m * n)))
  (↑x.val : ZMod (m * n))
Tactic: conv_rhs => rw [← ZMod.natCast_zmod_val x]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ Eq (α := ZMod (m * n))
    (if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x.cast)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x.cast)
    else (↑(↑(Nat.chineseRemainder h (val (n := m) x.cast.1) (val (n := n) x.cast.2)) : ℕ) : ZMod (m * n)))
    (↑x.val : ZMod (m * n))
have rw : (↑(Nat.chineseRemainder h (val (n := m) x.cast) (val (n := n) x.cast)) : ℕ) ≡ x.val [MOD m] ∧
  (↑(Nat.chineseRemainder h (val (n := m) x.cast) (val (n := n) x.cast)) : ℕ) ≡ x.val [MOD n]
Tactic: rw [if_neg hmn0, ZMod.natCast_eq_natCast_iff, ← Nat.modEq_and_modEq_iff_modEq_mul h,
          Prod.fst_zmod_cast, Prod.snd_zmod_cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ (↑(Nat.chineseRemainder h (val (n := m) x.cast) (val (n := n) x.cast)) : ℕ) ≡ x.val [MOD m] ∧
    (↑(Nat.chineseRemainder h (val (n := m) x.cast) (val (n := n) x.cast)) : ℕ) ≡ x.val [MOD n]
have refine_1 : val (n := m) x.cast ≡ x.val [MOD m]
Tactic: refine
          ⟨(Nat.chineseRemainder h (cast x : ZMod m).val (cast x : ZMod n).val).2.left.trans ?_,
            (Nat.chineseRemainder h (cast x : ZMod m).val (cast x : ZMod n).val).2.right.trans ?_⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
x : ZMod (m * n)
refine_1 : val (n := m) x.cast ≡ x.val [MOD m]
⊢ (↑(Nat.chineseRemainder h (val (n := m) x.cast) (val (n := n) x.cast)) : ℕ) ≡ x.val [MOD m] ∧
    (↑(Nat.chineseRemainder h (val (n := m) x.cast) (val (n := n) x.cast)) : ℕ) ≡ x.val [MOD n]
have refine_2 : val (n := n) x.cast ≡ x.val [MOD n]
Tactic: refine
          ⟨(Nat.chineseRemainder h (cast x : ZMod m).val (cast x : ZMod n).val).2.left.trans ?_,
            (Nat.chineseRemainder h (cast x : ZMod m).val (cast x : ZMod n).val).2.right.trans ?_⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ val (n := m) x.cast ≡ x.val [MOD m]
have refine_1 : Eq (α := ZMod m) (↑(val (n := m) x.cast) : ZMod m) (↑x.val : ZMod m)
Tactic: rw [← ZMod.natCast_eq_natCast_iff, ZMod.natCast_zmod_val, ZMod.natCast_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
x : ZMod (m * n)
refine_1 : Eq (α := ZMod m) (↑(val (n := m) x.cast) : ZMod m) (↑x.val : ZMod m)
⊢ val (n := m) x.cast ≡ x.val [MOD m]
have refine_1₁ : Eq (α := ZMod m) x.cast (↑x.val : ZMod m)
Tactic: rw [← ZMod.natCast_eq_natCast_iff, ZMod.natCast_zmod_val, ZMod.natCast_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
x : ZMod (m * n)
refine_1 : Eq (α := ZMod m) (↑(val (n := m) x.cast) : ZMod m) (↑x.val : ZMod m)
refine_1₁ : Eq (α := ZMod m) x.cast (↑x.val : ZMod m)
⊢ val (n := m) x.cast ≡ x.val [MOD m]
have refine_1₂ : Eq (α := ZMod m) x.cast x.cast
Tactic: rw [← ZMod.natCast_eq_natCast_iff, ZMod.natCast_zmod_val, ZMod.natCast_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ val (n := n) x.cast ≡ x.val [MOD n]
have refine_2 : Eq (α := ZMod n) (↑(val (n := n) x.cast) : ZMod n) (↑x.val : ZMod n)
Tactic: rw [← ZMod.natCast_eq_natCast_iff, ZMod.natCast_zmod_val, ZMod.natCast_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
x : ZMod (m * n)
refine_2 : Eq (α := ZMod n) (↑(val (n := n) x.cast) : ZMod n) (↑x.val : ZMod n)
⊢ val (n := n) x.cast ≡ x.val [MOD n]
have refine_2₁ : Eq (α := ZMod n) x.cast (↑x.val : ZMod n)
Tactic: rw [← ZMod.natCast_eq_natCast_iff, ZMod.natCast_zmod_val, ZMod.natCast_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
x : ZMod (m * n)
refine_2 : Eq (α := ZMod n) (↑(val (n := n) x.cast) : ZMod n) (↑x.val : ZMod n)
refine_2₁ : Eq (α := ZMod n) x.cast (↑x.val : ZMod n)
⊢ val (n := n) x.cast ≡ x.val [MOD n]
have refine_2₂ : Eq (α := ZMod n) x.cast x.cast
Tactic: rw [← ZMod.natCast_eq_natCast_iff, ZMod.natCast_zmod_val, ZMod.natCast_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
have left_inv : LeftInverse inv_fun to_fun
Tactic: have left_inv : Function.LeftInverse inv_fun to_fun := by
        intro x
        dsimp only [to_fun, inv_fun, ZMod.castHom_apply]
        conv_rhs => rw [← ZMod.natCast_zmod_val x]
        rw [if_neg hmn0, ZMod.natCast_eq_natCast_iff, ← Nat.modEq_and_modEq_iff_modEq_mul h,
          Prod.fst_zmod_cast, Prod.snd_zmod_cast]
        refine
          ⟨(Nat.chineseRemainder h (cast x : ZMod m).val (cast x : ZMod n).val).2.left.trans ?_,
            (Nat.chineseRemainder h (cast x : ZMod m).val (cast x : ZMod n).val).2.right.trans ?_⟩
        · rw [← ZMod.natCast_eq_natCast_iff, ZMod.natCast_zmod_val, ZMod.natCast_val]
        · rw [← ZMod.natCast_eq_natCast_iff, ZMod.natCast_zmod_val, ZMod.natCast_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
⊢ Subsingleton (ZMod n) ↔ n = 1
have mp : Subsingleton (ZMod n) → n = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
mp : Subsingleton (ZMod n) → n = 1
⊢ Subsingleton (ZMod n) ↔ n = 1
have mpr : n = 1 → Subsingleton (ZMod n)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
⊢ Subsingleton (ZMod n) → n = 1
have mp : Subsingleton (ZMod 0) → Eq (α := ℕ) 0 1
Tactic: obtain (_ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
mp : Subsingleton (ZMod 0) → Eq (α := ℕ) 0 1
⊢ Subsingleton (ZMod n) → n = 1
have mp₁ : Subsingleton (ZMod (HAdd.hAdd (α := ℕ) 0 1)) → HAdd.hAdd (α := ℕ) 0 1 = 1
Tactic: obtain (_ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
mp : Subsingleton (ZMod 0) → Eq (α := ℕ) 0 1
mp₁ : Subsingleton (ZMod (HAdd.hAdd (α := ℕ) 0 1)) → HAdd.hAdd (α := ℕ) 0 1 = 1
⊢ Subsingleton (ZMod n) → n = 1
have mp₂ : ∀ (n : ℕ), Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1
Tactic: obtain (_ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
⊢ Nontrivial (ZMod n) ↔ n ≠ 1
have rw : ¬Subsingleton (ZMod n) ↔ n ≠ 1
Tactic: rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
rw : ¬Subsingleton (ZMod n) ↔ n ≠ 1
⊢ Nontrivial (ZMod n) ↔ n ≠ 1
have rw₁ : ¬n = 1 ↔ n ≠ 1
Tactic: rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
hn : Odd n
a : ZMod n
⊢ a + a = 0 ↔ a = 0
have rw : ∀ (hn : Nat.Coprime 2 n) {a : ZMod n}, a + a = 0 ↔ a = 0
Tactic: rw [Nat.odd_iff, ← Nat.two_dvd_ne_zero, ← Nat.prime_two.coprime_iff_not_dvd] at hn
Cleared hypotheses: hn, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
⊢ a + a = 0 ↔ a = 0
have rw : a * 2 = 0 ↔ a = 0
Tactic: rw [← mul_two, ← @Nat.cast_two (ZMod n), ← ZMod.coe_unitOfCoprime 2 hn, Units.mul_left_eq_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
rw : a * 2 = 0 ↔ a = 0
⊢ a + a = 0 ↔ a = 0
have rw₁ : a * (↑2 : ZMod n) = 0 ↔ a = 0
Tactic: rw [← mul_two, ← @Nat.cast_two (ZMod n), ← ZMod.coe_unitOfCoprime 2 hn, Units.mul_left_eq_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
rw : a * 2 = 0 ↔ a = 0
rw₁ : a * (↑2 : ZMod n) = 0 ↔ a = 0
⊢ a + a = 0 ↔ a = 0
have rw₂ : a * (↑(unitOfCoprime 2 hn) : ZMod n) = 0 ↔ a = 0
Tactic: rw [← mul_two, ← @Nat.cast_two (ZMod n), ← ZMod.coe_unitOfCoprime 2 hn, Units.mul_left_eq_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
rw : a * 2 = 0 ↔ a = 0
rw₁ : a * (↑2 : ZMod n) = 0 ↔ a = 0
rw₂ : a * (↑(unitOfCoprime 2 hn) : ZMod n) = 0 ↔ a = 0
⊢ a + a = 0 ↔ a = 0
have rw₃ : a = 0 ↔ a = 0
Tactic: rw [← mul_two, ← @Nat.cast_two (ZMod n), ← ZMod.coe_unitOfCoprime 2 hn, Units.mul_left_eq_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
hn : Odd n
a : ZMod n
ha : a ≠ 0
⊢ a ≠ -a
have rwa : ¬a = -a
Tactic: rwa [Ne, eq_neg_iff_add_eq_zero, add_self_eq_zero_iff_eq_zero hn]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
hn : Odd n
a : ZMod n
ha : a ≠ 0
rwa : ¬a = -a
⊢ a ≠ -a
have rwa₁ : ¬a + a = 0
Tactic: rwa [Ne, eq_neg_iff_add_eq_zero, add_self_eq_zero_iff_eq_zero hn]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
hn : Odd n
a : ZMod n
ha : a ≠ 0
rwa : ¬a = -a
rwa₁ : ¬a + a = 0
⊢ a ≠ -a
have rwa₂ : ¬a = 0
Tactic: rwa [Ne, eq_neg_iff_add_eq_zero, add_self_eq_zero_iff_eq_zero hn]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ZMod 2
⊢ -a = a
have 0 : Eq (α := ZMod 2) (-(fun (i : Fin (1 + 1)) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin (1 + 1)) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ZMod 2
0 : Eq (α := ZMod 2) (-(fun (i : Fin (1 + 1)) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin (1 + 1)) ↦ i) ⟨0, ⋯⟩)
⊢ -a = a
have 1 : Eq (α := ZMod 2) (-(fun (i : Fin (1 + 1)) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin (1 + 1)) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
⊢ Eq (α := ZMod 2) (-(fun (i : Fin (1 + 1)) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin (1 + 1)) ↦ i) ⟨0, ⋯⟩)
have 0 : (↑(-(fun (i : Fin (1 + 1)) ↦ i) (⟨0, sorry⟩ : Fin (1 + 1))) : ℕ) = (↑((fun (i : Fin (1 + 1)) ↦ i) ⟨0, sorry⟩) : ℕ)
Tactic: apply Fin.ext
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
⊢ Eq (α := ZMod 2) (-(fun (i : Fin (1 + 1)) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin (1 + 1)) ↦ i) ⟨1, ⋯⟩)
have 1 : (↑(-(fun (i : Fin (1 + 1)) ↦ i) (⟨1, sorry⟩ : Fin (1 + 1))) : ℕ) = (↑((fun (i : Fin (1 + 1)) ↦ i) ⟨1, sorry⟩) : ℕ)
Tactic: apply Fin.ext
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℤ
⊢ Eq (α := ZMod 2) (↑|a| : ZMod 2) (↑a : ZMod 2)
have inl : a ≤ 0 → Eq (α := ZMod 2) (↑|a| : ZMod 2) (↑a : ZMod 2)
Tactic: cases le_total a 0
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℤ
inl : a ≤ 0 → Eq (α := ZMod 2) (↑|a| : ZMod 2) (↑a : ZMod 2)
⊢ Eq (α := ZMod 2) (↑|a| : ZMod 2) (↑a : ZMod 2)
have inr : 0 ≤ a → Eq (α := ZMod 2) (↑|a| : ZMod 2) (↑a : ZMod 2)
Tactic: cases le_total a 0
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
⊢ -a = a ↔ a = 0 ∨ 2 * a.val = n
have rw : 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n
Tactic: rw [neg_eq_iff_add_eq_zero, ← two_mul]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n
have zero : ∀ (a : ZMod 0), 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = 0
Tactic: cases n
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
zero : ∀ (a : ZMod 0), 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = 0
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n
have succ : ∀ (n : ℕ) (a : ZMod (n + 1)), 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n + 1
Tactic: cases n
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
| 2 * a = 0
have rw : n + 1 ∣ 2 * a.val
Tactic: rw [← a.natCast_zmod_val, ← Nat.cast_two, ← Nat.cast_mul, natCast_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n + 1
have succ : n + 1 ∣ 2 * a.val ↔ a = 0 ∨ 2 * a.val = n + 1
Tactic: conv_lhs =>
    rw [← a.natCast_zmod_val, ← Nat.cast_two, ← Nat.cast_mul, natCast_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
⊢ n + 1 ∣ 2 * a.val ↔ a = 0 ∨ 2 * a.val = n + 1
have succ : n + 1 ∣ 2 * a.val → a = 0 ∨ 2 * a.val = n + 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
succ : n + 1 ∣ 2 * a.val → a = 0 ∨ 2 * a.val = n + 1
⊢ n + 1 ∣ 2 * a.val ↔ a = 0 ∨ 2 * a.val = n + 1
have succ₁ : a = 0 ∨ 2 * a.val = n + 1 → n + 1 ∣ 2 * a.val
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
m : ℕ
he : 2 * a.val = (n + 1) * m
⊢ a = 0 ∨ 2 * a.val = n + 1
have succ : ∀ (he : 2 * a.val = (n + 1) * 0), a = 0 ∨ 2 * a.val = n + 1
Tactic: rcases m with - | m
Cleared hypotheses: m, he
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
m : ℕ
he : 2 * a.val = (n + 1) * m
succ : ∀ (he : 2 * a.val = (n + 1) * 0), a = 0 ∨ 2 * a.val = n + 1
⊢ a = 0 ∨ 2 * a.val = n + 1
have succ₁ : ∀ (m : ℕ) (he : 2 * a.val = (n + 1) * (m + 1)), a = 0 ∨ 2 * a.val = n + 1
Tactic: rcases m with - | m
Cleared hypotheses: m, he
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
a : ZMod (n + 1)
he : 2 * a.val = (n + 1) * 0
⊢ a = 0 ∨ 2 * a.val = n + 1
have he₁ : Eq (α := ℕ) 2 0 ∨ a.val = 0
Tactic: rw [mul_zero, mul_eq_zero] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
a : ZMod (n + 1)
he : Eq (α := ℕ) 2 0 ∨ a.val = 0
⊢ a = 0 ∨ 2 * a.val = n + 1
have he₁ : a.val = 0
Tactic: rcases he with (⟨⟨⟩⟩ | he)
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
m : ℕ
he : 2 * a.val = (n + 1) * (m + 1)
⊢ a = 0 ∨ 2 * a.val = n + 1
have succ : ∀ (he : 2 * a.val = (n + 1) * HAdd.hAdd (α := ℕ) 0 1), a = 0 ∨ 2 * a.val = n + 1
Tactic: cases m
Cleared hypotheses: m, he
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
m : ℕ
he : 2 * a.val = (n + 1) * (m + 1)
succ : ∀ (he : 2 * a.val = (n + 1) * HAdd.hAdd (α := ℕ) 0 1), a = 0 ∨ 2 * a.val = n + 1
⊢ a = 0 ∨ 2 * a.val = n + 1
have succ₁ : ∀ (n_1 : ℕ) (he : 2 * a.val = (n + 1) * (n_1 + 1 + 1)), a = 0 ∨ 2 * a.val = n + 1
Tactic: cases m
Cleared hypotheses: m, he
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
he : 2 * a.val = (n + 1) * HAdd.hAdd (α := ℕ) 0 1
⊢ a = 0 ∨ 2 * a.val = n + 1
have succ : 2 * a.val = n + 1
Tactic: right
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
he : 2 * a.val = (n + 1) * HAdd.hAdd (α := ℕ) 0 1
⊢ 2 * a.val = n + 1
have succ : ∀ (he : 2 * a.val = (n + 1) * 1), 2 * a.val = n + 1
Tactic: rwa [show 0 + 1 = 1 from rfl, mul_one] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
he : 2 * a.val = (n + 1) * HAdd.hAdd (α := ℕ) 0 1
succ : ∀ (he : 2 * a.val = (n + 1) * 1), 2 * a.val = n + 1
⊢ 2 * a.val = n + 1
have succ₁ : ∀ (he : 2 * a.val = n + 1), 2 * a.val = n + 1
Tactic: rwa [show 0 + 1 = 1 from rfl, mul_one] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
n_1 : ℕ
he : 2 * a.val = (n + 1) * (n_1 + 1 + 1)
⊢ a = 0 ∨ 2 * a.val = n + 1
have succ : 2 * (n + 1) ≤ 2 * a.val
Tactic: refine (a.val_lt.not_ge <| Nat.le_of_mul_le_mul_left ?_ zero_lt_two).elim
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
n_1 : ℕ
he : 2 * a.val = (n + 1) * (n_1 + 1 + 1)
⊢ 2 * (n + 1) ≤ 2 * a.val
have succ : (n + 1) * 2 ≤ (n + 1) * (n_1 + 1 + 1)
Tactic: rw [he, mul_comm]