case H
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
data : R × { x // x ∈ S }
⊢ Localization.mk data.fst data.snd • 0 = 0
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : Localization S
⊢ x • 0 = 0
induction' x using Localization.induction_on with data
case H.mk
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 }
⊢ Localization.mk (r, s).fst (r, s).snd • 0 = 0
case H
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
data : R × { x // x ∈ S }
⊢ Localization.mk data.fst data.snd • 0 = 0
rcases data with ⟨r, s⟩
no goals
case H.mk
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 }
⊢ Localization.mk (r, s).fst (r, s).snd • 0 = 0
rw [← zero_mk s, mk_smul_mk, smul_zero, zero_mk, zero_mk]