English
There is an instance IsLocalizedModule S2 (liftOfLE S1 S2 h f1 f2) with map_units = map_units f2, surj and exists_of_eq specified by mk'_surjective and related lemmas.
Русский
Существует инстанс IsLocalizedModule S2 для liftOfLE, с map_units = map_units f2, условий сюръективности и существования, задаваемых mk'_surjective и связанными леммами.
LaTeX
$$$$ \\text{IsLocalizedModule } S_2 (\\text{liftOfLE } S_1 S_2 h f_1 f_2) $$$$
Lean4
instance : IsLocalizedModule S₂ (liftOfLE S₁ S₂ h f₁ f₂)
where
map_units := map_units f₂
surj
y := by
obtain ⟨⟨y', s⟩, e⟩ := IsLocalizedModule.surj S₂ f₂ y
exact ⟨⟨f₁ y', s⟩, by simpa⟩
exists_of_eq := by
intro x₁ x₂ e
obtain ⟨x₁, s₁, rfl⟩ := mk'_surjective S₁ f₁ x₁
obtain ⟨x₂, s₂, rfl⟩ := mk'_surjective S₁ f₁ x₂
simp only [Function.uncurry, liftOfLE_mk', mk'_eq_mk'_iff, Submonoid.smul_def, ← mk'_smul] at e ⊢
obtain ⟨c, e⟩ := e
exact ⟨c, 1, by simpa [← smul_comm c.1]⟩
