[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : AddMonoid ι
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : ⨁ (i : ι), { x // x ∈ 𝒜 i }
i : ι
⊢ ↑(proj 𝒜 i) (↑(decompose 𝒜).symm a) = ↑(decompose 𝒜).symm (↑(of (fun i => (fun i => { x // x ∈ 𝒜 i }) i) i) (↑a i))
[PROOFSTEP]
rw [GradedRing.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddLeftCancelMonoid ι
inst✝ : GradedRing 𝒜
a b : A
a_mem : a ∈ 𝒜 i
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) (i + j)) = a * ↑(↑(↑(decompose 𝒜) b) j)
[PROOFSTEP]
lift a to 𝒜 i using a_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddLeftCancelMonoid ι
inst✝ : GradedRing 𝒜
b : A
a : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (↑a * b)) (i + j)) = ↑a * ↑(↑(↑(decompose 𝒜) b) j)
[PROOFSTEP]
rw [decompose_mul, decompose_coe, coe_of_mul_apply_add]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a b : A
b_mem : b ∈ 𝒜 j
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) (i + j)) = ↑(↑(↑(decompose 𝒜) a) i) * b
[PROOFSTEP]
lift b to 𝒜 j using b_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : { x // x ∈ 𝒜 j }
⊢ ↑(↑(↑(decompose 𝒜) (a * ↑b)) (i + j)) = ↑(↑(↑(decompose 𝒜) a) i) * ↑b
[PROOFSTEP]
rw [decompose_mul, decompose_coe, coe_mul_of_apply_add]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), { x // x ∈ 𝒜 i }
right_inv : AlgHom.comp (coeAlgHom 𝒜) decompose = AlgHom.id R A
left_inv : ∀ (i : ι) (x : { x // x ∈ 𝒜 i }), ↑decompose ↑x = ↑(of (fun i => { x // x ∈ 𝒜 i }) i) x
⊢ Function.RightInverse ↑(DirectSum.coeAddMonoidHom 𝒜) ↑decompose
[PROOFSTEP]
suffices decompose.comp (DirectSum.coeAlgHom 𝒜) = AlgHom.id _ _ from AlgHom.congr_fun this
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), { x // x ∈ 𝒜 i }
right_inv : AlgHom.comp (coeAlgHom 𝒜) decompose = AlgHom.id R A
left_inv : ∀ (i : ι) (x : { x // x ∈ 𝒜 i }), ↑decompose ↑x = ↑(of (fun i => { x // x ∈ 𝒜 i }) i) x
⊢ AlgHom.comp decompose (coeAlgHom 𝒜) = AlgHom.id R (⨁ (i : ι), { x // x ∈ 𝒜 i })
[PROOFSTEP]
refine DirectSum.algHom_ext' _ _ fun i => ?_
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), { x // x ∈ 𝒜 i }
right_inv : AlgHom.comp (coeAlgHom 𝒜) decompose = AlgHom.id R A
left_inv : ∀ (i : ι) (x : { x // x ∈ 𝒜 i }), ↑decompose ↑x = ↑(of (fun i => { x // x ∈ 𝒜 i }) i) x
i : ι
⊢ LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp decompose (coeAlgHom 𝒜))) (lof R ι (fun i => { x // x ∈ 𝒜 i }) i) =
    LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (⨁ (i : ι), { x // x ∈ 𝒜 i })))
      (lof R ι (fun i => { x // x ∈ 𝒜 i }) i)
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), { x // x ∈ 𝒜 i }
right_inv : AlgHom.comp (coeAlgHom 𝒜) decompose = AlgHom.id R A
left_inv : ∀ (i : ι) (x : { x // x ∈ 𝒜 i }), ↑decompose ↑x = ↑(of (fun i => { x // x ∈ 𝒜 i }) i) x
i : ι
x : { x // x ∈ 𝒜 i }
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp decompose (coeAlgHom 𝒜))) (lof R ι (fun i => { x // x ∈ 𝒜 i }) i))
      x =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (⨁ (i : ι), { x // x ∈ 𝒜 i })))
          (lof R ι (fun i => { x // x ∈ 𝒜 i }) i))
      x
[PROOFSTEP]
exact (decompose.congr_arg <| DirectSum.coeAlgHom_of _ _ _).trans (left_inv i x)
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
a : ⨁ (i : ι), { x // x ∈ 𝒜 i }
i : ι
⊢ ↑(proj 𝒜 i) (↑(decompose 𝒜).symm a) = ↑(decompose 𝒜).symm (↑(of (fun i => (fun i => { x // x ∈ 𝒜 i }) i) i) (↑a i))
[PROOFSTEP]
rw [GradedAlgebra.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ∀ (x y : A),
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (x * y) =
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } x *
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y
[PROOFSTEP]
refine' DirectSum.Decomposition.inductionOn 𝒜 (fun x => _) _ _
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : A
⊢ OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } (0 * x) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } 0 *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } x
[PROOFSTEP]
simp only [zero_mul, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ∀ {i : ι} (m : { x // x ∈ 𝒜 i }) (y : A),
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (↑m * y) =
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } ↑m *
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y
[PROOFSTEP]
rintro i ⟨c, hc⟩
[GOAL]
case refine'_2.mk
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
⊢ ∀ (y : A),
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (↑{ val := c, property := hc } * y) =
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
          ↑{ val := c, property := hc } *
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y
[PROOFSTEP]
refine' DirectSum.Decomposition.inductionOn 𝒜 _ _ _
[GOAL]
case refine'_2.mk.refine'_1
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
⊢ OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      (↑{ val := c, property := hc } * 0) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        ↑{ val := c, property := hc } *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } 0
[PROOFSTEP]
simp only [mul_zero, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
[GOAL]
case refine'_2.mk.refine'_2
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
⊢ ∀ {i_1 : ι} (m : { x // x ∈ 𝒜 i_1 }),
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (↑{ val := c, property := hc } * ↑m) =
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
          ↑{ val := c, property := hc } *
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } ↑m
[PROOFSTEP]
rintro j ⟨c', hc'⟩
[GOAL]
case refine'_2.mk.refine'_2.mk
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
⊢ OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      (↑{ val := c, property := hc } * ↑{ val := c', property := hc' }) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        ↑{ val := c, property := hc } *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        ↑{ val := c', property := hc' }
[PROOFSTEP]
simp only [Subtype.coe_mk]
[GOAL]
case refine'_2.mk.refine'_2.mk
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
⊢ ↑(↑(↑(decompose 𝒜) (c * c')) 0) = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) c') 0)
[PROOFSTEP]
by_cases h : i + j = 0
[GOAL]
case pos
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : i + j = 0
⊢ ↑(↑(↑(decompose 𝒜) (c * c')) 0) = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) c') 0)
[PROOFSTEP]
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_iff.mp h).1 ▸ hc),
  decompose_of_mem_same 𝒜 (show c' ∈ 𝒜 0 from (add_eq_zero_iff.mp h).2 ▸ hc')]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
⊢ ↑(↑(↑(decompose 𝒜) (c * c')) 0) = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) c') 0)
[PROOFSTEP]
rw [decompose_of_mem_ne 𝒜 (SetLike.GradedMul.mul_mem hc hc') h]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
⊢ 0 = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) c') 0)
[PROOFSTEP]
cases' show i ≠ 0 ∨ j ≠ 0 by rwa [add_eq_zero_iff, not_and_or] at h  with h' h'
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
⊢ i ≠ 0 ∨ j ≠ 0
[PROOFSTEP]
rwa [add_eq_zero_iff, not_and_or] at h 
[GOAL]
case neg.inl
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
h' : i ≠ 0
⊢ 0 = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) c') 0)
[PROOFSTEP]
simp only [decompose_of_mem_ne 𝒜 hc h', zero_mul]
[GOAL]
case neg.inr
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
h' : j ≠ 0
⊢ 0 = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) c') 0)
[PROOFSTEP]
simp only [decompose_of_mem_ne 𝒜 hc' h', mul_zero]
[GOAL]
case refine'_2.mk.refine'_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
⊢ ∀ (m m' : A),
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
          (↑{ val := c, property := hc } * m) =
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
            ↑{ val := c, property := hc } *
          OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
            m →
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
            (↑{ val := c, property := hc } * m') =
          OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              ↑{ val := c, property := hc } *
            OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              m' →
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
            (↑{ val := c, property := hc } * (m + m')) =
          OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              ↑{ val := c, property := hc } *
            OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              (m + m')
[PROOFSTEP]
intro _ _ hd he
[GOAL]
case refine'_2.mk.refine'_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
m✝ m'✝ : A
hd :
  OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      (↑{ val := c, property := hc } * m✝) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        ↑{ val := c, property := hc } *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } m✝
he :
  OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      (↑{ val := c, property := hc } * m'✝) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        ↑{ val := c, property := hc } *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } m'✝
⊢ OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      (↑{ val := c, property := hc } * (m✝ + m'✝)) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        ↑{ val := c, property := hc } *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (m✝ + m'✝)
[PROOFSTEP]
simp only at hd he 
[GOAL]
case refine'_2.mk.refine'_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
m✝ m'✝ : A
hd : ↑(↑(↑(decompose 𝒜) (c * m✝)) 0) = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) m✝) 0)
he : ↑(↑(↑(decompose 𝒜) (c * m'✝)) 0) = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) m'✝) 0)
⊢ OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      (↑{ val := c, property := hc } * (m✝ + m'✝)) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        ↑{ val := c, property := hc } *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (m✝ + m'✝)
[PROOFSTEP]
simp only [mul_add, decompose_add, add_apply, AddMemClass.coe_add, hd, he]
[GOAL]
case refine'_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ∀ (m m' : A),
    (∀ (y : A),
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
            (m * y) =
          OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              m *
            OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              y) →
      (∀ (y : A),
          OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              (m' * y) =
            OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                m' *
              OneHom.toFun
                { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y) →
        ∀ (y : A),
          OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              ((m + m') * y) =
            OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                (m + m') *
              OneHom.toFun
                { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y
[PROOFSTEP]
rintro _ _ ha hb _
[GOAL]
case refine'_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
m✝ m'✝ : A
ha :
  ∀ (y : A),
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (m✝ * y) =
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } m✝ *
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y
hb :
  ∀ (y : A),
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (m'✝ * y) =
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } m'✝ *
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y
y✝ : A
⊢ OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      ((m✝ + m'✝) * y✝) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (m✝ + m'✝) *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y✝
[PROOFSTEP]
simp only at ha hb 
[GOAL]
case refine'_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
m✝ m'✝ : A
ha : ∀ (y : A), ↑(↑(↑(decompose 𝒜) (m✝ * y)) 0) = ↑(↑(↑(decompose 𝒜) m✝) 0) * ↑(↑(↑(decompose 𝒜) y) 0)
hb : ∀ (y : A), ↑(↑(↑(decompose 𝒜) (m'✝ * y)) 0) = ↑(↑(↑(decompose 𝒜) m'✝) 0) * ↑(↑(↑(decompose 𝒜) y) 0)
y✝ : A
⊢ OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      ((m✝ + m'✝) * y✝) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (m✝ + m'✝) *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y✝
[PROOFSTEP]
simp only [add_mul, decompose_add, add_apply, AddMemClass.coe_add, ha, hb]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) },
          map_mul' :=
            (_ :
              ∀ (m y : A),
                OneHom.toFun
                    { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                    (m * y) =
                  OneHom.toFun
                      { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } m *
                    OneHom.toFun
                      { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                      y) })
      0 =
    0
[PROOFSTEP]
simp only
  -- Porting note: added
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ↑(↑(↑(decompose 𝒜) 0) 0) = 0
[PROOFSTEP]
rw [decompose_zero]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ↑(↑0 0) = 0
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x✝¹ x✝ : A
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) },
          map_mul' :=
            (_ :
              ∀ (m y : A),
                OneHom.toFun
                    { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                    (m * y) =
                  OneHom.toFun
                      { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } m *
                    OneHom.toFun
                      { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                      y) })
      (x✝¹ + x✝) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) },
            map_mul' :=
              (_ :
                ∀ (m y : A),
                  OneHom.toFun
                      { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                      (m * y) =
                    OneHom.toFun
                        { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                        m *
                      OneHom.toFun
                        { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                        y) })
        x✝¹ +
      OneHom.toFun
        (↑{ toOneHom := { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) },
            map_mul' :=
              (_ :
                ∀ (m y : A),
                  OneHom.toFun
                      { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                      (m * y) =
                    OneHom.toFun
                        { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                        m *
                      OneHom.toFun
                        { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                        y) })
        x✝
[PROOFSTEP]
simp only
  -- Porting note: added
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x✝¹ x✝ : A
⊢ ↑(↑(↑(decompose 𝒜) (x✝¹ + x✝)) 0) = ↑(↑(↑(decompose 𝒜) x✝¹) 0) + ↑(↑(↑(decompose 𝒜) x✝) 0)
[PROOFSTEP]
rw [decompose_add]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x✝¹ x✝ : A
⊢ ↑(↑(↑(decompose 𝒜) x✝¹ + ↑(decompose 𝒜) x✝) 0) = ↑(↑(↑(decompose 𝒜) x✝¹) 0) + ↑(↑(↑(decompose 𝒜) x✝) 0)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a b : A
n i : ι
a_mem : a ∈ 𝒜 i
h : ¬i ≤ n
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = 0
[PROOFSTEP]
lift a to 𝒜 i using a_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
b : A
n i : ι
h : ¬i ≤ n
a : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (↑a * b)) n) = 0
[PROOFSTEP]
rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_not_le]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a b : A
n i : ι
b_mem : b ∈ 𝒜 i
h : ¬i ≤ n
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = 0
[PROOFSTEP]
lift b to 𝒜 i using b_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : A
n i : ι
h : ¬i ≤ n
b : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (a * ↑b)) n) = 0
[PROOFSTEP]
rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_not_le]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁸ : Semiring A
inst✝⁷ : DecidableEq ι
inst✝⁶ : CanonicallyOrderedAddMonoid ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a_mem : a ∈ 𝒜 i
h : i ≤ n
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = a * ↑(↑(↑(decompose 𝒜) b) (n - i))
[PROOFSTEP]
lift a to 𝒜 i using a_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁸ : Semiring A
inst✝⁷ : DecidableEq ι
inst✝⁶ : CanonicallyOrderedAddMonoid ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : i ≤ n
a : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (↑a * b)) n) = ↑a * ↑(↑(↑(decompose 𝒜) b) (n - i))
[PROOFSTEP]
rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_le]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁸ : Semiring A
inst✝⁷ : DecidableEq ι
inst✝⁶ : CanonicallyOrderedAddMonoid ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b_mem : b ∈ 𝒜 i
h : i ≤ n
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = ↑(↑(↑(decompose 𝒜) a) (n - i)) * b
[PROOFSTEP]
lift b to 𝒜 i using b_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁸ : Semiring A
inst✝⁷ : DecidableEq ι
inst✝⁶ : CanonicallyOrderedAddMonoid ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : i ≤ n
b : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (a * ↑b)) n) = ↑(↑(↑(decompose 𝒜) a) (n - i)) * ↑b
[PROOFSTEP]
rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_le]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁹ : Semiring A
inst✝⁸ : DecidableEq ι
inst✝⁷ : CanonicallyOrderedAddMonoid ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a b : A
n✝ i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : ι
inst✝ : Decidable (i ≤ n)
a_mem : a ∈ 𝒜 i
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = if i ≤ n then a * ↑(↑(↑(decompose 𝒜) b) (n - i)) else 0
[PROOFSTEP]
lift a to 𝒜 i using a_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁹ : Semiring A
inst✝⁸ : DecidableEq ι
inst✝⁷ : CanonicallyOrderedAddMonoid ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
b : A
n✝ i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : ι
inst✝ : Decidable (i ≤ n)
a : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (↑a * b)) n) = if i ≤ n then ↑a * ↑(↑(↑(decompose 𝒜) b) (n - i)) else 0
[PROOFSTEP]
rw [decompose_mul, decompose_coe, coe_of_mul_apply]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁹ : Semiring A
inst✝⁸ : DecidableEq ι
inst✝⁷ : CanonicallyOrderedAddMonoid ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a b : A
n✝ i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : ι
inst✝ : Decidable (i ≤ n)
b_mem : b ∈ 𝒜 i
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = if i ≤ n then ↑(↑(↑(decompose 𝒜) a) (n - i)) * b else 0
[PROOFSTEP]
lift b to 𝒜 i using b_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁹ : Semiring A
inst✝⁸ : DecidableEq ι
inst✝⁷ : CanonicallyOrderedAddMonoid ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a : A
n✝ i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : ι
inst✝ : Decidable (i ≤ n)
b : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (a * ↑b)) n) = if i ≤ n then ↑(↑(↑(decompose 𝒜) a) (n - i)) * ↑b else 0
[PROOFSTEP]
rw [decompose_mul, decompose_coe, coe_mul_of_apply]
