awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℤ
mpr : HAdd.hAdd (α := ZMod p) (↑(↑z.val : ℤ) : ZMod p) (↑((↑p : ℤ) * k) : ZMod p) = z
mpr₁ : (↑(↑z.val : ℤ) : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
mpr₂ : (↑z.val : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
mpr₃ : (↑z.val : ZMod p) + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
mpr₄ : z.cast + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
mpr₅ : z.cast + HMul.hMul (α := ZMod p) 0 (↑k : ZMod p) = z
mpr₆ : HAdd.hAdd (α := ZMod p) z.cast 0 = z
⊢ (↑((↑z.val : ℤ) + (↑p : ℤ) * k) : ZMod p) = z
have mpr₇ : z.cast = z
Tactic: rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val,
      ZMod.natCast_self, zero_mul, add_zero, cast_id]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p : ℕ
z : ZMod p
inst : NeZero p
k : ℤ
mpr : HAdd.hAdd (α := ZMod p) (↑(↑z.val : ℤ) : ZMod p) (↑((↑p : ℤ) * k) : ZMod p) = z
mpr₁ : (↑(↑z.val : ℤ) : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
mpr₂ : (↑z.val : ZMod p) + HMul.hMul (α := ZMod p) (↑(↑p : ℤ) : ZMod p) (↑k : ZMod p) = z
mpr₃ : (↑z.val : ZMod p) + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
mpr₄ : z.cast + HMul.hMul (α := ZMod p) (↑p : ZMod p) (↑k : ZMod p) = z
mpr₅ : z.cast + HMul.hMul (α := ZMod p) 0 (↑k : ZMod p) = z
mpr₆ : HAdd.hAdd (α := ZMod p) z.cast 0 = z
mpr₇ : z.cast = z
⊢ (↑((↑z.val : ℤ) + (↑p : ℤ) * k) : ZMod p) = z
have mpr₈ : z = z
Tactic: rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val,
      ZMod.natCast_self, zero_mul, add_zero, cast_id]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℤ
b : ℕ
⊢ Eq (α := ZMod b) (↑(a % (↑b : ℤ)) : ZMod b) (↑a : ZMod b)
have rw : a % (↑b : ℤ) ≡ a [ZMOD (↑b : ℤ)]
Tactic: rw [ZMod.intCast_eq_intCast_iff]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
⊢ AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) = AddSubgroup.zmultiples (↑n : ℤ)
have h : ∀ (x : ℤ),
  x ∈ AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) ↔
    Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.zmultiples (↑n : ℤ)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ℤ
⊢ x ∈ AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) ↔
    Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.zmultiples (↑n : ℤ)) x
have h : x ∈ AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) ↔ (↑n : ℤ) ∣ x
Tactic: rw [Int.mem_zmultiples_iff, AddMonoidHom.mem_ker, Int.coe_castAddHom,
    intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ℤ
h : x ∈ AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) ↔ (↑n : ℤ) ∣ x
⊢ x ∈ AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) ↔
    Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.zmultiples (↑n : ℤ)) x
have h₁ : Eq (α := ZMod n) ((Int.castAddHom (ZMod n) : (a : ℤ) → ZMod n) x : ZMod n) (0 : ZMod n) ↔ (↑n : ℤ) ∣ x
Tactic: rw [Int.mem_zmultiples_iff, AddMonoidHom.mem_ker, Int.coe_castAddHom,
    intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ℤ
h : x ∈ AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) ↔ (↑n : ℤ) ∣ x
h₁ : Eq (α := ZMod n) ((Int.castAddHom (ZMod n) : (a : ℤ) → ZMod n) x : ZMod n) (0 : ZMod n) ↔ (↑n : ℤ) ∣ x
⊢ x ∈ AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) ↔
    Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.zmultiples (↑n : ℤ)) x
have h₂ : Eq (α := ZMod n) ((fun (x : ℤ) ↦ ((↑x : ZMod n) : ZMod n)) x) 0 ↔ (↑n : ℤ) ∣ x
Tactic: rw [Int.mem_zmultiples_iff, AddMonoidHom.mem_ker, Int.coe_castAddHom,
    intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
x : ℤ
h : x ∈ AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) ↔ (↑n : ℤ) ∣ x
h₁ : Eq (α := ZMod n) ((Int.castAddHom (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
⊢ x ∈ AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) ↔
    Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.zmultiples (↑n : ℤ)) x
have h₃ : (↑n : ℤ) ∣ x ↔ (↑n : ℤ) ∣ x
Tactic: rw [Int.mem_zmultiples_iff, AddMonoidHom.mem_ker, Int.coe_castAddHom,
    intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
nzm : NeZero (R := ℕ) 0
h : 0 ≤ n
⊢ Injective (α := ZMod 0) (β := ZMod n) cast
have out : Ne (α := ℕ) 0 0
Tactic: cases nzm
Cleared hypotheses: nzm
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : Eq (α := ZMod n) (cast (n := m + 1) (⟨x, hx⟩ : Fin (m + 1))) (cast (n := m + 1) (⟨y, hy⟩ : Fin (m + 1)))
⊢ (⟨x, hx⟩ : Fin (m + 1)) = ⟨y, hy⟩
have f₁ : x = y
Tactic: simp only [cast, val, natCast_eq_natCast_iff',
      Nat.mod_eq_of_lt (hx.trans_le h), Nat.mod_eq_of_lt (hy.trans_le h)] at f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : x = y
⊢ (⟨x, hx⟩ : Fin (m + 1)) = ⟨y, hy⟩
have succ : (↑(⟨x, hx⟩ : Fin (m + 1)) : ℕ) = (↑(⟨y, hy⟩ : Fin (m + 1)) : ℕ)
Tactic: apply Fin.ext
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
nzm : NeZero m
h : m ≤ n
⊢ Injective (α := ZMod m) (β := ZMod n) cast
have zero : ∀ [nzm : NeZero (R := ℕ) 0] (h : 0 ≤ n), Injective (α := ZMod 0) (β := ZMod n) cast
Tactic: cases m with
  | zero => cases nzm; simp_all
  | succ m =>
    rintro ⟨x, hx⟩ ⟨y, hy⟩ f
    simp only [cast, val, natCast_eq_natCast_iff',
      Nat.mod_eq_of_lt (hx.trans_le h), Nat.mod_eq_of_lt (hy.trans_le h)] at f
    apply Fin.ext
    exact f
Cleared hypotheses: m, nzm, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
nzm : NeZero m
h : m ≤ n
zero : ∀ [nzm : NeZero (R := ℕ) 0] (h : 0 ≤ n), Injective (α := ZMod 0) (β := ZMod n) cast
⊢ Injective (α := ZMod m) (β := ZMod n) cast
have succ : ∀ (m : ℕ) [nzm : NeZero (m + 1)] (h : m + 1 ≤ n), Injective (α := ZMod (m + 1)) (β := ZMod n) cast
Tactic: cases m with
  | zero => cases nzm; simp_all
  | succ m =>
    rintro ⟨x, hx⟩ ⟨y, hy⟩ f
    simp only [cast, val, natCast_eq_natCast_iff',
      Nat.mod_eq_of_lt (hx.trans_le h), Nat.mod_eq_of_lt (hy.trans_le h)] at f
    apply Fin.ext
    exact f
Cleared hypotheses: m, nzm, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
inst : NeZero m
h : m ≤ n
a : ZMod m
⊢ Eq (α := ZMod n) a.cast 0 ↔ a = 0
have rw : Eq (α := ZMod n) a.cast (cast (n := m) 0) ↔ a = 0
Tactic: rw [← ZMod.cast_zero (n := m)]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Injective (α := ZMod n) val
have zero : ∀ [NeZero (R := ℕ) 0], Injective (α := ZMod 0) val
Tactic: cases n
Cleared hypotheses: n, inst
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
zero : ∀ [NeZero (R := ℕ) 0], Injective (α := ZMod 0) val
⊢ Injective (α := ZMod n) val
have succ : ∀ (n : ℕ) [NeZero (n + 1)], Injective (α := ZMod (n + 1)) val
Tactic: cases n
Cleared hypotheses: n, inst
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero (n + 1)
a b : ZMod (n + 1)
h : a.val = b.val
⊢ a = b
have succ : (↑a : ℕ) = (↑b : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
⊢ val (n := n) 1 = 1 % n
have rw : val (n := n) (↑1 : ZMod n) = 1 % n
Tactic: rw [← Nat.cast_one, val_natCast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
rw : val (n := n) (↑1 : ZMod n) = 1 % n
⊢ val (n := n) 1 = 1 % n
have rw₁ : 1 % n = 1 % n
Tactic: rw [← Nat.cast_one, val_natCast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
⊢ val (n := n) 2 = 2 % n
have rw : val (n := n) (↑2 : ZMod n) = 2 % n
Tactic: rw [← Nat.cast_two, val_natCast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
rw : val (n := n) (↑2 : ZMod n) = 2 % n
⊢ val (n := n) 2 = 2 % n
have rw₁ : 2 % n = 2 % n
Tactic: rw [← Nat.cast_two, val_natCast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : Fact (1 < n)
⊢ val (n := n) 1 = 1
have rw : 1 % n = 1
Tactic: rw [val_one_eq_one_mod]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
⊢ (a + b).val = (a.val + b.val) % n
have zero : ∀ [NeZero (R := ℕ) 0] (a b : ZMod 0), (a + b).val = (a.val + b.val) % 0
Tactic: cases n
Cleared hypotheses: n, inst, a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
zero : ∀ [NeZero (R := ℕ) 0] (a b : ZMod 0), (a + b).val = (a.val + b.val) % 0
⊢ (a + b).val = (a.val + b.val) % n
have succ : ∀ (n : ℕ) [NeZero (n + 1)] (a b : ZMod (n + 1)), (a + b).val = (a.val + b.val) % (n + 1)
Tactic: cases n
Cleared hypotheses: n, inst, a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
⊢ NeZero n
have out : n ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
⊢ (a + b).val = a.val + b.val
have this : NeZero n
Tactic: have : NeZero n := by constructor; rintro rfl; simp at h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
this : NeZero n
⊢ (a + b).val = a.val + b.val
have rw : (a.val + b.val) % n = a.val + b.val
Tactic: rw [ZMod.val_add, Nat.mod_eq_of_lt h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
this : NeZero n
rw : (a.val + b.val) % n = a.val + b.val
⊢ (a + b).val = a.val + b.val
have rw₁ : a.val + b.val = a.val + b.val
Tactic: rw [ZMod.val_add, Nat.mod_eq_of_lt h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ a.val + b.val = (a + b).val + n
have rw : n ≤ a.val % n + b.val % n
Tactic: rw [val_add, Nat.add_mod_add_of_le_add_mod, Nat.mod_eq_of_lt (val_lt _),
    Nat.mod_eq_of_lt (val_lt _)]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ n ≤ a.val % n + b.val % n
have rwa : n ≤ a.val + b.val % n
Tactic: rwa [Nat.mod_eq_of_lt (val_lt _), Nat.mod_eq_of_lt (val_lt _)]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ (a + b).val = a.val + b.val - n
have rw : (a + b).val = (a + b).val + n - n
Tactic: rw [val_add_val_of_le h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : ZMod n
⊢ (a + b).val ≤ a.val + b.val
have zero : ∀ (a b : ZMod 0), (a + b).val ≤ a.val + b.val
Tactic: cases n
Cleared hypotheses: n, a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : ZMod n
zero : ∀ (a b : ZMod 0), (a + b).val ≤ a.val + b.val
⊢ (a + b).val ≤ a.val + b.val
have succ : ∀ (n : ℕ) (a b : ZMod (n + 1)), (a + b).val ≤ a.val + b.val
Tactic: cases n
Cleared hypotheses: n, a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : ZMod n
⊢ (a * b).val = a.val * b.val % n
have zero : ∀ (a b : ZMod 0), (a * b).val = a.val * b.val % 0
Tactic: cases n
Cleared hypotheses: n, a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : ZMod n
zero : ∀ (a b : ZMod 0), (a * b).val = a.val * b.val % 0
⊢ (a * b).val = a.val * b.val % n
have succ : ∀ (n : ℕ) (a b : ZMod (n + 1)), (a * b).val = a.val * b.val % (n + 1)
Tactic: cases n
Cleared hypotheses: n, a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a b : ZMod 0
⊢ (a * b).val = a.val * b.val % 0
have zero : (a * b).val = a.val * b.val
Tactic: rw [Nat.mod_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : ZMod n
⊢ (a * b).val ≤ a.val * b.val
have rw : a.val * b.val % n ≤ a.val * b.val
Tactic: rw [val_mul]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val
have rw : a.val * b.val % n = a.val * b.val
Tactic: rw [val_mul]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
⊢ (a * b).val = a.val * b.val ↔ a.val * b.val < n
have mp : (a * b).val = a.val * b.val → a.val * b.val < n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
mp : (a * b).val = a.val * b.val → a.val * b.val < n
⊢ (a * b).val = a.val * b.val ↔ a.val * b.val < n
have mpr : a.val * b.val < n → (a * b).val = a.val * b.val
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ a.val * b.val < n
have mp : (a * b).val < n
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n_1 n : ℕ
inst : Fact (1 < n)
h : Eq (α := ZMod n) 0 1
⊢ 0 = val (n := n) 0
have rw : Eq (α := ℕ) 0 0
Tactic: rw [val_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
⊢ Eq (α := ZMod n) 1 0 ↔ n = 1
have rw : Eq (α := ZMod n) (↑1 : ZMod n) 0 ↔ n = 1
Tactic: rw [← Nat.cast_one, natCast_eq_zero_iff, Nat.dvd_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
rw : Eq (α := ZMod n) (↑1 : ZMod n) 0 ↔ n = 1
⊢ Eq (α := ZMod n) 1 0 ↔ n = 1
have rw₁ : n ∣ 1 ↔ n = 1
Tactic: rw [← Nat.cast_one, natCast_eq_zero_iff, Nat.dvd_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
rw : Eq (α := ZMod n) (↑1 : ZMod n) 0 ↔ n = 1
rw₁ : n ∣ 1 ↔ n = 1
⊢ Eq (α := ZMod n) 1 0 ↔ n = 1
have rw₂ : n = 1 ↔ n = 1
Tactic: rw [← Nat.cast_one, natCast_eq_zero_iff, Nat.dvd_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
⊢ a * a⁻¹ = (↑(a.val.gcd n) : ZMod n)
have zero : ∀ (a : ZMod 0), a * a⁻¹ = (↑(a.val.gcd 0) : ZMod 0)
Tactic: rcases n with - | n
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
zero : ∀ (a : ZMod 0), a * a⁻¹ = (↑(a.val.gcd 0) : ZMod 0)
⊢ a * a⁻¹ = (↑(a.val.gcd n) : ZMod n)
have succ : ∀ (n : ℕ) (a : ZMod (n + 1)), a * a⁻¹ = (↑(a.val.gcd (n + 1)) : ZMod (n + 1))
Tactic: rcases n with - | n
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℤ
⊢ a * a.sign = (↑a.natAbs : ℤ)
have rw : Eq (α := ℤ) (↑a.natAbs : ℤ) (↑a.natAbs : ℤ)
Tactic: rw [Int.mul_sign_self]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℤ
⊢ Eq (α := ℤ) (↑a.natAbs : ℤ) (↑(a.natAbs.gcd 0) : ℤ)
have rw : Eq (α := ℤ) (↑a.natAbs : ℤ) (↑a.natAbs : ℤ)
Tactic: rw [Nat.gcd_zero_right]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℤ
⊢ a * a⁻¹ = (↑((val (n := 0) a).gcd 0) : ℤ)
have _ : a * a.sign = (↑a.natAbs : ℤ)
Tactic: calc
      _ = a * Int.sign a := rfl
      _ = a.natAbs := by rw [Int.mul_sign_self]
      _ = a.natAbs.gcd 0 := by rw [Nat.gcd_zero_right]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℤ
_ : a * a.sign = (↑a.natAbs : ℤ)
⊢ a * a⁻¹ = (↑((val (n := 0) a).gcd 0) : ℤ)
have _₁ : Eq (α := ℤ) (↑a.natAbs : ℤ) (↑(a.natAbs.gcd 0) : ℤ)
Tactic: calc
      _ = a * Int.sign a := rfl
      _ = a.natAbs := by rw [Int.mul_sign_self]
      _ = a.natAbs.gcd 0 := by rw [Nat.gcd_zero_right]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) (↑n.succ : ZMod (n + 1)) (↑(a.val.gcdB n.succ) : ZMod (n + 1))
have rw : a * a⁻¹ = a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) 0 (↑(a.val.gcdB n.succ) : ZMod (n + 1))
Tactic: rw [natCast_self, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
rw : a * a⁻¹ = a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) 0 (↑(a.val.gcdB n.succ) : ZMod (n + 1))
⊢ a * a⁻¹ = a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) (↑n.succ : ZMod (n + 1)) (↑(a.val.gcdB n.succ) : ZMod (n + 1))
have rw₁ : a * a⁻¹ = a * a⁻¹ + 0
Tactic: rw [natCast_self, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
rw : a * a⁻¹ = a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) 0 (↑(a.val.gcdB n.succ) : ZMod (n + 1))
rw₁ : a * a⁻¹ = a * a⁻¹ + 0
⊢ a * a⁻¹ = a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) (↑n.succ : ZMod (n + 1)) (↑(a.val.gcdB n.succ) : ZMod (n + 1))
have rw₂ : a * a⁻¹ = a * a⁻¹
Tactic: rw [natCast_self, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) (↑n.succ : ZMod (n + 1)) (↑(a.val.gcdB n.succ) : ZMod (n + 1)) =
    (↑((↑a.val : ℤ) * a.val.gcdA n.succ + (↑n.succ : ℤ) * a.val.gcdB n.succ) : ZMod (n + 1))
have push_cast : a * a⁻¹ + HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 * (↑(a.val.gcdB n.succ) : ZMod (n + 1)) =
  HMul.hMul (α := ZMod (n + 1)) (↑a.val : ZMod (n + 1)) (↑(a.val.gcdA n.succ) : ZMod (n + 1)) +
    HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 * (↑(a.val.gcdB n.succ) : ZMod (n + 1))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ + HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 * (↑(a.val.gcdB n.succ) : ZMod (n + 1)) =
    HMul.hMul (α := ZMod (n + 1)) (↑a.val : ZMod (n + 1)) (↑(a.val.gcdA n.succ) : ZMod (n + 1)) +
      HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 * (↑(a.val.gcdB n.succ) : ZMod (n + 1))
have rw : a * a⁻¹ + HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 * (↑(a.val.gcdB n.succ) : ZMod (n + 1)) =
  a * (↑(a.val.gcdA n.succ) : ZMod (n + 1)) +
    HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 * (↑(a.val.gcdB n.succ) : ZMod (n + 1))
Tactic: rw [natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
⊢ Eq (α := ZMod (n + 1)) (↑((↑a.val : ℤ) * a.val.gcdA n.succ + (↑n.succ : ℤ) * a.val.gcdB n.succ) : ZMod (n + 1))
    (↑(a.val.gcd n.succ) : ZMod (n + 1))
have rw : Eq (α := ZMod (n + 1)) (↑(↑(a.val.gcd n.succ) : ℤ) : ZMod (n + 1)) (↑(a.val.gcd n.succ) : ZMod (n + 1))
Tactic: rw [← Nat.gcd_eq_gcd_ab a.val n.succ]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = (↑(a.val.gcd (n + 1)) : ZMod (n + 1))
have a₁ : a * a⁻¹ = a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) (↑n.succ : ZMod (n + 1)) (↑(a.val.gcdB n.succ) : ZMod (n + 1))
Tactic: calc
      a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by
        rw [natCast_self, zero_mul, add_zero]
      _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) := by
        push_cast
        rw [natCast_zmod_val]
        rfl
      _ = Nat.gcd a.val n.succ := by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
a₁ : a * a⁻¹ = a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) (↑n.succ : ZMod (n + 1)) (↑(a.val.gcdB n.succ) : ZMod (n + 1))
⊢ a * a⁻¹ = (↑(a.val.gcd (n + 1)) : ZMod (n + 1))
have a₂ : a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) (↑n.succ : ZMod (n + 1)) (↑(a.val.gcdB n.succ) : ZMod (n + 1)) =
  (↑((↑a.val : ℤ) * a.val.gcdA n.succ + (↑n.succ : ℤ) * a.val.gcdB n.succ) : ZMod (n + 1))
Tactic: calc
      a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by
        rw [natCast_self, zero_mul, add_zero]
      _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) := by
        push_cast
        rw [natCast_zmod_val]
        rfl
      _ = Nat.gcd a.val n.succ := by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
a₁ : a * a⁻¹ = a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) (↑n.succ : ZMod (n + 1)) (↑(a.val.gcdB n.succ) : ZMod (n + 1))
a₂ :
  a * a⁻¹ + HMul.hMul (α := ZMod (n + 1)) (↑n.succ : ZMod (n + 1)) (↑(a.val.gcdB n.succ) : ZMod (n + 1)) =
    (↑((↑a.val : ℤ) * a.val.gcdA n.succ + (↑n.succ : ℤ) * a.val.gcdB n.succ) : ZMod (n + 1))
⊢ a * a⁻¹ = (↑(a.val.gcd (n + 1)) : ZMod (n + 1))
have a₃ : Eq (α := ZMod (n + 1)) (↑((↑a.val : ℤ) * a.val.gcdA n.succ + (↑n.succ : ℤ) * a.val.gcdB n.succ) : ZMod (n + 1))
  (↑(a.val.gcd n.succ) : ZMod (n + 1))
Tactic: calc
      a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by
        rw [natCast_self, zero_mul, add_zero]
      _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) := by
        push_cast
        rw [natCast_zmod_val]
        rfl
      _ = Nat.gcd a.val n.succ := by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
⊢ Eq (α := ZMod n) 1⁻¹ 1
have inl : Eq (α := ZMod 1) 1⁻¹ 1
Tactic: obtain rfl | hn := eq_or_ne n 1
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inl : Eq (α := ZMod 1) 1⁻¹ 1
⊢ Eq (α := ZMod n) 1⁻¹ 1
have inr : ∀ (hn : n ≠ 1), Eq (α := ZMod n) 1⁻¹ 1
Tactic: obtain rfl | hn := eq_or_ne n 1
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℤ
⊢ Eq (α := ZMod 2) (↑n : ZMod 2) 1 ↔ Odd n
have rw : n % (↑2 : ℤ) = HMod.hMod (α := ℤ) 1 (↑2 : ℤ) ↔ n % 2 = 1
Tactic: rw [← Int.cast_one, ZMod.intCast_eq_intCast_iff, Int.odd_iff, Int.ModEq]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n x : ℕ
h : x.Coprime n
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
have h₁ : (x % n).gcd n = 1
Tactic: rw [Nat.Coprime, Nat.gcd_comm, Nat.gcd_rec] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n x : ℕ
h : (x % n).gcd n = 1
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
have rw : Eq (α := ZMod n) (↑((val (n := n) (↑x : ZMod n)).gcd n) : ZMod n) 1
Tactic: rw [mul_inv_eq_gcd, val_natCast, h, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n x : ℕ
h : (x % n).gcd n = 1
rw : Eq (α := ZMod n) (↑((val (n := n) (↑x : ZMod n)).gcd n) : ZMod n) 1
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
have rw₁ : Eq (α := ZMod n) (↑((x % n).gcd n) : ZMod n) 1
Tactic: rw [mul_inv_eq_gcd, val_natCast, h, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n x : ℕ
h : (x % n).gcd n = 1
rw : Eq (α := ZMod n) (↑((val (n := n) (↑x : ZMod n)).gcd n) : ZMod n) 1
rw₁ : Eq (α := ZMod n) (↑((x % n).gcd n) : ZMod n) 1
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
have rw₂ : Eq (α := ZMod n) (↑1 : ZMod n) 1
Tactic: rw [mul_inv_eq_gcd, val_natCast, h, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n x : ℕ
h : (x % n).gcd n = 1
rw : Eq (α := ZMod n) (↑((val (n := n) (↑x : ZMod n)).gcd n) : ZMod n) 1
rw₁ : Eq (α := ZMod n) (↑((x % n).gcd n) : ZMod n) 1
rw₂ : Eq (α := ZMod n) (↑1 : ZMod n) 1
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
have rw₃ : Eq (α := ZMod n) 1 1
Tactic: rw [mul_inv_eq_gcd, val_natCast, h, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
hmn : m.Coprime n
⊢ HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) = 1
have inl : ∀ (hmn : m.Coprime 0), HMul.hMul (α := ZMod 0) (↑m : ZMod 0) (↑(val (n := 0) (↑m : ZMod 0)⁻¹) : ZMod 0) = 1
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n, hmn
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
hmn : m.Coprime n
inl : ∀ (hmn : m.Coprime 0), HMul.hMul (α := ZMod 0) (↑m : ZMod 0) (↑(val (n := 0) (↑m : ZMod 0)⁻¹) : ZMod 0) = 1
⊢ HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) = 1
have inr : ∀ (hn : n ≠ 0), HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) = 1
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
⊢ HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) = 1
have this : NeZero n
Tactic: haveI : NeZero n := ⟨hn⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
this : NeZero n
⊢ HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) = 1
have inr : HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑m : ZMod n)⁻¹ = 1
Tactic: rw [ZMod.natCast_zmod_val, ZMod.coe_mul_inv_eq_one _ hmn]