M : Type u_2
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type ?u.138727
inst✝³ : CommMonoid N
P : Type ?u.138733
inst✝² : CommMonoid P
R : Type u_1
R₁ : Type ?u.138742
R₂ : Type ?u.138745
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : { x // x ∈ S }
⊢ liftOn (mk a b) (fun a b => mk (SMul.smul c a) b)
      (_ :
        ∀ {a c_1 : M} {b d : { x // x ∈ S }},
          ↑(r S) (a, b) (c_1, d) → (fun a b => mk (SMul.smul c a) b) a b = (fun a b => mk (SMul.smul c a) b) c_1 d) =
    mk (SMul.smul c a) b
M : Type u_2
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type ?u.138727
inst✝³ : CommMonoid N
P : Type ?u.138733
inst✝² : CommMonoid P
R : Type u_1
R₁ : Type ?u.138742
R₂ : Type ?u.138745
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : { x // x ∈ S }
⊢ c • mk a b = mk (c • a) b
simp only [HSMul.hSMul, instHSMul, SMul.smul, instSMulLocalization, Localization.smul]
M : Type u_2
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type ?u.138727
inst✝³ : CommMonoid N
P : Type ?u.138733
inst✝² : CommMonoid P
R : Type u_1
R₁ : Type ?u.138742
R₂ : Type ?u.138745
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : { x // x ∈ S }
⊢ liftOn (mk a b) (fun a b => mk (c • a) b)
      (_ :
        ∀ {a c_1 : M} {b d : { x // x ∈ S }},
          ↑(r S) (a, b) (c_1, d) → (fun a b => mk (SMul.smul c a) b) a b = (fun a b => mk (SMul.smul c a) b) c_1 d) =
    mk (SMul.smul c a) b
M : Type u_2
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type ?u.138727
inst✝³ : CommMonoid N
P : Type ?u.138733
inst✝² : CommMonoid P
R : Type u_1
R₁ : Type ?u.138742
R₂ : Type ?u.138745
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : { x // x ∈ S }
⊢ liftOn (mk a b) (fun a b => mk (SMul.smul c a) b)
      (_ :
        ∀ {a c_1 : M} {b d : { x // x ∈ S }},
          ↑(r S) (a, b) (c_1, d) → (fun a b => mk (SMul.smul c a) b) a b = (fun a b => mk (SMul.smul c a) b) c_1 d) =
    mk (SMul.smul c a) b
show liftOn (mk a b) (fun a b => mk (c • a) b) _ = _
no goals
M : Type u_2
inst✝⁴ : CommMonoid M
S : Submonoid M
N : Type ?u.138727
inst✝³ : CommMonoid N
P : Type ?u.138733
inst✝² : CommMonoid P
R : Type u_1
R₁ : Type ?u.138742
R₂ : Type ?u.138745
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : { x // x ∈ S }
⊢ liftOn (mk a b) (fun a b => mk (c • a) b)
      (_ :
        ∀ {a c_1 : M} {b d : { x // x ∈ S }},
          ↑(r S) (a, b) (c_1, d) → (fun a b => mk (SMul.smul c a) b) a b = (fun a b => mk (SMul.smul c a) b) c_1 d) =
    mk (SMul.smul c a) b
exact liftOn_mk (fun a b => mk (c • a) b) _ a b