Theorem: lmap'_quotCompMap_apply (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 𝒜
i : ι
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
    ↑(((lmap' (quotCompMap R 𝒜 rel)) a) i)
Tactic:
simp only [lmap'_apply]
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 𝒜
i : ι
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
    ↑((quotCompMap R 𝒜 rel i) (a 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 𝒜
i : ι
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
    ↑((quotCompMap R 𝒜 rel i) (a i))
Tactic:
congr
State after:
case h.e_6.h.e_self.e_a
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 𝒜
i : ι
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a) = a

State before:
case h.e_6.h.e_self.e_a
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 𝒜
i : ι
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a) = a
Tactic:
exact h𝒜.right_inv a
State after:
no goals