-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem mul_smul (x y : R[S⁻¹]) (z : X[S⁻¹]) : (x * y) • z = x • y • z

Proof state:
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk.huv
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑(sc * sa) * r₁ = rc * ↑(sb * s₂)

Tactic:
rw [Submonoid.coe_mul, Submonoid.coe_mul, ← mul_assoc, ← hc, mul_assoc _ ra, ← ha, mul_assoc]

Result:
no goals

Proof state:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
y : OreLocalization S R
z : OreLocalization S X
r₁ : R
s₁ : ↥S
⊢ (r₁ /ₒ s₁ * y) • z = (r₁ /ₒ s₁) • y • z

Tactic:
induction' y with r₂ s₂

Result:
case c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
z : OreLocalization S X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) • z = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • z

Proof state:
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑sc * (ra * r₂) = rc * rb * ↑s₃

Tactic:
rw [← mul_assoc _ ra, hc, mul_assoc, hb, ← mul_assoc]

Result:
no goals

Proof state:
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ (rc * rb) • r₃ /ₒ (sc * (sa * s₁)) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))

Tactic:
rw [← mul_assoc, mul_smul]

Result:
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ rc • rb • r₃ /ₒ (sc * sa * s₁) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))

Proof state:
case c.c.c.mk.mk.intro.mk.mk.intro
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))

Tactic:
rcases oreCondition ra sb with ⟨rc, sc, hc⟩

Result:
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
x y : OreLocalization S R
z : OreLocalization S X
⊢ (x * y) • z = x • y • z

Tactic:
induction' x with r₁ s₁

Result:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
y : OreLocalization S R
z : OreLocalization S X
r₁ : R
s₁ : ↥S
⊢ (r₁ /ₒ s₁ * y) • z = (r₁ /ₒ s₁) • y • z

Proof state:
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ rc • rb • r₃ /ₒ (sc * sa * s₁) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))

Tactic:
symm

Result:
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂)) = rc • rb • r₃ /ₒ (sc * sa * s₁)

Proof state:
case c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
z : OreLocalization S X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) • z = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • z

Tactic:
induction' z with r₃ s₃

Result:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
⊢ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)