Theorem: quotDecompose_injective (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
x y : A
hxy : (RingQuot.mkAlgHom R rel) x = (RingQuot.mkAlgHom R rel) y
i : ι
⊢ (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' x) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' y) i)
Tactic:
rw [← AlgHom.coe_toRingHom, RingQuot.mkAlgHom_coe R rel, obvious_iff] at hxy ⊢
State after:
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
x y : A
hxy : RingConGen.Rel rel x y
i : ι
⊢ RingConGen.Rel rel ↑((Decomposition.decompose' x) i) ↑((Decomposition.decompose' y) i)

State before:
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
x y : A
hxy : RingConGen.Rel rel x y
i : ι
⊢ RingConGen.Rel rel ↑((Decomposition.decompose' x) i) ↑((Decomposition.decompose' y) i)
Tactic:
exact RingConGen.RelIsHomogeneous_of 𝒜 _ hrel hxy i
State after:
no goals