awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
⊢ HMul.hMul (α := R) a.cast b.cast = (a * b).cast
have succ : HMul.hMul (α := R) (↑(↑a : ℕ) : R) (↑(↑b : ℕ) : R) = (↑(↑(a * b) : ℕ) : R)
Tactic: dsimp [ZMod, ZMod.cast, ZMod.val]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
m : ℕ
inst_1 : CharP R m
n : ℕ
h : m ∣ n + 1
a b : ZMod (n + 1)
⊢ HMul.hMul (α := R) (↑(↑a : ℕ) : R) (↑(↑b : ℕ) : R) = (↑(↑(a * b) : ℕ) : R)
have succ : m ∣ (↑a : ℕ) * (↑b : ℕ) - (↑a : ℕ) * (↑b : ℕ) % (n + 1)
Tactic: rw [← Nat.cast_mul, Fin.val_mul, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _),
    @CharP.cast_eq_zero_iff R _ m]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n m : ℕ
h : m ∣ n
a : ZMod m
⊢ ∃ (a_1 : ZMod n), (castHom h (ZMod m) : (a : ZMod n) → ZMod m) a_1 = a
have 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)
Tactic: obtain ⟨a, rfl⟩ := intCast_surjective a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
⊢ Injective (α := ZMod n) (β := R) (⇑(castHom ⋯ R) : (a : ZMod n) → R)
have rw : ∀ (a : ZMod n), Eq (α := R) ((castHom sorry R : (a : ZMod n) → R) a : R) (0 : R) → a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
x : ZMod n
⊢ Eq (α := R) ((castHom ⋯ R : (a : ZMod n) → R) x : R) (0 : R) → x = 0
have obtain : ∀ (k : ℤ), Eq (α := R) ((castHom sorry R : (a : ZMod n) → R) (↑k : ZMod n) : R) (0 : R) → Eq (α := ZMod n) (↑k : ZMod n) 0
Tactic: obtain ⟨k, rfl⟩ := ZMod.intCast_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
k : ℤ
⊢ Eq (α := R) ((castHom ⋯ R : (a : ZMod n) → R) (↑k : ZMod n) : R) (0 : R) → Eq (α := ZMod n) (↑k : ZMod n) 0
have rw : (↑n : ℤ) ∣ k → (↑n : ℤ) ∣ k
Tactic: rw [map_intCast, CharP.intCast_eq_zero_iff R n, CharP.intCast_eq_zero_iff (ZMod n) n]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
inst_2 : Fintype R
h : Fintype.card R = n
hn : n = 0
⊢ False
have h₁ : Fintype.card R = 0
Tactic: rw [hn] at h
Cleared hypotheses: h, hn
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
inst_2 : Fintype R
h : Fintype.card R = n
⊢ Bijective (α := ZMod n) (β := R) (⇑(castHom ⋯ R) : (a : ZMod n) → R)
have this : NeZero n
Tactic: haveI : NeZero n :=
    ⟨by
      intro hn
      rw [hn] at h
      exact (Fintype.card_eq_zero_iff.mp h).elim' 0⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
inst_2 : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Bijective (α := ZMod n) (β := R) (⇑(castHom ⋯ R) : (a : ZMod n) → R)
have rw : Injective (α := ZMod n) (β := R) (⇑(castHom sorry R) : (a : ZMod n) → R)
Tactic: rw [Fintype.bijective_iff_injective_and_card, ZMod.card, h, eq_self_iff_true, and_true]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m = n
⊢ ZMod m ≃+* ZMod n
have zero : (h : 0 = n) → ZMod 0 ≃+* ZMod n
Tactic: rcases m with - | m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m = n
zero : (h : 0 = n) → ZMod 0 ≃+* ZMod n
⊢ ZMod m ≃+* ZMod n
have succ : (m : ℕ) → (h : m + 1 = n) → ZMod (m + 1) ≃+* ZMod n
Tactic: rcases m with - | m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
n : ℕ
h : 0 = n
⊢ ZMod 0 ≃+* ZMod n
have zero : (h : Eq (α := ℕ) 0 0) → ZMod 0 ≃+* ZMod 0
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
n : ℕ
h : 0 = n
zero : (h : Eq (α := ℕ) 0 0) → ZMod 0 ≃+* ZMod 0
⊢ ZMod 0 ≃+* ZMod n
have zero₁ : (n : ℕ) → (h : 0 = n + 1) → ZMod 0 ≃+* ZMod (n + 1)
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
n m : ℕ
h : m + 1 = n
⊢ ZMod (m + 1) ≃+* ZMod n
have succ : (h : m + 1 = 0) → ZMod (m + 1) ≃+* ZMod 0
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
n m : ℕ
h : m + 1 = n
succ : (h : m + 1 = 0) → ZMod (m + 1) ≃+* ZMod 0
⊢ ZMod (m + 1) ≃+* ZMod n
have succ₁ : (n : ℕ) → (h : m + 1 = n + 1) → ZMod (m + 1) ≃+* ZMod (n + 1)
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
n : ℕ
h : 0 = n + 1
⊢ ZMod 0 ≃+* ZMod (n + 1)
have zero : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n
m : ℕ
h : m + 1 = 0
⊢ ZMod (m + 1) ≃+* ZMod 0
have succ : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ Fin.cast h (a * b) = Fin.cast h a * Fin.cast h b
have h₁ : (↑(Fin.cast h (a * b)) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ (↑(Fin.cast h (a * b)) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
have h₁ : (↑(a * b) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
Tactic: rw [Fin.val_cast, Fin.val_mul, Fin.val_mul, Fin.val_cast, Fin.val_cast, ← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
h₁ : (↑(a * b) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
⊢ (↑(Fin.cast h (a * b)) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
have h₂ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
Tactic: rw [Fin.val_cast, Fin.val_mul, Fin.val_mul, Fin.val_cast, Fin.val_cast, ← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
h₁ : (↑(a * b) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
h₂ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
⊢ (↑(Fin.cast h (a * b)) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
have h₃ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑(Fin.cast h a) : ℕ) * (↑(Fin.cast h b) : ℕ) % (n + 1)
Tactic: rw [Fin.val_cast, Fin.val_mul, Fin.val_mul, Fin.val_cast, Fin.val_cast, ← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
h₁ : (↑(a * b) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
h₂ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
h₃ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑(Fin.cast h a) : ℕ) * (↑(Fin.cast h b) : ℕ) % (n + 1)
⊢ (↑(Fin.cast h (a * b)) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
have h₄ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑a : ℕ) * (↑(Fin.cast h b) : ℕ) % (n + 1)
Tactic: rw [Fin.val_cast, Fin.val_mul, Fin.val_mul, Fin.val_cast, Fin.val_cast, ← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
h₁ : (↑(a * b) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
h₂ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
h₃ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑(Fin.cast h a) : ℕ) * (↑(Fin.cast h b) : ℕ) % (n + 1)
h₄ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑a : ℕ) * (↑(Fin.cast h b) : ℕ) % (n + 1)
⊢ (↑(Fin.cast h (a * b)) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
have h₅ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑a : ℕ) * (↑b : ℕ) % (n + 1)
Tactic: rw [Fin.val_cast, Fin.val_mul, Fin.val_mul, Fin.val_cast, Fin.val_cast, ← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
h₁ : (↑(a * b) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
h₂ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
h₃ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑(Fin.cast h a) : ℕ) * (↑(Fin.cast h b) : ℕ) % (n + 1)
h₄ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑a : ℕ) * (↑(Fin.cast h b) : ℕ) % (n + 1)
h₅ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑a : ℕ) * (↑b : ℕ) % (n + 1)
⊢ (↑(Fin.cast h (a * b)) : ℕ) = (↑(Fin.cast h a * Fin.cast h b) : ℕ)
have h₆ : (↑a : ℕ) * (↑b : ℕ) % (m + 1) = (↑a : ℕ) * (↑b : ℕ) % (m + 1)
Tactic: rw [Fin.val_cast, Fin.val_mul, Fin.val_mul, Fin.val_cast, Fin.val_cast, ← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ Fin.cast h (a + b) = Fin.cast h a + Fin.cast h b
have h₁ : (↑(Fin.cast h (a + b)) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ (↑(Fin.cast h (a + b)) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
have h₁ : (↑(a + b) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
Tactic: rw [Fin.val_cast, Fin.val_add, Fin.val_add, Fin.val_cast, Fin.val_cast, ← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
h₁ : (↑(a + b) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
⊢ (↑(Fin.cast h (a + b)) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
have h₂ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
Tactic: rw [Fin.val_cast, Fin.val_add, Fin.val_add, Fin.val_cast, Fin.val_cast, ← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
h₁ : (↑(a + b) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
h₂ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
⊢ (↑(Fin.cast h (a + b)) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
have h₃ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = ((↑(Fin.cast h a) : ℕ) + (↑(Fin.cast h b) : ℕ)) % (n + 1)
Tactic: rw [Fin.val_cast, Fin.val_add, Fin.val_add, Fin.val_cast, Fin.val_cast, ← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
h₁ : (↑(a + b) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
h₂ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
h₃ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = ((↑(Fin.cast h a) : ℕ) + (↑(Fin.cast h b) : ℕ)) % (n + 1)
⊢ (↑(Fin.cast h (a + b)) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
have h₄ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = ((↑a : ℕ) + (↑(Fin.cast h b) : ℕ)) % (n + 1)
Tactic: rw [Fin.val_cast, Fin.val_add, Fin.val_add, Fin.val_cast, Fin.val_cast, ← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
h₁ : (↑(a + b) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
h₂ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
h₃ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = ((↑(Fin.cast h a) : ℕ) + (↑(Fin.cast h b) : ℕ)) % (n + 1)
h₄ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = ((↑a : ℕ) + (↑(Fin.cast h b) : ℕ)) % (n + 1)
⊢ (↑(Fin.cast h (a + b)) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
have h₅ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = ((↑a : ℕ) + (↑b : ℕ)) % (n + 1)
Tactic: rw [Fin.val_cast, Fin.val_add, Fin.val_add, Fin.val_cast, Fin.val_cast, ← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : Ring R
inst_1 : CharP R n_1
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
h₁ : (↑(a + b) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
h₂ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
h₃ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = ((↑(Fin.cast h a) : ℕ) + (↑(Fin.cast h b) : ℕ)) % (n + 1)
h₄ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = ((↑a : ℕ) + (↑(Fin.cast h b) : ℕ)) % (n + 1)
h₅ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = ((↑a : ℕ) + (↑b : ℕ)) % (n + 1)
⊢ (↑(Fin.cast h (a + b)) : ℕ) = (↑(Fin.cast h a + Fin.cast h b) : ℕ)
have h₆ : ((↑a : ℕ) + (↑b : ℕ)) % (m + 1) = ((↑a : ℕ) + (↑b : ℕ)) % (m + 1)
Tactic: rw [Fin.val_cast, Fin.val_add, Fin.val_add, Fin.val_cast, Fin.val_cast, ← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℕ
⊢ Eq (α := ZMod a ≃+* ZMod a) (ringEquivCongr ⋯) (RingEquiv.refl (ZMod a))
have zero : Eq (α := ZMod 0 ≃+* ZMod 0) (ringEquivCongr sorry) (RingEquiv.refl (ZMod 0))
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℕ
zero : Eq (α := ZMod 0 ≃+* ZMod 0) (ringEquivCongr ⋯) (RingEquiv.refl (ZMod 0))
⊢ Eq (α := ZMod a ≃+* ZMod a) (ringEquivCongr ⋯) (RingEquiv.refl (ZMod a))
have succ : ∀ (n : ℕ), Eq (α := ZMod (n + 1) ≃+* ZMod (n + 1)) (ringEquivCongr sorry) (RingEquiv.refl (ZMod (n + 1)))
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℕ
x : ZMod a
⊢ (ringEquivCongr ⋯ : (a_1 : ZMod a) → ZMod a) x = x
have rw : (RingEquiv.refl (ZMod a) : (a_1 : ZMod a) → ZMod a) x = x
Tactic: rw [ringEquivCongr_refl]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a b : ℕ
hab : a = b
⊢ (ringEquivCongr hab).symm = ringEquivCongr ⋯
have subst : (ringEquivCongr sorry).symm = ringEquivCongr sorry
Tactic: subst hab
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℕ
⊢ (ringEquivCongr ⋯).symm = ringEquivCongr ⋯
have zero : Eq (α := ZMod 0 ≃+* ZMod 0) (RingEquiv.symm (ringEquivCongr sorry)) (ringEquivCongr sorry)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℕ
zero : Eq (α := ZMod 0 ≃+* ZMod 0) (RingEquiv.symm (ringEquivCongr ⋯)) (ringEquivCongr ⋯)
⊢ (ringEquivCongr ⋯).symm = ringEquivCongr ⋯
have succ : ∀ (n : ℕ), (ringEquivCongr sorry).symm = ringEquivCongr sorry
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a b c : ℕ
hab : a = b
hbc : b = c
⊢ (ringEquivCongr hab).trans (ringEquivCongr hbc) = ringEquivCongr ⋯
have subst : (ringEquivCongr sorry).trans (ringEquivCongr sorry) = ringEquivCongr sorry
Tactic: subst hab hbc
Cleared hypotheses: b, c, hab, hbc
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℕ
⊢ (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯
have zero : Eq (α := ZMod 0 ≃+* ZMod 0) (RingEquiv.trans (ringEquivCongr sorry) (ringEquivCongr sorry)) (ringEquivCongr sorry)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℕ
zero : Eq (α := ZMod 0 ≃+* ZMod 0) (RingEquiv.trans (ringEquivCongr ⋯) (ringEquivCongr ⋯)) (ringEquivCongr ⋯)
⊢ (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯
have succ : ∀ (n : ℕ), (ringEquivCongr sorry).trans (ringEquivCongr sorry) = ringEquivCongr sorry
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a b c : ℕ
hab : a = b
hbc : b = c
x : ZMod a
⊢ Eq (α := ZMod c)
    ((ringEquivCongr hbc : (a : ZMod b) → ZMod c) ((ringEquivCongr hab : (a : ZMod a) → ZMod b) x) : ZMod c)
    ((ringEquivCongr ⋯ : (a : ZMod a) → ZMod c) x : ZMod c)
have rw : Eq (α := ZMod c)
  ((ringEquivCongr hbc : (a : ZMod b) → ZMod c) ((ringEquivCongr hab : (a : ZMod a) → ZMod b) x) : ZMod c)
  (((ringEquivCongr hab).trans (ringEquivCongr hbc) : (a : ZMod a) → ZMod c) x : ZMod c)
Tactic: rw [← ringEquivCongr_trans hab hbc]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a b : ℕ
h : a = b
x : ZMod a
⊢ val (n := b) ((ringEquivCongr h : (a : ZMod a) → ZMod b) x) = x.val
have subst : val (n := a) ((ringEquivCongr sorry : (a_1 : ZMod a) → ZMod a) x) = x.val
Tactic: subst h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℕ
x : ZMod a
⊢ val (n := a) ((ringEquivCongr ⋯ : (a_1 : ZMod a) → ZMod a) x) = x.val
have zero : ∀ (x : ZMod 0), val (n := 0) ((ringEquivCongr sorry : (a : ZMod 0) → ZMod 0) x) = x.val
Tactic: cases a
Cleared hypotheses: a, x
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℕ
x : ZMod a
zero : ∀ (x : ZMod 0), val (n := 0) ((ringEquivCongr ⋯ : (a : ZMod 0) → ZMod 0) x) = x.val
⊢ val (n := a) ((ringEquivCongr ⋯ : (a_1 : ZMod a) → ZMod a) x) = x.val
have succ : ∀ (n : ℕ) (x : ZMod (n + 1)), val (n := n + 1) ((ringEquivCongr sorry : (a : ZMod (n + 1)) → ZMod (n + 1)) x) = x.val
Tactic: cases a
Cleared hypotheses: a, x
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
⊢ a.val = 0 ↔ a = 0
have rw : a.val = 0 ↔ (↑a : ℕ) = (↑0 : ℕ)
Tactic: rw [Fin.ext_iff]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
a : ℤ
inst : NeZero n
⊢ (↑(val (n := n) (↑a : ZMod n)) : ℤ) = a % (↑n : ℤ)
have hle : LE.le (α := ℤ) 0 (↑(val (n := n) (↑a : ZMod n)) : ℤ)
Tactic: have hle : (0 : ℤ) ≤ ↑(a : ZMod n).val := Int.natCast_nonneg _
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
a : ℤ
inst : NeZero n
hle : LE.le (α := ℤ) 0 (↑(val (n := n) (↑a : ZMod n)) : ℤ)
⊢ (↑(val (n := n) (↑a : ZMod n)) : ℤ) = a % (↑n : ℤ)
have hlt : LT.lt (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ)
Tactic: have hlt : ↑(a : ZMod n).val < (n : ℤ) := Int.ofNat_lt.mpr (ZMod.val_lt a)
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ℤ
inst : NeZero n
hle : LE.le (α := ℤ) 0 (↑(val (n := n) (↑a : ZMod n)) : ℤ)
hlt : LT.lt (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ)
⊢ (↑(val (n := n) (↑a : ZMod n)) : ℤ) = a % (↑n : ℤ)
have refine : HMod.hMod (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ) = a % (↑n : ℤ)
Tactic: refine (Int.emod_eq_of_lt hle hlt).symm.trans ?_
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ℤ
inst : NeZero n
hle : LE.le (α := ℤ) 0 (↑(val (n := n) (↑a : ZMod n)) : ℤ)
hlt : LT.lt (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ)
⊢ HMod.hMod (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ) = a % (↑n : ℤ)
have rw : Eq (α := ZMod n) (↑(↑(val (n := n) (↑a : ZMod n)) : ℤ) : ZMod n) (↑a : ZMod n)
Tactic: rw [← ZMod.intCast_eq_intCast_iff', Int.cast_natCast, ZMod.natCast_val, ZMod.cast_id]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ℤ
inst : NeZero n
hle : LE.le (α := ℤ) 0 (↑(val (n := n) (↑a : ZMod n)) : ℤ)
hlt : LT.lt (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ)
rw : Eq (α := ZMod n) (↑(↑(val (n := n) (↑a : ZMod n)) : ℤ) : ZMod n) (↑a : ZMod n)
⊢ HMod.hMod (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ) = a % (↑n : ℤ)
have rw₁ : Eq (α := ZMod n) (↑(val (n := n) (↑a : ZMod n)) : ZMod n) (↑a : ZMod n)
Tactic: rw [← ZMod.intCast_eq_intCast_iff', Int.cast_natCast, ZMod.natCast_val, ZMod.cast_id]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ℤ
inst : NeZero n
hle : LE.le (α := ℤ) 0 (↑(val (n := n) (↑a : ZMod n)) : ℤ)
hlt : LT.lt (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ)
rw : Eq (α := ZMod n) (↑(↑(val (n := n) (↑a : ZMod n)) : ℤ) : ZMod n) (↑a : ZMod n)
rw₁ : Eq (α := ZMod n) (↑(val (n := n) (↑a : ZMod n)) : ZMod n) (↑a : ZMod n)
⊢ HMod.hMod (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ) = a % (↑n : ℤ)
have rw₂ : Eq (α := ZMod n) (cast (n := n) (↑a : ZMod n)) (↑a : ZMod n)
Tactic: rw [← ZMod.intCast_eq_intCast_iff', Int.cast_natCast, ZMod.natCast_val, ZMod.cast_id]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ℤ
inst : NeZero n
hle : LE.le (α := ℤ) 0 (↑(val (n := n) (↑a : ZMod n)) : ℤ)
hlt : LT.lt (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ)
rw : Eq (α := ZMod n) (↑(↑(val (n := n) (↑a : ZMod n)) : ℤ) : ZMod n) (↑a : ZMod n)
rw₁ : Eq (α := ZMod n) (↑(val (n := n) (↑a : ZMod n)) : ZMod n) (↑a : ZMod n)
rw₂ : Eq (α := ZMod n) (cast (n := n) (↑a : ZMod n)) (↑a : ZMod n)
⊢ HMod.hMod (α := ℤ) (↑(val (n := n) (↑a : ZMod n)) : ℤ) (↑n : ℤ) = a % (↑n : ℤ)
have rw₃ : Eq (α := ZMod n) (↑a : ZMod n) (↑a : ZMod n)
Tactic: rw [← ZMod.intCast_eq_intCast_iff', Int.cast_natCast, ZMod.natCast_val, ZMod.cast_id]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℤ
b : ℕ
⊢ Eq (α := ZMod b) (↑a : ZMod b) 0 ↔ (↑b : ℤ) ∣ a
have rw : Eq (α := ZMod b) (↑a : ZMod b) (↑0 : ZMod b) ↔ (↑b : ℤ) ∣ a
Tactic: rw [← Int.cast_zero, ZMod.intCast_eq_intCast_iff, Int.modEq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℤ
b : ℕ
rw : Eq (α := ZMod b) (↑a : ZMod b) (↑0 : ZMod b) ↔ (↑b : ℤ) ∣ a
⊢ Eq (α := ZMod b) (↑a : ZMod b) 0 ↔ (↑b : ℤ) ∣ a
have rw₁ : a ≡ 0 [ZMOD (↑b : ℤ)] ↔ (↑b : ℤ) ∣ a
Tactic: rw [← Int.cast_zero, ZMod.intCast_eq_intCast_iff, Int.modEq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℤ
b : ℕ
rw : Eq (α := ZMod b) (↑a : ZMod b) (↑0 : ZMod b) ↔ (↑b : ℤ) ∣ a
rw₁ : a ≡ 0 [ZMOD (↑b : ℤ)] ↔ (↑b : ℤ) ∣ a
⊢ Eq (α := ZMod b) (↑a : ZMod b) 0 ↔ (↑b : ℤ) ∣ a
have rw₂ : (↑b : ℤ) ∣ a ↔ (↑b : ℤ) ∣ a
Tactic: rw [← Int.cast_zero, ZMod.intCast_eq_intCast_iff, Int.modEq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a b : ℤ
c : ℕ
⊢ Eq (α := ZMod c) (↑a : ZMod c) (↑b : ZMod c) ↔ (↑c : ℤ) ∣ b - a
have rw : a ≡ b [ZMOD (↑c : ℤ)] ↔ (↑c : ℤ) ∣ b - a
Tactic: rw [ZMod.intCast_eq_intCast_iff, Int.modEq_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a b : ℤ
c : ℕ
rw : a ≡ b [ZMOD (↑c : ℤ)] ↔ (↑c : ℤ) ∣ b - a
⊢ Eq (α := ZMod c) (↑a : ZMod c) (↑b : ZMod c) ↔ (↑c : ℤ) ∣ b - a
have rw₁ : (↑c : ℤ) ∣ b - a ↔ (↑c : ℤ) ∣ b - a
Tactic: rw [ZMod.intCast_eq_intCast_iff, Int.modEq_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a b : ℕ
⊢ Eq (α := ZMod b) (↑a : ZMod b) 0 ↔ b ∣ a
have rw : Eq (α := ZMod b) (↑a : ZMod b) (↑0 : ZMod b) ↔ b ∣ a
Tactic: rw [← Nat.cast_zero, ZMod.natCast_eq_natCast_iff, Nat.modEq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a b : ℕ
rw : Eq (α := ZMod b) (↑a : ZMod b) (↑0 : ZMod b) ↔ b ∣ a
⊢ Eq (α := ZMod b) (↑a : ZMod b) 0 ↔ b ∣ a
have rw₁ : a ≡ 0 [MOD b] ↔ b ∣ a
Tactic: rw [← Nat.cast_zero, ZMod.natCast_eq_natCast_iff, Nat.modEq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a b : ℕ
rw : Eq (α := ZMod b) (↑a : ZMod b) (↑0 : ZMod b) ↔ b ∣ a
rw₁ : a ≡ 0 [MOD b] ↔ b ∣ a
⊢ Eq (α := ZMod b) (↑a : ZMod b) 0 ↔ b ∣ a
have rw₂ : b ∣ a ↔ b ∣ a
Tactic: rw [← Nat.cast_zero, ZMod.natCast_eq_natCast_iff, Nat.modEq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ℤ
⊢ cast (n := n) (↑a : ZMod n) = a % (↑n : ℤ)
have zero : cast (n := 0) (↑a : ZMod 0) = a % (↑0 : ℤ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ℤ
zero : cast (n := 0) (↑a : ZMod 0) = a % (↑0 : ℤ)
⊢ cast (n := n) (↑a : ZMod n) = a % (↑n : ℤ)
have succ : ∀ (n : ℕ), cast (n := n + 1) (↑a : ZMod (n + 1)) = a % (↑(n + 1) : ℤ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℤ
⊢ cast (n := 0) (↑a : ZMod 0) = a % (↑0 : ℤ)
have zero : cast (n := 0) a = a
Tactic: rw [Int.ofNat_zero, Int.emod_zero, Int.cast_id]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
a : ℤ
n : ℕ
⊢ cast (n := n + 1) (↑a : ZMod (n + 1)) = a % (↑(n + 1) : ℤ)
have succ : Eq (α := ℤ) (cast (n := n + 1) (↑a : ZMod (n + 1))) (↑(↑(↑a : ZMod (n + 1)) : ℕ) : ℤ)
Tactic: rw [← val_intCast, val]