∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] {C : Sort u_3} (P : X → ↥S → X → ↥S → C)
  (hP :
    ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
      P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩)
  (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S),
  (fun r₁ s₁ => OreLocalization.liftExpand (P r₁ s₁) ⋯) r₁ s₁ =
    (fun r₁ s₁ => OreLocalization.liftExpand (P r₁ s₁) ⋯) (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩