awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
x : R
i : I
rw :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x • idempotent V i
⊢ (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x * idempotent V i
have rw₁ : (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
  x • (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
Tactic: rw [← smul_eq_mul (a := x), idempotent, ← Submodule.coe_smul, ← smul_apply, ← decompose_smul,
    smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
x : R
i : I
rw :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x • idempotent V i
rw₁ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x • (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
⊢ (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x * idempotent V i
have rw₂ : (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
  (↑(x • ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
Tactic: rw [← smul_eq_mul (a := x), idempotent, ← Submodule.coe_smul, ← smul_apply, ← decompose_smul,
    smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
x : R
i : I
rw :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x • idempotent V i
rw₁ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x • (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
rw₂ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑(x • ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
⊢ (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x * idempotent V i
have rw₃ : (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
  (↑((HSMul.hSMul (β := ⨁ (i : I), ↥(V i)) x ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1) : (a : I) → ↥(V a)) i) : R)
Tactic: rw [← smul_eq_mul (a := x), idempotent, ← Submodule.coe_smul, ← smul_apply, ← decompose_smul,
    smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
x : R
i : I
rw :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x • idempotent V i
rw₁ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x • (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
rw₂ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑(x • ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
rw₃ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑((HSMul.hSMul (β := ⨁ (i : I), ↥(V i)) x ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1) : (a : I) → ↥(V a)) i) :
      R)
⊢ (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x * idempotent V i
have rw₄ : (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (HSMul.hSMul (β := R) x 1) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a))
        i) :
    R)
Tactic: rw [← smul_eq_mul (a := x), idempotent, ← Submodule.coe_smul, ← smul_apply, ← decompose_smul,
    smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
x : R
i : I
rw :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x • idempotent V i
rw₁ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x • (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
rw₂ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑(x • ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
rw₃ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑((HSMul.hSMul (β := ⨁ (i : I), ↥(V i)) x ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1) : (a : I) → ↥(V a)) i) :
      R)
rw₄ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (HSMul.hSMul (β := R) x 1) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a))
          i) :
      R)
⊢ (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x * idempotent V i
have rw₅ : (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (x * 1) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R)
Tactic: rw [← smul_eq_mul (a := x), idempotent, ← Submodule.coe_smul, ← smul_apply, ← decompose_smul,
    smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
x : R
i : I
rw :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x • idempotent V i
rw₁ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x • (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
rw₂ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑(x • ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
rw₃ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑((HSMul.hSMul (β := ⨁ (i : I), ↥(V i)) x ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1) : (a : I) → ↥(V a)) i) :
      R)
rw₄ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (HSMul.hSMul (β := R) x 1) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a))
          i) :
      R)
rw₅ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (x * 1) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R)
⊢ (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x * idempotent V i
have rw₆ : (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R)
Tactic: rw [← smul_eq_mul (a := x), idempotent, ← Submodule.coe_smul, ← smul_apply, ← decompose_smul,
    smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
i : I
⊢ IsIdempotentElem (idempotent V i)
have rw : idempotent V i * idempotent V i = idempotent V i
Tactic: rw [IsIdempotentElem, ← decompose_eq_mul_idempotent, idempotent, decompose_coe, of_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
i : I
rw : idempotent V i * idempotent V i = idempotent V i
⊢ IsIdempotentElem (idempotent V i)
have rw₁ : (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (idempotent V i) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
  idempotent V i
Tactic: rw [IsIdempotentElem, ← decompose_eq_mul_idempotent, idempotent, decompose_coe, of_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
i : I
rw : idempotent V i * idempotent V i = idempotent V i
rw₁ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (idempotent V i) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    idempotent V i
⊢ IsIdempotentElem (idempotent V i)
have rw₂ : (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i))
              (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R) :
            ⨁ (i : I), ↥(V i)) :
          (a : I) → ↥(V a))
        i) :
    R) =
  (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
Tactic: rw [IsIdempotentElem, ← decompose_eq_mul_idempotent, idempotent, decompose_coe, of_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
i : I
rw : idempotent V i * idempotent V i = idempotent V i
rw₁ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (idempotent V i) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    idempotent V i
rw₂ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i))
                (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R) :
              ⨁ (i : I), ↥(V i)) :
            (a : I) → ↥(V a))
          i) :
      R) =
    (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
⊢ IsIdempotentElem (idempotent V i)
have rw₃ : (↑(((((of.{u_2, u_1} (fun (i : I) ↦ ↥(V i)) i : ↥(V i) →+ ⨁ (i : I), ↥(V i)) : (a : ↥(V i)) → ⨁ (i : I), ↥(V i))
              (((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) :
            ⨁ (i : I), ↥(V i)) :
          (a : I) → ↥(V a))
        i) :
    R) =
  (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
Tactic: rw [IsIdempotentElem, ← decompose_eq_mul_idempotent, idempotent, decompose_coe, of_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
i : I
rw : idempotent V i * idempotent V i = idempotent V i
rw₁ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (idempotent V i) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    idempotent V i
rw₂ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i))
                (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R) :
              ⨁ (i : I), ↥(V i)) :
            (a : I) → ↥(V a))
          i) :
      R) =
    (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
rw₃ :
  (↑(((((of.{u_2, u_1} (fun (i : I) ↦ ↥(V i)) i : ↥(V i) →+ ⨁ (i : I), ↥(V i)) : (a : ↥(V i)) → ⨁ (i : I), ↥(V i))
                (((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) :
              ⨁ (i : I), ↥(V i)) :
            (a : I) → ↥(V a))
          i) :
      R) =
    (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
⊢ IsIdempotentElem (idempotent V i)
have rw₄ : (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R) =
  (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R)
Tactic: rw [IsIdempotentElem, ← decompose_eq_mul_idempotent, idempotent, decompose_coe, of_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
inst_3 : Fintype I
i j : I
hij : i ≠ j
⊢ idempotent V i * idempotent V j = 0
have rw : (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (idempotent V i) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) j) : R) = 0
Tactic: rw [← decompose_eq_mul_idempotent, idempotent, decompose_coe,
      of_eq_of_ne (h := hij.symm), Submodule.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
inst_3 : Fintype I
i j : I
hij : i ≠ j
rw :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (idempotent V i) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) j) : R) = 0
⊢ idempotent V i * idempotent V j = 0
have rw₁ : (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i))
              (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R) :
            ⨁ (i : I), ↥(V i)) :
          (a : I) → ↥(V a))
        j) :
    R) =
  0
Tactic: rw [← decompose_eq_mul_idempotent, idempotent, decompose_coe,
      of_eq_of_ne (h := hij.symm), Submodule.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
inst_3 : Fintype I
i j : I
hij : i ≠ j
rw :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (idempotent V i) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) j) : R) = 0
rw₁ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i))
                (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R) :
              ⨁ (i : I), ↥(V i)) :
            (a : I) → ↥(V a))
          j) :
      R) =
    0
⊢ idempotent V i * idempotent V j = 0
have rw₂ : (↑(((((of.{u_2, u_1} (fun (i : I) ↦ ↥(V i)) i : ↥(V i) →+ ⨁ (i : I), ↥(V i)) : (a : ↥(V i)) → ⨁ (i : I), ↥(V i))
              (((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) :
            ⨁ (i : I), ↥(V i)) :
          (a : I) → ↥(V a))
        j) :
    R) =
  0
Tactic: rw [← decompose_eq_mul_idempotent, idempotent, decompose_coe,
      of_eq_of_ne (h := hij.symm), Submodule.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
inst_3 : Fintype I
i j : I
hij : i ≠ j
rw :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (idempotent V i) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) j) : R) = 0
rw₁ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i))
                (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R) :
              ⨁ (i : I), ↥(V i)) :
            (a : I) → ↥(V a))
          j) :
      R) =
    0
rw₂ :
  (↑(((((of.{u_2, u_1} (fun (i : I) ↦ ↥(V i)) i : ↥(V i) →+ ⨁ (i : I), ↥(V i)) : (a : ↥(V i)) → ⨁ (i : I), ↥(V i))
                (((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) :
              ⨁ (i : I), ↥(V i)) :
            (a : I) → ↥(V a))
          j) :
      R) =
    0
⊢ idempotent V i * idempotent V j = 0
have rw₃ : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
Tactic: rw [← decompose_eq_mul_idempotent, idempotent, decompose_coe,
      of_eq_of_ne (h := hij.symm), Submodule.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
inst_3 : Fintype I
i j : I
hij : i ≠ j
rw :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (idempotent V i) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) j) : R) = 0
rw₁ :
  (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i))
                (↑(((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) : R) :
              ⨁ (i : I), ↥(V i)) :
            (a : I) → ↥(V a))
          j) :
      R) =
    0
rw₂ :
  (↑(((((of.{u_2, u_1} (fun (i : I) ↦ ↥(V i)) i : ↥(V i) →+ ⨁ (i : I), ↥(V i)) : (a : ↥(V i)) → ⨁ (i : I), ↥(V i))
                (((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i) :
              ⨁ (i : I), ↥(V i)) :
            (a : I) → ↥(V a))
          j) :
      R) =
    0
rw₃ : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
⊢ idempotent V i * idempotent V j = 0
have rw₄ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← decompose_eq_mul_idempotent, idempotent, decompose_coe,
      of_eq_of_ne (h := hij.symm), Submodule.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
inst_3 : Fintype I
⊢ Eq.{u_1 + 1} (α := R) (∑ i : I, idempotent V i) 1
have a : Eq (α := ⨁ (i : I), ↥(V i)) ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (∑ i : I, idempotent V i))
  ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1)
Tactic: apply (decompose V).injective
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
inst_3 : Fintype I
⊢ Eq (α := ⨁ (i : I), ↥(V i)) ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (∑ i : I, idempotent V i))
    ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1)
have a : ∀ (i : I),
  ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (∑ i : I, idempotent V i) : (a : I) → ↥(V a)) i =
    ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i
Tactic: refine DFunLike.ext _ _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
inst_3 : Fintype I
i : I
⊢ ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (∑ i : I, idempotent V i) : (a : I) → ↥(V a)) i =
    ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i
have a : ∑ a : I, (((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) (idempotent V a) : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i =
  ((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) 1 : (a : I) → ↥(V a)) i
Tactic: rw [decompose_sum, DFinsupp.finsetSum_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
S : Type u_3
R : Type u_4
inst : Zero ι
inst_1 : CommSemiring S
inst_2 : Semiring R
inst_3 : Algebra S R
A : ι → Submodule S R
inst_4 : GradedOne A
s : S
⊢ Membership.mem (α := R) (A 0) ((algebraMap S R : (a : S) → R) s : R)
have rw : HSMul.hSMul (β := R) s 1 ∈ A 0
Tactic: rw [Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddMonoidWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : GradedOne A
⊢ (↑0 : R) ∈ A 0
have zero : 0 ∈ A 0
Tactic: rw [Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddMonoidWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : GradedOne A
n : ℕ
n_ih : (↑n : R) ∈ A 0
⊢ (↑(n + 1) : R) ∈ A 0
have succ : HAdd.hAdd (α := R) (↑n : R) 1 ∈ A 0
Tactic: rw [Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddMonoidWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : GradedOne A
n : ℕ
⊢ (↑n : R) ∈ A 0
have zero : (↑0 : R) ∈ A 0
Tactic: induction n with
  | zero =>
    rw [Nat.cast_zero]
    exact zero_mem (A 0)
  | succ _ n_ih =>
    rw [Nat.cast_succ]
    exact add_mem n_ih (SetLike.one_mem_graded _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddMonoidWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : GradedOne A
n : ℕ
zero : (↑0 : R) ∈ A 0
⊢ (↑n : R) ∈ A 0
have succ : ∀ (n : ℕ) (n_ih : (↑n : R) ∈ A 0), (↑(n + 1) : R) ∈ A 0
Tactic: induction n with
  | zero =>
    rw [Nat.cast_zero]
    exact zero_mem (A 0)
  | succ _ n_ih =>
    rw [Nat.cast_succ]
    exact add_mem n_ih (SetLike.one_mem_graded _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddGroupWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubgroupClass σ R
A : ι → σ
inst_4 : GradedOne A
z : ℤ
⊢ (↑z : R) ∈ A 0
have ofNat : ∀ (a : ℕ), (↑(Int.ofNat a) : R) ∈ A 0
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddGroupWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubgroupClass σ R
A : ι → σ
inst_4 : GradedOne A
z : ℤ
ofNat : ∀ (a : ℕ), (↑(Int.ofNat a) : R) ∈ A 0
⊢ (↑z : R) ∈ A 0
have negSucc : ∀ (a : ℕ), (↑(Int.negSucc a) : R) ∈ A 0
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddGroupWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubgroupClass σ R
A : ι → σ
inst_4 : GradedOne A
a : ℕ
⊢ (↑(Int.ofNat a) : R) ∈ A 0
have ofNat : (↑a : R) ∈ A 0
Tactic: rw [Int.ofNat_eq_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : Zero ι
inst_1 : AddGroupWithOne R
inst_2 : SetLike σ R
inst_3 : AddSubgroupClass σ R
A : ι → σ
inst_4 : GradedOne A
a : ℕ
⊢ (↑(Int.negSucc a) : R) ∈ A 0
have negSucc : -(↑(a + 1) : R) ∈ A 0
Tactic: rw [Int.cast_negSucc]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : SetLike σ R
inst_3 : AddSubmonoidClass σ R
A : ι → σ
inst_4 : AddMonoid ι
inst_5 : SetLike.GradedMonoid A
inst_6 : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ (↑((r * r' : (a : ι) → ↥(A a)) n) : R) =
    ∑ ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' with
      ij.1 + ij.2 = n, (↑((r : (a : ι) → ↥(A a)) ij.1) : R) * (↑((r' : (a : ι) → ↥(A a)) ij.2) : R)
have rw : Eq.{u_4 + 1} (α := R)
  (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r',
    (↑(((((of.{u_1, u_4} (fun (i : ι) ↦ ↥(A i)) (i.1 + i.2) : ↥(A (i.1 + i.2)) →+ ⨁ (i : ι), ↥(A i)) :
                  (a : ↥(A (i.1 + i.2))) → ⨁ (i : ι), ↥(A i))
                (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(A i)) AddSemigroup.toAdd _ i.1 i.2
                  ((r : (a : ι) → ↥(A a)) i.1 : ↥(A i.1)) ((r' : (a : ι) → ↥(A a)) i.2 : ↥(A i.2))) :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          n) :
      R))
  (∑ ij ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r ×ˢ DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) r' with
    ij.1 + ij.2 = n, (↑((r : (a : ι) → ↥(A a)) ij.1) : R) * (↑((r' : (a : ι) → ↥(A a)) ij.2) : R))
Tactic: rw [mul_eq_sum_support_ghas_mul, DFinsupp.finsetSum_apply, AddSubmonoidClass.coe_finsetSum]