awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst_4 : AddRightCancelMonoid ι
inst_5 : GradedRing 𝒜
a : A
b : ↥(𝒜 j)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j)) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
have rw : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑b : A) : ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        (i + j)) :
    A) =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
Tactic: rw [decompose_mul, decompose_coe, coe_mul_of_apply_add]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst_4 : AddRightCancelMonoid ι
inst_5 : GradedRing 𝒜
a : A
b : ↥(𝒜 j)
rw :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑b : A) : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          (i + j)) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j)) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
have rw₁ : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
            (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) j : ↥(𝒜 j) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 j)) → ⨁ (i : ι), ↥(𝒜 i))
                b :
              ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        (i + j)) :
    A) =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
Tactic: rw [decompose_mul, decompose_coe, coe_mul_of_apply_add]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst_4 : AddRightCancelMonoid ι
inst_5 : GradedRing 𝒜
a : A
b : ↥(𝒜 j)
rw :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑b : A) : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          (i + j)) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
rw₁ :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
              (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) j : ↥(𝒜 j) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 j)) → ⨁ (i : ι), ↥(𝒜 i))
                  b :
                ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          (i + j)) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j)) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
have rw₂ : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A) =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
Tactic: rw [decompose_mul, decompose_coe, coe_mul_of_apply_add]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
j : ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
a b : A
a_mem : a ∈ 𝒜 0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) =
    a * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
have lift : ∀ (a : ↥(𝒜 0)),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
Tactic: lift a to 𝒜 0 using a_mem
Cleared hypotheses: a, a_mem
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
j : ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
b : A
a : ↥(𝒜 0)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
have rw : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑a : A) : ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        j) :
    A) =
  (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
Tactic: rw [decompose_mul, decompose_coe, coe_of_mul_apply_of_mem_zero]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
j : ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
b : A
a : ↥(𝒜 0)
rw :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑a : A) : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          j) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
have rw₁ : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                a :
              ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        j) :
    A) =
  (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
Tactic: rw [decompose_mul, decompose_coe, coe_of_mul_apply_of_mem_zero]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
j : ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
b : A
a : ↥(𝒜 0)
rw :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑a : A) : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          j) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
rw₁ :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                  a :
                ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          j) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
have rw₂ : (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) =
  (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
Tactic: rw [decompose_mul, decompose_coe, coe_of_mul_apply_of_mem_zero]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i : ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
a b : A
b_mem : b ∈ 𝒜 0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * b
have lift : ∀ (b : ↥(𝒜 0)),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
Tactic: lift b to 𝒜 0 using b_mem
Cleared hypotheses: b, b_mem
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i : ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
a : A
b : ↥(𝒜 0)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
have rw : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑b : A) : ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        i) :
    A) =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
Tactic: rw [decompose_mul, decompose_coe, coe_mul_of_apply_of_mem_zero]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i : ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
a : A
b : ↥(𝒜 0)
rw :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑b : A) : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
have rw₁ : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
            (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                b :
              ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        i) :
    A) =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
Tactic: rw [decompose_mul, decompose_coe, coe_mul_of_apply_of_mem_zero]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i : ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
a : A
b : ↥(𝒜 0)
rw :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑b : A) : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
rw₁ :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
              (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                  b :
                ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
have rw₂ : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A) =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
Tactic: rw [decompose_mul, decompose_coe, coe_mul_of_apply_of_mem_zero]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), ↥(𝒜 i)
right_inv : AlgHom.comp (coeAlgHom 𝒜) decompose = AlgHom.id R A
left_inv :
  ∀ (i : ι) (x : ↥(𝒜 i)),
    Eq (α := ⨁ (i : ι), ↥(𝒜 i)) ((decompose : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i))
      (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i)) x :
        ⨁ (i : ι), ↥(𝒜 i))
⊢ Function.RightInverse (α := A) (β := ⨁ (i : ι), ↥(𝒜 i)) (⇑(DirectSum.coeAddMonoidHom 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
    (⇑decompose : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
have suffices : decompose.comp (coeAlgHom 𝒜) = AlgHom.id R (⨁ (i : ι), ↥(𝒜 i))
Tactic: suffices decompose.comp (DirectSum.coeAlgHom 𝒜) = AlgHom.id _ _ from AlgHom.congr_fun this
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), ↥(𝒜 i)
right_inv : AlgHom.comp (coeAlgHom 𝒜) decompose = AlgHom.id R A
left_inv :
  ∀ (i : ι) (x : ↥(𝒜 i)),
    Eq (α := ⨁ (i : ι), ↥(𝒜 i)) ((decompose : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i))
      (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i)) x :
        ⨁ (i : ι), ↥(𝒜 i))
⊢ decompose.comp (coeAlgHom 𝒜) = AlgHom.id R (⨁ (i : ι), ↥(𝒜 i))
have h : ∀ (i : ι) (x : ↥(𝒜 i)),
  Eq (α := ⨁ (i : ι), ↥(𝒜 i))
    ((AlgHom.toLinearMap (decompose.comp (coeAlgHom 𝒜)) ∘ₗ lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(𝒜 i)) i :
          (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
        x :
      ⨁ (i : ι), ↥(𝒜 i))
    ((AlgHom.toLinearMap (AlgHom.id R (⨁ (i : ι), ↥(𝒜 i))) ∘ₗ lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(𝒜 i)) i :
          (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
        x :
      ⨁ (i : ι), ↥(𝒜 i))
Tactic: ext i x : 2
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ Eq (α := A) ((proj 𝒜 i : (a : A) → A) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a : A) : A)
    ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
        (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            ((a : (a : ι) → ↥(𝒜 a)) i) :
          ⨁ (i : ι), ↥(𝒜 i)) :
      A)
have rw : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a) :
            ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        i) :
    A) =
  (Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
    (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
        ((a : (a : ι) → ↥(𝒜 a)) i) :
      ⨁ (i : ι), ↥(𝒜 i))
Tactic: rw [GradedAlgebra.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
rw :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A) =
    (Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
      (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
          ((a : (a : ι) → ↥(𝒜 a)) i) :
        ⨁ (i : ι), ↥(𝒜 i))
⊢ Eq (α := A) ((proj 𝒜 i : (a : A) → A) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a : A) : A)
    ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
        (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            ((a : (a : ι) → ↥(𝒜 a)) i) :
          ⨁ (i : ι), ↥(𝒜 i)) :
      A)
have rw₁ : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a) :
            ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        i) :
    A) =
  (↑((a : (a : ι) → ↥(𝒜 a)) i) : A)
Tactic: rw [GradedAlgebra.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
rw :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A) =
    (Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
      (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
          ((a : (a : ι) → ↥(𝒜 a)) i) :
        ⨁ (i : ι), ↥(𝒜 i))
rw₁ :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A) =
    (↑((a : (a : ι) → ↥(𝒜 a)) i) : A)
⊢ Eq (α := A) ((proj 𝒜 i : (a : A) → A) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a : A) : A)
    ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
        (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            ((a : (a : ι) → ↥(𝒜 a)) i) :
          ⨁ (i : ι), ↥(𝒜 i)) :
      A)
have rw₂ : (↑((a : (a : ι) → ↥(𝒜 a)) i) : A) = (↑((a : (a : ι) → ↥(𝒜 a)) i) : A)
Tactic: rw [GradedAlgebra.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
⊢ ∀ (x y : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
have refine_1 : ∀ (x : A),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (0 * x) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
Tactic: refine DirectSum.Decomposition.inductionOn 𝒜 (fun x => ?_) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
refine_1 :
  ∀ (x : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (0 * x) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
      (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) 0) : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
⊢ ∀ (x y : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
have refine_2 : ∀ {i : ι} (m : ↥(𝒜 i)) (y : A),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑m : A) * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑m : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
Tactic: refine DirectSum.Decomposition.inductionOn 𝒜 (fun x => ?_) ?_ ?_