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 𝒜
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)
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)
⊢ (↑((((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₂ : (↑((((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 : ⨁ (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
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 𝒜
a : ↥(𝒜 0)
⊢ ((projZeroRingHom' 𝒜 : A →+* ↥(𝒜 0)) : (a : A) → ↥(𝒜 0)) (↑a : A) = a
have a₁ : (↑(((projZeroRingHom' 𝒜 : A →+* ↥(𝒜 0)) : (a : A) → ↥(𝒜 0)) (↑a : A)) : A) = (↑a : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
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 𝒜
a b : A
n i : ι
a_mem : a ∈ 𝒜 i
h : ¬i ≤ n
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 0
have lift : ∀ (a : ↥(𝒜 i)),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 0
Tactic: lift a to 𝒜 i 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 : 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 𝒜
b : A
n i : ι
h : ¬i ≤ n
a : ↥(𝒜 i)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 0
have rwa : (↑((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))
        n) :
    A) =
  0
Tactic: rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_not_le]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
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 𝒜
b : A
n i : ι
h : ¬i ≤ n
a : ↥(𝒜 i)
rwa :
  (↑((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))
          n) :
      A) =
    0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 0
have rwa₁ : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                a :
              ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        n) :
    A) =
  0
Tactic: rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_not_le]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
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 𝒜
b : A
n i : ι
h : ¬i ≤ n
a : ↥(𝒜 i)
rwa :
  (↑((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))
          n) :
      A) =
    0
rwa₁ :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                  a :
                ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          n) :
      A) =
    0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 0
have rwa₂ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_not_le]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
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 𝒜
a b : A
n i : ι
b_mem : b ∈ 𝒜 i
h : ¬i ≤ n
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 0
have lift : ∀ (b : ↥(𝒜 i)),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 0
Tactic: lift b to 𝒜 i 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 : 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 𝒜
a : A
n i : ι
h : ¬i ≤ n
b : ↥(𝒜 i)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 0
have rwa : (↑((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))
        n) :
    A) =
  0
Tactic: rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_not_le]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
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 𝒜
a : A
n i : ι
h : ¬i ≤ n
b : ↥(𝒜 i)
rwa :
  (↑((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))
          n) :
      A) =
    0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 0
have rwa₁ : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
            (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                b :
              ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        n) :
    A) =
  0
Tactic: rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_not_le]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
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 𝒜
a : A
n i : ι
h : ¬i ≤ n
b : ↥(𝒜 i)
rwa :
  (↑((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))
          n) :
      A) =
    0
rwa₁ :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
              (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                  b :
                ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          n) :
      A) =
    0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 0
have rwa₂ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_not_le]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
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 𝒜
a b : A
n i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
a_mem : a ∈ 𝒜 i
h : i ≤ n
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    a * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
have lift : ∀ (a : ↥(𝒜 i)),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
Tactic: lift a to 𝒜 i 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 : 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 𝒜
b : A
n i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
h : i ≤ n
a : ↥(𝒜 i)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
have rwa : (↑((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))
        n) :
    A) =
  (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
Tactic: rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_le]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
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 𝒜
b : A
n i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
h : i ≤ n
a : ↥(𝒜 i)
rwa :
  (↑((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))
          n) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
have rwa₁ : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                a :
              ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        n) :
    A) =
  (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
Tactic: rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_le]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
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 𝒜
b : A
n i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
h : i ≤ n
a : ↥(𝒜 i)
rwa :
  (↑((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))
          n) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
rwa₁ :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                  a :
                ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          n) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
have rwa₂ : (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) =
  (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
Tactic: rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_le]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
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 𝒜
a b : A
n i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
b_mem : b ∈ 𝒜 i
h : i ≤ n
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * b
have lift : ∀ (b : ↥(𝒜 i)),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
Tactic: lift b to 𝒜 i 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 : 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 𝒜
a : A
n i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
h : i ≤ n
b : ↥(𝒜 i)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
have rwa : (↑((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))
        n) :
    A) =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
Tactic: rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_le]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
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 𝒜
a : A
n i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
h : i ≤ n
b : ↥(𝒜 i)
rwa :
  (↑((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))
          n) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
have rwa₁ : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
            (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                b :
              ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        n) :
    A) =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
Tactic: rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_le]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
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 𝒜
a : A
n i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
h : i ≤ n
b : ↥(𝒜 i)
rwa :
  (↑((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))
          n) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
rwa₁ :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
              (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                  b :
                ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          n) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
have rwa₂ : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A) =
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
Tactic: rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_le]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
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 𝒜
a b : A
i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
n : ι
inst_11 : Decidable (i ≤ n)
a_mem : a ∈ 𝒜 i
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    if i ≤ n then
      a * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
    else 0
have lift : ∀ (a : ↥(𝒜 i)),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    if i ≤ n then
      (↑a : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
    else 0
Tactic: lift a to 𝒜 i using a_mem
Cleared hypotheses: a, a_mem