English
A streamlined form of the previous result showing that a single step of equivalence suffices via simp lemmas.
Русский
Упрощённая форма предыдущего результата, показывающая достаточность одного шага через подобные леммы.
LaTeX
$$$\\text{eq_of_fg_of_subtype_eq'}\\text{ (simp) }$$$
Lean4
theorem eq_of_fg_of_subtype_eq' (h : rTensor N P.subtype t = rTensor N P'.subtype t') :
∃ (Q : Submodule R M) (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
Q.FG ∧ rTensor N (inclusion hPQ) t = rTensor N (inclusion hP'Q) t' :=
by
simp only [← subtype_comp_inclusion _ _ (le_sup_left : _ ≤ P ⊔ P'),
← subtype_comp_inclusion _ _ (le_sup_right : _ ≤ P ⊔ P'), rTensor_comp, coe_comp, Function.comp_apply] at h
let ⟨Q, hQ_le, hQ, h⟩ := TensorProduct.eq_of_fg_of_subtype_eq (hP.sup hP') h
use Q, le_trans le_sup_left hQ_le, le_trans le_sup_right hQ_le, hQ
simpa [← comp_apply, ← rTensor_comp] using h
