awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ZMod.Basic
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
⊢ NeZero (m * n)

Tactic:
haveI : NeZero (m * n) := ⟨hmn0⟩
-- Module: Mathlib.Data.ZMod.Basic
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 : NeZero (m * n)
⊢ NeZero m

Tactic:
haveI : NeZero m := ⟨left_ne_zero_of_mul hmn0⟩
-- Module: Mathlib.Data.ZMod.Basic
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 : NeZero m
⊢ NeZero n

Tactic:
haveI : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩
-- Module: Mathlib.Data.ZMod.Basic
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)
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
⊢ inv_fun (to_fun x) = x

Tactic:
dsimp only [to_fun, inv_fun, ZMod.castHom_apply]

Premises used: ZMod.castHom_apply
-- Module: Mathlib.Data.ZMod.Basic
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)
rw : (↑x.val : ZMod (m * n))
| x

Tactic:
rw [← ZMod.natCast_zmod_val x]

Premises used: ZMod.natCast_zmod_val
-- Module: Mathlib.Data.ZMod.Basic
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)
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))
⊢ (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:
conv_rhs => rw [← ZMod.natCast_zmod_val x]

Premises used: ZMod.natCast_zmod_val
-- Module: Mathlib.Data.ZMod.Basic
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)
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]
⊢ 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:
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]

Premises used: Prod.fst_zmod_cast, Prod.snd_zmod_cast, ZMod.natCast_eq_natCast_iff, Nat.modEq_and_modEq_iff_modEq_mul, if_neg
-- Module: Mathlib.Data.ZMod.Basic
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]

Tactic:
⟨(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 ?_⟩

Premises used: ZMod.cast, Nat.chineseRemainder, And.right, And.left, And.intro, Nat.ModEq.trans, Subtype.property, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
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]
refine_2 : val (n := n) x.cast ≡ x.val [MOD 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]

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 ?_⟩
-- Module: Mathlib.Data.ZMod.Basic
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)
refine_1₂ refine_1₃ : Eq (α := ZMod m) x.cast x.cast
⊢ val (n := m) x.cast ≡ x.val [MOD m]

Tactic:
rw [← ZMod.natCast_eq_natCast_iff, ZMod.natCast_zmod_val, ZMod.natCast_val]

Premises used: ZMod.natCast_val, ZMod.natCast_zmod_val, ZMod.natCast_eq_natCast_iff
-- Module: Mathlib.Data.ZMod.Basic
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)
refine_2₂ refine_2₃ : Eq (α := ZMod n) x.cast x.cast
⊢ val (n := n) x.cast ≡ x.val [MOD n]

Tactic:
rw [← ZMod.natCast_eq_natCast_iff, ZMod.natCast_zmod_val, ZMod.natCast_val]

Premises used: ZMod.natCast_val, ZMod.natCast_zmod_val, ZMod.natCast_eq_natCast_iff
-- Module: Mathlib.Data.ZMod.Basic
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

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]
-- Module: Mathlib.Data.ZMod.Basic
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
left_inv : LeftInverse inv_fun to_fun
⊢ Fintype.card (ZMod m × ZMod n) ≤ Fintype.card (ZMod (m * n))

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
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
left_inv : LeftInverse inv_fun to_fun
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun

Tactic:
exact ⟨left_inv, left_inv.rightInverse_of_card_le (by simp)⟩
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
mp : Subsingleton (ZMod n) → n = 1
mpr : n = 1 → Subsingleton (ZMod n)
⊢ Subsingleton (ZMod n) ↔ n = 1

Tactic:
constructor
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
mp : Subsingleton (ZMod 0) → Eq (α := ℕ) 0 1
mp₁ : Subsingleton (ZMod (HAdd.hAdd (α := ℕ) 0 1)) → HAdd.hAdd (α := ℕ) 0 1 = 1
mp₂ : ∀ (n : ℕ), Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1
⊢ Subsingleton (ZMod n) → n = 1

Tactic:
obtain (_ | _ | n) := n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ Subsingleton (ZMod 0) → Eq (α := ℕ) 0 1

Tactic:
simpa [ZMod] using not_subsingleton _

Premises used: ZMod, not_subsingleton
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ Subsingleton (ZMod (HAdd.hAdd (α := ℕ) 0 1)) → HAdd.hAdd (α := ℕ) 0 1 = 1

Tactic:
simp [ZMod]

Premises used: ZMod
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1

Tactic:
simpa [ZMod] using not_subsingleton _

Premises used: ZMod, not_subsingleton
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ Subsingleton (ZMod 1)

Tactic:
infer_instance
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
rw : ¬Subsingleton (ZMod n) ↔ n ≠ 1
rw₁ rw₂ : ¬n = 1 ↔ n ≠ 1
⊢ Nontrivial (ZMod n) ↔ n ≠ 1

Tactic:
rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]

Premises used: ZMod.subsingleton_iff, not_subsingleton_iff_nontrivial
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
⊢ ∀ (a b : (ZMod 2)ˣ), a = b

Tactic:
decide
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
hn : Odd n
a : ZMod n
rw : ∀ (hn : Nat.Coprime 2 n) {a : ZMod n}, a + a = 0 ↔ a = 0
⊢ a + a = 0 ↔ a = 0

Tactic:
rw [Nat.odd_iff, ← Nat.two_dvd_ne_zero, ← Nat.prime_two.coprime_iff_not_dvd] at hn

Premises used: Nat.two_dvd_ne_zero, Nat.prime_two, Nat.Prime.coprime_iff_not_dvd, Nat.odd_iff
-- Module: Mathlib.Data.ZMod.Basic
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
rw₃ rw₄ : a = 0 ↔ a = 0
⊢ a + a = 0 ↔ a = 0

Tactic:
rw [← mul_two, ← @Nat.cast_two (ZMod n), ← ZMod.coe_unitOfCoprime 2 hn, Units.mul_left_eq_zero]

Premises used: ZMod.coe_unitOfCoprime, OfNat.ofNat, Units.mul_left_eq_zero, mul_two, Nat.cast_two
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
hn : Odd n
a : ZMod n
ha : a ≠ 0
rwa : ¬a = -a
rwa₁ : ¬a + a = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ¬a = 0
⊢ a ≠ -a

Tactic:
rwa [Ne, eq_neg_iff_add_eq_zero, add_self_eq_zero_iff_eq_zero hn]

Premises used: ZMod.add_self_eq_zero_iff_eq_zero, Ne, eq_neg_iff_add_eq_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : Fact (2 < n)
⊢ Ne (α := ZMod n) (-1) 1

Tactic:
CharP.neg_one_ne_one (ZMod n) n

Premises used: CharP.neg_one_ne_one, ZMod
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ZMod 2
0 : Eq (α := ZMod 2) (-(fun (i : Fin (1 + 1)) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin (1 + 1)) ↦ i) ⟨0, ⋯⟩)
1 : Eq (α := ZMod 2) (-(fun (i : Fin (1 + 1)) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin (1 + 1)) ↦ i) ⟨1, ⋯⟩)
⊢ -a = a

Tactic:
fin_cases a
-- Module: Mathlib.Data.ZMod.Basic
Goal:
0 : (↑(-(fun (i : Fin (1 + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (1 + 1))) : ℕ) = (↑((fun (i : Fin (1 + 1)) ↦ i) ⟨0, ⋯⟩) : ℕ)
⊢ Eq (α := ZMod 2) (-(fun (i : Fin (1 + 1)) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin (1 + 1)) ↦ i) ⟨0, ⋯⟩)

Tactic:
apply Fin.ext

Premises used: Fin.ext
-- Module: Mathlib.Data.ZMod.Basic
Goal:
1 : (↑(-(fun (i : Fin (1 + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (1 + 1))) : ℕ) = (↑((fun (i : Fin (1 + 1)) ↦ i) ⟨1, ⋯⟩) : ℕ)
⊢ Eq (α := ZMod 2) (-(fun (i : Fin (1 + 1)) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin (1 + 1)) ↦ i) ⟨1, ⋯⟩)

Tactic:
apply Fin.ext

Premises used: Fin.ext
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ (↑(-(fun (i : Fin (1 + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (1 + 1))) : ℕ) = (↑((fun (i : Fin (1 + 1)) ↦ i) ⟨0, ⋯⟩) : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ (↑(-1) : ℕ) = 1

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℤ
inl : a ≤ 0 → Eq (α := ZMod 2) (↑|a| : ZMod 2) (↑a : ZMod 2)
inr : 0 ≤ a → Eq (α := ZMod 2) (↑|a| : ZMod 2) (↑a : ZMod 2)
⊢ Eq (α := ZMod 2) (↑|a| : ZMod 2) (↑a : ZMod 2)

Tactic:
cases le_total a 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℤ
h : a ≤ 0
⊢ Eq (α := ZMod 2) (↑|a| : ZMod 2) (↑a : ZMod 2)

Tactic:
simp [abs_of_nonneg, abs_of_nonpos, *]

Premises used: abs_of_nonpos, abs_of_nonneg
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℤ
h : 0 ≤ a
⊢ Eq (α := ZMod 2) (↑|a| : ZMod 2) (↑a : ZMod 2)

Tactic:
simp [abs_of_nonneg, abs_of_nonpos, *]

Premises used: abs_of_nonpos, abs_of_nonneg
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℤ
⊢ Eq (α := ZMod 2) (↑a.natAbs : ZMod 2) (↑a : ZMod 2)

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod n
⊢ a.val ≠ 0 ↔ a ≠ 0

Tactic:
(val_eq_zero a).not

Premises used: Iff.not, ZMod.val_eq_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod n
⊢ 0 < a.val ↔ a ≠ 0

Tactic:
simp [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
hn : LT.lt (α := ℕ) 1 0
x : ZMod 0
⊢ x.val = 1 ↔ x = 1

Tactic:
simp at hn
-- Module: Mathlib.Data.ZMod.Basic
Goal:
hn : LT.lt (α := ℕ) 1 1
x : ZMod 1
⊢ x.val = 1 ↔ x = 1

Tactic:
simp at hn
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
h : 1 < n + 2
x : ZMod (n + 2)
⊢ x.val = 1 ↔ x = 1

Tactic:
simp only [val, ZMod, Fin.ext_iff, Fin.val_one]

Premises used: Fin.ext_iff, Fin.val_one, ZMod, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod n
rw : 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n
⊢ -a = a ↔ a = 0 ∨ 2 * a.val = n

Tactic:
rw [neg_eq_iff_add_eq_zero, ← two_mul]

Premises used: neg_eq_iff_add_eq_zero, two_mul
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod n
zero : ∀ (a : ZMod 0), 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = 0
succ : ∀ (n : ℕ) (a : ZMod (n + 1)), 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n + 1
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ZMod 0
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = 0

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
rw : n + 1 ∣ 2 * a.val
| 2 * a = 0

Tactic:
rw [← a.natCast_zmod_val, ← Nat.cast_two, ← Nat.cast_mul, natCast_eq_zero_iff]

Premises used: ZMod.natCast_eq_zero_iff, ZMod.natCast_zmod_val, Nat.cast_mul, Nat.cast_two
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
succ : n + 1 ∣ 2 * a.val ↔ a = 0 ∨ 2 * a.val = n + 1
⊢ 2 * a = 0 ↔ 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]

Premises used: ZMod.natCast_eq_zero_iff, ZMod.natCast_zmod_val, Nat.cast_mul, Nat.cast_two
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
succ : n + 1 ∣ 2 * a.val → a = 0 ∨ 2 * a.val = n + 1
succ₁ : a = 0 ∨ 2 * a.val = n + 1 → n + 1 ∣ 2 * a.val
⊢ n + 1 ∣ 2 * a.val ↔ a = 0 ∨ 2 * a.val = n + 1

Tactic:
constructor
-- Module: Mathlib.Data.ZMod.Basic
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
succ₁ : ∀ (m : ℕ) (he : 2 * a.val = (n + 1) * (m + 1)), a = 0 ∨ 2 * a.val = n + 1
⊢ a = 0 ∨ 2 * a.val = n + 1

Tactic:
rcases m with - | m
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
he : 2 * a.val = (n + 1) * 0
⊢ Eq (α := ℕ) 2 0 ∨ a.val = 0

Tactic:
rw [mul_zero, mul_eq_zero] at he

Premises used: mul_eq_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
he : Eq (α := ℕ) 2 0 ∨ a.val = 0
⊢ a.val = 0

Tactic:
rcases he with (⟨⟨⟩⟩ | he)
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
he : a.val = 0
⊢ a = 0 ∨ 2 * a.val = n + 1

Tactic:
Or.inl (a.val_eq_zero.1 he)

Premises used: Iff.mp, Or.inl, ZMod.val_eq_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
he : a.val = 0
⊢ a = 0 ∨ 2 * a.val = n + 1

Tactic:
exact Or.inl (a.val_eq_zero.1 he)

Premises used: Iff.mp, Or.inl, ZMod.val_eq_zero
-- Module: Mathlib.Data.ZMod.Basic
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
succ₁ : ∀ (n_1 : ℕ) (he : 2 * a.val = (n + 1) * (n_1 + 1 + 1)), a = 0 ∨ 2 * a.val = n + 1
⊢ a = 0 ∨ 2 * a.val = n + 1

Tactic:
cases m
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
he : 2 * a.val = (n + 1) * HAdd.hAdd (α := ℕ) 0 1
succ : 2 * a.val = n + 1
⊢ a = 0 ∨ 2 * a.val = n + 1

Tactic:
right
-- Module: Mathlib.Data.ZMod.Basic
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
succ₁ succ₂ succ₃ succ₄ : ∀ (he : 2 * a.val = n + 1), 2 * a.val = n + 1
⊢ 2 * a.val = n + 1

Tactic:
rwa [show 0 + 1 = 1 from rfl, mul_one] at he

Premises used: mul_one, rfl
-- Module: Mathlib.Data.ZMod.Basic
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

Tactic:
(a.val_lt.not_ge <| Nat.le_of_mul_le_mul_left ?_ zero_lt_two).elim

Premises used: False.elim, Nat.le_of_mul_le_mul_left, LT.lt.not_ge, zero_lt_two, ZMod.val_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
n_1 : ℕ
he : 2 * a.val = (n + 1) * (n_1 + 1 + 1)
succ : 2 * (n + 1) ≤ 2 * a.val
⊢ a = 0 ∨ 2 * a.val = n + 1

Tactic:
refine (a.val_lt.not_ge <| Nat.le_of_mul_le_mul_left ?_ zero_lt_two).elim

Premises used: False.elim, Nat.le_of_mul_le_mul_left, LT.lt.not_ge, zero_lt_two, ZMod.val_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
n_1 : ℕ
he : 2 * a.val = (n + 1) * (n_1 + 1 + 1)
succ : (n + 1) * 2 ≤ (n + 1) * (n_1 + 1 + 1)
⊢ 2 * (n + 1) ≤ 2 * a.val

Tactic:
rw [he, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
n_1 : ℕ
he : 2 * a.val = (n + 1) * (n_1 + 1 + 1)
succ : 2 ≤ n_1 + 1 + 1
⊢ (n + 1) * 2 ≤ (n + 1) * (n_1 + 1 + 1)

Tactic:
apply Nat.mul_le_mul_left

Premises used: Nat.mul_le_mul_left
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
n_1 : ℕ
he : 2 * a.val = (n + 1) * (n_1 + 1 + 1)
⊢ 2 ≤ n_1 + 1 + 1

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ n + 1 ∣ 0

Tactic:
apply dvd_zero

Premises used: dvd_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
h : 2 * a.val = n + 1
succ succ₁ : n + 1 ∣ n + 1
⊢ n + 1 ∣ 2 * a.val

Tactic:
rw [h]