case H
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y : Localization S
z : LocalizedModule S M
datax : R × { x // x ∈ S }
⊢ (Localization.mk datax.fst datax.snd + y) • z = Localization.mk datax.fst datax.snd • z + y • z
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : Localization S
z : LocalizedModule S M
⊢ (x + y) • z = x • z + y • z
induction' x using Localization.induction_on with datax
case H.H
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
z : LocalizedModule S M
datax datay : R × { x // x ∈ S }
⊢ (Localization.mk datax.fst datax.snd + Localization.mk datay.fst datay.snd) • z =
    Localization.mk datax.fst datax.snd • z + Localization.mk datay.fst datay.snd • z
case H
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y : Localization S
z : LocalizedModule S M
datax : R × { x // x ∈ S }
⊢ (Localization.mk datax.fst datax.snd + y) • z = Localization.mk datax.fst datax.snd • z + y • z
induction' y using Localization.induction_on with datay
case H.H.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
datax datay : R × { x // x ∈ S }
m : M
t : { x // x ∈ S }
⊢ (Localization.mk datax.fst datax.snd + Localization.mk datay.fst datay.snd) • mk m t =
    Localization.mk datax.fst datax.snd • mk m t + Localization.mk datay.fst datay.snd • mk m t
case H.H
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
z : LocalizedModule S M
datax datay : R × { x // x ∈ S }
⊢ (Localization.mk datax.fst datax.snd + Localization.mk datay.fst datay.snd) • z =
    Localization.mk datax.fst datax.snd • z + Localization.mk datay.fst datay.snd • z
induction' z using LocalizedModule.induction_on with m t
case H.H.h.mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
t : { x // x ∈ S }
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) • mk m t =
    Localization.mk (r, s).fst (r, s).snd • mk m t + Localization.mk (r', s').fst (r', s').snd • mk m t
case H.H.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
datax datay : R × { x // x ∈ S }
m : M
t : { x // x ∈ S }
⊢ (Localization.mk datax.fst datax.snd + Localization.mk datay.fst datay.snd) • mk m t =
    Localization.mk datax.fst datax.snd • mk m t + Localization.mk datay.fst datay.snd • mk m t
rcases datax, datay with ⟨⟨r, s⟩, ⟨r', s'⟩⟩
case H.H.h.mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
t : { x // x ∈ S }
r : R
s : { x // x ∈ S }
r' : R
s' : { x // x ∈ S }
⊢ ∃ u,
    u • ((r, s).snd * t * ((r', s').snd * t)) • (↑(r, s).snd * (r', s').fst + ↑(r', s').snd * (r, s).fst) • m =
      u • ((r, s).snd * (r', s').snd * t) • (((r', s').snd * t) • (r, s).fst • m + ((r, s).snd * t) • (r', s').fst • m)
case H.H.h.mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
t : { x // x ∈ S }
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) • mk m t =
    Localization.mk (r, s).fst (r, s).snd • mk m t + Localization.mk (r', s').fst (r', s').snd • mk m t
rw [Localization.add_mk, mk_smul_mk, mk_smul_mk, mk_smul_mk, mk_add_mk, mk_eq]
case H.H.h.mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
t : { x // x ∈ S }
r : R
s : { x // x ∈ S }
r' : R
s' : { x // x ∈ S }
⊢ 1 • ((r, s).snd * t * ((r', s').snd * t)) • (↑(r, s).snd * (r', s').fst + ↑(r', s').snd * (r, s).fst) • m =
    1 • ((r, s).snd * (r', s').snd * t) • (((r', s').snd * t) • (r, s).fst • m + ((r, s).snd * t) • (r', s').fst • m)
case H.H.h.mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
t : { x // x ∈ S }
r : R
s : { x // x ∈ S }
r' : R
s' : { x // x ∈ S }
⊢ ∃ u,
    u • ((r, s).snd * t * ((r', s').snd * t)) • (↑(r, s).snd * (r', s').fst + ↑(r', s').snd * (r, s).fst) • m =
      u • ((r, s).snd * (r', s').snd * t) • (((r', s').snd * t) • (r, s).fst • m + ((r, s).snd * t) • (r', s').fst • m)
use 1
case H.H.h.mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
t : { x // x ∈ S }
r : R
s : { x // x ∈ S }
r' : R
s' : { x // x ∈ S }
⊢ (↑s * ↑t * (↑s' * ↑t) * (↑s * r')) • m + (↑s * ↑t * (↑s' * ↑t) * (↑s' * r)) • m =
    (↑s * ↑s' * ↑t * (↑s' * ↑t * r)) • m + (↑s * ↑s' * ↑t * (↑s * ↑t * r')) • m
case H.H.h.mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
t : { x // x ∈ S }
r : R
s : { x // x ∈ S }
r' : R
s' : { x // x ∈ S }
⊢ 1 • ((r, s).snd * t * ((r', s').snd * t)) • (↑(r, s).snd * (r', s').fst + ↑(r', s').snd * (r, s).fst) • m =
    1 • ((r, s).snd * (r', s').snd * t) • (((r', s').snd * t) • (r, s).fst • m + ((r, s).snd * t) • (r', s').fst • m)
simp only [one_smul, add_smul, smul_add, ← mul_smul, Submonoid.smul_def, Submonoid.coe_mul,
  Submonoid.coe_one]
case H.H.h.mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
t : { x // x ∈ S }
r : R
s : { x // x ∈ S }
r' : R
s' : { x // x ∈ S }
⊢ (↑s * ↑t * (↑s' * ↑t) * (↑s' * r)) • m + (↑s * ↑t * (↑s' * ↑t) * (↑s * r')) • m =
    (↑s * ↑s' * ↑t * (↑s' * ↑t * r)) • m + (↑s * ↑s' * ↑t * (↑s * ↑t * r')) • m
case H.H.h.mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
t : { x // x ∈ S }
r : R
s : { x // x ∈ S }
r' : R
s' : { x // x ∈ S }
⊢ (↑s * ↑t * (↑s' * ↑t) * (↑s * r')) • m + (↑s * ↑t * (↑s' * ↑t) * (↑s' * r)) • m =
    (↑s * ↑s' * ↑t * (↑s' * ↑t * r)) • m + (↑s * ↑s' * ↑t * (↑s * ↑t * r')) • m
rw [add_comm]
no goals
case H.H.h.mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
t : { x // x ∈ S }
r : R
s : { x // x ∈ S }
r' : R
s' : { x // x ∈ S }
⊢ (↑s * ↑t * (↑s' * ↑t) * (↑s' * r)) • m + (↑s * ↑t * (↑s' * ↑t) * (↑s * r')) • m =
    (↑s * ↑s' * ↑t * (↑s' * ↑t * r)) • m + (↑s * ↑s' * ↑t * (↑s * ↑t * r')) • m
ring_nf