awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
h₁ : Ne.{u_1 + 1} (α := R) 1 0
h₂ : Eq.{u_1 + 1} (α := R) 2 0
n : ℕ
hn : Odd n
⊢ ¬Eq.{u_1 + 1} (α := R) (↑n : R) 0
have inr : ¬Eq.{u_1 + 1} (α := R) 1 0
Tactic: rwa [natCast_eq_one_of_odd_of_two_eq_zero hn h₂]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
⊢ Eq.{u_1 + 1} (α := R) 2 0
have rw : Eq.{u_1 + 1} (α := R) (↑2 : R) 0
Tactic: rw [← Nat.cast_two, CharP.cast_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
rw : Eq.{u_1 + 1} (α := R) (↑2 : R) 0
⊢ Eq.{u_1 + 1} (α := R) 2 0
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← Nat.cast_two, CharP.cast_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) (if Even n then 0 else 1)
have zero : Eq.{u_1 + 1} (α := R) (↑0 : R) (if Even (α := ℕ) 0 then 0 else 1)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
n : ℕ
zero : Eq.{u_1 + 1} (α := R) (↑0 : R) (if Even (α := ℕ) 0 then 0 else 1)
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) (if Even n then 0 else 1)
have succ : ∀ (n : ℕ),
  Eq.{u_1 + 1} (α := R) (↑n : R) (if Even n then 0 else 1) →
    Eq.{u_1 + 1} (α := R) (↑(n + 1) : R) (if Even (n + 1) then 0 else 1)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
⊢ Eq (α := Set R) (Set.range Nat.cast) {0, 1}
have hp : ∃ (a : ℕ), Even a
Tactic: rw [funext natCast_eq_ite, Set.range_ite_const]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
hp : ∃ (a : ℕ), Even a
⊢ Eq (α := Set R) (Set.range Nat.cast) {0, 1}
have hn : ∃ (a : ℕ), ¬Even a
Tactic: rw [funext natCast_eq_ite, Set.range_ite_const]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
⊢ ∃ (a : ℕ), Even a
have h : Even (α := ℕ) 0
Tactic: use 0
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
⊢ ∃ (a : ℕ), ¬Even a
have h : ¬Even (α := ℕ) 1
Tactic: use 1
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
x : R
⊢ x + x = 0
have rw : 2 * x = 0
Tactic: rw [← two_mul x, two_eq_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
x : R
rw : 2 * x = 0
⊢ x + x = 0
have rw₁ : 0 * x = 0
Tactic: rw [← two_mul x, two_eq_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
x : R
rw : 2 * x = 0
rw₁ : 0 * x = 0
⊢ x + x = 0
have rw₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← two_mul x, two_eq_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
x : R
⊢ HSMul.hSMul (α := ℕ) 2 x = 0
have rw : x + x = 0
Tactic: rw [two_nsmul, add_self_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
x : R
rw : x + x = 0
⊢ HSMul.hSMul (α := ℕ) 2 x = 0
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [two_nsmul, add_self_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
a b : R
⊢ a + (a + b) = b
have rw : a + a + b = b
Tactic: rw [← add_assoc, add_self_eq_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
a b : R
rw : a + a + b = b
⊢ a + (a + b) = b
have rw₁ : 0 + b = b
Tactic: rw [← add_assoc, add_self_eq_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
a b : R
rw : a + a + b = b
rw₁ : 0 + b = b
⊢ a + (a + b) = b
have rw₂ : b = b
Tactic: rw [← add_assoc, add_self_eq_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
a b : R
⊢ a + b + b = a
have rw : a + (b + b) = a
Tactic: rw [add_assoc, add_self_eq_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
a b : R
rw : a + (b + b) = a
⊢ a + b + b = a
have rw₁ : a + 0 = a
Tactic: rw [add_assoc, add_self_eq_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
a b : R
rw : a + (b + b) = a
rw₁ : a + 0 = a
⊢ a + b + b = a
have rw₂ : a = a
Tactic: rw [add_assoc, add_self_eq_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
x : R
⊢ -x = x
have rw : x + x = 0
Tactic: rw [neg_eq_iff_add_eq_zero, add_self_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
x : R
rw : x + x = 0
⊢ -x = x
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [neg_eq_iff_add_eq_zero, add_self_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
x y : R
⊢ x - y = x + y
have rw : x + -y = x + y
Tactic: rw [sub_eq_add_neg, neg_eq]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
x y : R
rw : x + -y = x + y
⊢ x - y = x + y
have rw₁ : x + y = x + y
Tactic: rw [sub_eq_add_neg, neg_eq]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
a b c : R
⊢ a + b = c ↔ a = c + b
have rw : a + b = c ↔ a - b = c
Tactic: rw [← sub_eq_iff_eq_add, sub_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
a b c : R
rw : a + b = c ↔ a - b = c
⊢ a + b = c ↔ a = c + b
have rw₁ : a + b = c ↔ a + b = c
Tactic: rw [← sub_eq_iff_eq_add, sub_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
a b c : R
⊢ a = b + c ↔ a + c = b
have rw : a = b + c ↔ a = b - c
Tactic: rw [← eq_sub_iff_add_eq, sub_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
a b c : R
rw : a = b + c ↔ a = b - c
⊢ a = b + c ↔ a + c = b
have rw₁ : a = b + c ↔ a = b + c
Tactic: rw [← eq_sub_iff_add_eq, sub_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
x : R
⊢ HSMul.hSMul (α := ℤ) 2 x = 0
have rw : x + x = 0
Tactic: rw [two_zsmul, add_self_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
x : R
rw : x + x = 0
⊢ HSMul.hSMul (α := ℤ) 2 x = 0
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [two_zsmul, add_self_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
a b : R
⊢ a + b = 0 ↔ a = b
have rw : a - b = 0 ↔ a = b
Tactic: rw [← CharTwo.sub_eq_add, sub_eq_iff_eq_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
a b : R
rw : a - b = 0 ↔ a = b
⊢ a + b = 0 ↔ a = b
have rw₁ : a = 0 + b ↔ a = b
Tactic: rw [← CharTwo.sub_eq_add, sub_eq_iff_eq_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
a b : R
rw : a - b = 0 ↔ a = b
rw₁ : a = 0 + b ↔ a = b
⊢ a + b = 0 ↔ a = b
have rw₂ : a = b ↔ a = b
Tactic: rw [← CharTwo.sub_eq_add, sub_eq_iff_eq_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
n : ℤ
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) (if Even n then 0 else 1)
have inl : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑(↑n : ℤ) : R) (if Even (α := ℤ) (↑n : ℤ) then 0 else 1)
Tactic: obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
n : ℤ
inl : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑(↑n : ℤ) : R) (if Even (α := ℤ) (↑n : ℤ) then 0 else 1)
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) (if Even n then 0 else 1)
have inr : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑(-(↑n : ℤ)) : R) (if Even (α := ℤ) (-(↑n : ℤ)) then 0 else 1)
Tactic: obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
⊢ Eq (α := Set R) (Set.range Int.cast) {0, 1}
have hp : ∃ (a : ℤ), Even a
Tactic: rw [funext intCast_eq_ite, Set.range_ite_const]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
hp : ∃ (a : ℤ), Even a
⊢ Eq (α := Set R) (Set.range Int.cast) {0, 1}
have hn : ∃ (a : ℤ), ¬Even a
Tactic: rw [funext intCast_eq_ite, Set.range_ite_const]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
⊢ ∃ (a : ℤ), Even a
have h : Even (α := ℤ) 0
Tactic: use 0
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
⊢ ∃ (a : ℤ), ¬Even a
have h : ¬Even (α := ℤ) 1
Tactic: use 1
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : CharP R 2
x y : R
⊢ (x + y) * (x + y) = x * x + y * y
have rw : HPow.hPow (β := ℕ) (x + y) 2 = x * x + y * y
Tactic: rw [← pow_two, ← pow_two, ← pow_two, add_sq]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : CharP R 2
x y : R
rw : HPow.hPow (β := ℕ) (x + y) 2 = x * x + y * y
⊢ (x + y) * (x + y) = x * x + y * y
have rw₁ : HPow.hPow (β := ℕ) (x + y) 2 = HPow.hPow (β := ℕ) x 2 + y * y
Tactic: rw [← pow_two, ← pow_two, ← pow_two, add_sq]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : CharP R 2
x y : R
rw : HPow.hPow (β := ℕ) (x + y) 2 = x * x + y * y
rw₁ : HPow.hPow (β := ℕ) (x + y) 2 = HPow.hPow (β := ℕ) x 2 + y * y
⊢ (x + y) * (x + y) = x * x + y * y
have rw₂ : HPow.hPow (β := ℕ) (x + y) 2 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: rw [← pow_two, ← pow_two, ← pow_two, add_sq]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : CharP R 2
x y : R
rw : HPow.hPow (β := ℕ) (x + y) 2 = x * x + y * y
rw₁ : HPow.hPow (β := ℕ) (x + y) 2 = HPow.hPow (β := ℕ) x 2 + y * y
rw₂ : HPow.hPow (β := ℕ) (x + y) 2 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ (x + y) * (x + y) = x * x + y * y
have rw₃ : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: rw [← pow_two, ← pow_two, ← pow_two, add_sq]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : CharP R 2
l : List R
⊢ l.sum * l.sum = List.sum (List.map (fun (x : R) ↦ x * x) l)
have simp_rw : HPow.hPow (β := ℕ) l.sum 2 = List.sum (List.map (fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) l)
Tactic: simp_rw [← pow_two, list_sum_sq]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : CharP R 2
l : Multiset R
⊢ l.sum * l.sum = Multiset.sum (Multiset.map (fun (x : R) ↦ x * x) l)
have simp_rw : HPow.hPow (β := ℕ) l.sum 2 = Multiset.sum (Multiset.map (fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) l)
Tactic: simp_rw [← pow_two, multiset_sum_sq]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring R
inst_1 : CharP R 2
s : Finset ι
f : ι → R
⊢ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, f i) = ∑ i ∈ s, f i * f i
have simp_rw : HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, f i) 2 = ∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2
Tactic: simp_rw [← pow_two, sum_sq]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharP R 2
inst_2 : NoZeroDivisors R
x y : R
h : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) x) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) y)
⊢ x = y
have rwa : ∀ (h : HAdd.hAdd (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) x) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) y) = 0),
  x = y
Tactic: rwa [← CharTwo.add_eq_zero, ← add_sq, pow_eq_zero_iff two_ne_zero, CharTwo.add_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharP R 2
inst_2 : NoZeroDivisors R
x y : R
h : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) x) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) y)
rwa :
  ∀ (h : HAdd.hAdd (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) x) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) y) = 0),
    x = y
⊢ x = y
have rwa₁ : ∀ (h : HPow.hPow (β := ℕ) (x + y) 2 = 0), x = y
Tactic: rwa [← CharTwo.add_eq_zero, ← add_sq, pow_eq_zero_iff two_ne_zero, CharTwo.add_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharP R 2
inst_2 : NoZeroDivisors R
x y : R
h : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) x) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) y)
rwa :
  ∀ (h : HAdd.hAdd (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) x) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) y) = 0),
    x = y
rwa₁ : ∀ (h : HPow.hPow (β := ℕ) (x + y) 2 = 0), x = y
⊢ x = y
have rwa₂ : ∀ (h : x + y = 0), x = y
Tactic: rwa [← CharTwo.add_eq_zero, ← add_sq, pow_eq_zero_iff two_ne_zero, CharTwo.add_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharP R 2
inst_2 : NoZeroDivisors R
x y : R
h : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) x) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) y)
rwa :
  ∀ (h : HAdd.hAdd (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) x) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 2) y) = 0),
    x = y
rwa₁ : ∀ (h : HPow.hPow (β := ℕ) (x + y) 2 = 0), x = y
rwa₂ : ∀ (h : x + y = 0), x = y
⊢ x = y
have rwa₃ : ∀ (h : x = y), x = y
Tactic: rwa [← CharTwo.add_eq_zero, ← add_sq, pow_eq_zero_iff two_ne_zero, CharTwo.add_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
⊢ Eq.{u_1 + 1} (α := R) (-1) 1 ↔ ringChar R = 2
have refine : ∀ (h : Eq.{u_1 + 1} (α := R) (-1) 1), ringChar R = 2
Tactic: refine ⟨fun h => ?_, fun h => @CharTwo.neg_eq _ _ (ringChar.of_eq h) 1⟩
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
h : Eq.{u_1 + 1} (α := R) (-1) 1
⊢ ringChar R = 2
have h₁ : Eq.{u_1 + 1} (α := R) (↑(HAdd.hAdd (α := ℕ) 1 1) : R) 0
Tactic: rw [eq_comm, ← sub_eq_zero, sub_neg_eq_add, ← Nat.cast_one, ← Nat.cast_add] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharZero.AddMonoidHom (goal)
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoidWithOne M
inst_1 : AddCommMonoidWithOne N
inst_2 : CharZero M
e : M →+ N
he : Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) 1 : N) (1 : N)
he' : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑e : (a : M) → N)
n m : ℕ
h : Eq.{u_2 + 1} (α := N) (↑n : N) (↑m : N)
⊢ n = m
have rwa : ∀ (h : Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) (↑n : M) : N) ((↑m : N) : N)), n = m
Tactic: rwa [← map_natCast' _ he, ← map_natCast' _ he, he'.eq_iff, Nat.cast_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharZero.AddMonoidHom (goal)
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoidWithOne M
inst_1 : AddCommMonoidWithOne N
inst_2 : CharZero M
e : M →+ N
he : Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) 1 : N) (1 : N)
he' : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑e : (a : M) → N)
n m : ℕ
h : Eq.{u_2 + 1} (α := N) (↑n : N) (↑m : N)
rwa : ∀ (h : Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) (↑n : M) : N) ((↑m : N) : N)), n = m
⊢ n = m
have rwa₁ : ∀ (h : Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) (↑n : M) : N) ((e : (a : M) → N) (↑m : M) : N)), n = m
Tactic: rwa [← map_natCast' _ he, ← map_natCast' _ he, he'.eq_iff, Nat.cast_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharZero.AddMonoidHom (goal)
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoidWithOne M
inst_1 : AddCommMonoidWithOne N
inst_2 : CharZero M
e : M →+ N
he : Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) 1 : N) (1 : N)
he' : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑e : (a : M) → N)
n m : ℕ
h : Eq.{u_2 + 1} (α := N) (↑n : N) (↑m : N)
rwa : ∀ (h : Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) (↑n : M) : N) ((↑m : N) : N)), n = m
rwa₁ : ∀ (h : Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) (↑n : M) : N) ((e : (a : M) → N) (↑m : M) : N)), n = m
⊢ n = m
have rwa₂ : ∀ (h : Eq.{u_1 + 1} (α := M) (↑n : M) (↑m : M)), n = m
Tactic: rwa [← map_natCast' _ he, ← map_natCast' _ he, he'.eq_iff, Nat.cast_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharZero.AddMonoidHom (goal)
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoidWithOne M
inst_1 : AddCommMonoidWithOne N
inst_2 : CharZero M
e : M →+ N
he : Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) 1 : N) (1 : N)
he' : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑e : (a : M) → N)
n m : ℕ
h : Eq.{u_2 + 1} (α := N) (↑n : N) (↑m : N)
rwa : ∀ (h : Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) (↑n : M) : N) ((↑m : N) : N)), n = m
rwa₁ : ∀ (h : Eq.{u_2 + 1} (α := N) ((e : (a : M) → N) (↑n : M) : N) ((e : (a : M) → N) (↑m : M) : N)), n = m
rwa₂ : ∀ (h : Eq.{u_1 + 1} (α := M) (↑n : M) (↑m : M)), n = m
⊢ n = m
have rwa₃ : ∀ (h : n = m), n = m
Tactic: rwa [← map_natCast' _ he, ← map_natCast' _ he, he'.eq_iff, Nat.cast_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑0 : R) (↑n : R)
⊢ 0 = n
have zero : Eq.{u_1 + 1} (α := R) (↑n : R) 0
Tactic: rw [H n]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑0 : R) (↑n : R)
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0
have zero : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
Tactic: rw [← h, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑0 : R) (↑n : R)
zero : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0
have zero₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← h, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), m = n
n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑n : R)
⊢ m + 1 = n
have succ : ∀ (h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑0 : R)), m + 1 = 0
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), m = n
n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑n : R)
succ : ∀ (h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑0 : R)), m + 1 = 0
⊢ m + 1 = n
have succ₁ : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑(n + 1) : R)), m + 1 = n + 1
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), m = n
h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑0 : R)
⊢ m + 1 = 0
have succ : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) 0
Tactic: apply H
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), m = n
h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑0 : R)
⊢ Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) 0
have succ : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
Tactic: rw [h, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), m = n
h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑0 : R)
succ : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
⊢ Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) 0
have succ₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [h, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (hypothesis)
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), m = n
n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑(n + 1) : R)
⊢ m + 1 = n + 1
have h₁ : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)
Tactic: simp only [Nat.cast_succ, add_right_cancel_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), m = n
n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)
⊢ m + 1 = n + 1
have succ : n + 1 = n + 1
Tactic: rwa [ih]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)
⊢ m = n
have zero : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑0 : R) (↑n : R)), 0 = n
Tactic: induction m generalizing n with
    | zero => rw [H n]; rw [← h, Nat.cast_zero]
    | succ m ih =>
      cases n
      · apply H; rw [h, Nat.cast_zero]
      · simp only [Nat.cast_succ, add_right_cancel_iff] at h; rwa [ih]
Cleared hypotheses: m, n, h
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
H : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0
m n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)
zero : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑0 : R) (↑n : R)), 0 = n
⊢ m = n
have succ : ∀ (m : ℕ) (ih : ∀ (n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), m = n) (n : ℕ)
  (h : Eq.{u_1 + 1} (α := R) (↑(m + 1) : R) (↑n : R)), m + 1 = n
Tactic: induction m generalizing n with
    | zero => rw [H n]; rw [← h, Nat.cast_zero]
    | succ m ih =>
      cases n
      · apply H; rw [h, Nat.cast_zero]
      · simp only [Nat.cast_succ, add_right_cancel_iff] at h; rwa [ih]
Cleared hypotheses: m, n, h
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0 ↔ n = 0
have rw : Eq.{u_1 + 1} (α := R) (↑n : R) (↑0 : R) ↔ n = 0
Tactic: rw [← cast_zero, cast_inj]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
n : ℕ
rw : Eq.{u_1 + 1} (α := R) (↑n : R) (↑0 : R) ↔ n = 0
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0 ↔ n = 0
have rw₁ : n = 0 ↔ n = 0
Tactic: rw [← cast_zero, cast_inj]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 1 ↔ n = 1
have rw : Eq.{u_1 + 1} (α := R) (↑n : R) (↑1 : R) ↔ n = 1
Tactic: rw [← cast_one, cast_inj]