-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem add_assoc' (x y z : LocalizedModule S M) : x + y + z = x + (y + z)

Proof state:
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 : ↥S
my : M
sy : ↥S
⊢ mk mx sx + mk my sy + z = mk mx sx + (mk my sy + z)

Tactic:
induction' z with mz sz

Result:
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 : ↥S
my : M
sy : ↥S
mz : M
sz : ↥S
⊢ mk mx sx + mk my sy + mk mz sz = mk mx sx + (mk my sy + mk mz sz)

Proof state:
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 : ↥S
my : M
sy : ↥S
mz : M
sz : ↥S
⊢ sz • sy • mx + sz • sx • my + (sx * sy) • mz = (sy * sz) • mx + (sx • sz • my + sx • sy • mz)

Tactic:
rw [eq_comm, mul_comm, add_assoc, mul_smul, mul_smul, ← mul_smul sx sz, mul_comm, mul_smul]

Result:
no goals

Proof state:
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 : ↥S
my : M
sy : ↥S
mz : M
sz : ↥S
⊢ mk mx sx + mk my sy + mk mz sz = mk mx sx + (mk my sy + mk mz sz)

Tactic:
simp only [mk_add_mk, smul_add]

Result:
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 : ↥S
my : M
sy : ↥S
mz : M
sz : ↥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))

Proof state:
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)

Tactic:
induction' x with mx sx

Result:
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 : ↥S
⊢ mk mx sx + y + z = mk mx sx + (y + z)

Proof state:
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 : ↥S
my : M
sy : ↥S
mz : M
sz : ↥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))

Tactic:
refine mk_eq.mpr ⟨1, ?_⟩

Result:
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 : ↥S
my : M
sy : ↥S
mz : M
sz : ↥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))

Proof state:
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 : ↥S
my : M
sy : ↥S
mz : M
sz : ↥S
⊢ sx * (sy * sz) = sx * sy * sz

Tactic:
rw [mul_assoc]

Result:
no goals

Proof state:
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 : ↥S
⊢ mk mx sx + y + z = mk mx sx + (y + z)

Tactic:
induction' y with my sy

Result:
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 : ↥S
my : M
sy : ↥S
⊢ mk mx sx + mk my sy + z = mk mx sx + (mk my sy + z)

Proof state:
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 : ↥S
my : M
sy : ↥S
mz : M
sz : ↥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))

Tactic:
congr 1

Result:
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 : ↥S
my : M
sy : ↥S
mz : M
sz : ↥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 : ↥S
my : M
sy : ↥S
mz : M
sz : ↥S
⊢ sz • sy • mx + sz • sx • my + (sx * sy) • mz = (sy * sz) • mx + (sx • sz • my + sx • sy • mz)

Proof state:
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 : ↥S
my : M
sy : ↥S
mz : M
sz : ↥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))

Tactic:
rw [one_smul, one_smul]

Result:
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 : ↥S
my : M
sy : ↥S
mz : M
sz : ↥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))