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 }
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ b
have simp_rw : (↑(aᶜ ⊔ bᶜ)ᶜ : R × R).1 * (↑b : R × R).1 = (↑(aᶜ ⊔ bᶜ)ᶜ : R × R).1
Tactic: simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup,
    mul_assoc, (IsIdempotentElem.of_mul_add b.2.1 b.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 * (↑b : R × R).1 = (↑(aᶜ ⊔ bᶜ)ᶜ : R × R).1
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ b
have simp_rw₁ : (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ : R × R).1 * (↑b : R × R).1 = (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ : R × R).1
Tactic: simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup,
    mul_assoc, (IsIdempotentElem.of_mul_add b.2.1 b.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 * (↑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
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ b
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 *
    (↑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) 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_assoc, (IsIdempotentElem.of_mul_add b.2.1 b.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 * (↑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
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ b
have simp_rw₃ : (↑a : R × R).1 * (↑b : R × R).1 * (↑b : R × R).1 = (↑a : R × R).1 * (↑b : R × R).1
Tactic: simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup,
    mul_assoc, (IsIdempotentElem.of_mul_add b.2.1 b.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 * (↑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
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ b
have simp_rw₄ : (↑a : R × R).1 * ((↑b : R × R).1 * (↑b : R × R).1) = (↑a : R × R).1 * (↑b : R × R).1
Tactic: simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup,
    mul_assoc, (IsIdempotentElem.of_mul_add b.2.1 b.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 c : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : a ≤ b
hac : a ≤ c
⊢ a ≤ (bᶜ ⊔ cᶜ)ᶜ
have simp_rw : (↑a : R × R).1 * (↑b : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1
Tactic: simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup, ← 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 }
hab : a ≤ b
hac : a ≤ c
⊢ (↑a : R × R).1 * (↑b : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1
have rw : (↑a : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1
Tactic: rw [hab, hac]
-- 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 }
hab : a ≤ b
hac : a ≤ c
rw : (↑a : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1
⊢ (↑a : R × R).1 * (↑b : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1
have rw₁ : (↑a : R × R).1 = (↑a : R × R).1
Tactic: rw [hab, hac]
-- 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 }
⊢ (↑((a ⊔ b) ⊓ (a ⊔ c)) : R × R).2 = (↑(a ⊔ b ⊓ c) : R × R).2
have simp_rw : (↑(SemilatticeSup.sup a b ⊓ SemilatticeSup.sup a c) : R × R).2 = (↑(SemilatticeSup.sup a (b ⊓ c)) : R × R).2
Tactic: simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup, add_mul, mul_add,
      mul_mul_mul_comm _ b.1.1, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, ← mul_assoc, a.2.1,
      zero_mul, zero_add]
-- 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 }
simp_rw : (↑(SemilatticeSup.sup a b ⊓ SemilatticeSup.sup a c) : R × R).2 = (↑(SemilatticeSup.sup a (b ⊓ c)) : R × R).2
⊢ (↑((a ⊔ b) ⊓ (a ⊔ c)) : R × R).2 = (↑(a ⊔ b ⊓ c) : R × R).2
have simp_rw₁ : (↑(SemilatticeSup.sup (SemilatticeSup.sup a b)ᶜ (SemilatticeSup.sup a c)ᶜ)ᶜ : R × R).2 =
  (↑(SemilatticeSup.sup a (SemilatticeSup.sup bᶜ cᶜ)ᶜ) : R × R).2
Tactic: simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup, add_mul, mul_add,
      mul_mul_mul_comm _ b.1.1, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, ← mul_assoc, a.2.1,
      zero_mul, zero_add]
-- 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 }
simp_rw : (↑(SemilatticeSup.sup a b ⊓ SemilatticeSup.sup a c) : R × R).2 = (↑(SemilatticeSup.sup a (b ⊓ c)) : R × R).2
simp_rw₁ :
  (↑(SemilatticeSup.sup (SemilatticeSup.sup a b)ᶜ (SemilatticeSup.sup a c)ᶜ)ᶜ : R × R).2 =
    (↑(SemilatticeSup.sup a (SemilatticeSup.sup bᶜ cᶜ)ᶜ) : R × R).2
⊢ (↑((a ⊔ b) ⊓ (a ⊔ c)) : R × R).2 = (↑(a ⊔ b ⊓ c) : R × R).2
have simp_rw₂ : (↑(SemilatticeSup.sup
          (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
            ((↑(SemilatticeSup.sup a b) : R × R).2, (↑(SemilatticeSup.sup a b) : R × R).1) sorry)
          (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
            ((↑(SemilatticeSup.sup a c) : R × R).2, (↑(SemilatticeSup.sup a c) : R × R).1) sorry)) :
      R × R).1 =
  (↑(SemilatticeSup.sup a
          (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
            ((↑(SemilatticeSup.sup
                      (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)
                      (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
                        ((↑c : R × R).2, (↑c : R × R).1) sorry)) :
                  R × R).2,
              (↑(SemilatticeSup.sup
                      (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)
                      (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
                        ((↑c : R × R).2, (↑c : R × R).1) sorry)) :
                  R × R).1)
            sorry)) :
      R × R).2
Tactic: simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup, add_mul, mul_add,
      mul_mul_mul_comm _ b.1.1, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, ← mul_assoc, a.2.1,
      zero_mul, zero_add]
-- 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 }
simp_rw : (↑(SemilatticeSup.sup a b ⊓ SemilatticeSup.sup a c) : R × R).2 = (↑(SemilatticeSup.sup a (b ⊓ c)) : R × R).2
simp_rw₁ :
  (↑(SemilatticeSup.sup (SemilatticeSup.sup a b)ᶜ (SemilatticeSup.sup a c)ᶜ)ᶜ : R × R).2 =
    (↑(SemilatticeSup.sup a (SemilatticeSup.sup bᶜ cᶜ)ᶜ) : R × R).2
simp_rw₂ :
  (↑(SemilatticeSup.sup
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
              ((↑(SemilatticeSup.sup a b) : R × R).2, (↑(SemilatticeSup.sup a b) : R × R).1) ⋯)
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
              ((↑(SemilatticeSup.sup a c) : R × R).2, (↑(SemilatticeSup.sup a c) : R × R).1) ⋯)) :
        R × R).1 =
    (↑(SemilatticeSup.sup a
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
              ((↑(SemilatticeSup.sup
                        (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) ⋯)
                        (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
                          ((↑c : R × R).2, (↑c : R × R).1) ⋯)) :
                    R × R).2,
                (↑(SemilatticeSup.sup
                        (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) ⋯)
                        (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
                          ((↑c : R × R).2, (↑c : R × R).1) ⋯)) :
                    R × R).1)
              ⋯)) :
        R × R).2
⊢ (↑((a ⊔ b) ⊓ (a ⊔ c)) : R × R).2 = (↑(a ⊔ b ⊓ c) : R × R).2
have simp_rw₃ : (↑a : R × R).2 * (↑b : R × R).2 +
    ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1) * ((↑a : R × R).2 * (↑c : R × R).2) =
  (↑a : R × R).2 * ((↑b : R × R).2 + (↑b : R × R).1 * (↑c : R × R).2)
Tactic: simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup, add_mul, mul_add,
      mul_mul_mul_comm _ b.1.1, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, ← mul_assoc, a.2.1,
      zero_mul, zero_add]
-- 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 }
simp_rw : (↑(SemilatticeSup.sup a b ⊓ SemilatticeSup.sup a c) : R × R).2 = (↑(SemilatticeSup.sup a (b ⊓ c)) : R × R).2
simp_rw₁ :
  (↑(SemilatticeSup.sup (SemilatticeSup.sup a b)ᶜ (SemilatticeSup.sup a c)ᶜ)ᶜ : R × R).2 =
    (↑(SemilatticeSup.sup a (SemilatticeSup.sup bᶜ cᶜ)ᶜ) : R × R).2
simp_rw₂ :
  (↑(SemilatticeSup.sup
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
              ((↑(SemilatticeSup.sup a b) : R × R).2, (↑(SemilatticeSup.sup a b) : R × R).1) ⋯)
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
              ((↑(SemilatticeSup.sup a c) : R × R).2, (↑(SemilatticeSup.sup a c) : R × R).1) ⋯)) :
        R × R).1 =
    (↑(SemilatticeSup.sup a
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
              ((↑(SemilatticeSup.sup
                        (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) ⋯)
                        (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
                          ((↑c : R × R).2, (↑c : R × R).1) ⋯)) :
                    R × R).2,
                (↑(SemilatticeSup.sup
                        (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) ⋯)
                        (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
                          ((↑c : R × R).2, (↑c : R × R).1) ⋯)) :
                    R × R).1)
              ⋯)) :
        R × R).2
simp_rw₃ :
  (↑a : R × R).2 * (↑b : R × R).2 +
      ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1) * ((↑a : R × R).2 * (↑c : R × R).2) =
    (↑a : R × R).2 * ((↑b : R × R).2 + (↑b : R × R).1 * (↑c : R × R).2)
⊢ (↑((a ⊔ b) ⊓ (a ⊔ c)) : R × R).2 = (↑(a ⊔ b ⊓ c) : R × R).2
have simp_rw₄ : (↑a : R × R).2 * (↑b : R × R).2 +
    ((↑a : R × R).1 * ((↑a : R × R).2 * (↑c : R × R).2) +
      (↑a : R × R).2 * (↑b : R × R).1 * ((↑a : R × R).2 * (↑c : R × R).2)) =
  (↑a : R × R).2 * ((↑b : R × R).2 + (↑b : R × R).1 * (↑c : R × R).2)
Tactic: simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup, add_mul, mul_add,
      mul_mul_mul_comm _ b.1.1, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, ← mul_assoc, a.2.1,
      zero_mul, zero_add]
-- 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 }
simp_rw : (↑(SemilatticeSup.sup a b ⊓ SemilatticeSup.sup a c) : R × R).2 = (↑(SemilatticeSup.sup a (b ⊓ c)) : R × R).2
simp_rw₁ :
  (↑(SemilatticeSup.sup (SemilatticeSup.sup a b)ᶜ (SemilatticeSup.sup a c)ᶜ)ᶜ : R × R).2 =
    (↑(SemilatticeSup.sup a (SemilatticeSup.sup bᶜ cᶜ)ᶜ) : R × R).2
simp_rw₂ :
  (↑(SemilatticeSup.sup
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
              ((↑(SemilatticeSup.sup a b) : R × R).2, (↑(SemilatticeSup.sup a b) : R × R).1) ⋯)
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
              ((↑(SemilatticeSup.sup a c) : R × R).2, (↑(SemilatticeSup.sup a c) : R × R).1) ⋯)) :
        R × R).1 =
    (↑(SemilatticeSup.sup a
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
              ((↑(SemilatticeSup.sup
                        (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) ⋯)
                        (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
                          ((↑c : R × R).2, (↑c : R × R).1) ⋯)) :
                    R × R).2,
                (↑(SemilatticeSup.sup
                        (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) ⋯)
                        (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
                          ((↑c : R × R).2, (↑c : R × R).1) ⋯)) :
                    R × R).1)
              ⋯)) :
        R × R).2
simp_rw₃ :
  (↑a : R × R).2 * (↑b : R × R).2 +
      ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1) * ((↑a : R × R).2 * (↑c : R × R).2) =
    (↑a : R × R).2 * ((↑b : R × R).2 + (↑b : R × R).1 * (↑c : R × R).2)
simp_rw₄ :
  (↑a : R × R).2 * (↑b : R × R).2 +
      ((↑a : R × R).1 * ((↑a : R × R).2 * (↑c : R × R).2) +
        (↑a : R × R).2 * (↑b : R × R).1 * ((↑a : R × R).2 * (↑c : R × R).2)) =
    (↑a : R × R).2 * ((↑b : R × R).2 + (↑b : R × R).1 * (↑c : R × R).2)
⊢ (↑((a ⊔ b) ⊓ (a ⊔ c)) : R × R).2 = (↑(a ⊔ b ⊓ c) : R × R).2
have simp_rw₅ : (↑a : R × R).2 * (↑b : R × R).2 +
    ((↑a : R × R).1 * ((↑a : R × R).2 * (↑c : R × R).2) +
      (↑a : R × R).2 * (↑b : R × R).1 * ((↑a : R × R).2 * (↑c : R × R).2)) =
  (↑a : R × R).2 * (↑b : R × R).2 + (↑a : R × R).2 * ((↑b : R × R).1 * (↑c : R × R).2)
Tactic: simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup, add_mul, mul_add,
      mul_mul_mul_comm _ b.1.1, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, ← mul_assoc, a.2.1,
      zero_mul, zero_add]
-- 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 }
simp_rw : (↑(SemilatticeSup.sup a b ⊓ SemilatticeSup.sup a c) : R × R).2 = (↑(SemilatticeSup.sup a (b ⊓ c)) : R × R).2
simp_rw₁ :
  (↑(SemilatticeSup.sup (SemilatticeSup.sup a b)ᶜ (SemilatticeSup.sup a c)ᶜ)ᶜ : R × R).2 =
    (↑(SemilatticeSup.sup a (SemilatticeSup.sup bᶜ cᶜ)ᶜ) : R × R).2
simp_rw₂ :
  (↑(SemilatticeSup.sup
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
              ((↑(SemilatticeSup.sup a b) : R × R).2, (↑(SemilatticeSup.sup a b) : R × R).1) ⋯)
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
              ((↑(SemilatticeSup.sup a c) : R × R).2, (↑(SemilatticeSup.sup a c) : R × R).1) ⋯)) :
        R × R).1 =
    (↑(SemilatticeSup.sup a
            (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
              ((↑(SemilatticeSup.sup
                        (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) ⋯)
                        (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
                          ((↑c : R × R).2, (↑c : R × R).1) ⋯)) :
                    R × R).2,
                (↑(SemilatticeSup.sup
                        (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) ⋯)
                        (Subtype.mk (p := fun (a : R × R) ↦ a.1 * a.2 = 0 ∧ a.1 + a.2 = 1)
                          ((↑c : R × R).2, (↑c : R × R).1) ⋯)) :
                    R × R).1)
              ⋯)) :
        R × R).2
simp_rw₃ :
  (↑a : R × R).2 * (↑b : R × R).2 +
      ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1) * ((↑a : R × R).2 * (↑c : R × R).2) =
    (↑a : R × R).2 * ((↑b : R × R).2 + (↑b : R × R).1 * (↑c : R × R).2)
simp_rw₄ :
  (↑a : R × R).2 * (↑b : R × R).2 +
      ((↑a : R × R).1 * ((↑a : R × R).2 * (↑c : R × R).2) +
        (↑a : R × R).2 * (↑b : R × R).1 * ((↑a : R × R).2 * (↑c : R × R).2)) =
    (↑a : R × R).2 * ((↑b : R × R).2 + (↑b : R × R).1 * (↑c : R × R).2)
simp_rw₅ :
  (↑a : R × R).2 * (↑b : R × R).2 +
      ((↑a : R × R).1 * ((↑a : R × R).2 * (↑c : R × R).2) +
        (↑a : R × R).2 * (↑b : R × R).1 * ((↑a : R × R).2 * (↑c : R × R).2)) =
    (↑a : R × R).2 * (↑b : R × R).2 + (↑a : R × R).2 * ((↑b : R × R).1 * (↑c : R × R).2)
⊢ (↑((a ⊔ b) ⊓ (a ⊔ c)) : R × R).2 = (↑(a ⊔ b ⊓ c) : R × R).2
have simp_rw₆ : (↑a : R × R).2 * (↑b : R × R).2 +
    ((↑a : R × R).1 * ((↑a : R × R).2 * (↑c : R × R).2) +
      (↑a : R × R).2 * (↑a : R × R).2 * ((↑b : R × R).1 * (↑c : R × R).2)) =
  (↑a : R × R).2 * (↑b : R × R).2 + (↑a : R × R).2 * ((↑b : R × R).1 * (↑c : R × R).2)
Tactic: simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup, add_mul, mul_add,
      mul_mul_mul_comm _ b.1.1, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, ← mul_assoc, a.2.1,
      zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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 }
⊢ (↑(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
have simp_rw : (↑(a ⊓ aᶜ) : R × R).2 = 1
Tactic: simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup,
      (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq, add_comm, 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 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
⊢ (↑(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
have simp_rw₃ : (↑(SemilatticeSup.sup aᶜ aᶜᶜ)ᶜ : R × R).2 = 1
Tactic: simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup,
      (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq, add_comm, 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 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
⊢ (↑(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
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) ((↑a : R × R).1, (↑a : R × R).2) sorry)) :
      R × R).1 =
  1
Tactic: simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup,
      (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq, add_comm, 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 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
⊢ (↑(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
have simp_rw₅ : (↑a : R × R).2 + (↑a : R × R).1 * (↑a : R × R).1 = 1
Tactic: simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup,
      (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq, add_comm, 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 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
⊢ (↑(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
have simp_rw₆ : (↑a : R × R).2 + (↑a : R × R).1 = 1
Tactic: simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup,
      (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq, add_comm, 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 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
⊢ (↑(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
have simp_rw₇ : (↑a : R × R).1 + (↑a : R × R).2 = 1
Tactic: simp_rw +instances [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup,
      (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq, add_comm, a.2.2]