awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
x_1 : NonAssocSemiring α
x_2 : NonAssocSemiring β
x_3 : NonAssocSemiring γ
g : β →+* γ
f₁ f₂ : α →+* β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)

Tactic:
rw [← comp_apply, h, comp_apply]

Premises used: RingHom.comp_apply
-- Module: Mathlib.Algebra.Ring.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : Semiring β
f : α →+* β
a : α
⊢ ∀ (n : ℕ), (f : (a : α) → β) (a ^ n) = HPow.hPow (α := β) ((f : (a : α) → β) a : β) n

Tactic:
map_pow f a

Premises used: map_pow
-- Module: Mathlib.Algebra.Ring.Hom.Defs
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 : β
⊢ (f : (a : β) → α) ((x + y) * (x + y)) =
    HMul.hMul (α := α) (β := α) ((f : (a : β) → α) (x + y) : α) ((f : (a : β) → α) (x + y) : α)

Tactic:
have hxy := h (x + y)
-- Module: Mathlib.Algebra.Ring.Hom.Defs
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 :
  (f : (a : β) → α) ((x + y) * (x + y)) =
    HMul.hMul (α := α) (β := α) ((f : (a : β) → α) (x + y) : α) ((f : (a : β) → α) (x + y) : α)
⊢ 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

Tactic:
rw [mul_add, add_mul, add_mul, f.map_add, f.map_add, f.map_add, f.map_add, h x, h y, add_mul,
        mul_add, mul_add, ← sub_eq_zero, add_comm (f x * f x + f (y * x)), ← sub_sub, ← sub_sub,
        ← sub_sub, mul_comm y x, mul_comm (f y) (f x)] at hxy

Premises used: add_mul, HMul.hMul, sub_eq_zero, add_comm, sub_sub, HAdd.hAdd, mul_comm, mul_add, AddMonoidHom.map_add, DFunLike.coe
-- Module: Mathlib.Algebra.Ring.Hom.Defs
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
⊢ 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

Premises used: add_sub_assoc, add_assoc, add_sub_cancel
-- Module: Mathlib.Algebra.Ring.Hom.Defs
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
⊢ ¬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

Premises used: add_sub_assoc, mul_sub, sub_eq_zero, two_mul, mul_eq_zero, sub_sub, Classical.or_iff_not_imp_left
-- Module: Mathlib.Algebra.Ring.Hom.Defs
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 :
  ¬Eq.{u_2 + 1} (α := α) 2 0 →
    (f : (a : β) → α) (x * y) = HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α)
⊢ (↑f : ZeroHom β α).toFun (x * y) = (↑f : ZeroHom β α).toFun x * (↑f : ZeroHom β α).toFun y

Tactic:
hxy h_two
-- Module: Mathlib.Algebra.Ring.Hom.Defs
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 :
  ¬Eq.{u_2 + 1} (α := α) 2 0 →
    (f : (a : β) → α) (x * y) = HMul.hMul (α := α) (β := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α)
⊢ (↑f : ZeroHom β α).toFun (x * y) = (↑f : ZeroHom β α).toFun x * (↑f : ZeroHom β α).toFun y

Tactic:
exact hxy h_two
-- Module: Mathlib.Algebra.Ring.Hom.Defs
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 : α)
⊢ Eq (α := (a : β) → α) (⇑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) : (a : β) → α) (⇑f : (a : β) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Hom.Defs
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 : α)
h₁ :
  ∀ (x : β),
    Eq.{u_2 + 1} (α := α) (((↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) : β →+ α) : (a : β) → α) x : α)
      ((f : (a : β) → α) x : α)
⊢ (↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) : β →+ α) = f

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Hom.Defs
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 : α)
x : β
⊢ Eq.{u_2 + 1} (α := α) (((↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) : β →+ α) : (a : β) → α) x : α)
    ((f : (a : β) → α) x : α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.Idempotent
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
rw₇ rw₈ : 1 - a = 1 - a
⊢ IsIdempotentElem (1 - a)

Tactic:
rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]

Premises used: mul_sub, sub_self, sub_zero, sub_mul, IsIdempotentElem, IsIdempotentElem.eq, mul_one, one_mul
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonAssocRing R
a : R
⊢ IsIdempotentElem (1 - a) ↔ IsIdempotentElem a

Tactic:
⟨fun h => sub_sub_cancel 1 a ▸ h.one_sub, IsIdempotentElem.one_sub⟩

Premises used: IsIdempotentElem.one_sub, Eq.rec, sub_sub_cancel, Iff.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Idempotent
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
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ a * (1 - a) = 0

Tactic:
rw [mul_sub, mul_one, h.eq, sub_self]

Premises used: mul_sub, sub_self, IsIdempotentElem.eq, mul_one
-- Module: Mathlib.Algebra.Ring.Idempotent
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
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (1 - a) * a = 0

Tactic:
rw [sub_mul, one_mul, h.eq, sub_self]

Premises used: sub_self, sub_mul, IsIdempotentElem.eq, one_mul
-- Module: Mathlib.Algebra.Ring.Idempotent
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
rw₄ rw₅ : a * a = a ↔ a * a = a
⊢ IsIdempotentElem a ↔ a * (1 - a) = 0

Tactic:
rw [mul_sub, mul_one, sub_eq_zero, eq_comm, IsIdempotentElem]

Premises used: mul_sub, sub_eq_zero, eq_comm, IsIdempotentElem, mul_one
-- Module: Mathlib.Algebra.Ring.Idempotent
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
rw₄ rw₅ : a * a = a ↔ a * a = a
⊢ IsIdempotentElem a ↔ (1 - a) * a = 0

Tactic:
rw [sub_mul, one_mul, sub_eq_zero, eq_comm, IsIdempotentElem]

Premises used: sub_eq_zero, eq_comm, sub_mul, IsIdempotentElem, one_mul
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonAssocRing R
a : { a : R // IsIdempotentElem a }
⊢ (↑aᶜ : R) = 1 - (↑a : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonAssocRing R
a : { a : R // IsIdempotentElem a }
a₁ : (↑aᶜᶜ : R) = (↑a : R)
⊢ aᶜᶜ = a

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonAssocRing R
a : { a : R // IsIdempotentElem a }
⊢ (↑aᶜᶜ : R) = (↑a : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonAssocRing R
a : Eq.{u_1 + 1} (α := R) (↑0ᶜ : R) (↑1 : R)
⊢ Eq.{u_1 + 1} (α := { a : R // IsIdempotentElem a }) 0ᶜ 1

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonAssocRing R
⊢ Eq.{u_1 + 1} (α := R) (↑0ᶜ : R) (↑1 : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonAssocRing R
a : Eq.{u_1 + 1} (α := R) (↑1ᶜ : R) (↑0 : R)
⊢ Eq.{u_1 + 1} (α := { a : R // IsIdempotentElem a }) 1ᶜ 0

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonAssocRing R
⊢ Eq.{u_1 + 1} (α := R) (↑1ᶜ : R) (↑0 : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
left : a * a = a
right : b * b = b
⊢ a * a = a ∧ b * b = b

Tactic:
constructor
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
rw : a * a
| a

Tactic:
rw [← mul_one a, ← add, mul_add, mul, add_zero]

Premises used: mul_add, mul_one, add_zero
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
conv_rhs : a * a = a
left : a * a = a * a
⊢ a * a = a

Tactic:
conv_rhs => rw [← mul_one a, ← add, mul_add, mul, add_zero]

Premises used: mul_add, mul_one, add_zero
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
rw : b * b
| b

Tactic:
rw [← one_mul b, ← add, add_mul, mul, zero_add]

Premises used: add_mul, zero_add, one_mul
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
conv_rhs : b * b = b
right : b * b = b * b
⊢ b * b = b

Tactic:
conv_rhs => rw [← one_mul b, ← add, add_mul, mul, zero_add]

Premises used: add_mul, zero_add, one_mul
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
a b : R
h : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
simp : a * (b * a) + b * a - b * (a * (b * a)) = b * a
⊢ IsIdempotentElem (a + b - a * b)

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]

Premises used: add_mul, mul_sub, add_sub_cancel_left, IsIdempotentElem.mul_self_mul, sub_right_inj, mul_assoc, sub_mul, IsIdempotentElem, mul_add, IsIdempotentElem.eq, add_sub_cancel_right, Commute.eq
-- Module: Mathlib.Algebra.Ring.Idempotent
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
rw₄ rw₅ : b * a = b * a
⊢ a * (b * a) + 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]

Premises used: IsIdempotentElem.mul_self_mul, add_sub_cancel_right, Commute.eq
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a b : R
hp : IsIdempotentElem a
hq : IsIdempotentElem b
⊢ IsIdempotentElem (a + b - a * b)

Tactic:
add_sub_mul_of_commute (.all ..) hp hq

Premises used: IsIdempotentElem.add_sub_mul_of_commute, Commute.all
-- Module: Mathlib.Algebra.Ring.Idempotent
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
simp_rw₈ : a + (0 + b) = a + b
⊢ IsIdempotentElem (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]

Premises used: add_mul, add_assoc, zero_add, IsIdempotentElem, mul_add, IsIdempotentElem.eq, add_add_add_comm
-- Module: Mathlib.Algebra.Ring.Idempotent
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

Tactic:
⟨fun h ↦ ?_, ha.add hb⟩

Premises used: IsIdempotentElem.add, Iff.intro
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
refine : ∀ (h : IsIdempotentElem (a + b)), a * b + b * a = 0
⊢ IsIdempotentElem (a + b) ↔ a * b + b * a = 0

Tactic:
refine ⟨fun h ↦ ?_, ha.add hb⟩
-- Module: Mathlib.Algebra.Ring.Idempotent
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)
rw : a + b * a + (a * b + b) = a + (0 + b)
⊢ a * b + b * a = 0

Tactic:
rw [← add_right_cancel_iff (a := b), add_assoc, ← add_left_cancel_iff (a := a),
    ← add_assoc, add_add_add_comm]

Premises used: add_assoc, add_left_cancel_iff, add_right_cancel_iff, add_add_add_comm
-- Module: Mathlib.Algebra.Ring.Idempotent
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 * a + (a * b + b) = a + (0 + b)

Tactic:
simpa [add_mul, mul_add, ha.eq, hb.eq] using h.eq

Premises used: add_mul, mul_add, IsIdempotentElem.eq
-- Module: Mathlib.Algebra.Ring.Idempotent
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
simp_rw₇ : b - a - 0 = b - a
⊢ IsIdempotentElem (b - a)

Tactic:
simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero]

Premises used: mul_sub, sub_self, sub_zero, sub_mul, IsIdempotentElem, IsIdempotentElem.eq
-- Module: Mathlib.Algebra.Ring.Idempotent
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 : HAdd.hAdd (α := ℕ) 1 1 • (a * b * a) = 0
⊢ a * b * a = 0

Tactic:
rw [← nsmul_right_inj ((Nat.zero_ne_add_one 1).symm), nsmul_zero]

Premises used: nsmul_zero, Ne.symm, nsmul_right_inj, OfNat.ofNat, Nat.zero_ne_add_one
-- Module: Mathlib.Algebra.Ring.Idempotent
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ a * (a * b + b * a) * a = 0

Tactic:
rw [hab, mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Ring.Idempotent
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

Tactic:
have : a * (a * b + b * a) * a = 0 := by rw [hab, mul_zero, zero_mul]
-- Module: Mathlib.Algebra.Ring.Idempotent
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 * (a * b + b * a) * a = 0
⊢ HSMul.hSMul (α := ℕ) 2 (a * b * a) = 0

Tactic:
simp_rw [mul_add, add_mul, mul_assoc, ha.eq, ← mul_assoc, ha.eq, ← two_nsmul] at this

Premises used: add_mul, mul_assoc, mul_add, IsIdempotentElem.eq, two_nsmul
-- Module: Mathlib.Algebra.Ring.Idempotent
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 : HSMul.hSMul (α := ℕ) 2 (a * b * a) = 0
⊢ HAdd.hAdd (α := ℕ) 1 1 • (a * b * a) = 0

Tactic:
this
-- Module: Mathlib.Algebra.Ring.Idempotent
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 : HSMul.hSMul (α := ℕ) 2 (a * b * a) = 0
⊢ HAdd.hAdd (α := ℕ) 1 1 • (a * b * a) = 0

Tactic:
exact this
-- Module: Mathlib.Algebra.Ring.Idempotent
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

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
-- Module: Mathlib.Algebra.Ring.Idempotent
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
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : a * b = 0), a * b = 0
⊢ a * b = 0

Tactic:
rwa [h, add_zero, ha.eq] at this

Premises used: IsIdempotentElem.eq, add_zero
-- Module: Mathlib.Algebra.Ring.Idempotent
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
suffices : a * a * b + a * b * a = 0
⊢ a * b = 0

Tactic:
suffices a * a * b + a * b * a = 0 by rwa [h, add_zero, ha.eq] at this
-- Module: Mathlib.Algebra.Ring.Idempotent
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
rw₄ rw₅ : Eq.{u_1 + 1} (α := R) 0 0
⊢ a * a * b + a * b * a = 0

Tactic:
rw [mul_assoc, mul_assoc, ← mul_add, hab, mul_zero]

Premises used: mul_assoc, MulZeroClass.mul_zero, mul_add
-- Module: Mathlib.Algebra.Ring.Idempotent
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

Tactic:
have := mul_eq_zero_of_anticommute ha hab
-- Module: Mathlib.Algebra.Ring.Idempotent
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
⊢ b * a = 0

Tactic:
rw [this, zero_add] at hab

Premises used: zero_add
-- Module: Mathlib.Algebra.Ring.Idempotent
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
hab₁ : b * a = 0
⊢ a * b = 0

Tactic:
rw [this, zero_add] at hab

Premises used: zero_add
-- Module: Mathlib.Algebra.Ring.Idempotent
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
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Commute a b

Tactic:
rw [Commute, SemiconjBy, hab, this]

Premises used: SemiconjBy, Commute
-- Module: Mathlib.Algebra.Ring.Idempotent
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

Tactic:
⟨fun hqp ↦ ?_, fun ⟨h1, h2⟩ => hp.sub hq h1 h2⟩

Premises used: HSub.hSub, IsIdempotentElem, Iff.intro, _private.0.IsIdempotentElem.sub_iff.match_1, IsIdempotentElem.sub
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
refine : ∀ (hqp : IsIdempotentElem (q - p)), p * q = p ∧ q * p = p
⊢ IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p

Tactic:
refine ⟨fun hqp ↦ ?_, fun ⟨h1, h2⟩ => hp.sub hq h1 h2⟩
-- Module: Mathlib.Algebra.Ring.Idempotent
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 = 0

Tactic:
have h : p * (q - p) + (q - p) * p = 0 := hp.add_iff hqp |>.mp ((add_sub_cancel p q).symm ▸ hq)