Theorem: quotDecompose_left_inv'_aux_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
x : ⨁ (i : ι), ↥(𝒜 i)
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) x) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)
Tactic:
let e := quotDecompose_left_inv'_aux R 𝒜 rel
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
x : ⨁ (i : ι), ↥(𝒜 i)
e : (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ lmap' (quotCompMap R 𝒜 rel) =
  (RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜 :=
  quotDecompose_left_inv'_aux R 𝒜 rel
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) x) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)

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
x : ⨁ (i : ι), ↥(𝒜 i)
e : (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ lmap' (quotCompMap R 𝒜 rel) =
  (RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜 :=
  quotDecompose_left_inv'_aux R 𝒜 rel
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) x) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)
Tactic:
simp only [LinearMap.ext_iff, LinearMap.comp_apply, AlgHom.toLinearMap_apply] at e
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
x : ⨁ (i : ι), ↥(𝒜 i)
e :
  ∀ (x : ⨁ (i : ι), ↥(𝒜 i)),
    (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) x) =
      (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) x) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)

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
x : ⨁ (i : ι), ↥(𝒜 i)
e :
  ∀ (x : ⨁ (i : ι), ↥(𝒜 i)),
    (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) x) =
      (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) x) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)
Tactic:
apply e
State after:
no goals