-- 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)
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)
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 * (↑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 * (↑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]