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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t'
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
let P'' := P ⊔ 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 : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t'
P'' : Submodule R M := P ⊔ P'
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) 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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t'
P'' : Submodule R M := P ⊔ P'
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
let _hP_le := (le_sup_left : P ≤ 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 : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t'
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) 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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t'
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
let _hP'_le := (le_sup_right : P' ≤ 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 : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t'
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) 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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t'
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
rw [← Submodule.subtype_comp_inclusion _ _ _hP_le] 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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
h : (LinearMap.rTensor N ((P ⊔ P').subtype ∘ₗ Submodule.inclusion _hP_le)) t = (LinearMap.rTensor N P'.subtype) t'
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) 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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
h : (LinearMap.rTensor N ((P ⊔ P').subtype ∘ₗ Submodule.inclusion _hP_le)) t = (LinearMap.rTensor N P'.subtype) t'
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
rw [← Submodule.subtype_comp_inclusion _ _ _hP'_le] 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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h :
  (LinearMap.rTensor N ((P ⊔ P').subtype ∘ₗ Submodule.inclusion _hP_le)) t =
    (LinearMap.rTensor N ((P ⊔ P').subtype ∘ₗ Submodule.inclusion _hP'_le)) t'
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) 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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h :
  (LinearMap.rTensor N ((P ⊔ P').subtype ∘ₗ Submodule.inclusion _hP_le)) t =
    (LinearMap.rTensor N ((P ⊔ P').subtype ∘ₗ Submodule.inclusion _hP'_le)) t'
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
simp only [LinearMap.rTensor_comp, LinearMap.coe_comp, Function.comp_apply] 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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) 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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
let ⟨Q, hQ_le, hQ, h⟩ := TensorProduct.eq_of_fg_of_subtype_eq
  (Submodule.FG.sup hP hP') _ _ 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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h✝ :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) 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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h✝ :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
⊢ ∃ Q,
    ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
      Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
Tactic:
use Q, le_trans _hP_le hQ_le, le_trans _hP'_le hQ_le, hQ
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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h✝ :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
⊢ (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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h✝ :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (Submodule.inclusion hQ_le)) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
⊢ (LinearMap.rTensor N (Submodule.inclusion ⋯)) t = (LinearMap.rTensor N (Submodule.inclusion ⋯)) t'
Tactic:
simp only [← LinearMap.comp_apply, ← LinearMap.rTensor_comp, Submodule.subtype_comp_inclusion] at h
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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h✝ :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  (LinearMap.rTensor N (Submodule.inclusion hQ_le ∘ₗ Submodule.inclusion _hP_le)) t =
    (LinearMap.rTensor N (Submodule.inclusion hQ_le ∘ₗ Submodule.inclusion _hP'_le)) t'
⊢ (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 : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
P'' : Submodule R M := P ⊔ P'
_hP_le : P ≤ P ⊔ P' := le_sup_left
_hP'_le : P' ≤ P ⊔ P' := le_sup_right
h✝ :
  (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP_le)) t) =
    (LinearMap.rTensor N (P ⊔ P').subtype) ((LinearMap.rTensor N (Submodule.inclusion _hP'_le)) t')
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  (LinearMap.rTensor N (Submodule.inclusion hQ_le ∘ₗ Submodule.inclusion _hP_le)) t =
    (LinearMap.rTensor N (Submodule.inclusion hQ_le ∘ₗ Submodule.inclusion _hP'_le)) t'
⊢ (LinearMap.rTensor N (Submodule.inclusion ⋯)) t = (LinearMap.rTensor N (Submodule.inclusion ⋯)) t'
Tactic:
exact h
State after:
no goals