awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (hypothesis)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommRing α
inst_1 : IsDomain α
inst_2 : CommRing β
f : β →+ α
h :
  ∀ (x : β), (f : (a : β) → α) (x * x) = HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) x : α)
h_two : Ne.{u_2 + 1} (α := α) 2 0
h_one : Eq.{u_2 + 1} (α := α) ((f : (a : β) → α) 1 : α) (1 : α)
x y : β
hxy :
  HAdd.hAdd (α := α) ((f : (a : β) → α) (x * y) : α)
                (HMul.hMul (α := α) (β := α) ((f : (a : β) → α) y : α) ((f : (a : β) → α) y : α)) +
              HAdd.hAdd (β := α) (HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) x : α))
                ((f : (a : β) → α) (x * y) : α) -
            HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) x : α) -
          HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α) -
        HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α) -
      HMul.hMul (α := α) (β := α) ((f : (a : β) → α) y : α) ((f : (a : β) → α) y : α) =
    0
⊢ (↑f : ZeroHom β α).toFun (x * y) = (↑f : ZeroHom β α).toFun x * (↑f : ZeroHom β α).toFun y
have hxy₁ : HAdd.hAdd (α := α) ((f : (a : β) → α) (x * y) : α)
    (HSub.hSub (α := α) ((f : (a : β) → α) (x * y) : α)
        (HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α)) -
      HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α)) =
  0
Tactic: simp only [add_assoc, add_sub_assoc, add_sub_cancel] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (hypothesis)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommRing α
inst_1 : IsDomain α
inst_2 : CommRing β
f : β →+ α
h :
  ∀ (x : β), (f : (a : β) → α) (x * x) = HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) x : α)
h_two : Ne.{u_2 + 1} (α := α) 2 0
h_one : Eq.{u_2 + 1} (α := α) ((f : (a : β) → α) 1 : α) (1 : α)
x y : β
hxy :
  HAdd.hAdd (α := α) ((f : (a : β) → α) (x * y) : α)
      (HSub.hSub (α := α) ((f : (a : β) → α) (x * y) : α)
          (HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α)) -
        HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α)) =
    0
⊢ (↑f : ZeroHom β α).toFun (x * y) = (↑f : ZeroHom β α).toFun x * (↑f : ZeroHom β α).toFun y
have hxy₁ : ¬Eq.{u_2 + 1} (α := α) 2 0 →
  (f : (a : β) → α) (x * y) = HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α)
Tactic: rw [sub_sub, ← two_mul, ← add_sub_assoc, ← two_mul, ← mul_sub, mul_eq_zero (M₀ := α),
        sub_eq_zero, or_iff_not_imp_left] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Ring.Hom.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : IsDomain α
inst_2 : CommRing β
f : β →+ α
h :
  ∀ (x : β), (f : (a : β) → α) (x * x) = HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) x : α)
h_two : Ne.{u_2 + 1} (α := α) 2 0
h_one : Eq.{u_2 + 1} (α := α) ((f : (a : β) → α) 1 : α) (1 : α)
⊢ (↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) : β →+ α) = f
have h₁ : ∀ (x : β),
  Eq.{u_2 + 1} (α := α) (((↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) : β →+ α) : (a : β) → α) x : α)
    ((f : (a : β) → α) x : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ IsIdempotentElem (1 - a)
have rw : (1 - a) * (1 - a) = 1 - a
Tactic: rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
rw : (1 - a) * (1 - a) = 1 - a
⊢ IsIdempotentElem (1 - a)
have rw₁ : (1 - a) * 1 - (1 - a) * a = 1 - a
Tactic: rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
rw : (1 - a) * (1 - a) = 1 - a
rw₁ : (1 - a) * 1 - (1 - a) * a = 1 - a
⊢ IsIdempotentElem (1 - a)
have rw₂ : 1 - a - (1 - a) * a = 1 - a
Tactic: rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
rw : (1 - a) * (1 - a) = 1 - a
rw₁ : (1 - a) * 1 - (1 - a) * a = 1 - a
rw₂ : 1 - a - (1 - a) * a = 1 - a
⊢ IsIdempotentElem (1 - a)
have rw₃ : 1 - a - (1 * a - a * a) = 1 - a
Tactic: rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
rw : (1 - a) * (1 - a) = 1 - a
rw₁ : (1 - a) * 1 - (1 - a) * a = 1 - a
rw₂ : 1 - a - (1 - a) * a = 1 - a
rw₃ : 1 - a - (1 * a - a * a) = 1 - a
⊢ IsIdempotentElem (1 - a)
have rw₄ : 1 - a - (a - a * a) = 1 - a
Tactic: rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
rw : (1 - a) * (1 - a) = 1 - a
rw₁ : (1 - a) * 1 - (1 - a) * a = 1 - a
rw₂ : 1 - a - (1 - a) * a = 1 - a
rw₃ : 1 - a - (1 * a - a * a) = 1 - a
rw₄ : 1 - a - (a - a * a) = 1 - a
⊢ IsIdempotentElem (1 - a)
have rw₅ : 1 - a - (a - a) = 1 - a
Tactic: rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
rw : (1 - a) * (1 - a) = 1 - a
rw₁ : (1 - a) * 1 - (1 - a) * a = 1 - a
rw₂ : 1 - a - (1 - a) * a = 1 - a
rw₃ : 1 - a - (1 * a - a * a) = 1 - a
rw₄ : 1 - a - (a - a * a) = 1 - a
rw₅ : 1 - a - (a - a) = 1 - a
⊢ IsIdempotentElem (1 - a)
have rw₆ : 1 - a - 0 = 1 - a
Tactic: rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
rw : (1 - a) * (1 - a) = 1 - a
rw₁ : (1 - a) * 1 - (1 - a) * a = 1 - a
rw₂ : 1 - a - (1 - a) * a = 1 - a
rw₃ : 1 - a - (1 * a - a * a) = 1 - a
rw₄ : 1 - a - (a - a * a) = 1 - a
rw₅ : 1 - a - (a - a) = 1 - a
rw₆ : 1 - a - 0 = 1 - a
⊢ IsIdempotentElem (1 - a)
have rw₇ : 1 - a = 1 - a
Tactic: rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ a * (1 - a) = 0
have rw : a * 1 - a * a = 0
Tactic: rw [mul_sub, mul_one, h.eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
rw : a * 1 - a * a = 0
⊢ a * (1 - a) = 0
have rw₁ : a - a * a = 0
Tactic: rw [mul_sub, mul_one, h.eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
rw : a * 1 - a * a = 0
rw₁ : a - a * a = 0
⊢ a * (1 - a) = 0
have rw₂ : a - a = 0
Tactic: rw [mul_sub, mul_one, h.eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
rw : a * 1 - a * a = 0
rw₁ : a - a * a = 0
rw₂ : a - a = 0
⊢ a * (1 - a) = 0
have rw₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [mul_sub, mul_one, h.eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ (1 - a) * a = 0
have rw : 1 * a - a * a = 0
Tactic: rw [sub_mul, one_mul, h.eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
rw : 1 * a - a * a = 0
⊢ (1 - a) * a = 0
have rw₁ : a - a * a = 0
Tactic: rw [sub_mul, one_mul, h.eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
rw : 1 * a - a * a = 0
rw₁ : a - a * a = 0
⊢ (1 - a) * a = 0
have rw₂ : a - a = 0
Tactic: rw [sub_mul, one_mul, h.eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
h : IsIdempotentElem a
rw : 1 * a - a * a = 0
rw₁ : a - a * a = 0
rw₂ : a - a = 0
⊢ (1 - a) * a = 0
have rw₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [sub_mul, one_mul, h.eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
⊢ IsIdempotentElem a ↔ a * (1 - a) = 0
have rw : IsIdempotentElem a ↔ a * 1 - a * a = 0
Tactic: rw [mul_sub, mul_one, sub_eq_zero, eq_comm, IsIdempotentElem]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
rw : IsIdempotentElem a ↔ a * 1 - a * a = 0
⊢ IsIdempotentElem a ↔ a * (1 - a) = 0
have rw₁ : IsIdempotentElem a ↔ a - a * a = 0
Tactic: rw [mul_sub, mul_one, sub_eq_zero, eq_comm, IsIdempotentElem]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
rw : IsIdempotentElem a ↔ a * 1 - a * a = 0
rw₁ : IsIdempotentElem a ↔ a - a * a = 0
⊢ IsIdempotentElem a ↔ a * (1 - a) = 0
have rw₂ : IsIdempotentElem a ↔ a = a * a
Tactic: rw [mul_sub, mul_one, sub_eq_zero, eq_comm, IsIdempotentElem]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
rw : IsIdempotentElem a ↔ a * 1 - a * a = 0
rw₁ : IsIdempotentElem a ↔ a - a * a = 0
rw₂ : IsIdempotentElem a ↔ a = a * a
⊢ IsIdempotentElem a ↔ a * (1 - a) = 0
have rw₃ : IsIdempotentElem a ↔ a * a = a
Tactic: rw [mul_sub, mul_one, sub_eq_zero, eq_comm, IsIdempotentElem]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
rw : IsIdempotentElem a ↔ a * 1 - a * a = 0
rw₁ : IsIdempotentElem a ↔ a - a * a = 0
rw₂ : IsIdempotentElem a ↔ a = a * a
rw₃ : IsIdempotentElem a ↔ a * a = a
⊢ IsIdempotentElem a ↔ a * (1 - a) = 0
have rw₄ : a * a = a ↔ a * a = a
Tactic: rw [mul_sub, mul_one, sub_eq_zero, eq_comm, IsIdempotentElem]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
⊢ IsIdempotentElem a ↔ (1 - a) * a = 0
have rw : IsIdempotentElem a ↔ 1 * a - a * a = 0
Tactic: rw [sub_mul, one_mul, sub_eq_zero, eq_comm, IsIdempotentElem]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
rw : IsIdempotentElem a ↔ 1 * a - a * a = 0
⊢ IsIdempotentElem a ↔ (1 - a) * a = 0
have rw₁ : IsIdempotentElem a ↔ a - a * a = 0
Tactic: rw [sub_mul, one_mul, sub_eq_zero, eq_comm, IsIdempotentElem]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
rw : IsIdempotentElem a ↔ 1 * a - a * a = 0
rw₁ : IsIdempotentElem a ↔ a - a * a = 0
⊢ IsIdempotentElem a ↔ (1 - a) * a = 0
have rw₂ : IsIdempotentElem a ↔ a = a * a
Tactic: rw [sub_mul, one_mul, sub_eq_zero, eq_comm, IsIdempotentElem]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
rw : IsIdempotentElem a ↔ 1 * a - a * a = 0
rw₁ : IsIdempotentElem a ↔ a - a * a = 0
rw₂ : IsIdempotentElem a ↔ a = a * a
⊢ IsIdempotentElem a ↔ (1 - a) * a = 0
have rw₃ : IsIdempotentElem a ↔ a * a = a
Tactic: rw [sub_mul, one_mul, sub_eq_zero, eq_comm, IsIdempotentElem]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
rw : IsIdempotentElem a ↔ 1 * a - a * a = 0
rw₁ : IsIdempotentElem a ↔ a - a * a = 0
rw₂ : IsIdempotentElem a ↔ a = a * a
rw₃ : IsIdempotentElem a ↔ a * a = a
⊢ IsIdempotentElem a ↔ (1 - a) * a = 0
have rw₄ : a * a = a ↔ a * a = a
Tactic: rw [sub_mul, one_mul, sub_eq_zero, eq_comm, IsIdempotentElem]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
a : { a : R // IsIdempotentElem a }
⊢ aᶜᶜ = a
have a₁ : (↑aᶜᶜ : R) = (↑a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
⊢ Eq.{u_1 + 1} (α := { a : R // IsIdempotentElem a }) 0ᶜ 1
have a : Eq.{u_1 + 1} (α := R) (↑0ᶜ : R) (↑1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
⊢ Eq.{u_1 + 1} (α := { a : R // IsIdempotentElem a }) 1ᶜ 0
have a : Eq.{u_1 + 1} (α := R) (↑1ᶜ : R) (↑0 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ a * a = a ∧ b * b = b
have left : a * a = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
left : a * a = a
⊢ a * a = a ∧ b * b = b
have right : b * b = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
| a
have rw : a * a
Tactic: rw [← mul_one a, ← add, mul_add, mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ a * a = a
have conv_rhs : a * a = a
Tactic: conv_rhs => rw [← mul_one a, ← add, mul_add, mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
conv_rhs : a * a = a
⊢ a * a = a
have left : a * a = a * a
Tactic: conv_rhs => rw [← mul_one a, ← add, mul_add, mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
| b
have rw : b * b
Tactic: rw [← one_mul b, ← add, add_mul, mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ b * b = b
have conv_rhs : b * b = b
Tactic: conv_rhs => rw [← one_mul b, ← add, add_mul, mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
conv_rhs : b * b = b
⊢ b * b = b
have right : b * b = b * b
Tactic: conv_rhs => rw [← one_mul b, ← add, add_mul, mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
a b : R
h : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ IsIdempotentElem (a + b - a * b)
have simp : a * (b * a) + b * a - b * (a * (b * a)) = b * a
Tactic: simp only [IsIdempotentElem, h.eq, mul_sub, mul_add, sub_mul, add_mul, ha.eq,
    mul_assoc, add_sub_cancel_right, hb.eq, hb.mul_self_mul, add_sub_cancel_left, sub_right_inj]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
a b : R
h : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ a * (b * a) + b * a - b * (a * (b * a)) = b * a
have rw : a * (a * b) + a * b - b * (a * (a * b)) = a * b
Tactic: rw [← h.eq, ha.mul_self_mul, h.eq, hb.mul_self_mul, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
a b : R
h : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
rw : a * (a * b) + a * b - b * (a * (a * b)) = a * b
⊢ a * (b * a) + b * a - b * (a * (b * a)) = b * a
have rw₁ : a * b + a * b - b * (a * b) = a * b
Tactic: rw [← h.eq, ha.mul_self_mul, h.eq, hb.mul_self_mul, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
a b : R
h : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
rw : a * (a * b) + a * b - b * (a * (a * b)) = a * b
rw₁ : a * b + a * b - b * (a * b) = a * b
⊢ a * (b * a) + b * a - b * (a * (b * a)) = b * a
have rw₂ : b * a + b * a - b * (b * a) = b * a
Tactic: rw [← h.eq, ha.mul_self_mul, h.eq, hb.mul_self_mul, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
a b : R
h : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
rw : a * (a * b) + a * b - b * (a * (a * b)) = a * b
rw₁ : a * b + a * b - b * (a * b) = a * b
rw₂ : b * a + b * a - b * (b * a) = b * a
⊢ a * (b * a) + b * a - b * (a * (b * a)) = b * a
have rw₃ : b * a + b * a - b * a = b * a
Tactic: rw [← h.eq, ha.mul_self_mul, h.eq, hb.mul_self_mul, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
a b : R
h : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
rw : a * (a * b) + a * b - b * (a * (a * b)) = a * b
rw₁ : a * b + a * b - b * (a * b) = a * b
rw₂ : b * a + b * a - b * (b * a) = b * a
rw₃ : b * a + b * a - b * a = b * a
⊢ a * (b * a) + b * a - b * (a * (b * a)) = b * a
have rw₄ : b * a = b * a
Tactic: rw [← h.eq, ha.mul_self_mul, h.eq, hb.mul_self_mul, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
⊢ IsIdempotentElem (a + b)
have simp_rw : (a + b) * (a + b) = a + b
Tactic: simp_rw [IsIdempotentElem, mul_add, add_mul, ha.eq, hb.eq, add_add_add_comm, ← add_assoc,
    add_assoc a, hab, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
simp_rw : (a + b) * (a + b) = a + b
⊢ IsIdempotentElem (a + b)
have simp_rw₁ : (a + b) * a + (a + b) * b = a + b
Tactic: simp_rw [IsIdempotentElem, mul_add, add_mul, ha.eq, hb.eq, add_add_add_comm, ← add_assoc,
    add_assoc a, hab, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
simp_rw : (a + b) * (a + b) = a + b
simp_rw₁ : (a + b) * a + (a + b) * b = a + b
⊢ IsIdempotentElem (a + b)
have simp_rw₂ : a * a + b * a + (a * b + b * b) = a + b
Tactic: simp_rw [IsIdempotentElem, mul_add, add_mul, ha.eq, hb.eq, add_add_add_comm, ← add_assoc,
    add_assoc a, hab, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
simp_rw : (a + b) * (a + b) = a + b
simp_rw₁ : (a + b) * a + (a + b) * b = a + b
simp_rw₂ : a * a + b * a + (a * b + b * b) = a + b
⊢ IsIdempotentElem (a + b)
have simp_rw₃ : a + b * a + (a * b + b * b) = a + b
Tactic: simp_rw [IsIdempotentElem, mul_add, add_mul, ha.eq, hb.eq, add_add_add_comm, ← add_assoc,
    add_assoc a, hab, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
simp_rw : (a + b) * (a + b) = a + b
simp_rw₁ : (a + b) * a + (a + b) * b = a + b
simp_rw₂ : a * a + b * a + (a * b + b * b) = a + b
simp_rw₃ : a + b * a + (a * b + b * b) = a + b
⊢ IsIdempotentElem (a + b)
have simp_rw₄ : a + b * a + (a * b + b) = a + b
Tactic: simp_rw [IsIdempotentElem, mul_add, add_mul, ha.eq, hb.eq, add_add_add_comm, ← add_assoc,
    add_assoc a, hab, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
simp_rw : (a + b) * (a + b) = a + b
simp_rw₁ : (a + b) * a + (a + b) * b = a + b
simp_rw₂ : a * a + b * a + (a * b + b * b) = a + b
simp_rw₃ : a + b * a + (a * b + b * b) = a + b
simp_rw₄ : a + b * a + (a * b + b) = a + b
⊢ IsIdempotentElem (a + b)
have simp_rw₅ : a + a * b + (b * a + b) = a + b
Tactic: simp_rw [IsIdempotentElem, mul_add, add_mul, ha.eq, hb.eq, add_add_add_comm, ← add_assoc,
    add_assoc a, hab, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
simp_rw : (a + b) * (a + b) = a + b
simp_rw₁ : (a + b) * a + (a + b) * b = a + b
simp_rw₂ : a * a + b * a + (a * b + b * b) = a + b
simp_rw₃ : a + b * a + (a * b + b * b) = a + b
simp_rw₄ : a + b * a + (a * b + b) = a + b
simp_rw₅ : a + a * b + (b * a + b) = a + b
⊢ IsIdempotentElem (a + b)
have simp_rw₆ : a + a * b + b * a + b = a + b
Tactic: simp_rw [IsIdempotentElem, mul_add, add_mul, ha.eq, hb.eq, add_add_add_comm, ← add_assoc,
    add_assoc a, hab, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
simp_rw : (a + b) * (a + b) = a + b
simp_rw₁ : (a + b) * a + (a + b) * b = a + b
simp_rw₂ : a * a + b * a + (a * b + b * b) = a + b
simp_rw₃ : a + b * a + (a * b + b * b) = a + b
simp_rw₄ : a + b * a + (a * b + b) = a + b
simp_rw₅ : a + a * b + (b * a + b) = a + b
simp_rw₆ : a + a * b + b * a + b = a + b
⊢ IsIdempotentElem (a + b)
have simp_rw₇ : a + (a * b + b * a + b) = a + b
Tactic: simp_rw [IsIdempotentElem, mul_add, add_mul, ha.eq, hb.eq, add_add_add_comm, ← add_assoc,
    add_assoc a, hab, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
simp_rw : (a + b) * (a + b) = a + b
simp_rw₁ : (a + b) * a + (a + b) * b = a + b
simp_rw₂ : a * a + b * a + (a * b + b * b) = a + b
simp_rw₃ : a + b * a + (a * b + b * b) = a + b
simp_rw₄ : a + b * a + (a * b + b) = a + b
simp_rw₅ : a + a * b + (b * a + b) = a + b
simp_rw₆ : a + a * b + b * a + b = a + b
simp_rw₇ : a + (a * b + b * a + b) = a + b
⊢ IsIdempotentElem (a + b)
have simp_rw₈ : a + (0 + b) = a + b
Tactic: simp_rw [IsIdempotentElem, mul_add, add_mul, ha.eq, hb.eq, add_add_add_comm, ← add_assoc,
    add_assoc a, hab, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ IsIdempotentElem (a + b) ↔ a * b + b * a = 0
have refine : ∀ (h : IsIdempotentElem (a + b)), a * b + b * a = 0
Tactic: refine ⟨fun h ↦ ?_, ha.add hb⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a * b + b * a = 0
have rw : a + b * a + (a * b + b) = a + (0 + b)
Tactic: rw [← add_right_cancel_iff (a := b), add_assoc, ← add_left_cancel_iff (a := a),
    ← add_assoc, add_add_add_comm]
-- 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
⊢ IsIdempotentElem (b - a)
have simp_rw : (b - a) * (b - 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
⊢ IsIdempotentElem (b - a)
have simp_rw₁ : b * (b - a) - a * (b - a) = b - a
Tactic: simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero]