Theorem: Ideal.quotDecomposition_left_inv'_aux (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
⊢ coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I) =
    (Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜
Tactic:
apply linearMap_ext
State after:
case H
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
⊢ ∀ (i : ι),
    (coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
      ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i

State before:
case H
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
⊢ ∀ (i : ι),
    (coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
      ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Tactic:
intro i
State after:
case H
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
i : ι
⊢ (coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
    ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i

State before:
case H
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
i : ι
⊢ (coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
    ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Tactic:
ext x
State after:
case H.h
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
i : ι
x : ↥(𝒜 i)
⊢ ((coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) x =
    (((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) x

State before:
case H.h
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
i : ι
x : ↥(𝒜 i)
⊢ ((coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) x =
    (((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) x
Tactic:
dsimp only [LinearMap.coe_comp, comp_apply]
State after:
case H.h
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
i : ι
x : ↥(𝒜 i)
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((lmap' (quotCompMap R 𝒜 I)) ((lof R ι (fun i => ↥(𝒜 i)) i) x)) =
    ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) x)

State before:
case H.h
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
i : ι
x : ↥(𝒜 i)
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((lmap' (quotCompMap R 𝒜 I)) ((lof R ι (fun i => ↥(𝒜 i)) i) x)) =
    ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) x)
Tactic:
change _ = (Submodule.mkQ (Submodule.restrictScalars R I)) (_)
State after:
case H.h
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
i : ι
x : ↥(𝒜 i)
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((lmap' (quotCompMap R 𝒜 I)) ((lof R ι (fun i => ↥(𝒜 i)) i) x)) =
    (Submodule.restrictScalars R I).mkQ ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) x))

State before:
case H.h
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
i : ι
x : ↥(𝒜 i)
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((lmap' (quotCompMap R 𝒜 I)) ((lof R ι (fun i => ↥(𝒜 i)) i) x)) =
    (Submodule.restrictScalars R I).mkQ ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) x))
Tactic:
rw [lmap'_lof]
State after:
case H.h
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
i : ι
x : ↥(𝒜 i)
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) ((quotCompMap R 𝒜 I i) x)) =
    (Submodule.restrictScalars R I).mkQ ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) x))

State before:
case H.h
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
i : ι
x : ↥(𝒜 i)
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) ((quotCompMap R 𝒜 I i) x)) =
    (Submodule.restrictScalars R I).mkQ ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) x))
Tactic:
simp only [lof_eq_of, coeLinearMap_of, Submodule.mkQ_apply]
State after:
case H.h
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
i : ι
x : ↥(𝒜 i)
⊢ ↑((quotCompMap R 𝒜 I i) x) = Submodule.Quotient.mk ↑x

State before:
case H.h
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
i : ι
x : ↥(𝒜 i)
⊢ ↑((quotCompMap R 𝒜 I i) x) = Submodule.Quotient.mk ↑x
Tactic:
rfl
State after:
no goals