awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
refine_3 : (↑b : R × R).1 + (↑a : R × R).2 = 1
refine_3₁ : (↑b : R × R).1 + (↑b : R × R).2 = 1
refine_3₂ refine_3₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ (↑a : R × R).2 + (↑b : R × R).1 = 1

Tactic:
rw [add_comm, eq, b.2.2]

Premises used: add_comm, And.right, Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b c : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a : R × R).1 * (↑b : R × R).1 = (↑a : R × R).1
hbc : (↑b : R × R).1 * (↑c : R × R).1 = (↑b : R × R).1
rw : (↑a : R × R).1 * (↑b : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1 * (↑b : R × R).1
rw₁ : (↑a : R × R).1 * ((↑b : R × R).1 * (↑c : R × R).1) = (↑a : R × R).1 * (↑b : R × R).1
rw₂ rw₃ : (↑a : R × R).1 * (↑b : R × R).1 = (↑a : R × R).1 * (↑b : R × R).1
⊢ (↑a : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1

Tactic:
rw [← hab, mul_assoc, hbc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a : R × R).1 * (↑b : R × R).1 = (↑a : R × R).1
hba : (↑b : R × R).1 * (↑a : R × R).1 = (↑b : R × R).1
rw : (↑a : R × R).1 * (↑b : R × R).1 = (↑b : R × R).1
rw₁ : (↑b : R × R).1 * (↑a : R × R).1 = (↑b : R × R).1
rw₂ rw₃ : (↑b : R × R).1 = (↑b : R × R).1
⊢ (↑a : R × R).1 = (↑b : R × R).1

Tactic:
rw [← hab, mul_comm, hba]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
simp_rw simp_rw₁ : ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1) * ((↑a : R × R).2 * (↑b : R × R).2) = 0
simp_rw₂ :
  (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) +
      (↑a : R × R).2 * (↑b : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) =
    0
simp_rw₃ :
  (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) +
      (↑a : R × R).2 * (↑a : R × R).2 * ((↑b : R × R).1 * (↑b : R × R).2) =
    0
simp_rw₄ : (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) + (↑a : R × R).2 * (↑a : R × R).2 * 0 = 0
simp_rw₅ : (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) + 0 = 0
simp_rw₆ : (↑a : R × R).1 * (↑a : R × R).2 * (↑b : R × R).2 + 0 = 0
simp_rw₇ : 0 * (↑b : R × R).2 + 0 = 0
simp_rw₈ : HAdd.hAdd (α := R) 0 0 = 0
⊢ ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2).1 *
      ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2).2 =
    0

Tactic:
simp_rw [add_mul,
      mul_mul_mul_comm _ b.1.1, b.2.1, mul_zero, ← mul_assoc, a.2.1, zero_mul, add_zero]

Premises used: add_mul, mul_mul_mul_comm, MulZeroClass.zero_mul, mul_assoc, Prod.fst, MulZeroClass.mul_zero, And.left, add_zero, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
simp_rw simp_rw₁ : (↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1 + (↑a : R × R).2 * (↑b : R × R).2 = 1
simp_rw₂ : (↑a : R × R).1 + ((↑a : R × R).2 * (↑b : R × R).1 + (↑a : R × R).2 * (↑b : R × R).2) = 1
simp_rw₃ : (↑a : R × R).1 + (↑a : R × R).2 * ((↑b : R × R).1 + (↑b : R × R).2) = 1
simp_rw₄ : (↑a : R × R).1 + (↑a : R × R).2 * 1 = 1
simp_rw₅ : (↑a : R × R).1 + (↑a : R × R).2 = 1
⊢ ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2).1 +
      ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2).2 =
    1

Tactic:
simp_rw [add_assoc, ← mul_add, b.2.2, mul_one, a.2.2]

Premises used: add_assoc, And.right, mul_add, mul_one, Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
simp_rw : (↑a : R × R).1 * ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1) = (↑a : R × R).1
simp_rw₁ : (↑a : R × R).1 * (↑a : R × R).1 + (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).1) = (↑a : R × R).1
simp_rw₂ : (↑a : R × R).1 * (↑a : R × R).1 + (↑a : R × R).1 * (↑a : R × R).2 * (↑b : R × R).1 = (↑a : R × R).1
simp_rw₃ : (↑a : R × R).1 * (↑a : R × R).1 + 0 * (↑b : R × R).1 = (↑a : R × R).1
simp_rw₄ : (↑a : R × R).1 * (↑a : R × R).1 + 0 = (↑a : R × R).1
simp_rw₅ : (↑a : R × R).1 * (↑a : R × R).1 = (↑a : R × R).1
⊢ a ≤
    Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
      ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2) ⋯

Tactic:
simp_rw [(· ≤ ·), mul_add, ← mul_assoc, a.2.1, zero_mul, add_zero,
      (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq]

Premises used: IsIdempotentElem.of_mul_add, MulZeroClass.zero_mul, mul_assoc, LE.le, And.right, And.left, mul_add, IsIdempotentElem.eq, add_zero, Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
simp_rw : (↑b : R × R).1 * ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1) = (↑b : R × R).1
simp_rw₁ : (↑b : R × R).1 * (↑a : R × R).1 + (↑b : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).1) = (↑b : R × R).1
simp_rw₂ : (↑b : R × R).1 * (↑a : R × R).1 + (↑b : R × R).1 * ((↑b : R × R).1 * (↑a : R × R).2) = (↑b : R × R).1
simp_rw₃ : (↑b : R × R).1 * (↑a : R × R).1 + (↑b : R × R).1 * (↑b : R × R).1 * (↑a : R × R).2 = (↑b : R × R).1
simp_rw₄ : (↑b : R × R).1 * (↑a : R × R).1 + (↑b : R × R).1 * (↑a : R × R).2 = (↑b : R × R).1
simp_rw₅ : (↑b : R × R).1 * ((↑a : R × R).1 + (↑a : R × R).2) = (↑b : R × R).1
simp_rw₆ : (↑b : R × R).1 * 1 = (↑b : R × R).1
⊢ b ≤
    Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
      ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2) ⋯

Tactic:
simp_rw [(· ≤ ·), mul_add, mul_comm a.1.2, ← mul_assoc,
      (IsIdempotentElem.of_mul_add b.2.1 b.2.2).1.eq, ← mul_add, a.2.2, mul_one]

Premises used: IsIdempotentElem.of_mul_add, mul_assoc, LE.le, And.right, And.left, mul_comm, mul_add, IsIdempotentElem.eq, mul_one, Subtype.val, Prod.snd, Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b c : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hac : a ≤ c
hbc : b ≤ c
simp_rw :
  (↑a : R × R).1 * (↑c : R × R).1 + (↑a : R × R).2 * ((↑b : R × R).1 * (↑c : R × R).1) =
    (↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1
⊢ Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
      ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2) ⋯ ≤
    c

Tactic:
simp_rw [(· ≤ ·), add_mul, mul_assoc]

Premises used: add_mul, mul_assoc, LE.le
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b c : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hac : a ≤ c
hbc : b ≤ c
rw :
  (↑a : R × R).1 + (↑a : R × R).2 * ((↑b : R × R).1 * (↑c : R × R).1) = (↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1
rw₁ rw₂ : (↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1 = (↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1
⊢ (↑a : R × R).1 * (↑c : R × R).1 + (↑a : R × R).2 * ((↑b : R × R).1 * (↑c : R × R).1) =
    (↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1

Tactic:
rw [hac, hbc]
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
simp_rw : (↑(aᶜ ⊔ bᶜ)ᶜ : R × R).1 * (↑a : R × R).1 = (↑(aᶜ ⊔ bᶜ)ᶜ : R × R).1
simp_rw₁ : (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ : R × R).1 * (↑a : R × R).1 = (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ : R × R).1
simp_rw₂ :
  (↑(SemilatticeSup.sup
              (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1) ((↑a : R × R).2, (↑a : R × R).1) ⋯)
              (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1) ((↑b : R × R).2, (↑b : R × R).1) ⋯)) :
          R × R).2 *
      (↑a : R × R).1 =
    (↑(SemilatticeSup.sup
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1) ((↑a : R × R).2, (↑a : R × R).1) ⋯)
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1) ((↑b : R × R).2, (↑b : R × R).1) ⋯)) :
        R × R).2
simp_rw₃ : (↑a : R × R).1 * (↑b : R × R).1 * (↑a : R × R).1 = (↑a : R × R).1 * (↑b : R × R).1
simp_rw₄ : (↑a : R × R).1 * (↑a : R × R).1 * (↑b : R × R).1 = (↑a : R × R).1 * (↑b : R × R).1
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ a

Tactic:
simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup,
    mul_right_comm, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq]

Premises used: IsIdempotentElem.of_mul_add, Compl.compl, LE.le, And.right, And.left, Max.max, mul_right_comm, IsIdempotentElem.eq, Subtype.property, SemilatticeSup.sup
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
simp_rw : (↑(aᶜ ⊔ bᶜ)ᶜ : R × R).1 * (↑b : R × R).1 = (↑(aᶜ ⊔ bᶜ)ᶜ : R × R).1
simp_rw₁ : (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ : R × R).1 * (↑b : R × R).1 = (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ : R × R).1
simp_rw₂ :
  (↑(SemilatticeSup.sup
              (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1) ((↑a : R × R).2, (↑a : R × R).1) ⋯)
              (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1) ((↑b : R × R).2, (↑b : R × R).1) ⋯)) :
          R × R).2 *
      (↑b : R × R).1 =
    (↑(SemilatticeSup.sup
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1) ((↑a : R × R).2, (↑a : R × R).1) ⋯)
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1) ((↑b : R × R).2, (↑b : R × R).1) ⋯)) :
        R × R).2
simp_rw₃ : (↑a : R × R).1 * (↑b : R × R).1 * (↑b : R × R).1 = (↑a : R × R).1 * (↑b : R × R).1
simp_rw₄ : (↑a : R × R).1 * ((↑b : R × R).1 * (↑b : R × R).1) = (↑a : R × R).1 * (↑b : R × R).1
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ b

Tactic:
simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup,
    mul_assoc, (IsIdempotentElem.of_mul_add b.2.1 b.2.2).1.eq]

Premises used: IsIdempotentElem.of_mul_add, Compl.compl, mul_assoc, LE.le, And.right, And.left, Max.max, IsIdempotentElem.eq, Subtype.property, SemilatticeSup.sup
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b c : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : a ≤ b
hac : a ≤ c
simp_rw : (↑a : R × R).1 * (↑b : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1
⊢ a ≤ (bᶜ ⊔ cᶜ)ᶜ

Tactic:
simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup, ← mul_assoc]

Premises used: Compl.compl, mul_assoc, LE.le, Max.max, SemilatticeSup.sup
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b c : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : a ≤ b
hac : a ≤ c
rw : (↑a : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1
rw₁ rw₂ : (↑a : R × R).1 = (↑a : R × R).1
⊢ (↑a : R × R).1 * (↑b : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1

Tactic:
rw [hab, hac]
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b a : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
simp_rw simp_rw₁ : (↑(a ⊓ aᶜ) : R × R).2 = 1
simp_rw₂ : (↑(a ⊓ aᶜ) : R × R).2 = 1
simp_rw₃ : (↑(SemilatticeSup.sup aᶜ aᶜᶜ)ᶜ : R × R).2 = 1
simp_rw₄ :
  (↑(SemilatticeSup.sup
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1) ((↑a : R × R).2, (↑a : R × R).1) ⋯)
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1) ((↑a : R × R).1, (↑a : R × R).2) ⋯)) :
        R × R).1 =
    1
simp_rw₅ : (↑a : R × R).2 + (↑a : R × R).1 * (↑a : R × R).1 = 1
simp_rw₆ : (↑a : R × R).2 + (↑a : R × R).1 = 1
simp_rw₇ : (↑a : R × R).1 + (↑a : R × R).2 = 1
⊢ (↑(a ⊓ aᶜ) : R × R).2 = (↑(Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1) (0, 1) ⋯) : R × R).2

Tactic:
simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup,
      (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq, add_comm, a.2.2]

Premises used: IsIdempotentElem.of_mul_add, Compl.compl, add_comm, And.right, And.left, Max.max, IsIdempotentElem.eq, Min.min, Subtype.property, SemilatticeSup.sup
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b a : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
simp_rw simp_rw₁ : 1 = (↑(a ⊔ aᶜ) : R × R).1
simp_rw₂ : 1 = (↑(SemilatticeSup.sup a aᶜ) : R × R).1
simp_rw₃ :
  1 =
    (↑(SemilatticeSup.sup a
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1) ((↑a : R × R).2, (↑a : R × R).1) ⋯)) :
        R × R).1
simp_rw₄ : 1 = (↑a : R × R).1 + (↑a : R × R).2 * (↑a : R × R).2
simp_rw₅ : 1 = (↑a : R × R).1 + (↑a : R × R).2
⊢ (↑(Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1) (1, 0) ⋯) : R × R).1 = (↑(a ⊔ aᶜ) : R × R).1

Tactic:
simp_rw [(· ⊔ ·), (·ᶜ),
    SemilatticeSup.sup, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, a.2.2]

Premises used: IsIdempotentElem.of_mul_add, Compl.compl, And.right, And.left, Max.max, IsIdempotentElem.eq, Subtype.property, SemilatticeSup.sup
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
S : Type u_2
inst : CommSemigroup S
a b c : { a : S // IsIdempotentElem a }
hab : (↑a : S) * (↑b : S) = (↑a : S)
hbc : (↑b : S) * (↑c : S) = (↑b : S)
rw : (↑a : S) * (↑b : S) * (↑c : S) = (↑a : S) * (↑b : S)
rw₁ : (↑a : S) * ((↑b : S) * (↑c : S)) = (↑a : S) * (↑b : S)
rw₂ rw₃ : (↑a : S) * (↑b : S) = (↑a : S) * (↑b : S)
⊢ (↑a : S) * (↑c : S) = (↑a : S)

Tactic:
rw [← hab, mul_assoc, hbc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
S : Type u_2
inst : CommSemigroup S
a b : { a : S // IsIdempotentElem a }
hab : (↑a : S) * (↑b : S) = (↑a : S)
hba : (↑b : S) * (↑a : S) = (↑b : S)
rw : (↑a : S) * (↑b : S) = (↑b : S)
rw₁ : (↑b : S) * (↑a : S) = (↑b : S)
rw₂ rw₃ : (↑b : S) = (↑b : S)
⊢ (↑a : S) = (↑b : S)

Tactic:
rw [← hab, mul_comm, hba]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
S : Type u_2
inst : CommSemigroup S
a b : { a : S // IsIdempotentElem a }
simp_rw : (↑a : S) * (↑a : S) * (↑b : S) = (↑a : S) * (↑b : S)
⊢ (↑(Subtype.mk (p := fun (a : S) ↦ IsIdempotentElem a) ((↑a : S) * (↑b : S)) ⋯) : S) * (↑a : S) =
    (↑(Subtype.mk (p := fun (a : S) ↦ IsIdempotentElem a) ((↑a : S) * (↑b : S)) ⋯) : S)

Tactic:
simp_rw [mul_right_comm]

Premises used: mul_right_comm
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
S : Type u_2
inst : CommSemigroup S
a b : { a : S // IsIdempotentElem a }
rw rw₁ : (↑a : S) * (↑b : S) = (↑a : S) * (↑b : S)
⊢ (↑a : S) * (↑a : S) * (↑b : S) = (↑a : S) * (↑b : S)

Tactic:
rw [a.2]

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
S : Type u_2
inst : CommSemigroup S
a b : { a : S // IsIdempotentElem a }
simp_rw : (↑a : S) * ((↑b : S) * (↑b : S)) = (↑a : S) * (↑b : S)
⊢ (↑(Subtype.mk (p := fun (a : S) ↦ IsIdempotentElem a) ((↑a : S) * (↑b : S)) ⋯) : S) * (↑b : S) =
    (↑(Subtype.mk (p := fun (a : S) ↦ IsIdempotentElem a) ((↑a : S) * (↑b : S)) ⋯) : S)

Tactic:
simp_rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
S : Type u_2
inst : CommSemigroup S
a b : { a : S // IsIdempotentElem a }
rw rw₁ : (↑a : S) * (↑b : S) = (↑a : S) * (↑b : S)
⊢ (↑a : S) * ((↑b : S) * (↑b : S)) = (↑a : S) * (↑b : S)

Tactic:
rw [b.2]

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
S : Type u_2
inst : CommSemigroup S
a b c : { a : S // IsIdempotentElem a }
hab : (↑a : S) * (↑b : S) = (↑a : S)
hac : (↑a : S) * (↑c : S) = (↑a : S)
simp_rw : (↑a : S) * (↑b : S) * (↑c : S) = (↑a : S)
⊢ (↑a : S) * (↑(Subtype.mk (p := fun (a : S) ↦ IsIdempotentElem a) ((↑b : S) * (↑c : S)) ⋯) : S) = (↑a : S)

Tactic:
simp_rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
S : Type u_2
inst : CommSemigroup S
a b c : { a : S // IsIdempotentElem a }
hab : (↑a : S) * (↑b : S) = (↑a : S)
hac : (↑a : S) * (↑c : S) = (↑a : S)
rw : (↑a : S) * (↑c : S) = (↑a : S)
rw₁ rw₂ : (↑a : S) = (↑a : S)
⊢ (↑a : S) * (↑b : S) * (↑c : S) = (↑a : S)

Tactic:
rw [hab, hac]
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a b : { a : R // IsIdempotentElem a }
simp_rw : (↑a : R) * (↑a : R) + (↑a : R) * (↑b : R) - (↑a : R) * ((↑a : R) * (↑b : R)) = (↑a : R)
⊢ (↑a : R) * (↑(Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) ((↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)) ⋯) : R) =
    (↑a : R)

Tactic:
simp_rw [mul_sub, mul_add]

Premises used: mul_sub, mul_add
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a b : { a : R // IsIdempotentElem a }
rw : (↑a : R) * (↑a : R) + (↑a : R) * (↑b : R) - (↑a : R) * (↑a : R) * (↑b : R) = (↑a : R)
rw₁ : (↑a : R) + (↑a : R) * (↑b : R) - (↑a : R) * (↑b : R) = (↑a : R)
rw₂ rw₃ : (↑a : R) = (↑a : R)
⊢ (↑a : R) * (↑a : R) + (↑a : R) * (↑b : R) - (↑a : R) * ((↑a : R) * (↑b : R)) = (↑a : R)

Tactic:
rw [← mul_assoc, a.2, add_sub_cancel_right]

Premises used: mul_assoc, add_sub_cancel_right, Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a b : { a : R // IsIdempotentElem a }
simp_rw : (↑b : R) * (↑a : R) + (↑b : R) * (↑b : R) - (↑b : R) * ((↑a : R) * (↑b : R)) = (↑b : R)
⊢ (↑b : R) * (↑(Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) ((↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)) ⋯) : R) =
    (↑b : R)

Tactic:
simp_rw [mul_sub, mul_add]

Premises used: mul_sub, mul_add
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a b : { a : R // IsIdempotentElem a }
rw : (↑b : R) * (↑a : R) + (↑b : R) * (↑b : R) - (↑b : R) * (↑a : R) * (↑b : R) = (↑b : R)
rw₁ : (↑b : R) * (↑a : R) + (↑b : R) * (↑b : R) - (↑b : R) * (↑b : R) * (↑a : R) = (↑b : R)
rw₂ : (↑b : R) * (↑a : R) + (↑b : R) - (↑b : R) * (↑a : R) = (↑b : R)
rw₃ rw₄ : (↑b : R) = (↑b : R)
⊢ (↑b : R) * (↑a : R) + (↑b : R) * (↑b : R) - (↑b : R) * ((↑a : R) * (↑b : R)) = (↑b : R)

Tactic:
rw [← mul_assoc, mul_right_comm, b.2, add_sub_cancel_left]

Premises used: add_sub_cancel_left, mul_assoc, mul_right_comm, Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a b c : { a : R // IsIdempotentElem a }
hac : a ≤ c
hbc : b ≤ c
simp_rw :
  (↑a : R) * (↑c : R) + (↑b : R) * (↑c : R) - (↑a : R) * ((↑b : R) * (↑c : R)) =
    (↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)
⊢ (↑(Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) ((↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)) ⋯) : R) * (↑c : R) =
    (↑(Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) ((↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)) ⋯) : R)

Tactic:
simp_rw [sub_mul, add_mul, mul_assoc]

Premises used: add_mul, mul_assoc, sub_mul
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a b c : { a : R // IsIdempotentElem a }
hac : a ≤ c
hbc : b ≤ c
rw : (↑a : R) * (↑c : R) + (↑b : R) - (↑a : R) * (↑b : R) = (↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)
rw₁ rw₂ : (↑a : R) + (↑b : R) - (↑a : R) * (↑b : R) = (↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)
⊢ (↑a : R) * (↑c : R) + (↑b : R) * (↑c : R) - (↑a : R) * ((↑b : R) * (↑c : R)) =
    (↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)

Tactic:
rw [hbc, hac]
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a b c : { x : R // IsIdempotentElem x }
simp_rw :
  (↑a : R) * (↑b : R) + (↑a : R) * (↑c : R) - (↑a : R) * ((↑b : R) * (↑c : R)) =
    (↑a : R) * (↑b : R) + (↑a : R) * (↑c : R) - (↑a : R) * (↑a : R) * ((↑b : R) * (↑c : R))
⊢ (↑(a ⊓ (b ⊔ c)) : R) = (↑(a ⊓ b ⊔ a ⊓ c) : R)

Tactic:
simp_rw [(· ⊔ ·), (· ⊓ ·), SemilatticeSup.sup, SemilatticeInf.inf, Lattice.inf,
      SemilatticeInf.inf, mul_sub, mul_add, mul_mul_mul_comm]

Premises used: mul_mul_mul_comm, mul_sub, SemilatticeInf.inf, Max.max, mul_add, Lattice.inf, Min.min, SemilatticeSup.sup
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a b c : { x : R // IsIdempotentElem x }
rw rw₁ :
  (↑a : R) * (↑b : R) + (↑a : R) * (↑c : R) - (↑a : R) * ((↑b : R) * (↑c : R)) =
    (↑a : R) * (↑b : R) + (↑a : R) * (↑c : R) - (↑a : R) * ((↑b : R) * (↑c : R))
⊢ (↑a : R) * (↑b : R) + (↑a : R) * (↑c : R) - (↑a : R) * ((↑b : R) * (↑c : R)) =
    (↑a : R) * (↑b : R) + (↑a : R) * (↑c : R) - (↑a : R) * (↑a : R) * ((↑b : R) * (↑c : R))

Tactic:
rw [a.2]

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
rw : (↑a : R) - (↑a : R) = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (↑a : R) - (↑a : R) * (↑a : R) = 0

Tactic:
rw [a.2, sub_self]

Premises used: sub_self, Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
simp_rw : 1 - ((↑a : R) - (↑a : R) * (↑a : R)) = (↑⊤ : R)
⊢ (↑(a ⊔ Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) (1 - (↑a : R)) ⋯) : R) = (↑⊤ : R)

Tactic:
simp_rw [(· ⊔ ·), SemilatticeSup.sup, add_sub_cancel, mul_sub, mul_one]

Premises used: mul_sub, add_sub_cancel, Max.max, mul_one, SemilatticeSup.sup
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
rw : Eq.{u_1 + 1} (α := R) 1 (↑⊤ : R)
⊢ 1 - ((↑a : R) - (↑a : R) * (↑a : R)) = (↑⊤ : R)

Tactic:
rw [a.2, sub_self, sub_zero]

Premises used: sub_self, sub_zero, Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
⊢ Eq.{u_1 + 1} (α := R) 1 (↑⊤ : R)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a b : { a : R // IsIdempotentElem a }
simp_rw simp_rw₁ :
  1 - (↑a : R) * (1 - (↑b : R)) = (↑(b ⊔ Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) (1 - (↑a : R)) ⋯) : R)
simp_rw₂ :
  1 - (↑a : R) * (1 - (↑b : R)) =
    (↑(SemilatticeSup.sup b (Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) (1 - (↑a : R)) ⋯)) : R)
simp_rw₃ : 1 - (↑a : R) * (1 - (↑b : R)) = (↑b : R) + (1 - (↑a : R)) - (↑b : R) * (1 - (↑a : R))
simp_rw₄ : 1 - (↑a : R) * (1 - (↑b : R)) = 1 - (↑a : R) + (↑b : R) - (↑b : R) * (1 - (↑a : R))
simp_rw₅ : 1 - (↑a : R) * (1 - (↑b : R)) = 1 - (↑a : R) + ((↑b : R) - (↑b : R) * (1 - (↑a : R)))
simp_rw₆ : 1 - ((↑a : R) * 1 - (↑a : R) * (↑b : R)) = 1 - (↑a : R) + ((↑b : R) - ((↑b : R) * 1 - (↑b : R) * (↑a : R)))
simp_rw₇ : 1 - ((↑a : R) - (↑a : R) * (↑b : R)) = 1 - (↑a : R) + ((↑b : R) - ((↑b : R) - (↑b : R) * (↑a : R)))
simp_rw₈ : 1 - ((↑a : R) - (↑a : R) * (↑b : R)) = 1 - (↑a : R) + (↑b : R) * (↑a : R)
simp_rw₉ : 1 - ((↑a : R) - (↑a : R) * (↑b : R)) = 1 - ((↑a : R) - (↑b : R) * (↑a : R))
⊢ (↑(Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) (1 - (↑a : R) * (1 - (↑b : R))) ⋯) : R) =
    (↑(b ⊔ Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) (1 - (↑a : R)) ⋯) : R)

Tactic:
simp_rw [(· ⊔ ·), SemilatticeSup.sup,
    add_comm b.1, add_sub_assoc, mul_sub, mul_one, sub_sub_cancel, sub_add, mul_comm]

Premises used: sub_add, add_sub_assoc, mul_sub, add_comm, sub_sub_cancel, Max.max, mul_comm, mul_one, Subtype.val, SemilatticeSup.sup
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
simp_rw simp_rw₁ : (↑a : R) * (1 - (↑a : R)) = 0
simp_rw₂ : (↑a : R) * 1 - (↑a : R) * (↑a : R) = 0
simp_rw₃ : (↑a : R) - (↑a : R) * (↑a : R) = 0
simp_rw₄ : (↑a : R) - (↑a : R) = 0
⊢ ((↑a : R), 1 - (↑a : R)).1 * ((↑a : R), 1 - (↑a : R)).2 = 0

Tactic:
simp_rw [mul_sub, mul_one, a.2.eq, sub_self]

Premises used: mul_sub, sub_self, IsIdempotentElem.eq, mul_one, Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
rw rw₁ : Eq.{u_1 + 1} (α := R) 1 1
⊢ ((↑a : R), 1 - (↑a : R)).1 + ((↑a : R), 1 - (↑a : R)).2 = 1

Tactic:
rw [add_sub_cancel]

Premises used: add_sub_cancel