R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
m : M
s t : { x // x ∈ S }
⊢ Localization.liftOn (Localization.mk r s)
      (fun r s =>
        liftOn (mk m t) (fun p => mk (SMul.smul r p.fst) (s * p.snd))
          (_ :
            ∀ (p p' : M × { x // x ∈ S }),
              p ≈ p' → (fun p => mk (r • p.fst) (s * p.snd)) p = (fun p => mk (r • p.fst) (s * p.snd)) p'))
      (_ :
        ∀ {a c : R} {b d : { x // x ∈ S }},
          ↑(Localization.r S) (a, b) (c, d) →
            (fun r s =>
                  liftOn (mk m t) (fun p => mk (r • p.fst) (s * p.snd))
                    (_ :
                      ∀ (p p' : M × { x // x ∈ S }),
                        p ≈ p' → (fun p => mk (r • p.fst) (s * p.snd)) p = (fun p => mk (r • p.fst) (s * p.snd)) p'))
                a b =
              (fun r s =>
                  liftOn (mk m t) (fun p => mk (r • p.fst) (s * p.snd))
                    (_ :
                      ∀ (p p' : M × { x // x ∈ S }),
                        p ≈ p' → (fun p => mk (r • p.fst) (s * p.snd)) p = (fun p => mk (r • p.fst) (s * p.snd)) p'))
                c d) =
    mk (SMul.smul r m) (s * t)
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
m : M
s t : { x // x ∈ S }
⊢ Localization.mk r s • mk m t = mk (r • m) (s * t)
dsimp only [HSMul.hSMul, SMul.smul]
no goals
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
m : M
s t : { x // x ∈ S }
⊢ Localization.liftOn (Localization.mk r s)
      (fun r s =>
        liftOn (mk m t) (fun p => mk (SMul.smul r p.fst) (s * p.snd))
          (_ :
            ∀ (p p' : M × { x // x ∈ S }),
              p ≈ p' → (fun p => mk (r • p.fst) (s * p.snd)) p = (fun p => mk (r • p.fst) (s * p.snd)) p'))
      (_ :
        ∀ {a c : R} {b d : { x // x ∈ S }},
          ↑(Localization.r S) (a, b) (c, d) →
            (fun r s =>
                  liftOn (mk m t) (fun p => mk (r • p.fst) (s * p.snd))
                    (_ :
                      ∀ (p p' : M × { x // x ∈ S }),
                        p ≈ p' → (fun p => mk (r • p.fst) (s * p.snd)) p = (fun p => mk (r • p.fst) (s * p.snd)) p'))
                a b =
              (fun r s =>
                  liftOn (mk m t) (fun p => mk (r • p.fst) (s * p.snd))
                    (_ :
                      ∀ (p p' : M × { x // x ∈ S }),
                        p ≈ p' → (fun p => mk (r • p.fst) (s * p.snd)) p = (fun p => mk (r • p.fst) (s * p.snd)) p'))
                c d) =
    mk (SMul.smul r m) (s * t)
rw [Localization.liftOn_mk, liftOn_mk]