awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : AddGroupWithOne R
zero :
  Eq.{u_1 + 1} (α := R)
    ((match (motive := (x : ℕ) → ZMod x → R) 0 with
        | 0 => Int.cast
        | n.succ => fun (i : ZMod (n + 1)) ↦ (↑i.val : R))
        0 :
      R)
    (0 : R)
succ :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := R)
      ((match (motive := (x : ℕ) → ZMod x → R) n + 1 with
          | 0 => Int.cast
          | n.succ => fun (i : ZMod (n + 1)) ↦ (↑i.val : R))
          0 :
        R)
      (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((match (motive := (x : ℕ) → ZMod x → R) n with
        | 0 => Int.cast
        | n.succ => fun (i : ZMod (n + 1)) ↦ (↑i.val : R))
        0 :
      R)
    (0 : R)

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
⊢ Eq.{u_1 + 1} (α := R)
    ((match (motive := (x : ℕ) → ZMod x → R) 0 with
        | 0 => Int.cast
        | n.succ => fun (i : ZMod (n + 1)) ↦ (↑i.val : R))
        0 :
      R)
    (0 : R)

Tactic:
Int.cast_zero

Premises used: Int.cast_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
⊢ Eq.{u_1 + 1} (α := R)
    ((match (motive := (x : ℕ) → ZMod x → R) 0 with
        | 0 => Int.cast
        | n.succ => fun (i : ZMod (n + 1)) ↦ (↑i.val : R))
        0 :
      R)
    (0 : R)

Tactic:
exact Int.cast_zero

Premises used: Int.cast_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    ((match (motive := (x : ℕ) → ZMod x → R) n + 1 with
        | 0 => Int.cast
        | n.succ => fun (i : ZMod (n + 1)) ↦ (↑i.val : R))
        0 :
      R)
    (0 : R)

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : AddGroupWithOne R
inst_1 : NeZero n
a : ZMod n
zero : ∀ [NeZero (R := ℕ) 0] (a : ZMod 0), Eq.{u_1 + 1} (α := R) a.cast (↑a.val : R)
succ : ∀ (n : ℕ) [NeZero (n + 1)] (a : ZMod (n + 1)), Eq.{u_1 + 1} (α := R) a.cast (↑a.val : R)
⊢ Eq.{u_1 + 1} (α := R) a.cast (↑a.val : R)

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
inst_1 : NeZero (R := ℕ) 0
a : ZMod 0
⊢ Eq.{u_1 + 1} (α := R) a.cast (↑a.val : R)

Tactic:
cases NeZero.ne 0 rfl

Premises used: OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
n : ℕ
inst_1 : NeZero (n + 1)
a : ZMod (n + 1)
⊢ Eq.{u_1 + 1} (α := R) a.cast (↑a.val : R)

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : AddGroupWithOne R
S : Type u_2
inst_1 : AddGroupWithOne S
a : ZMod n
zero : ∀ (a : ZMod 0), Eq.{u_1 + 1} (α := R) a.cast.1 a.cast
succ : ∀ (n : ℕ) (a : ZMod (n + 1)), Eq.{u_1 + 1} (α := R) a.cast.1 a.cast
⊢ Eq.{u_1 + 1} (α := R) a.cast.1 a.cast

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
S : Type u_2
inst_1 : AddGroupWithOne S
a : ZMod 0
⊢ Eq.{u_1 + 1} (α := R) a.cast.1 a.cast

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
S : Type u_2
inst_1 : AddGroupWithOne S
n : ℕ
a : ZMod (n + 1)
⊢ Eq.{u_1 + 1} (α := R) a.cast.1 a.cast

Tactic:
simp [ZMod.cast]

Premises used: ZMod.cast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : AddGroupWithOne R
S : Type u_2
inst_1 : AddGroupWithOne S
a : ZMod n
zero : ∀ (a : ZMod 0), Eq.{u_2 + 1} (α := S) a.cast.2 a.cast
succ : ∀ (n : ℕ) (a : ZMod (n + 1)), Eq.{u_2 + 1} (α := S) a.cast.2 a.cast
⊢ Eq.{u_2 + 1} (α := S) a.cast.2 a.cast

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
S : Type u_2
inst_1 : AddGroupWithOne S
a : ZMod 0
⊢ Eq.{u_2 + 1} (α := S) a.cast.2 a.cast

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
S : Type u_2
inst_1 : AddGroupWithOne S
n : ℕ
a : ZMod (n + 1)
⊢ Eq.{u_2 + 1} (α := S) a.cast.2 a.cast

Tactic:
simp [ZMod.cast]

Premises used: ZMod.cast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
zero : ∀ [NeZero (R := ℕ) 0] (a : ZMod 0), (↑a.val : ZMod 0) = a
succ : ∀ (n : ℕ) [NeZero (n + 1)] (a : ZMod (n + 1)), (↑a.val : ZMod (n + 1)) = a
⊢ (↑a.val : ZMod n) = a

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
inst : NeZero (R := ℕ) 0
a : ZMod 0
⊢ (↑a.val : ZMod 0) = a

Tactic:
cases NeZero.ne 0 rfl

Premises used: OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero (n + 1)
a : ZMod (n + 1)
⊢ (↑a.val : ZMod (n + 1)) = a

Tactic:
apply Fin.cast_val_eq_self

Premises used: Fin.cast_val_eq_self
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ RightInverse (β := ZMod n) val Nat.cast

Tactic:
natCast_zmod_val

Premises used: Function.LeftInverse, ZMod.natCast_zmod_val, Function.RightInverse
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ Surjective (β := ZMod n) Nat.cast

Tactic:
natCast_rightInverse.surjective

Premises used: ZMod.natCast_rightInverse, Function.RightInverse.surjective
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod n
zero : ∀ (a : ZMod 0), (↑a.cast : ZMod 0) = a
succ : ∀ (n : ℕ) (a : ZMod (n + 1)), (↑a.cast : ZMod (n + 1)) = a
⊢ (↑a.cast : ZMod n) = a

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ZMod 0
⊢ (↑a.cast : ZMod 0) = a

Tactic:
simp [ZMod.cast, ZMod]

Premises used: ZMod.cast, ZMod
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod (n + 1)
succ : (↑a.val : ZMod (n + 1)) = a
succ₁ succ₂ : a = a
⊢ (↑(↑a.val : ℤ) : ZMod (n + 1)) = a

Tactic:
rw [Int.cast_natCast, natCast_zmod_val]

Premises used: Int.cast_natCast, ZMod.natCast_zmod_val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ RightInverse (β := ZMod n) cast Int.cast

Tactic:
intCast_zmod_cast

Premises used: Function.LeftInverse, Function.RightInverse, ZMod.intCast_zmod_cast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ Surjective (β := ZMod n) Int.cast

Tactic:
intCast_rightInverse.surjective

Premises used: ZMod.intCast_rightInverse, Function.RightInverse.surjective
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
P : ZMod n → Prop
⊢ (∀ (x : ZMod n), P x) ↔ ∀ (x : ℤ), P (↑x : ZMod n)

Tactic:
intCast_surjective.forall

Premises used: Function.Surjective.forall, ZMod.intCast_surjective
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
P : ZMod n → Prop
⊢ (∃ (x : ZMod n), P x) ↔ ∃ (x : ℤ), P (↑x : ZMod n)

Tactic:
intCast_surjective.exists

Premises used: Function.Surjective.exists, ZMod.intCast_surjective
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ Eq (α := ZMod n → ZMod n) cast id

Tactic:
funext (cast_id n)

Premises used: funext, ZMod.cast_id
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : NeZero n
zero : ∀ [NeZero (R := ℕ) 0], Eq.{u_1 + 1} (α := ZMod 0 → R) (Nat.cast ∘ val) cast
succ : ∀ (n : ℕ) [NeZero (n + 1)], Eq.{u_1 + 1} (α := ZMod (n + 1) → R) (Nat.cast ∘ val) cast
⊢ Eq.{u_1 + 1} (α := ZMod n → R) (Nat.cast ∘ val) cast

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : NeZero (R := ℕ) 0
⊢ Eq.{u_1 + 1} (α := ZMod 0 → R) (Nat.cast ∘ val) cast

Tactic:
cases NeZero.ne 0 rfl

Premises used: OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
n : ℕ
inst_1 : NeZero (n + 1)
⊢ Eq.{u_1 + 1} (α := ZMod (n + 1) → R) (Nat.cast ∘ val) cast

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
zero : Eq.{u_1 + 1} (α := ZMod 0 → R) (Int.cast ∘ cast) cast
succ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := ZMod (n + 1) → R) (Int.cast ∘ cast) cast
⊢ Eq.{u_1 + 1} (α := ZMod n → R) (Int.cast ∘ cast) cast

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
⊢ Eq.{u_1 + 1} (α := ZMod 0 → R) (Int.cast ∘ cast) cast

Tactic:
congr_arg (Int.cast ∘ ·) ZMod.cast_id'

Premises used: Int.cast, ZMod.cast, Function.comp, ZMod, congr_arg, ZMod.cast_id'
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
⊢ Eq.{u_1 + 1} (α := ZMod 0 → R) (Int.cast ∘ cast) cast

Tactic:
exact congr_arg (Int.cast ∘ ·) ZMod.cast_id'

Premises used: Int.cast, Function.comp, congr_arg
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
n : ℕ
succ : ∀ (x : ZMod (n + 1)), Eq.{u_1 + 1} (α := R) ((Int.cast ∘ cast) x) x.cast
⊢ Eq.{u_1 + 1} (α := ZMod (n + 1) → R) (Int.cast ∘ cast) cast

Tactic:
ext
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
n : ℕ
x : ZMod (n + 1)
⊢ Eq.{u_1 + 1} (α := R) ((Int.cast ∘ cast) x) x.cast

Tactic:
simp [ZMod, ZMod.cast]

Premises used: ZMod.cast, ZMod
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : NeZero n
i : ZMod n
⊢ Eq.{u_1 + 1} (α := R) (↑i.val : R) i.cast

Tactic:
congr_fun (natCast_comp_val R) i

Premises used: ZMod.natCast_comp_val, congr_fun
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
i : ZMod n
⊢ Eq.{u_1 + 1} (α := R) (↑i.cast : R) i.cast

Tactic:
congr_fun (intCast_comp_cast R) i

Premises used: ZMod.intCast_comp_cast, congr_fun
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : ZMod n
zero :
  ∀ (a b : ZMod 0),
    (a + b).cast =
      if (↑0 : ℤ) ≤ HAdd.hAdd (α := ℤ) a.cast b.cast then HAdd.hAdd (α := ℤ) a.cast b.cast - (↑0 : ℤ)
      else HAdd.hAdd (α := ℤ) a.cast b.cast
succ :
  ∀ (n : ℕ) (a b : ZMod (n + 1)),
    (a + b).cast =
      if (↑(n + 1) : ℤ) ≤ HAdd.hAdd (α := ℤ) a.cast b.cast then HAdd.hAdd (α := ℤ) a.cast b.cast - (↑(n + 1) : ℤ)
      else HAdd.hAdd (α := ℤ) a.cast b.cast
⊢ (a + b).cast =
    if (↑n : ℤ) ≤ HAdd.hAdd (α := ℤ) a.cast b.cast then HAdd.hAdd (α := ℤ) a.cast b.cast - (↑n : ℤ)
    else HAdd.hAdd (α := ℤ) a.cast b.cast

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b : ZMod 0
zero : (a + b).cast = HAdd.hAdd (α := ℤ) a.cast b.cast
⊢ (a + b).cast =
    if (↑0 : ℤ) ≤ HAdd.hAdd (α := ℤ) a.cast b.cast then HAdd.hAdd (α := ℤ) a.cast b.cast - (↑0 : ℤ)
    else HAdd.hAdd (α := ℤ) a.cast b.cast

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a b : ZMod 0
⊢ (a + b).cast = HAdd.hAdd (α := ℤ) a.cast b.cast

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : ZMod (n + 1)
succ :
  ∀ (a b : Fin (n + 1)),
    (a + b).cast =
      if (↑(n + 1) : ℤ) ≤ HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) then
        HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
      else HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)
⊢ (a + b).cast =
    if (↑(n + 1) : ℤ) ≤ HAdd.hAdd (α := ℤ) a.cast b.cast then HAdd.hAdd (α := ℤ) a.cast b.cast - (↑(n + 1) : ℤ)
    else HAdd.hAdd (α := ℤ) a.cast b.cast

Tactic:
change Fin (n + 1) at a b

Premises used: HAdd.hAdd, OfNat.ofNat, Fin
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : Fin (n + 1)
succ :
  (↑(if n + 1 ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - (n + 1) else (↑a : ℕ) + (↑b : ℕ)) : ℤ) =
    if HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ≤ HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) then
      HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
    else HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)
⊢ (↑(↑(a + b) : ℕ) : ℤ) =
    if (↑(n + 1) : ℤ) ≤ HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) then
      HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
    else HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)

Tactic:
simp only [Fin.val_add_eq_ite, Int.natCast_succ]

Premises used: Fin.val_add_eq_ite, Int.natCast_succ
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : Fin (n + 1)
succ :
  (↑(if n + 1 ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - (n + 1) else (↑a : ℕ) + (↑b : ℕ)) : ℤ) =
    if n + 1 ≤ (↑a : ℕ) + (↑b : ℕ) then HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
    else HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)
⊢ (↑(if n + 1 ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - (n + 1) else (↑a : ℕ) + (↑b : ℕ)) : ℤ) =
    if HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ≤ HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) (↑(↑b : ℕ) : ℤ) then
      HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
    else HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)

Tactic:
norm_cast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : Fin (n + 1)
pos :
  ∀ (h : n + 1 ≤ (↑a : ℕ) + (↑b : ℕ)),
    (↑((↑a : ℕ) + (↑b : ℕ) - (n + 1)) : ℤ) =
      HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
neg :
  ∀ (h : ¬n + 1 ≤ (↑a : ℕ) + (↑b : ℕ)),
    (↑((↑a : ℕ) + (↑b : ℕ)) : ℤ) = HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)
⊢ (↑(if n + 1 ≤ (↑a : ℕ) + (↑b : ℕ) then (↑a : ℕ) + (↑b : ℕ) - (n + 1) else (↑a : ℕ) + (↑b : ℕ)) : ℤ) =
    if n + 1 ≤ (↑a : ℕ) + (↑b : ℕ) then HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
    else HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ (↑a : ℕ) + (↑b : ℕ)
pos :
  HSub.hSub (α := ℤ) (↑((↑a : ℕ) + (↑b : ℕ)) : ℤ) (↑(n + 1) : ℤ) =
    HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)
⊢ (↑((↑a : ℕ) + (↑b : ℕ) - (n + 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)

Tactic:
rw [Nat.cast_sub h]

Premises used: Nat.cast_sub
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ (↑a : ℕ) + (↑b : ℕ)
⊢ HSub.hSub (α := ℤ) (↑((↑a : ℕ) + (↑b : ℕ)) : ℤ) (↑(n + 1) : ℤ) =
    HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b) - (↑(n + 1) : ℤ)

Tactic:
congr
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : Fin (n + 1)
h : ¬n + 1 ≤ (↑a : ℕ) + (↑b : ℕ)
⊢ (↑((↑a : ℕ) + (↑b : ℕ)) : ℤ) = HAdd.hAdd (α := ℤ) (cast (n := n + 1) a) (cast (n := n + 1) b)

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
zero : ∀ (h : m ∣ 0), Eq.{u_1 + 1} (α := R) (cast (n := 0) 1) 1
succ : ∀ (n : ℕ) (h : m ∣ n + 1), Eq.{u_1 + 1} (α := R) (cast (n := n + 1) 1) 1
⊢ Eq.{u_1 + 1} (α := R) (cast (n := n) 1) 1

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ 0
⊢ Eq.{u_1 + 1} (α := R) (cast (n := 0) 1) 1

Tactic:
Int.cast_one

Premises used: ZMod.cast, Int.cast_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ 0
⊢ Eq.{u_1 + 1} (α := R) (cast (n := 0) 1) 1

Tactic:
exact Int.cast_one

Premises used: Int.cast_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
succ : Eq.{u_1 + 1} (α := R) (↑(1 % (n + 1)) : R) 1
⊢ Eq.{u_1 + 1} (α := R) (cast (n := n + 1) 1) 1

Tactic:
change ((1 % (n + 1) : ℕ) : R) = 1

Premises used: Nat.cast, HMod.hMod, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
succ : ∀ (h : m ∣ HAdd.hAdd (α := ℕ) 0 1), Eq.{u_1 + 1} (α := R) (↑(1 % HAdd.hAdd (α := ℕ) 0 1) : R) 1
succ₁ : ∀ (n : ℕ) (h : m ∣ n + 1 + 1), Eq.{u_1 + 1} (α := R) (↑(1 % (n + 1 + 1)) : R) 1
⊢ Eq.{u_1 + 1} (α := R) (↑(1 % (n + 1)) : R) 1

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ HAdd.hAdd (α := ℕ) 0 1
⊢ m = 1

Tactic:
rw [Nat.dvd_one] at h

Premises used: Nat.dvd_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m = 1
⊢ CharP R 1

Tactic:
subst m
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 1
⊢ Eq.{u_1 + 1} (α := R) (↑(1 % HAdd.hAdd (α := ℕ) 0 1) : R) 1

Tactic:
subsingleton [CharP.CharOne.subsingleton]

Premises used: CharP.CharOne.subsingleton
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1 + 1
succ : Eq.{u_1 + 1} (α := R) (↑1 : R) 1
succ₁ : 1 < n + 1 + 1
⊢ Eq.{u_1 + 1} (α := R) (↑(1 % (n + 1 + 1)) : R) 1

Tactic:
rw [Nat.mod_eq_of_lt]

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1 + 1
⊢ Eq.{u_1 + 1} (α := R) (↑1 : R) 1

Tactic:
Nat.cast_one

Premises used: Nat.cast_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1 + 1
⊢ Eq.{u_1 + 1} (α := R) (↑1 : R) 1

Tactic:
exact Nat.cast_one

Premises used: Nat.cast_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1 + 1
⊢ 1 < n + 1 + 1

Tactic:
Nat.lt_of_sub_eq_succ rfl

Premises used: Nat.lt_of_sub_eq_succ, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1 + 1
⊢ 1 < n + 1 + 1

Tactic:
exact Nat.lt_of_sub_eq_succ rfl

Premises used: Nat.lt_of_sub_eq_succ
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
a b : ZMod n
zero : ∀ (h : m ∣ 0) (a b : ZMod 0), (a + b).cast = HAdd.hAdd (α := R) a.cast b.cast
succ : ∀ (n : ℕ) (h : m ∣ n + 1) (a b : ZMod (n + 1)), (a + b).cast = HAdd.hAdd (α := R) a.cast b.cast
⊢ (a + b).cast = HAdd.hAdd (α := R) a.cast b.cast

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ 0
a b : ZMod 0
⊢ (a + b).cast = HAdd.hAdd (α := R) a.cast b.cast

Tactic:
apply Int.cast_add

Premises used: Int.cast_add
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
succ : HAdd.hAdd (α := R) a.cast b.cast = (a + b).cast
⊢ (a + b).cast = HAdd.hAdd (α := R) a.cast b.cast

Tactic:
symm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
succ : HAdd.hAdd (α := R) (↑(↑a : ℕ) : R) (↑(↑b : ℕ) : R) = (↑(↑(a + b) : ℕ) : R)
⊢ HAdd.hAdd (α := R) a.cast b.cast = (a + b).cast

Tactic:
dsimp [ZMod, ZMod.cast, ZMod.val]

Premises used: ZMod.cast, ZMod, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
succ : m ∣ (↑a : ℕ) + (↑b : ℕ) - ((↑a : ℕ) + (↑b : ℕ)) % (n + 1)
⊢ HAdd.hAdd (α := R) (↑(↑a : ℕ) : R) (↑(↑b : ℕ) : R) = (↑(↑(a + b) : ℕ) : R)

Tactic:
rw [← Nat.cast_add, Fin.val_add, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _),
    @CharP.cast_eq_zero_iff R _ m]

Premises used: Fin.val_add, Nat.cast_sub, sub_eq_zero, Nat.cast_add, Nat.mod_le, CharP.cast_eq_zero_iff
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
⊢ m ∣ (↑a : ℕ) + (↑b : ℕ) - ((↑a : ℕ) + (↑b : ℕ)) % (n + 1)

Tactic:
h.trans (Nat.dvd_sub_mod _)

Premises used: Nat.dvd_sub_mod, Dvd.dvd.trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
⊢ m ∣ (↑a : ℕ) + (↑b : ℕ) - ((↑a : ℕ) + (↑b : ℕ)) % (n + 1)

Tactic:
exact h.trans (Nat.dvd_sub_mod _)

Premises used: Nat.dvd_sub_mod, Dvd.dvd.trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
a b : ZMod n
zero : ∀ (h : m ∣ 0) (a b : ZMod 0), (a * b).cast = HMul.hMul (α := R) a.cast b.cast
succ : ∀ (n : ℕ) (h : m ∣ n + 1) (a b : ZMod (n + 1)), (a * b).cast = HMul.hMul (α := R) a.cast b.cast
⊢ (a * b).cast = HMul.hMul (α := R) a.cast b.cast

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ 0
a b : ZMod 0
⊢ (a * b).cast = HMul.hMul (α := R) a.cast b.cast

Tactic:
apply Int.cast_mul

Premises used: Int.cast_mul
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
succ : HMul.hMul (α := R) a.cast b.cast = (a * b).cast
⊢ (a * b).cast = HMul.hMul (α := R) a.cast b.cast

Tactic:
symm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
succ : HMul.hMul (α := R) (↑(↑a : ℕ) : R) (↑(↑b : ℕ) : R) = (↑(↑(a * b) : ℕ) : R)
⊢ HMul.hMul (α := R) a.cast b.cast = (a * b).cast

Tactic:
dsimp [ZMod, ZMod.cast, ZMod.val]

Premises used: ZMod.cast, ZMod, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
succ : m ∣ (↑a : ℕ) * (↑b : ℕ) - (↑a : ℕ) * (↑b : ℕ) % (n + 1)
⊢ HMul.hMul (α := R) (↑(↑a : ℕ) : R) (↑(↑b : ℕ) : R) = (↑(↑(a * b) : ℕ) : R)

Tactic:
rw [← Nat.cast_mul, Fin.val_mul, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _),
    @CharP.cast_eq_zero_iff R _ m]

Premises used: Nat.cast_sub, sub_eq_zero, Nat.cast_mul, Fin.val_mul, Nat.mod_le, CharP.cast_eq_zero_iff
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
⊢ m ∣ (↑a : ℕ) * (↑b : ℕ) - (↑a : ℕ) * (↑b : ℕ) % (n + 1)

Tactic:
h.trans (Nat.dvd_sub_mod _)

Premises used: Nat.dvd_sub_mod, Dvd.dvd.trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
⊢ m ∣ (↑a : ℕ) * (↑b : ℕ) - (↑a : ℕ) * (↑b : ℕ) % (n + 1)

Tactic:
exact h.trans (Nat.dvd_sub_mod _)

Premises used: Nat.dvd_sub_mod, Dvd.dvd.trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
i : ZMod n
⊢ Eq (α := R) ((castHom h R : (a : ZMod n) → R) i : R) (i.cast : R)

Tactic:
rfl

Premises used: ZMod.cast, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
a b : ZMod n
⊢ (a - b).cast = HSub.hSub (α := R) a.cast b.cast

Tactic:
(castHom h R).map_sub a b

Premises used: ZMod.cast, RingHom.map_sub, ZMod.castHom
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
a : ZMod n
⊢ Eq.{u_1 + 1} (α := R) (-a).cast (-a.cast)

Tactic:
(castHom h R).map_neg a

Premises used: RingHom.map_neg, ZMod.cast, ZMod.castHom
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
a : ZMod n
k : ℕ
⊢ (a ^ k).cast = HPow.hPow (α := R) a.cast k

Tactic:
(castHom h R).map_pow a k

Premises used: ZMod.cast, ZMod.castHom, RingHom.map_pow
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
k : ℕ
⊢ Eq.{u_1 + 1} (α := R) (cast (n := n) (↑k : ZMod n)) (↑k : R)

Tactic:
map_natCast (castHom h R) k

Premises used: ZMod.cast, map_natCast, ZMod.castHom
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
h : m ∣ n
k : ℤ
⊢ Eq.{u_1 + 1} (α := R) (cast (n := n) (↑k : ZMod n)) (↑k : R)

Tactic:
map_intCast (castHom h R) k

Premises used: ZMod.cast, map_intCast, ZMod.castHom
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n m : ℕ
h : m ∣ n
a : ZMod m
obtain :
  ∀ (a : ℤ),
    ∃ (a_1 : ZMod n),
      Eq (α := ZMod m) ((castHom h (ZMod m) : (a : ZMod n) → ZMod m) a_1 : ZMod m) ((↑a : ZMod m) : ZMod m)
⊢ ∃ (a_1 : ZMod n), (castHom h (ZMod m) : (a : ZMod n) → ZMod m) a_1 = a

Tactic:
obtain ⟨a, rfl⟩ := intCast_surjective a

Premises used: ZMod.intCast_surjective, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n m : ℕ
h : m ∣ n
a : ℤ
⊢ ∃ (a_1 : ZMod n),
    Eq (α := ZMod m) ((castHom h (ZMod m) : (a : ZMod n) → ZMod m) a_1 : ZMod m) ((↑a : ZMod m) : ZMod m)

Tactic:
⟨a, map_intCast ..⟩

Premises used: Int.cast, map_intCast, Exists.intro
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n m : ℕ
h : m ∣ n
a : ℤ
⊢ ∃ (a_1 : ZMod n),
    Eq (α := ZMod m) ((castHom h (ZMod m) : (a : ZMod n) → ZMod m) a_1 : ZMod m) ((↑a : ZMod m) : ZMod m)

Tactic:
exact ⟨a, map_intCast ..⟩
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
⊢ Eq.{u_1 + 1} (α := R) (cast (n := n) 1) 1

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
a b : ZMod n
⊢ (a + b).cast = HAdd.hAdd (α := R) a.cast b.cast

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
a b : ZMod n
⊢ (a * b).cast = HMul.hMul (α := R) a.cast b.cast

Tactic:
simp