Theorem: quotDecompose_left_inv'_aux (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
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ 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
⊢ ∀ (i : ι),
    ((coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ 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
⊢ ∀ (i : ι),
    ((coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ 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
i : ι
⊢ ((coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ 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
i : ι
⊢ ((coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ 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
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ (((coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ 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
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ (((coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ 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 [quotCompMap, LinearMap.coe_comp, comp_apply, AlgHom.toLinearMap_apply, lmap'_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
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))
      ((lof R ι (fun i => ↥(Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))) i)
        ({ toFun := fun u => ⟨(RingQuot.mkAlgHom R rel) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⟨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
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))
      ((lof R ι (fun i => ↥(Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))) i)
        ({ toFun := fun u => ⟨(RingQuot.mkAlgHom R rel) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⟨x, hx⟩)) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩))
Tactic:
simp only [lof_eq_of, coeLinearMap_of]
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
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ ↑({ toFun := fun u => ⟨(RingQuot.mkAlgHom R rel) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⟨x, hx⟩) =
    (RingQuot.mkAlgHom R rel) x

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
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ ↑({ toFun := fun u => ⟨(RingQuot.mkAlgHom R rel) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⟨x, hx⟩) =
    (RingQuot.mkAlgHom R rel) x
Tactic:
rfl
State after:
no goals