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 a : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑(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
have simp_rw : 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]
-- 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₁ : 1 = (↑(a ⊔ aᶜ) : R × R).1
⊢ (↑(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
have simp_rw₂ : 1 = (↑(SemilatticeSup.sup 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]
-- 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₁ : 1 = (↑(a ⊔ aᶜ) : R × R).1
simp_rw₂ : 1 = (↑(SemilatticeSup.sup a aᶜ) : R × R).1
⊢ (↑(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
have 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) sorry)) :
      R × R).1
Tactic: simp_rw [(· ⊔ ·), (·ᶜ),
    SemilatticeSup.sup, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, 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₁ : 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
⊢ (↑(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
have simp_rw₄ : 1 = (↑a : R × R).1 + (↑a : R × R).2 * (↑a : R × R).2
Tactic: simp_rw [(· ⊔ ·), (·ᶜ),
    SemilatticeSup.sup, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, 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₁ : 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
⊢ (↑(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
have simp_rw₅ : 1 = (↑a : R × R).1 + (↑a : R × R).2
Tactic: simp_rw [(· ⊔ ·), (·ᶜ),
    SemilatticeSup.sup, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, a.2.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑a : S) * (↑c : S) = (↑a : S)
have rw : (↑a : S) * (↑b : S) * (↑c : S) = (↑a : S) * (↑b : S)
Tactic: rw [← hab, mul_assoc, hbc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑a : S) * (↑c : S) = (↑a : S)
have rw₁ : (↑a : S) * ((↑b : S) * (↑c : S)) = (↑a : S) * (↑b : S)
Tactic: rw [← hab, mul_assoc, hbc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑a : S) * (↑c : S) = (↑a : S)
have rw₂ : (↑a : S) * (↑b : S) = (↑a : S) * (↑b : S)
Tactic: rw [← hab, mul_assoc, hbc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑a : S) = (↑b : S)
have rw : (↑a : S) * (↑b : S) = (↑b : S)
Tactic: rw [← hab, mul_comm, hba]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑a : S) = (↑b : S)
have rw₂ : (↑b : S) = (↑b : S)
Tactic: rw [← hab, mul_comm, hba]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemigroup S
a b : { a : S // IsIdempotentElem a }
⊢ (↑(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)
have simp_rw : (↑a : S) * (↑a : S) * (↑b : S) = (↑a : S) * (↑b : S)
Tactic: simp_rw [mul_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemigroup S
a b : { a : S // IsIdempotentElem a }
⊢ (↑a : S) * (↑a : S) * (↑b : S) = (↑a : S) * (↑b : S)
have rw : (↑a : S) * (↑b : S) = (↑a : S) * (↑b : S)
Tactic: rw [a.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemigroup S
a b : { a : S // IsIdempotentElem a }
⊢ (↑(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)
have simp_rw : (↑a : S) * ((↑b : S) * (↑b : S)) = (↑a : S) * (↑b : S)
Tactic: simp_rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemigroup S
a b : { a : S // IsIdempotentElem a }
⊢ (↑a : S) * ((↑b : S) * (↑b : S)) = (↑a : S) * (↑b : S)
have rw : (↑a : S) * (↑b : S) = (↑a : S) * (↑b : S)
Tactic: rw [b.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑a : S) * (↑(Subtype.mk (p := fun (a : S) ↦ IsIdempotentElem a) ((↑b : S) * (↑c : S)) ⋯) : S) = (↑a : S)
have simp_rw : (↑a : S) * (↑b : S) * (↑c : S) = (↑a : S)
Tactic: simp_rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑a : S) * (↑b : S) * (↑c : S) = (↑a : S)
have rw₁ : (↑a : S) = (↑a : S)
Tactic: rw [hab, hac]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : { a : R // IsIdempotentElem a }
⊢ (↑a : R) * (↑(Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) ((↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)) ⋯) : R) =
    (↑a : R)
have simp_rw : (↑a : R) * (↑a : R) + (↑a : R) * (↑b : R) - (↑a : R) * ((↑a : R) * (↑b : R)) = (↑a : R)
Tactic: simp_rw [mul_sub, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : { a : R // IsIdempotentElem a }
⊢ (↑a : R) * (↑a : R) + (↑a : R) * (↑b : R) - (↑a : R) * ((↑a : R) * (↑b : R)) = (↑a : R)
have rw : (↑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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑a : R) * (↑a : R) + (↑a : R) * (↑b : R) - (↑a : R) * ((↑a : R) * (↑b : R)) = (↑a : R)
have rw₁ : (↑a : R) + (↑a : R) * (↑b : R) - (↑a : R) * (↑b : R) = (↑a : R)
Tactic: rw [← mul_assoc, a.2, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑a : R) * (↑a : R) + (↑a : R) * (↑b : R) - (↑a : R) * ((↑a : R) * (↑b : R)) = (↑a : R)
have rw₂ : (↑a : R) = (↑a : R)
Tactic: rw [← mul_assoc, a.2, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : { a : R // IsIdempotentElem a }
⊢ (↑b : R) * (↑(Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) ((↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)) ⋯) : R) =
    (↑b : R)
have simp_rw : (↑b : R) * (↑a : R) + (↑b : R) * (↑b : R) - (↑b : R) * ((↑a : R) * (↑b : R)) = (↑b : R)
Tactic: simp_rw [mul_sub, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : { a : R // IsIdempotentElem a }
⊢ (↑b : R) * (↑a : R) + (↑b : R) * (↑b : R) - (↑b : R) * ((↑a : R) * (↑b : R)) = (↑b : R)
have rw : (↑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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑b : R) * (↑a : R) + (↑b : R) * (↑b : R) - (↑b : R) * ((↑a : R) * (↑b : R)) = (↑b : R)
have rw₁ : (↑b : R) * (↑a : R) + (↑b : R) * (↑b : R) - (↑b : R) * (↑b : R) * (↑a : R) = (↑b : R)
Tactic: rw [← mul_assoc, mul_right_comm, b.2, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑b : R) * (↑a : R) + (↑b : R) * (↑b : R) - (↑b : R) * ((↑a : R) * (↑b : R)) = (↑b : R)
have rw₂ : (↑b : R) * (↑a : R) + (↑b : R) - (↑b : R) * (↑a : R) = (↑b : R)
Tactic: rw [← mul_assoc, mul_right_comm, b.2, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑b : R) * (↑a : R) + (↑b : R) * (↑b : R) - (↑b : R) * ((↑a : R) * (↑b : R)) = (↑b : R)
have rw₃ : (↑b : R) = (↑b : R)
Tactic: rw [← mul_assoc, mul_right_comm, b.2, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a b c : { a : R // IsIdempotentElem a }
hac : a ≤ c
hbc : b ≤ c
⊢ (↑(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)
have simp_rw : (↑a : R) * (↑c : R) + (↑b : R) * (↑c : R) - (↑a : R) * ((↑b : R) * (↑c : R)) = (↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)
Tactic: simp_rw [sub_mul, add_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a b c : { a : R // IsIdempotentElem a }
hac : a ≤ c
hbc : b ≤ c
⊢ (↑a : R) * (↑c : R) + (↑b : R) * (↑c : R) - (↑a : R) * ((↑b : R) * (↑c : R)) =
    (↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)
have rw : (↑a : R) * (↑c : R) + (↑b : R) - (↑a : R) * (↑b : R) = (↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)
Tactic: rw [hbc, hac]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑a : R) * (↑c : R) + (↑b : R) * (↑c : R) - (↑a : R) * ((↑b : R) * (↑c : R)) =
    (↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)
have rw₁ : (↑a : R) + (↑b : R) - (↑a : R) * (↑b : R) = (↑a : R) + (↑b : R) - (↑a : R) * (↑b : R)
Tactic: rw [hbc, hac]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a b c : { x : R // IsIdempotentElem x }
⊢ (↑(a ⊓ (b ⊔ c)) : R) = (↑(a ⊓ b ⊔ a ⊓ c) : R)
have 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))
Tactic: simp_rw [(· ⊔ ·), (· ⊓ ·), SemilatticeSup.sup, SemilatticeInf.inf, Lattice.inf,
      SemilatticeInf.inf, mul_sub, mul_add, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a b c : { x : R // IsIdempotentElem x }
⊢ (↑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))
have 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))
Tactic: rw [a.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
⊢ (↑a : R) - (↑a : R) * (↑a : R) = 0
have rw : (↑a : R) - (↑a : R) = 0
Tactic: rw [a.2, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
rw : (↑a : R) - (↑a : R) = 0
⊢ (↑a : R) - (↑a : R) * (↑a : R) = 0
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [a.2, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
⊢ (↑(a ⊔ Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) (1 - (↑a : R)) ⋯) : R) = (↑⊤ : R)
have simp_rw : 1 - ((↑a : R) - (↑a : R) * (↑a : R)) = (↑⊤ : R)
Tactic: simp_rw [(· ⊔ ·), SemilatticeSup.sup, add_sub_cancel, mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
⊢ 1 - ((↑a : R) - (↑a : R) * (↑a : R)) = (↑⊤ : R)
have rw : Eq.{u_1 + 1} (α := R) 1 (↑⊤ : R)
Tactic: rw [a.2, sub_self, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : { a : R // IsIdempotentElem a }
⊢ (↑(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)
have simp_rw : 1 - (↑a : R) * (1 - (↑b : R)) = (↑(b ⊔ Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) (1 - (↑a : R)) sorry) : R)
Tactic: simp_rw [(· ⊔ ·), SemilatticeSup.sup,
    add_comm b.1, add_sub_assoc, mul_sub, mul_one, sub_sub_cancel, sub_add, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑(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)
have simp_rw₂ : 1 - (↑a : R) * (1 - (↑b : R)) =
  (↑(SemilatticeSup.sup b (Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) (1 - (↑a : R)) sorry)) : R)
Tactic: simp_rw [(· ⊔ ·), SemilatticeSup.sup,
    add_comm b.1, add_sub_assoc, mul_sub, mul_one, sub_sub_cancel, sub_add, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)
⊢ (↑(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)
have simp_rw₃ : 1 - (↑a : R) * (1 - (↑b : R)) = (↑b : R) + (1 - (↑a : R)) - (↑b : R) * (1 - (↑a : R))
Tactic: simp_rw [(· ⊔ ·), SemilatticeSup.sup,
    add_comm b.1, add_sub_assoc, mul_sub, mul_one, sub_sub_cancel, sub_add, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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))
⊢ (↑(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)
have simp_rw₄ : 1 - (↑a : R) * (1 - (↑b : R)) = 1 - (↑a : R) + (↑b : R) - (↑b : R) * (1 - (↑a : R))
Tactic: simp_rw [(· ⊔ ·), SemilatticeSup.sup,
    add_comm b.1, add_sub_assoc, mul_sub, mul_one, sub_sub_cancel, sub_add, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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))
⊢ (↑(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)
have simp_rw₅ : 1 - (↑a : R) * (1 - (↑b : R)) = 1 - (↑a : R) + ((↑b : R) - (↑b : R) * (1 - (↑a : R)))
Tactic: simp_rw [(· ⊔ ·), SemilatticeSup.sup,
    add_comm b.1, add_sub_assoc, mul_sub, mul_one, sub_sub_cancel, sub_add, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)))
⊢ (↑(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)
have simp_rw₆ : 1 - ((↑a : R) * 1 - (↑a : R) * (↑b : R)) = 1 - (↑a : R) + ((↑b : R) - ((↑b : R) * 1 - (↑b : R) * (↑a : R)))
Tactic: simp_rw [(· ⊔ ·), SemilatticeSup.sup,
    add_comm b.1, add_sub_assoc, mul_sub, mul_one, sub_sub_cancel, sub_add, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)))
⊢ (↑(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)
have simp_rw₇ : 1 - ((↑a : R) - (↑a : R) * (↑b : R)) = 1 - (↑a : R) + ((↑b : R) - ((↑b : R) - (↑b : R) * (↑a : R)))
Tactic: simp_rw [(· ⊔ ·), SemilatticeSup.sup,
    add_comm b.1, add_sub_assoc, mul_sub, mul_one, sub_sub_cancel, sub_add, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
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)))
⊢ (↑(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)
have simp_rw₈ : 1 - ((↑a : R) - (↑a : R) * (↑b : R)) = 1 - (↑a : R) + (↑b : R) * (↑a : R)
Tactic: simp_rw [(· ⊔ ·), SemilatticeSup.sup,
    add_comm b.1, add_sub_assoc, mul_sub, mul_one, sub_sub_cancel, sub_add, mul_comm]