-- Mathlib/RingTheory/OreLocalization/Ring.lean
theorem add_smul (y z : R[S⁻¹]) (x : X[S⁻¹]) :
    (y + z) • x = y • x + z • x

Proof state:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
⊢ (r₂ /ₒ s₂ + r₃ /ₒ s₃) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)

Tactic:
rcases oreDivAddChar' r₂ r₃ s₂ s₃ with ⟨ra, sa, ha, q⟩

Result:
case c.c.c.mk.mk.intro
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
q : r₂ /ₒ s₂ + r₃ /ₒ s₃ = (sa • r₂ + ra • r₃) /ₒ (sa * s₂)
⊢ (r₂ /ₒ s₂ + r₃ /ₒ s₃) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)

Proof state:
case c.c.c.mk.mk.intro
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (sa • r₂ /ₒ (sa * s₂)) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)

Tactic:
rcases oreDivSMulChar' (sa • r₂) r₁ (sa * s₂) s₁ with ⟨rb, sb, hb, q⟩

Result:
case c.c.c.mk.mk.intro.mk.mk.intro
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
q : (sa • r₂ /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂))
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (sa • r₂ /ₒ (sa * s₂)) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)

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

Tactic:
clear q

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

Proof state:
case c.c.c.mk.mk.intro
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
q : r₂ /ₒ s₂ + r₃ /ₒ s₃ = (sa • r₂ + ra • r₃) /ₒ (sa * s₂)
⊢ (r₂ /ₒ s₂ + r₃ /ₒ s₃) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)

Tactic:
rw [q]

Result:
case c.c.c.mk.mk.intro
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
q : r₂ /ₒ s₂ + r₃ /ₒ s₃ = (sa • r₂ + ra • r₃) /ₒ (sa * s₂)
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)

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

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

Result:
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk.intro
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * (↑sa * r₂) = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((↑sc * rb + rc) * ↑s₁ /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) = (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
y z : OreLocalization S R
x : OreLocalization S X
⊢ (y + z) • x = y • x + z • x

Tactic:
induction' x with r₁ s₁

Result:
case c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
y z : OreLocalization S R
r₁ : X
s₁ : ↥S
⊢ (y + z) • (r₁ /ₒ s₁) = y • (r₁ /ₒ s₁) + z • (r₁ /ₒ s₁)

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

Tactic:
rw [q]

Result:
case c.c.c.mk.mk.intro.mk.mk.intro
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
q : (sa • r₂ /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂))
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂)) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)

Proof state:
case c.c.c.mk.mk.intro
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
q : r₂ /ₒ s₂ + r₃ /ₒ s₃ = (sa • r₂ + ra • r₃) /ₒ (sa * s₂)
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)

Tactic:
clear q

Result:
case c.c.c.mk.mk.intro
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
⊢ ↑sb * (↑sa * ↑s₂) ∈ S

Tactic:
norm_cast

Result:
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
⊢ ↑(sb * (sa * s₂)) ∈ S