awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ ∀ (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_3 : ∀ (m m' : A),
  (∀ (y : A),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (m * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) m : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)) →
    (∀ (y : A),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (m' * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) m' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)) →
      ∀ (y : A),
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((m + m') * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) :
            A) =
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (m + m') : ⨁ (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 => ?_) ?_ ?_
-- 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
⊢ ∀ (y : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * y) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            0) :
        A) =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
                  ⨁ (i : ι), ↥(𝒜 i)) :
                (a : ι) → ↥(𝒜 a))
              0) :
          A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
have refine_2 : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * 0) :
            ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        0) :
    A) =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) *
    (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) 0) : A)
Tactic: refine DirectSum.Decomposition.inductionOn 𝒜 ?_ ?_ ?_
-- 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
refine_2 :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * 0) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            0) :
        A) *
      (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) 0) : A)
⊢ ∀ (y : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * y) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            0) :
        A) =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
                  ⨁ (i : ι), ↥(𝒜 i)) :
                (a : ι) → ↥(𝒜 a))
              0) :
          A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
have refine_2₁ : ∀ {i_1 : ι} (m : ↥(𝒜 i_1)),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * (↑m : A)) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            0) :
        A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑m : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
Tactic: refine DirectSum.Decomposition.inductionOn 𝒜 ?_ ?_ ?_
-- 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) *
                  (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) c' hc') : A)) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            0) :
        A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) c' hc') : A) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            0) :
        A)
have refine_2 : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (c * c') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
Tactic: simp only
-- 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (c * c') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
have pos : ∀ (h : i + j = 0),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (c * c') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
Tactic: by_cases h : i + j = 0
-- 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
pos :
  ∀ (h : i + j = 0),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (c * c') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (c * c') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
have neg : ∀ (h : ¬i + j = 0),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (c * c') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
Tactic: by_cases h : i + j = 0
-- 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : i + j = 0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (c * c') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
have pos : c * c' =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
Tactic: rw [decompose_of_mem_same 𝒜
              (show c * c' ∈ 𝒜 0 from h ▸ SetLike.GradedMul.mul_mem hc hc'),
            decompose_of_mem_same 𝒜 (show c ∈ 𝒜 0 from (add_eq_zero.mp h).1 ▸ hc),
            decompose_of_mem_same 𝒜 (show c' ∈ 𝒜 0 from (add_eq_zero.mp h).2 ▸ hc')]
-- 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : i + j = 0
pos :
  c * c' =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (c * c') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
have pos₁ : c * c' = c * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
Tactic: rw [decompose_of_mem_same 𝒜
              (show c * c' ∈ 𝒜 0 from h ▸ SetLike.GradedMul.mul_mem hc hc'),
            decompose_of_mem_same 𝒜 (show c ∈ 𝒜 0 from (add_eq_zero.mp h).1 ▸ hc),
            decompose_of_mem_same 𝒜 (show c' ∈ 𝒜 0 from (add_eq_zero.mp h).2 ▸ hc')]
-- 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : i + j = 0
pos :
  c * c' =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
pos₁ : c * c' = c * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (c * c') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
have pos₂ : c * c' = c * c'
Tactic: rw [decompose_of_mem_same 𝒜
              (show c * c' ∈ 𝒜 0 from h ▸ SetLike.GradedMul.mul_mem hc hc'),
            decompose_of_mem_same 𝒜 (show c ∈ 𝒜 0 from (add_eq_zero.mp h).1 ▸ hc),
            decompose_of_mem_same 𝒜 (show c' ∈ 𝒜 0 from (add_eq_zero.mp h).2 ▸ hc')]
-- 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (c * c') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
have neg : 0 =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
Tactic: rw [decompose_of_mem_ne 𝒜 (SetLike.GradedMul.mul_mem hc hc') h]
-- 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
⊢ i ≠ 0 ∨ j ≠ 0
have rwa : ∀ (h : ¬(i = 0 ∧ j = 0)), i ≠ 0 ∨ j ≠ 0
Tactic: rwa [add_eq_zero, not_and_or] at h
Cleared hypotheses: h
-- 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
rwa : ∀ (h : ¬(i = 0 ∧ j = 0)), i ≠ 0 ∨ j ≠ 0
⊢ i ≠ 0 ∨ j ≠ 0
have rwa₁ : ∀ (h : ¬i = 0 ∨ ¬j = 0), i ≠ 0 ∨ j ≠ 0
Tactic: rwa [add_eq_zero, not_and_or] at h
Cleared hypotheses: h
-- 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
⊢ 0 =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
have neg : ∀ (h' : i ≠ 0),
  0 =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
Tactic: rcases show i ≠ 0 ∨ j ≠ 0 by rwa [add_eq_zero, not_and_or] at h with h' | h'
-- 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
neg :
  ∀ (h' : i ≠ 0),
    0 =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
⊢ 0 =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
have neg₁ : ∀ (h' : j ≠ 0),
  0 =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
Tactic: rcases show i ≠ 0 ∨ j ≠ 0 by rwa [add_eq_zero, not_and_or] at h with h' | h'
-- 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 𝒜
⊢ (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
have rw : (↑(((0 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
Tactic: rw [decompose_zero, zero_apply, ZeroMemClass.coe_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 : 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 𝒜
rw : (↑(((0 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
⊢ (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
have rw₁ : Eq.{u_3 + 1} (α := A) (↑0 : A) 0
Tactic: rw [decompose_zero, zero_apply, ZeroMemClass.coe_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 : 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 𝒜
rw : (↑(((0 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
rw₁ : Eq.{u_3 + 1} (α := A) (↑0 : A) 0
⊢ (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
have rw₂ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [decompose_zero, zero_apply, ZeroMemClass.coe_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 : 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 x_1 : A
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x + x_1) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) +
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
have rw : (↑((HAdd.hAdd (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        0) :
    A) =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) +
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
Tactic: rw [decompose_add, add_apply, AddMemClass.coe_add]
-- 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 x_1 : A
rw :
  (↑((HAdd.hAdd (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) +
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x + x_1) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) +
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
have rw₁ : (↑(HAdd.hAdd (α := ↥(𝒜 0)) ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0)
        ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0)) :
    A) =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) +
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
Tactic: rw [decompose_add, add_apply, AddMemClass.coe_add]