Theorem: quotDecompose'_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
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a)
Tactic:
suffices (quotDecompose' R 𝒜 rel).comp (lmap' (quotCompMap R 𝒜 rel)) =
    (RingQuot.mkAlgHom R rel).toLinearMap.comp (coeLinearMap 𝒜) by
  simp only [LinearMap.ext_iff, LinearMap.comp_apply, AlgHom.toLinearMap_apply] at this
  apply this
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
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel) = (RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜

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
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel) = (RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜
Tactic:
apply linearMap_ext
State after:
case H
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
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ ∀ (i : ι),
    (quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
      ((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i

State before:
case H
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
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ ∀ (i : ι),
    (quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
      ((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Tactic:
intro i
State after:
case H
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
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ (quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
    ((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i

State before:
case H
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
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ (quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
    ((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Tactic:
ext ⟨x, hx⟩
State after:
case H.h.mk
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
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ ((quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩ =
    (((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩

State before:
case H.h.mk
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
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ ((quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩ =
    (((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
Tactic:
simp only [quotDecompose', LinearMap.coe_comp, comp_apply, AlgHom.toLinearMap_apply,
  lmap'_lof, toModule_lof]
State after:
case H.h.mk
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
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ (quotSubmodule R 𝒜 rel i).subtype ((quotCompMap R 𝒜 rel i) ⟨x, hx⟩) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩))

State before:
case H.h.mk
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
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ (quotSubmodule R 𝒜 rel i).subtype ((quotCompMap R 𝒜 rel i) ⟨x, hx⟩) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩))
Tactic:
simp only [lof_eq_of, coeLinearMap_of, quotCompMap, LinearMap.coe_mk,
  AddHom.coe_mk, Submodule.coeSubtype]
State after:
no goals

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

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