liftOn₂ — Mathlib

Lean4
/-- If `f : M → ℕ+ → M → ℕ+ → α` respects the equivalence on
localization, lift it to a function `DivisibleHull M → DivisibleHull M → α`. -/
def liftOn₂ {α : Type*} (x y : DivisibleHull M) (f : M → ℕ+ → M → ℕ+ → α)
    (h : ∀ (m n m' n' : M) (s t s' t' : ℕ+), mk m s = mk m' s' → mk n t = mk n' t' → f m s n t = f m' s' n' t') : α :=
  LocalizedModule.liftOn₂ x y (fun p q ↦ f p.1 (↑ⁿ.symm p.2) q.1 (↑ⁿ.symm q.2)) fun p q p' q' heq heq' ↦
    h p.1 q.1 p'.1 q'.1 (↑ⁿ.symm p.2) (↑ⁿ.symm q.2) (↑ⁿ.symm p'.2) (↑ⁿ.symm q'.2)
      (by
        obtain ⟨u, hu⟩ := heq
        exact mk_eq_mk.mpr ⟨↑ⁿ.symm u, hu⟩)
      (by
        obtain ⟨u, hu⟩ := heq'
        exact mk_eq_mk.mpr ⟨↑ⁿ.symm u, hu⟩)
Похожие утверждения