Theorem: rTensor_fg_directedSystem (DividedPowers/ForMathlib/DirectLimit.lean)

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
p : ↥↑P ⊗[R] N
hP : P ≤ P
⊢ (LinearMap.rTensor N (Submodules_fg_inclusion R M P P hP)) p = p
Tactic:
rw [← LinearMap.id_apply (R := R) p]
State after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
p : ↥↑P ⊗[R] N
hP : P ≤ P
⊢ (LinearMap.rTensor N (Submodules_fg_inclusion R M P P hP)) (LinearMap.id p) = LinearMap.id p

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
p : ↥↑P ⊗[R] N
hP : P ≤ P
⊢ (LinearMap.rTensor N (Submodules_fg_inclusion R M P P hP)) (LinearMap.id p) = LinearMap.id p
Tactic:
apply DFunLike.congr_fun
State after:
case h₁
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
p : ↥↑P ⊗[R] N
hP : P ≤ P
⊢ LinearMap.rTensor N (Submodules_fg_inclusion R M P P hP) = LinearMap.id

State before:
case h₁
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
p : ↥↑P ⊗[R] N
hP : P ≤ P
⊢ LinearMap.rTensor N (Submodules_fg_inclusion R M P P hP) = LinearMap.id
Tactic:
ext p n
State after:
case h₁.a.h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
p✝ : ↥↑P ⊗[R] N
hP : P ≤ P
p : ↥↑P
n : N
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor N (Submodules_fg_inclusion R M P P hP))) p) n =
    ((AlgebraTensorModule.curry LinearMap.id) p) n

State before:
case h₁.a.h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodules_fg R M
p✝ : ↥↑P ⊗[R] N
hP : P ≤ P
p : ↥↑P
n : N
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor N (Submodules_fg_inclusion R M P P hP))) p) n =
    ((AlgebraTensorModule.curry LinearMap.id) p) n
Tactic:
rfl
State after:
no goals

State before:
R✝ : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R✝
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
inst✝¹ : AddCommGroup N
inst✝ : Module R✝ N
P Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p : ↥↑P ⊗[R✝] N
⊢ (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M Q R hRQ))
      ((LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P Q hPQ)) p) =
    (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P R ⋯)) p
Tactic:
rw [← LinearMap.comp_apply, ← LinearMap.rTensor_comp]
State after:
R✝ : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R✝
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
inst✝¹ : AddCommGroup N
inst✝ : Module R✝ N
P Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p : ↥↑P ⊗[R✝] N
⊢ (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M Q R hRQ ∘ₗ Submodules_fg_inclusion R✝ M P Q hPQ)) p =
    (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P R ⋯)) p

State before:
R✝ : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R✝
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
inst✝¹ : AddCommGroup N
inst✝ : Module R✝ N
P Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p : ↥↑P ⊗[R✝] N
⊢ (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M Q R hRQ ∘ₗ Submodules_fg_inclusion R✝ M P Q hPQ)) p =
    (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P R ⋯)) p
Tactic:
apply DFunLike.congr_fun
State after:
case h₁
R✝ : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R✝
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
inst✝¹ : AddCommGroup N
inst✝ : Module R✝ N
P Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p : ↥↑P ⊗[R✝] N
⊢ LinearMap.rTensor N (Submodules_fg_inclusion R✝ M Q R hRQ ∘ₗ Submodules_fg_inclusion R✝ M P Q hPQ) =
    LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P R ⋯)

State before:
case h₁
R✝ : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R✝
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
inst✝¹ : AddCommGroup N
inst✝ : Module R✝ N
P Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p : ↥↑P ⊗[R✝] N
⊢ LinearMap.rTensor N (Submodules_fg_inclusion R✝ M Q R hRQ ∘ₗ Submodules_fg_inclusion R✝ M P Q hPQ) =
    LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P R ⋯)
Tactic:
ext p n
State after:
case h₁.a.h.h
R✝ : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R✝
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
inst✝¹ : AddCommGroup N
inst✝ : Module R✝ N
P Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p✝ : ↥↑P ⊗[R✝] N
p : ↥↑P
n : N
⊢ ((AlgebraTensorModule.curry
          (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M Q R hRQ ∘ₗ Submodules_fg_inclusion R✝ M P Q hPQ)))
        p)
      n =
    ((AlgebraTensorModule.curry (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P R ⋯))) p) n

State before:
case h₁.a.h.h
R✝ : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R✝
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
inst✝¹ : AddCommGroup N
inst✝ : Module R✝ N
P Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p✝ : ↥↑P ⊗[R✝] N
p : ↥↑P
n : N
⊢ ((AlgebraTensorModule.curry
          (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M Q R hRQ ∘ₗ Submodules_fg_inclusion R✝ M P Q hPQ)))
        p)
      n =
    ((AlgebraTensorModule.curry (LinearMap.rTensor N (Submodules_fg_inclusion R✝ M P R ⋯))) p) n
Tactic:
simp
State after:
case h₁.a.h.h
R✝ : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R✝
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
inst✝¹ : AddCommGroup N
inst✝ : Module R✝ N
P Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p✝ : ↥↑P ⊗[R✝] N
p : ↥↑P
n : N
⊢ (Submodules_fg_inclusion R✝ M Q R hRQ) ((Submodules_fg_inclusion R✝ M P Q hPQ) p) ⊗ₜ[R✝] n =
    (Submodules_fg_inclusion R✝ M P R ⋯) p ⊗ₜ[R✝] n

State before:
case h₁.a.h.h
R✝ : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R✝
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
inst✝¹ : AddCommGroup N
inst✝ : Module R✝ N
P Q R : Submodules_fg R✝ M
hPQ : P ≤ Q
hRQ : Q ≤ R
p✝ : ↥↑P ⊗[R✝] N
p : ↥↑P
n : N
⊢ (Submodules_fg_inclusion R✝ M Q R hRQ) ((Submodules_fg_inclusion R✝ M P Q hPQ) p) ⊗ₜ[R✝] n =
    (Submodules_fg_inclusion R✝ M P R ⋯) p ⊗ₜ[R✝] n
Tactic:
rfl
State after:
no goals