Theorem: TensorProduct.eq_of_fg_of_subtype_eq (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 : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P.subtype) t'
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'
Tactic:
rw [← sub_eq_zero, ← map_sub, ← rTensor_fgEquiv_of R M N ⟨P,hP⟩,
  LinearEquiv.map_eq_zero_iff] at h
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 : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'

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 : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'
Tactic:
have := rTensor_fg_directedSystem R M N
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 : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'

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 : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'
Tactic:
have := Module.DirectLimit.of.zero_exact h
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 : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this✝ : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
this : ∃ j, ∃ (hij : ⟨P, hP⟩ ≤ j), (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ j hij)) (t - t') = 0
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'

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 : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this✝ : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
this : ∃ j, ∃ (hij : ⟨P, hP⟩ ≤ j), (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ j hij)) (t - t') = 0
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'
Tactic:
let ⟨Q, hPQ, h⟩ := this
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 : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h✝ :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this✝ : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
this : ∃ j, ∃ (hij : ⟨P, hP⟩ ≤ j), (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ j hij)) (t - t') = 0
Q : Submodules_fg R M
hPQ : ⟨P, hP⟩ ≤ Q
h : (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ Q hPQ)) (t - t') = 0
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'

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 : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h✝ :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this✝ : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
this : ∃ j, ∃ (hij : ⟨P, hP⟩ ≤ j), (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ j hij)) (t - t') = 0
Q : Submodules_fg R M
hPQ : ⟨P, hP⟩ ≤ Q
h : (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ Q hPQ)) (t - t') = 0
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'
Tactic:
use Q.val, Subtype.coe_le_coe.mpr hPQ, Q.property
State after:
case right
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 : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h✝ :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this✝ : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
this : ∃ j, ∃ (hij : ⟨P, hP⟩ ≤ j), (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ j hij)) (t - t') = 0
Q : Submodules_fg R M
hPQ : ⟨P, hP⟩ ≤ Q
h : (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ Q hPQ)) (t - t') = 0
⊢ (LinearMap.rTensor N (Submodule.inclusion ⋯)) t = (LinearMap.rTensor N (Submodule.inclusion ⋯)) t'

State before:
case right
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 : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h✝ :
  (Module.DirectLimit.of R (Submodules_fg R M) (fun P => ↥↑P ⊗[R] N)
        (fun P Q hPQ => LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ)) ⟨P, hP⟩)
      (t - t') =
    0
this✝ : DirectedSystem (fun P => ↥↑P ⊗[R] N) fun P Q hPQ => ⇑(LinearMap.rTensor N (Submodules_fg_inclusion R M P Q hPQ))
this : ∃ j, ∃ (hij : ⟨P, hP⟩ ≤ j), (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ j hij)) (t - t') = 0
Q : Submodules_fg R M
hPQ : ⟨P, hP⟩ ≤ Q
h : (LinearMap.rTensor N (Submodules_fg_inclusion R M ⟨P, hP⟩ Q hPQ)) (t - t') = 0
⊢ (LinearMap.rTensor N (Submodule.inclusion ⋯)) t = (LinearMap.rTensor N (Submodule.inclusion ⋯)) t'
Tactic:
simpa only [sub_eq_zero, map_sub] using h
State after:
no goals