awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ ((↑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
have simp_rw₆ : (↑a : R × R).1 * (↑a : R × R).2 * (↑b : R × R).2 + 0 = 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ ((↑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
have simp_rw₇ : 0 * (↑b : R × R).2 + 0 = 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ ((↑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
have simp_rw₈ : HAdd.hAdd (α := R) 0 0 = 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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 }
⊢ ((↑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
have simp_rw : (↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1 + (↑a : R × R).2 * (↑b : R × R).2 = 1
Tactic: simp_rw [add_assoc, ← mul_add, b.2.2, mul_one, a.2.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ ((↑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
have simp_rw₂ : (↑a : R × R).1 + ((↑a : R × R).2 * (↑b : R × R).1 + (↑a : R × R).2 * (↑b : R × R).2) = 1
Tactic: simp_rw [add_assoc, ← mul_add, b.2.2, mul_one, a.2.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ ((↑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
have simp_rw₃ : (↑a : R × R).1 + (↑a : R × R).2 * ((↑b : R × R).1 + (↑b : R × R).2) = 1
Tactic: simp_rw [add_assoc, ← mul_add, b.2.2, mul_one, a.2.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ ((↑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
have simp_rw₄ : (↑a : R × R).1 + (↑a : R × R).2 * 1 = 1
Tactic: simp_rw [add_assoc, ← mul_add, b.2.2, mul_one, a.2.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ ((↑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
have simp_rw₅ : (↑a : R × R).1 + (↑a : R × R).2 = 1
Tactic: simp_rw [add_assoc, ← mul_add, b.2.2, mul_one, a.2.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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 }
⊢ 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) ⋯
have simp_rw : (↑a : R × R).1 * ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1) = (↑a : R × R).1
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ 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) ⋯
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ 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) ⋯
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ 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) ⋯
have simp_rw₃ : (↑a : R × R).1 * (↑a : R × R).1 + 0 * (↑b : R × R).1 = (↑a : R × R).1
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ 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) ⋯
have simp_rw₄ : (↑a : R × R).1 * (↑a : R × R).1 + 0 = (↑a : R × R).1
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ 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) ⋯
have simp_rw₅ : (↑a : R × R).1 * (↑a : R × R).1 = (↑a : R × R).1
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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 }
⊢ 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) ⋯
have simp_rw : (↑b : R × R).1 * ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1) = (↑b : R × R).1
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ 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) ⋯
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ 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) ⋯
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ 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) ⋯
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ 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) ⋯
have simp_rw₄ : (↑b : R × R).1 * (↑a : R × R).1 + (↑b : R × R).1 * (↑a : R × R).2 = (↑b : R × R).1
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ 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) ⋯
have simp_rw₅ : (↑b : R × R).1 * ((↑a : R × R).1 + (↑a : R × R).2) = (↑b : R × R).1
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ 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) ⋯
have simp_rw₆ : (↑b : R × R).1 * 1 = (↑b : R × R).1
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ 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
have 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
Tactic: simp_rw [(· ≤ ·), add_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ (↑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
have 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
Tactic: rw [hac, hbc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ (↑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
have 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
Tactic: rw [hac, hbc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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 }
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ a
have simp_rw : (↑(aᶜ ⊔ bᶜ)ᶜ : R × R).1 * (↑a : R × R).1 = (↑(aᶜ ⊔ bᶜ)ᶜ : R × R).1
Tactic: simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup,
    mul_right_comm, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ a
have simp_rw₁ : (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ : R × R).1 * (↑a : R × R).1 = (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ : R × R).1
Tactic: simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup,
    mul_right_comm, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ a
have 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) sorry)
            (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) sorry)) :
        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) sorry)
          (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) sorry)) :
      R × R).2
Tactic: simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup,
    mul_right_comm, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ a
have simp_rw₃ : (↑a : R × R).1 * (↑b : R × R).1 * (↑a : R × R).1 = (↑a : R × R).1 * (↑b : R × R).1
Tactic: simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup,
    mul_right_comm, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ a
have simp_rw₄ : (↑a : R × R).1 * (↑a : R × R).1 * (↑b : R × R).1 = (↑a : R × R).1 * (↑b : R × R).1
Tactic: simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup,
    mul_right_comm, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq]