awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
simp_rw : (b - a) * (b - a) = b - a
simp_rw₁ : b * (b - a) - a * (b - a) = b - a
⊢ IsIdempotentElem (b - a)
have simp_rw₂ : b * b - b * a - (a * b - a * a) = b - a
Tactic: simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
simp_rw : (b - a) * (b - a) = b - a
simp_rw₁ : b * (b - a) - a * (b - a) = b - a
simp_rw₂ : b * b - b * a - (a * b - a * a) = b - a
⊢ IsIdempotentElem (b - a)
have simp_rw₃ : b * b - b * a - (a - a * a) = b - a
Tactic: simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
simp_rw : (b - a) * (b - a) = b - a
simp_rw₁ : b * (b - a) - a * (b - a) = b - a
simp_rw₂ : b * b - b * a - (a * b - a * a) = b - a
simp_rw₃ : b * b - b * a - (a - a * a) = b - a
⊢ IsIdempotentElem (b - a)
have simp_rw₄ : b * b - a - (a - a * a) = b - a
Tactic: simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
simp_rw : (b - a) * (b - a) = b - a
simp_rw₁ : b * (b - a) - a * (b - a) = b - a
simp_rw₂ : b * b - b * a - (a * b - a * a) = b - a
simp_rw₃ : b * b - b * a - (a - a * a) = b - a
simp_rw₄ : b * b - a - (a - a * a) = b - a
⊢ IsIdempotentElem (b - a)
have simp_rw₅ : b * b - a - (a - a) = b - a
Tactic: simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
simp_rw : (b - a) * (b - a) = b - a
simp_rw₁ : b * (b - a) - a * (b - a) = b - a
simp_rw₂ : b * b - b * a - (a * b - a * a) = b - a
simp_rw₃ : b * b - b * a - (a - a * a) = b - a
simp_rw₄ : b * b - a - (a - a * a) = b - a
simp_rw₅ : b * b - a - (a - a) = b - a
⊢ IsIdempotentElem (b - a)
have simp_rw₆ : b - a - (a - a) = b - a
Tactic: simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
simp_rw : (b - a) * (b - a) = b - a
simp_rw₁ : b * (b - a) - a * (b - a) = b - a
simp_rw₂ : b * b - b * a - (a * b - a * a) = b - a
simp_rw₃ : b * b - b * a - (a - a * a) = b - a
simp_rw₄ : b * b - a - (a - a * a) = b - a
simp_rw₅ : b * b - a - (a - a) = b - a
simp_rw₆ : b - a - (a - a) = b - a
⊢ IsIdempotentElem (b - a)
have simp_rw₇ : b - a - 0 = b - a
Tactic: simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ a * b * a = 0
have rw : HAdd.hAdd (α := ℕ) 1 1 • (a * b * a) = 0
Tactic: rw [← nsmul_right_inj ((Nat.zero_ne_add_one 1).symm), nsmul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ a * (a * b + b * a) * a = 0
have rw : a * 0 * a = 0
Tactic: rw [hab, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
rw : a * 0 * a = 0
⊢ a * (a * b + b * a) * a = 0
have rw₁ : 0 * a = 0
Tactic: rw [hab, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
rw : a * 0 * a = 0
rw₁ : 0 * a = 0
⊢ a * (a * b + b * a) * a = 0
have rw₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [hab, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (hypothesis)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ HAdd.hAdd (α := ℕ) 1 1 • (a * b * a) = 0
have this : a * (a * b + b * a) * a = 0
Tactic: have : a * (a * b + b * a) * a = 0 := by rw [hab, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (hypothesis)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ a * b = 0
have h : a * b * a = 0
Tactic: have h : a * b * a = 0 := by
    rw [← nsmul_right_inj ((Nat.zero_ne_add_one 1).symm), nsmul_zero]
    have : a * (a * b + b * a) * a = 0 := by rw [hab, mul_zero, zero_mul]
    simp_rw [mul_add, add_mul, mul_assoc, ha.eq, ← mul_assoc, ha.eq, ← two_nsmul] at this
    exact this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
this : a * a * b + a * b * a = 0
⊢ a * b = 0
have rwa : ∀ (this : a * a * b + 0 = 0), a * b = 0
Tactic: rwa [h, add_zero, ha.eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
this : a * a * b + a * b * a = 0
rwa : ∀ (this : a * a * b + 0 = 0), a * b = 0
⊢ a * b = 0
have rwa₁ : ∀ (this : a * a * b = 0), a * b = 0
Tactic: rwa [h, add_zero, ha.eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
this : a * a * b + a * b * a = 0
rwa : ∀ (this : a * a * b + 0 = 0), a * b = 0
rwa₁ : ∀ (this : a * a * b = 0), a * b = 0
⊢ a * b = 0
have rwa₂ : ∀ (this : a * b = 0), a * b = 0
Tactic: rwa [h, add_zero, ha.eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
⊢ a * b = 0
have suffices : a * a * b + a * b * a = 0
Tactic: suffices a * a * b + a * b * a = 0 by rwa [h, add_zero, ha.eq] at this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
⊢ a * a * b + a * b * a = 0
have rw : a * (a * b) + a * b * a = 0
Tactic: rw [mul_assoc, mul_assoc, ← mul_add, hab, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
rw : a * (a * b) + a * b * a = 0
⊢ a * a * b + a * b * a = 0
have rw₁ : a * (a * b) + a * (b * a) = 0
Tactic: rw [mul_assoc, mul_assoc, ← mul_add, hab, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
rw : a * (a * b) + a * b * a = 0
rw₁ : a * (a * b) + a * (b * a) = 0
⊢ a * a * b + a * b * a = 0
have rw₂ : a * (a * b + b * a) = 0
Tactic: rw [mul_assoc, mul_assoc, ← mul_add, hab, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
rw : a * (a * b) + a * b * a = 0
rw₁ : a * (a * b) + a * (b * a) = 0
rw₂ : a * (a * b + b * a) = 0
⊢ a * a * b + a * b * a = 0
have rw₃ : a * 0 = 0
Tactic: rw [mul_assoc, mul_assoc, ← mul_add, hab, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
rw : a * (a * b) + a * b * a = 0
rw₁ : a * (a * b) + a * (b * a) = 0
rw₂ : a * (a * b + b * a) = 0
rw₃ : a * 0 = 0
⊢ a * a * b + a * b * a = 0
have rw₄ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [mul_assoc, mul_assoc, ← mul_add, hab, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (hypothesis)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ Commute a b
have this : a * b = 0
Tactic: have := mul_eq_zero_of_anticommute ha hab
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (hypothesis)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
this : a * b = 0
⊢ Commute a b
have hab₁ : b * a = 0
Tactic: rw [this, zero_add] at hab
Cleared hypotheses: hab, this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : b * a = 0
this : a * b = 0
⊢ Commute a b
have rw : SemiconjBy a b b
Tactic: rw [Commute, SemiconjBy, hab, this]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : b * a = 0
this : a * b = 0
rw : SemiconjBy a b b
⊢ Commute a b
have rw₁ : a * b = b * a
Tactic: rw [Commute, SemiconjBy, hab, this]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
a b : R
inst : NonUnitalSemiring R
inst_1 : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : b * a = 0
this : a * b = 0
rw : SemiconjBy a b b
rw₁ : a * b = b * a
rw₂ : a * b = 0
⊢ Commute a b
have rw₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [Commute, SemiconjBy, hab, this]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
⊢ IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p
have refine : ∀ (hqp : IsIdempotentElem (q - p)), p * q = p ∧ q * p = p
Tactic: refine ⟨fun hqp ↦ ?_, fun ⟨h1, h2⟩ => hp.sub hq h1 h2⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
⊢ p * q = p ∧ q * p = p
have h : p * (q - p) + (q - p) * p = 0
Tactic: have h : p * (q - p) + (q - p) * p = 0 := hp.add_iff hqp |>.mp ((add_sub_cancel p q).symm ▸ hq)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
⊢ Commute p q
have hqp₁ : p * q + q * p - p = p
Tactic: simp_rw [IsIdempotentElem, mul_sub, sub_mul,
    hp.eq, hq.eq, ← sub_add_eq_sub_sub, sub_right_inj, add_sub] at hqp
Cleared hypotheses: hqp
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
⊢ Commute p q
have h1 : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ q * x) (p * q + q * p - p)) ((fun (x : R) ↦ q * x) p)
Tactic: have h1 := congr_arg (q * ·) hqp
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h1 : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ q * x) (p * q + q * p - p)) ((fun (x : R) ↦ q * x) p)
⊢ Commute p q
have h2 : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ x * q) (p * q + q * p - p)) ((fun (x : R) ↦ x * q) p)
Tactic: have h2 := congr_arg (· * q) hqp
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h1 : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ q * x) (p * q + q * p - p)) ((fun (x : R) ↦ q * x) p)
h2 : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ x * q) (p * q + q * p - p)) ((fun (x : R) ↦ x * q) p)
⊢ Commute p q
have h1₁ : q * p * q = q * p
Tactic: simp_rw [mul_sub, mul_add, ← mul_assoc, hq.eq, add_sub_cancel_right] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h2 : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ x * q) (p * q + q * p - p)) ((fun (x : R) ↦ x * q) p)
h1 : q * p * q = q * p
⊢ Commute p q
have h2₁ : q * p * q = p * q
Tactic: simp_rw [sub_mul, add_mul, mul_assoc, hq.eq, add_sub_cancel_left, ← mul_assoc] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
⊢ p * q = p ∧ q * p = p
have hpq : Commute p q
Tactic: have hpq : Commute p q := by
    simp_rw [IsIdempotentElem, mul_sub, sub_mul,
    hp.eq, hq.eq, ← sub_add_eq_sub_sub, sub_right_inj, add_sub] at hqp
    have h1 := congr_arg (q * ·) hqp
    have h2 := congr_arg (· * q) hqp
    simp_rw [mul_sub, mul_add, ← mul_assoc, hq.eq, add_sub_cancel_right] at h1
    simp_rw [sub_mul, add_mul, mul_assoc, hq.eq, add_sub_cancel_left, ← mul_assoc] at h2
    exact h2.symm.trans h1
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
hpq : Commute p q
⊢ p * q = p ∧ q * p = p
have rw : HSMul.hSMul (α := ℕ) 2 (q * p) = 0 + HSMul.hSMul (α := ℕ) 2 p
Tactic: rw [hpq.eq, and_self, ← nsmul_right_inj (by simp : 2 ≠ 0), ← zero_add (2 • p)]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
hpq : Commute p q
⊢ HSMul.hSMul (α := ℕ) 2 (q * p) = 0 + HSMul.hSMul (α := ℕ) 2 p
have h₁ : HSMul.hSMul (α := ℕ) 2 (q * p) = p * (q - p) + (q - p) * p + HSMul.hSMul (α := ℕ) 2 p
Tactic: convert! congrArg (· + 2 • p) h using 1
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
f : S → R
hf : Injective f
inst_11 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
⊢ f (-x * y) = f (-(x * y))
have rw : f (-x * y) = -f (x * y)
Tactic: rw [neg, mul, neg, neg_mul, mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
f : S → R
hf : Injective f
inst_11 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
rw : f (-x * y) = -f (x * y)
⊢ f (-x * y) = f (-(x * y))
have rw₁ : f (-x) * f y = -f (x * y)
Tactic: rw [neg, mul, neg, neg_mul, mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
f : S → R
hf : Injective f
inst_11 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
rw : f (-x * y) = -f (x * y)
rw₁ : f (-x) * f y = -f (x * y)
⊢ f (-x * y) = f (-(x * y))
have rw₂ : -f x * f y = -f (x * y)
Tactic: rw [neg, mul, neg, neg_mul, mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
f : S → R
hf : Injective f
inst_11 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
rw : f (-x * y) = -f (x * y)
rw₁ : f (-x) * f y = -f (x * y)
rw₂ : -f x * f y = -f (x * y)
⊢ f (-x * y) = f (-(x * y))
have rw₃ : -(f x * f y) = -f (x * y)
Tactic: rw [neg, mul, neg, neg_mul, mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
f : S → R
hf : Injective f
inst_11 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
rw : f (-x * y) = -f (x * y)
rw₁ : f (-x) * f y = -f (x * y)
rw₂ : -f x * f y = -f (x * y)
rw₃ : -(f x * f y) = -f (x * y)
⊢ f (-x * y) = f (-(x * y))
have rw₄ : -(f x * f y) = -(f x * f y)
Tactic: rw [neg, mul, neg, neg_mul, mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
f : S → R
hf : Injective f
inst_11 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
⊢ f (x * -y) = f (-(x * y))
have rw : f (x * -y) = -f (x * y)
Tactic: rw [neg, mul, neg, mul_neg, mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
f : S → R
hf : Injective f
inst_11 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
rw : f (x * -y) = -f (x * y)
⊢ f (x * -y) = f (-(x * y))
have rw₁ : f x * f (-y) = -f (x * y)
Tactic: rw [neg, mul, neg, mul_neg, mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
f : S → R
hf : Injective f
inst_11 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
rw : f (x * -y) = -f (x * y)
rw₁ : f x * f (-y) = -f (x * y)
⊢ f (x * -y) = f (-(x * y))
have rw₂ : f x * -f y = -f (x * y)
Tactic: rw [neg, mul, neg, mul_neg, mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
f : S → R
hf : Injective f
inst_11 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
rw : f (x * -y) = -f (x * y)
rw₁ : f x * f (-y) = -f (x * y)
rw₂ : f x * -f y = -f (x * y)
⊢ f (x * -y) = f (-(x * y))
have rw₃ : -(f x * f y) = -f (x * y)
Tactic: rw [neg, mul, neg, mul_neg, mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
f : S → R
hf : Injective f
inst_11 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
rw : f (x * -y) = -f (x * y)
rw₁ : f x * f (-y) = -f (x * y)
rw₂ : f x * -f y = -f (x * y)
rw₃ : -(f x * f y) = -f (x * y)
⊢ f (x * -y) = f (-(x * y))
have rw₄ : -(f x * f y) = -(f x * f y)
Tactic: rw [neg, mul, neg, mul_neg, mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
⊢ f (↑0 : S) = f 0
have rw : (↑0 : R) = f 0
Tactic: rw [natCast, Nat.cast_zero, zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
rw : (↑0 : R) = f 0
⊢ f (↑0 : S) = f 0
have rw₁ : 0 = f 0
Tactic: rw [natCast, Nat.cast_zero, zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.InjSurj (goal)
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
rw : (↑0 : R) = f 0
rw₁ : 0 = f 0
⊢ f (↑0 : S) = f 0
have rw₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [natCast, Nat.cast_zero, zero]