Theorem: Ideal.quotDecomposeLaux_of_mem_eq_zero (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
i : ι
⊢ ((quotDecomposeLaux R 𝒜 I) x) i = 0
Tactic:
rw [Ideal.quotDecomposeLaux, LinearMap.comp_apply, lmap'_apply, quotCompMap]
State after:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
i : ι
⊢ { toFun := fun u => ⟨(Quotient.mkₐ R I) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
      (((decomposeAlgEquiv 𝒜).toLinearMap x) i) =
    0

State before:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
i : ι
⊢ { toFun := fun u => ⟨(Quotient.mkₐ R I) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
      (((decomposeAlgEquiv 𝒜).toLinearMap x) i) =
    0
Tactic:
simp only [Ideal.Quotient.mkₐ_eq_mk, AlgEquiv.toLinearMap_apply, decomposeAlgEquiv_apply,
  LinearMap.coe_mk, AddHom.coe_mk, Submodule.mk_eq_zero]
State after:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
i : ι
⊢ (Quotient.mk I) ↑(((decompose 𝒜) x) i) = 0

State before:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
i : ι
⊢ (Quotient.mk I) ↑(((decompose 𝒜) x) i) = 0
Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem]
State after:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
i : ι
⊢ ↑(((decompose 𝒜) x) i) ∈ I

State before:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
i : ι
⊢ ↑(((decompose 𝒜) x) i) ∈ I
Tactic:
exact hI i hx
State after:
no goals