case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y z : LocalizedModule S M
mx : M
sx : { x // x ∈ S }
⊢ mk mx sx + y + z = mk mx sx + (y + z)
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : LocalizedModule S M
⊢ x + y + z = x + (y + z)
induction' x using LocalizedModule.induction_on with mx sx
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
mx : M
sx : { x // x ∈ S }
my : M
sy : { x // x ∈ S }
⊢ mk mx sx + mk my sy + z = mk mx sx + (mk my sy + z)
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y z : LocalizedModule S M
mx : M
sx : { x // x ∈ S }
⊢ mk mx sx + y + z = mk mx sx + (y + z)
induction' y using LocalizedModule.induction_on with my sy
case h.h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
mx : M
sx : { x // x ∈ S }
my : M
sy : { x // x ∈ S }
mz : M
sz : { x // x ∈ S }
⊢ mk mx sx + mk my sy + mk mz sz = mk mx sx + (mk my sy + mk mz sz)
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
mx : M
sx : { x // x ∈ S }
my : M
sy : { x // x ∈ S }
⊢ mk mx sx + mk my sy + z = mk mx sx + (mk my sy + z)
induction' z using LocalizedModule.induction_on with mz sz
case h.h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
mx : M
sx : { x // x ∈ S }
my : M
sy : { x // x ∈ S }
mz : M
sz : { x // x ∈ S }
⊢ mk (sz • sy • mx + sz • sx • my + (sx * sy) • mz) (sx * sy * sz) =
    mk ((sy * sz) • mx + (sx • sz • my + sx • sy • mz)) (sx * (sy * sz))
case h.h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
mx : M
sx : { x // x ∈ S }
my : M
sy : { x // x ∈ S }
mz : M
sz : { x // x ∈ S }
⊢ mk mx sx + mk my sy + mk mz sz = mk mx sx + (mk my sy + mk mz sz)
simp only [mk_add_mk, smul_add]
case h.h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
mx : M
sx : { x // x ∈ S }
my : M
sy : { x // x ∈ S }
mz : M
sz : { x // x ∈ S }
⊢ 1 • (sx * (sy * sz)) • (sz • sy • mx + sz • sx • my + (sx * sy) • mz) =
    1 • (sx * sy * sz) • ((sy * sz) • mx + (sx • sz • my + sx • sy • mz))
case h.h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
mx : M
sx : { x // x ∈ S }
my : M
sy : { x // x ∈ S }
mz : M
sz : { x // x ∈ S }
⊢ mk (sz • sy • mx + sz • sx • my + (sx * sy) • mz) (sx * sy * sz) =
    mk ((sy * sz) • mx + (sx • sz • my + sx • sy • mz)) (sx * (sy * sz))
refine' mk_eq.mpr ⟨1, _⟩
case h.h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
mx : M
sx : { x // x ∈ S }
my : M
sy : { x // x ∈ S }
mz : M
sz : { x // x ∈ S }
⊢ (sx * (sy * sz)) • (sz • sy • mx + sz • sx • my + (sx * sy) • mz) =
    (sx * sy * sz) • ((sy * sz) • mx + (sx • sz • my + sx • sy • mz))
case h.h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
mx : M
sx : { x // x ∈ S }
my : M
sy : { x // x ∈ S }
mz : M
sz : { x // x ∈ S }
⊢ 1 • (sx * (sy * sz)) • (sz • sy • mx + sz • sx • my + (sx * sy) • mz) =
    1 • (sx * sy * sz) • ((sy * sz) • mx + (sx • sz • my + sx • sy • mz))
rw [one_smul, one_smul]
case h.h.h.e_a
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
mx : M
sx : { x // x ∈ S }
my : M
sy : { x // x ∈ S }
mz : M
sz : { x // x ∈ S }
⊢ sx * (sy * sz) = sx * sy * sz

case h.h.h.e_a
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
mx : M
sx : { x // x ∈ S }
my : M
sy : { x // x ∈ S }
mz : M
sz : { x // x ∈ S }
⊢ sz • sy • mx + sz • sx • my + (sx * sy) • mz = (sy * sz) • mx + (sx • sz • my + sx • sy • mz)
case h.h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
mx : M
sx : { x // x ∈ S }
my : M
sy : { x // x ∈ S }
mz : M
sz : { x // x ∈ S }
⊢ (sx * (sy * sz)) • (sz • sy • mx + sz • sx • my + (sx * sy) • mz) =
    (sx * sy * sz) • ((sy * sz) • mx + (sx • sz • my + sx • sy • mz))
congr 1
no goals
case h.h.h.e_a
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
mx : M
sx : { x // x ∈ S }
my : M
sy : { x // x ∈ S }
mz : M
sz : { x // x ∈ S }
⊢ sx * (sy * sz) = sx * sy * sz
rw [mul_assoc]
no goals
case h.h.h.e_a
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
mx : M
sx : { x // x ∈ S }
my : M
sy : { x // x ∈ S }
mz : M
sz : { x // x ∈ S }
⊢ sz • sy • mx + sz • sx • my + (sx * sy) • mz = (sy * sz) • mx + (sx • sz • my + sx • sy • mz)
rw [eq_comm, mul_comm, add_assoc, mul_smul, mul_smul, ← mul_smul sx sz, mul_comm, mul_smul]