case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : { x // x ∈ S }
⊢ 1 • mk m s = mk m s
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : LocalizedModule S M
⊢ 1 • m = m
induction' m using LocalizedModule.induction_on with m s
no goals
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : { x // x ∈ S }
⊢ 1 • mk m s = mk m s
rw [← Localization.mk_one, mk_smul_mk, one_smul, one_mul]