English
If rTensor on subtypes t and t' are equal, there exist a FG submodule Q containing P with hPQ and equality after inclusion on t and t'.
Русский
Если значения rTensor на подтипах совпадают, существует FG-подмодуль Q, содержащий P, с включениями, приводящими к равенству на t и t'.
LaTeX
$$$\\exists Q\\,(hPQ: P\\le Q)\\,(hP'Q: P'\\le Q)\\, (Q.FG)\\land rTensor N (inclusion hPQ) t = rTensor N (inclusion hP'Q) t'.$$$
Lean4
theorem eq_of_fg_of_subtype_eq {t' : P ⊗[R] N} (h : rTensor N P.subtype t = rTensor N P.subtype t') :
∃ (Q : Submodule R M) (hPQ : P ≤ Q), Q.FG ∧ rTensor N (inclusion hPQ) t = rTensor N (inclusion hPQ) t' := by
classical
simp only [← Submodule.FG.rTensor.directLimit_apply' R M N hP, EmbeddingLike.apply_eq_iff_eq] at h
obtain ⟨Q, hPQ, h⟩ := Module.DirectLimit.exists_eq_of_of_eq h
use Q.val, Subtype.coe_le_coe.mpr hPQ, Q.property
