case H
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y : Localization S
m : LocalizedModule S M
data : R × { x // x ∈ S }
⊢ (Localization.mk data.fst data.snd * y) • m = Localization.mk data.fst data.snd • y • m
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : Localization S
m : LocalizedModule S M
⊢ (x * y) • m = x • y • m
induction' x using Localization.induction_on with data
case H.H
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : LocalizedModule S M
data data' : R × { x // x ∈ S }
⊢ (Localization.mk data.fst data.snd * Localization.mk data'.fst data'.snd) • m =
    Localization.mk data.fst data.snd • Localization.mk data'.fst data'.snd • m
case H
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y : Localization S
m : LocalizedModule S M
data : R × { x // x ∈ S }
⊢ (Localization.mk data.fst data.snd * y) • m = Localization.mk data.fst data.snd • y • m
induction' y using Localization.induction_on with data'
case H.H.mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : LocalizedModule S M
r : R
s : { x // x ∈ S }
r' : R
s' : { x // x ∈ S }
⊢ (Localization.mk (r, s).fst (r, s).snd * Localization.mk (r', s').fst (r', s').snd) • m =
    Localization.mk (r, s).fst (r, s).snd • Localization.mk (r', s').fst (r', s').snd • m
case H.H
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : LocalizedModule S M
data data' : R × { x // x ∈ S }
⊢ (Localization.mk data.fst data.snd * Localization.mk data'.fst data'.snd) • m =
    Localization.mk data.fst data.snd • Localization.mk data'.fst data'.snd • m
rcases data, data' with ⟨⟨r, s⟩, ⟨r', s'⟩⟩
case H.H.mk.mk.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
s : { x // x ∈ S }
r' : R
s' : { x // x ∈ S }
m : M
t : { x // x ∈ S }
⊢ (Localization.mk (r, s).fst (r, s).snd * Localization.mk (r', s').fst (r', s').snd) • mk m t =
    Localization.mk (r, s).fst (r, s).snd • Localization.mk (r', s').fst (r', s').snd • mk m t
case H.H.mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : LocalizedModule S M
r : R
s : { x // x ∈ S }
r' : R
s' : { x // x ∈ S }
⊢ (Localization.mk (r, s).fst (r, s).snd * Localization.mk (r', s').fst (r', s').snd) • m =
    Localization.mk (r, s).fst (r, s).snd • Localization.mk (r', s').fst (r', s').snd • m
induction' m using LocalizedModule.induction_on with m t
no goals
case H.H.mk.mk.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
s : { x // x ∈ S }
r' : R
s' : { x // x ∈ S }
m : M
t : { x // x ∈ S }
⊢ (Localization.mk (r, s).fst (r, s).snd * Localization.mk (r', s').fst (r', s').snd) • mk m t =
    Localization.mk (r, s).fst (r, s).snd • Localization.mk (r', s').fst (r', s').snd • mk m t
rw [Localization.mk_mul, mk_smul_mk, mk_smul_mk, mk_smul_mk, mul_smul, mul_assoc]