awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : NonAssocSemiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))
⊢ Eq (α := R) ((φ : (a : ℤ) → R) k : R) ((ψ : (a : ℤ) → R) k : R)
have a : Eq (α := R) ((ψ : (a : ℤ) → R) k : R) ((ψ : (a : ℤ) → R) k : R)
Tactic: rw [φ.ext_int ψ]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Semiring R
f g : ZMod n ≃+* R
⊢ f = g
have rw : Eq (α := ZMod n →+* R) (↑f : ZMod n →+* R) (↑g : ZMod n →+* R)
Tactic: rw [RingEquiv.coe_ringHom_inj_iff]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : NonAssocRing R
f : R →+* ZMod n
k : ZMod n
⊢ (f : (a : R) → ZMod n) k.cast = k
have zero : ∀ (f : R →+* ZMod 0) (k : ZMod 0), (f : (a : R) → ZMod 0) k.cast = k
Tactic: cases n
Cleared hypotheses: n, f, k
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : NonAssocRing R
f : R →+* ZMod n
k : ZMod n
zero : ∀ (f : R →+* ZMod 0) (k : ZMod 0), (f : (a : R) → ZMod 0) k.cast = k
⊢ (f : (a : R) → ZMod n) k.cast = k
have succ : ∀ (n : ℕ) (f : R →+* ZMod (n + 1)) (k : ZMod (n + 1)), (f : (a : R) → ZMod (n + 1)) k.cast = k
Tactic: cases n
Cleared hypotheses: n, f, k
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
f : R →+* ZMod 0
k : ZMod 0
⊢ (f : (a : R) → ZMod 0) k.cast = k
have zero : (f : (a : R) → ℤ) (↑k : R) = k
Tactic: dsimp +instances [ZMod, ZMod.cast] at f k ⊢
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
n : ℕ
f : R →+* ZMod (n + 1)
k : ZMod (n + 1)
⊢ (f : (a : R) → ZMod (n + 1)) k.cast = k
have succ : (f : (a : R) → ZMod (n + 1)) (↑k.val : R) = k
Tactic: dsimp [ZMod.cast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
n : ℕ
f : R →+* ZMod (n + 1)
k : ZMod (n + 1)
⊢ (f : (a : R) → ZMod (n + 1)) (↑k.val : R) = k
have succ : (↑k.val : ZMod (n + 1)) = k
Tactic: rw [map_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
n : ℕ
f : R →+* ZMod (n + 1)
k : ZMod (n + 1)
succ : (↑k.val : ZMod (n + 1)) = k
⊢ (f : (a : R) → ZMod (n + 1)) (↑k.val : R) = k
have succ₁ : k = k
Tactic: rw [map_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
A : Type u_2
inst : AddGroup A
f : ℤ →+ A
⊢ Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) ↔
    AddMonoidHom.ker (M := ZMod n) (Int.castAddHom (ZMod n)) ≤ f.ker
have rw : Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) ↔ AddSubgroup.zmultiples (↑n : ℤ) ≤ f.ker
Tactic: rw [ker_intCastAddHom]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
A : Type u_2
inst : AddGroup A
f : ℤ →+ A
⊢ Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) ↔ AddSubgroup.zmultiples (↑n : ℤ) ≤ f.ker
have mp : Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) → AddSubgroup.zmultiples (↑n : ℤ) ≤ f.ker
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
A : Type u_2
inst : AddGroup A
f : ℤ →+ A
mp : Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) → AddSubgroup.zmultiples (↑n : ℤ) ≤ f.ker
⊢ Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A) ↔ AddSubgroup.zmultiples (↑n : ℤ) ≤ f.ker
have mpr : AddSubgroup.zmultiples (↑n : ℤ) ≤ f.ker → Eq (α := A) ((f : (a : ℤ) → A) (↑n : ℤ) : A) (0 : A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : Nontrivial G
inst_2 : Module (ZMod 1) G
⊢ False
have obtain : ∀ (x : G) (hx : x ≠ 0), False
Tactic: obtain ⟨x, hx⟩ := exists_ne (0 : G)
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
G : Type u_2
inst : AddCommGroup G
inst_1 : Module (ZMod n) G
inst_2 : NeZero n
inst_3 : Nontrivial G
⊢ 2 ≤ n
have this : n ≠ 0
Tactic: have := NeZero.ne n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
G : Type u_2
inst : AddCommGroup G
inst_1 : Module (ZMod n) G
inst_2 : NeZero n
inst_3 : Nontrivial G
this : n ≠ 0
⊢ 2 ≤ n
have this₁ : n ≠ 1
Tactic: have := char_ne_one n G
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
α : Type u_1
inst : Group α
n : ℕ
hn : (Nat.card α).gcd n = 1
a : α
⊢ (a ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) ^ n = a
have hn₁ : (Nat.card α).Coprime n
Tactic: replace hn : (Nat.card α).Coprime n := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
α : Type u_1
inst : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
⊢ (a ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) ^ n = a
have rw : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) = a
Tactic: rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
    ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
α : Type u_1
inst : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
rw : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) = a
⊢ (a ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) ^ n = a
have rw₁ : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹ % Nat.card α) = a
Tactic: rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
    ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
α : Type u_1
inst : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
rw : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) = a
rw₁ : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹ % Nat.card α) = a
⊢ (a ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) ^ n = a
have rw₂ : a ^ val (n := Nat.card α) (↑(n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) : ZMod (Nat.card α)) = a
Tactic: rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
    ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
α : Type u_1
inst : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
rw : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) = a
rw₁ : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹ % Nat.card α) = a
rw₂ : a ^ val (n := Nat.card α) (↑(n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) : ZMod (Nat.card α)) = a
⊢ (a ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) ^ n = a
have rw₃ : a ^
    (HMul.hMul (α := ZMod (Nat.card α)) (↑n : ZMod (Nat.card α))
        (↑(val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) : ZMod (Nat.card α))).val =
  a
Tactic: rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
    ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
α : Type u_1
inst : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
rw : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) = a
rw₁ : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹ % Nat.card α) = a
rw₂ : a ^ val (n := Nat.card α) (↑(n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) : ZMod (Nat.card α)) = a
rw₃ :
  a ^
      (HMul.hMul (α := ZMod (Nat.card α)) (↑n : ZMod (Nat.card α))
          (↑(val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) : ZMod (Nat.card α))).val =
    a
⊢ (a ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) ^ n = a
have rw₄ : a ^ val (n := Nat.card α) 1 = a
Tactic: rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
    ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
α : Type u_1
inst : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
rw : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) = a
rw₁ : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹ % Nat.card α) = a
rw₂ : a ^ val (n := Nat.card α) (↑(n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) : ZMod (Nat.card α)) = a
rw₃ :
  a ^
      (HMul.hMul (α := ZMod (Nat.card α)) (↑n : ZMod (Nat.card α))
          (↑(val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) : ZMod (Nat.card α))).val =
    a
rw₄ : a ^ val (n := Nat.card α) 1 = a
⊢ (a ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) ^ n = a
have rw₅ : a ^ (1 % Nat.card α) = a
Tactic: rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
    ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
α : Type u_1
inst : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
rw : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) = a
rw₁ : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹ % Nat.card α) = a
rw₂ : a ^ val (n := Nat.card α) (↑(n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) : ZMod (Nat.card α)) = a
rw₃ :
  a ^
      (HMul.hMul (α := ZMod (Nat.card α)) (↑n : ZMod (Nat.card α))
          (↑(val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) : ZMod (Nat.card α))).val =
    a
rw₄ : a ^ val (n := Nat.card α) 1 = a
rw₅ : a ^ (1 % Nat.card α) = a
⊢ (a ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) ^ n = a
have rw₆ : HPow.hPow (β := ℕ) a 1 = a
Tactic: rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
    ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
α : Type u_1
inst : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
rw : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) = a
rw₁ : a ^ (n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹ % Nat.card α) = a
rw₂ : a ^ val (n := Nat.card α) (↑(n * val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) : ZMod (Nat.card α)) = a
rw₃ :
  a ^
      (HMul.hMul (α := ZMod (Nat.card α)) (↑n : ZMod (Nat.card α))
          (↑(val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) : ZMod (Nat.card α))).val =
    a
rw₄ : a ^ val (n := Nat.card α) 1 = a
rw₅ : a ^ (1 % Nat.card α) = a
rw₆ : HPow.hPow (β := ℕ) a 1 = a
⊢ (a ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) ^ n = a
have rw₇ : a = a
Tactic: rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
    ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
α : Type u_1
inst : Group α
n : ℕ
hn : (Nat.card α).gcd n = 1
a : α
⊢ (a ^ n) ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹ = a
have rw : (a ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) ^ n = a
Tactic: rw [pow_right_comm, pow_zmod_val_inv_pow hn]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
α : Type u_1
inst : Group α
n : ℕ
hn : (Nat.card α).gcd n = 1
a : α
rw : (a ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹) ^ n = a
⊢ (a ^ n) ^ val (n := Nat.card α) (↑n : ZMod (Nat.card α))⁻¹ = a
have rw₁ : a = a
Tactic: rw [pow_right_comm, pow_zmod_val_inv_pow hn]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m k : ℕ
⊢ Eq (α := Set ℕ) (Set.range fun (n : ℕ) ↦ m * n + k) {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n}
have h : ∀ (n : ℕ),
  Membership.mem (γ := Set ℕ) (Set.range fun (n : ℕ) ↦ m * n + k) n ↔
    Membership.mem (γ := Set ℕ) {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m k n : ℕ
| (∃ (y : ℕ), m * y + k = n) ↔ Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
have h : ∀ (y : ℕ), m * y + k = n
Tactic: enter [1, 1, y]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m k n y : ℕ
| m * y + k = n
have h : n = k + m * y
Tactic: rw [add_comm, eq_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m k n : ℕ
| (∃ (y : ℕ), m * y + k = n) ↔ Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
have h : ∀ (y : ℕ), n = k + m * y
Tactic: enter [1, 1, y]; rw [add_comm, eq_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m k n : ℕ
⊢ (∃ (y : ℕ), m * y + k = n) ↔ Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
have h : (∃ (y : ℕ), n = k + m * y) ↔ Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
Tactic: conv => enter [1, 1, y]; rw [add_comm, eq_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m k n : ℕ
⊢ (∃ (y : ℕ), n = k + m * y) ↔ Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
have h : (∃ (y : ℕ), n = k + m * y) → ∀ (a : ℕ) (ha : n = k + m * a), Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)
Tactic: refine ⟨fun ⟨a, ha⟩ ↦ ⟨?_, le_iff_exists_add.mpr ⟨_, ha⟩⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m k n : ℕ
h : (∃ (y : ℕ), n = k + m * y) → ∀ (a : ℕ) (ha : n = k + m * a), Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)
⊢ (∃ (y : ℕ), n = k + m * y) ↔ Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
have h₁ : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n →
  ∀ (H₁ : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)) (H₂ : k ≤ n), ∃ (y : ℕ), n = k + m * y
Tactic: refine ⟨fun ⟨a, ha⟩ ↦ ⟨?_, le_iff_exists_add.mpr ⟨_, ha⟩⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m k n : ℕ
h : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
H₁ : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)
H₂ : k ≤ n
⊢ ∃ (y : ℕ), n = k + m * y
have h : ∀ (a : ℕ) (ha : n = k + a), ∃ (y : ℕ), n = k + m * y
Tactic: obtain ⟨a, ha⟩ := le_iff_exists_add.mp H₂
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
m k n : ℕ
h : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
H₁ : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)
H₂ : k ≤ n
a : ℕ
ha : n = k + a
⊢ ∃ (y : ℕ), n = k + m * y
have H₃ : m ∣ a
Tactic: simp only [ha, Nat.cast_add, add_eq_left, ZMod.natCast_eq_zero_iff] at H₁
Cleared hypotheses: H₁
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m k n : ℕ
h : Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n
H₂ : k ≤ n
a : ℕ
ha : n = k + a
H₁ : m ∣ a
⊢ ∃ (y : ℕ), n = k + m * y
have h : ∀ (b : ℕ) (ha : n = k + m * b), ∃ (y : ℕ), n = k + m * y
Tactic: obtain ⟨b, rfl⟩ := H₁
Cleared hypotheses: a, ha, H₁
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
N : ℕ
inst : NeZero N
p : ZMod N × ℕ
⊢ (fun (n : ℕ) ↦ (((↑n : ZMod N), n / N) : ZMod N × ℕ)) ((fun (p : ZMod N × ℕ) ↦ p.1.val + N * p.2) p) = p
have fst : ((fun (n : ℕ) ↦ (((↑n : ZMod N), n / N) : ZMod N × ℕ)) ((fun (p : ZMod N × ℕ) ↦ p.1.val + N * p.2) p)).1 = p.1
Tactic: ext1
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
N : ℕ
inst : NeZero N
p : ZMod N × ℕ
fst : ((fun (n : ℕ) ↦ (((↑n : ZMod N), n / N) : ZMod N × ℕ)) ((fun (p : ZMod N × ℕ) ↦ p.1.val + N * p.2) p)).1 = p.1
⊢ (fun (n : ℕ) ↦ (((↑n : ZMod N), n / N) : ZMod N × ℕ)) ((fun (p : ZMod N × ℕ) ↦ p.1.val + N * p.2) p) = p
have snd : ((fun (n : ℕ) ↦ (((↑n : ZMod N), n / N) : ZMod N × ℕ)) ((fun (p : ZMod N × ℕ) ↦ p.1.val + N * p.2) p)).2 = p.2
Tactic: ext1
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
M : Type u_1
inst : AddCommMonoid M
⊢ Subsingleton.{max (u_1 + 1) 1} (Module (ZMod n) M)
have zero : Subsingleton.{max (u_1 + 1) 1} (Module (ZMod 0) M)
Tactic: obtain _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
M : Type u_1
inst : AddCommMonoid M
zero : Subsingleton.{max (u_1 + 1) 1} (Module (ZMod 0) M)
⊢ Subsingleton.{max (u_1 + 1) 1} (Module (ZMod n) M)
have succ : ∀ (n : ℕ), Subsingleton.{max (u_1 + 1) 1} (Module (ZMod (n + 1)) M)
Tactic: obtain _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
n : ℕ
⊢ Subsingleton.{max (u_1 + 1) 1} (Module (ZMod (n + 1)) M)
have succ : ∀ (m1 m2 : Module (ZMod (n + 1)) M) (r : ZMod (n + 1)) (m : M), r • m = r • m
Tactic: refine ⟨fun m1 m2 ↦ Module.ext' _ _ fun r m ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
n : ℕ
m1 m2 : Module (ZMod (n + 1)) M
r : ZMod (n + 1)
m : M
⊢ r • m = r • m
have succ : ∀ (r : ℕ), HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) m = HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) m
Tactic: obtain ⟨r, rfl⟩ := ZMod.natCast_zmod_surjective r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
n : ℕ
m1 m2 : Module (ZMod (n + 1)) M
m : M
r : ℕ
⊢ HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) m = HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) m
have succ : r • m = HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) m
Tactic: rw [(letI := m1; Nat.cast_smul_eq_nsmul _ r m), Nat.cast_smul_eq_nsmul _ r m]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
n : ℕ
m1 m2 : Module (ZMod (n + 1)) M
m : M
r : ℕ
succ : r • m = HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) m
⊢ HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) m = HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) m
have succ₁ : r • m = r • m
Tactic: rw [(letI := m1; Nat.cast_smul_eq_nsmul _ r m), Nat.cast_smul_eq_nsmul _ r m]
-- Lean 4 proof step from Mathlib.Data.ZMod.Coprime (goal)
Goal:
n : ℤ
m : ℕ
⊢ IsUnit (M := ZMod m) (↑n : ZMod m) ↔ IsCoprime (↑m : ℤ) n
have rw : Associated (M := ZMod m) (↑n : ZMod m) (↑n.natAbs : ZMod (↑m : ℤ).natAbs)
Tactic: rw [Int.isCoprime_iff_nat_coprime, Nat.coprime_comm, ← isUnit_iff_coprime, Associated.isUnit_iff]
-- Lean 4 proof step from Mathlib.Data.ZMod.Coprime (goal)
Goal:
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ a.gcd (↑p : ℤ) ≠ 1
have rw : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬a.gcd (↑p : ℤ) = 1
Tactic: rw [Ne, Int.gcd_comm, ← Int.isCoprime_iff_gcd_eq_one,
    (Nat.prime_iff_prime_int.1 pp.1).coprime_iff_not_dvd, Classical.not_not,
    intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Coprime (goal)
Goal:
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
rw : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬a.gcd (↑p : ℤ) = 1
⊢ Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ a.gcd (↑p : ℤ) ≠ 1
have rw₁ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬Int.gcd (↑p : ℤ) a = 1
Tactic: rw [Ne, Int.gcd_comm, ← Int.isCoprime_iff_gcd_eq_one,
    (Nat.prime_iff_prime_int.1 pp.1).coprime_iff_not_dvd, Classical.not_not,
    intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Coprime (goal)
Goal:
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
rw : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬a.gcd (↑p : ℤ) = 1
rw₁ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬Int.gcd (↑p : ℤ) a = 1
⊢ Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ a.gcd (↑p : ℤ) ≠ 1
have rw₂ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬IsCoprime (↑p : ℤ) a
Tactic: rw [Ne, Int.gcd_comm, ← Int.isCoprime_iff_gcd_eq_one,
    (Nat.prime_iff_prime_int.1 pp.1).coprime_iff_not_dvd, Classical.not_not,
    intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Coprime (goal)
Goal:
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
rw : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬a.gcd (↑p : ℤ) = 1
rw₁ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬Int.gcd (↑p : ℤ) a = 1
rw₂ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬IsCoprime (↑p : ℤ) a
⊢ Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ a.gcd (↑p : ℤ) ≠ 1
have rw₃ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬¬(↑p : ℤ) ∣ a
Tactic: rw [Ne, Int.gcd_comm, ← Int.isCoprime_iff_gcd_eq_one,
    (Nat.prime_iff_prime_int.1 pp.1).coprime_iff_not_dvd, Classical.not_not,
    intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Coprime (goal)
Goal:
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
rw : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬a.gcd (↑p : ℤ) = 1
rw₁ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬Int.gcd (↑p : ℤ) a = 1
rw₂ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬IsCoprime (↑p : ℤ) a
rw₃ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬¬(↑p : ℤ) ∣ a
⊢ Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ a.gcd (↑p : ℤ) ≠ 1
have rw₄ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ (↑p : ℤ) ∣ a
Tactic: rw [Ne, Int.gcd_comm, ← Int.isCoprime_iff_gcd_eq_one,
    (Nat.prime_iff_prime_int.1 pp.1).coprime_iff_not_dvd, Classical.not_not,
    intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Coprime (goal)
Goal:
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
rw : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬a.gcd (↑p : ℤ) = 1
rw₁ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬Int.gcd (↑p : ℤ) a = 1
rw₂ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬IsCoprime (↑p : ℤ) a
rw₃ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ ¬¬(↑p : ℤ) ∣ a
rw₄ : Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ (↑p : ℤ) ∣ a
⊢ Eq (α := ZMod p) (↑a : ZMod p) 0 ↔ a.gcd (↑p : ℤ) ≠ 1
have rw₅ : (↑p : ℤ) ∣ a ↔ (↑p : ℤ) ∣ a
Tactic: rw [Ne, Int.gcd_comm, ← Int.isCoprime_iff_gcd_eq_one,
    (Nat.prime_iff_prime_int.1 pp.1).coprime_iff_not_dvd, Classical.not_not,
    intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℤ
⊢ (↑(↑x : Fin n) : ℕ) = (x % (↑n : ℤ)).toNat
have rw : (↑(if 0 ≤ x then (↑x.natAbs : Fin n) else -(↑x.natAbs : Fin n)) : ℕ) = (x % (↑n : ℤ)).toNat
Tactic: rw [Fin.intCast_def']
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℤ
⊢ (↑(if 0 ≤ x then (↑x.natAbs : Fin n) else -(↑x.natAbs : Fin n)) : ℕ) = (x % (↑n : ℤ)).toNat
have isTrue : 0 ≤ x → (↑(↑x.natAbs : Fin n) : ℕ) = (x % (↑n : ℤ)).toNat
Tactic: split
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℤ
isTrue : 0 ≤ x → (↑(↑x.natAbs : Fin n) : ℕ) = (x % (↑n : ℤ)).toNat
⊢ (↑(if 0 ≤ x then (↑x.natAbs : Fin n) else -(↑x.natAbs : Fin n)) : ℕ) = (x % (↑n : ℤ)).toNat
have isFalse : ¬0 ≤ x → (↑(-(↑x.natAbs : Fin n)) : ℕ) = (x % (↑n : ℤ)).toNat
Tactic: split
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h : ¬0 ≤ x
⊢ (↑(-(↑x.natAbs : Fin n)) : ℕ) = (x % (↑n : ℤ)).toNat
have isFalse : (if n ∣ x.natAbs then 0 else n - x.natAbs % n) = (x % (↑n : ℤ)).toNat
Tactic: simp only [Fin.val_neg, Fin.natCast_eq_zero, Fin.val_natCast]
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h : ¬0 ≤ x
⊢ (if n ∣ x.natAbs then 0 else n - x.natAbs % n) = (x % (↑n : ℤ)).toNat
have isFalse : n ∣ x.natAbs → 0 = (x % (↑n : ℤ)).toNat
Tactic: split
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h : ¬0 ≤ x
isFalse : n ∣ x.natAbs → 0 = (x % (↑n : ℤ)).toNat
⊢ (if n ∣ x.natAbs then 0 else n - x.natAbs % n) = (x % (↑n : ℤ)).toNat
have isFalse₁ : ¬n ∣ x.natAbs → n - x.natAbs % n = (x % (↑n : ℤ)).toNat
Tactic: split
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (hypothesis)
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : n ∣ x.natAbs
⊢ 0 = (x % (↑n : ℤ)).toNat
have h₁ : (↑n : ℤ) ∣ x
Tactic: rw [← Int.natCast_dvd] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : (↑n : ℤ) ∣ x
⊢ 0 = (x % (↑n : ℤ)).toNat
have isFalse : 0 = toNat 0
Tactic: rw [Int.emod_eq_zero_of_dvd h, Int.toNat_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : (↑n : ℤ) ∣ x
isFalse : 0 = toNat 0
⊢ 0 = (x % (↑n : ℤ)).toNat
have isFalse₁ : Eq (α := ℕ) 0 0
Tactic: rw [Int.emod_eq_zero_of_dvd h, Int.toNat_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ ¬(↑n : ℤ) ∣ x
have rwa : ∀ (h : ¬(↑n : ℤ) ∣ x), ¬(↑n : ℤ) ∣ x
Tactic: rwa [← Int.natCast_dvd] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ n - x.natAbs % n = (x % (↑n : ℤ)).toNat
have isFalse : n - (n - (x % (↑n : ℤ)).toNat) = (x % (↑n : ℤ)).toNat
Tactic: rw [Int.emod_natAbs_of_neg (by lia) (NeZero.ne n),
        if_neg (by rwa [← Int.natCast_dvd] at h)]
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (hypothesis)
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ LT.lt (α := ℤ) 0 (↑n : ℤ)
have this : n ≠ 0
Tactic: have := NeZero.ne n
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (hypothesis)
Goal:
n : ℕ
inst : NeZero n
x : ℤ
h_1 : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ n - (n - (x % (↑n : ℤ)).toNat) = (x % (↑n : ℤ)).toNat
have this : x % (↑n : ℤ) < (↑n : ℤ)
Tactic: have : x % n < n := Int.emod_lt_of_pos x (by have := NeZero.ne n; lia)