-- Mathlib/RingTheory/OreLocalization/Basic.lean
theorem add''_char (r₁ : X) (s₁ : S) (r₂ : X) (s₂ : S) (rb : R) (sb : R)
    (hb : sb * s₁ = rb * s₂) (h : sb * s₁ ∈ S) :
    add'' r₁ s₁ r₂ s₂ = (sb • r₁ + rb • r₂) /ₒ ⟨sb * s₁, h⟩

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ha : ↑(oreDenom (↑s₁) s₂) * ↑s₁ = oreNum (↑s₁) s₂ * ↑s₂
⊢ (oreDenom (↑s₁) s₂ • r₁ + oreNum (↑s₁) s₂ • r₂) /ₒ (oreDenom (↑s₁) s₂ * s₁) = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩

Tactic:
generalize oreNum (s₁ : R) s₂ = ra at *

Result:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
ha : ↑(oreDenom (↑s₁) s₂) * ↑s₁ = ra * ↑s₂
⊢ (oreDenom (↑s₁) s₂ • r₁ + ra • r₂) /ₒ (oreDenom (↑s₁) s₂ * s₁) = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩

Proof state:
case mk.mk
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
⊢ ∃ u v, u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑u * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)

Tactic:
rcases ore_right_cancel _ _ s₂ this with ⟨sd, hd⟩

Result:
case mk.mk.intro
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ ∃ u v, u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑u * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)

Proof state:
case h.right
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ ↑sd * ↑sc * (sb * ↑s₁) = ↑sd * rc * (↑sa * ↑s₁)

Tactic:
rw [mul_assoc, ← mul_assoc (sc : R), hc, mul_assoc, mul_assoc]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ ∃ v, (sd * sc) • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑(sd * sc) * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)

Tactic:
use sd * rc

Result:
case h
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ (sd * sc) • (sb • r₁ + rb • r₂) = (↑sd * rc) • (sa • r₁ + ra • r₂) ∧
    ↑(sd * sc) * ↑⟨sb * ↑s₁, h⟩ = ↑sd * rc * ↑(sa * s₁)

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
ha : ↑(oreDenom (↑s₁) s₂) * ↑s₁ = ra * ↑s₂
⊢ (oreDenom (↑s₁) s₂ • r₁ + ra • r₂) /ₒ (oreDenom (↑s₁) s₂ * s₁) = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩

Tactic:
generalize oreDenom (s₁ : R) s₂ = sa at *

Result:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
⊢ (sa • r₁ + ra • r₂) /ₒ (sa * s₁) = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
⊢ OreLocalization.add'' r₁ s₁ r₂ s₂ = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩

Tactic:
simp only [add'']

Result:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
⊢ (oreDenom (↑s₁) s₂ • r₁ + oreNum (↑s₁) s₂ • r₂) /ₒ (oreDenom (↑s₁) s₂ * s₁) = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
⊢ ↑sc * rb * ↑s₂ = rc * ra * ↑s₂

Tactic:
rw [mul_assoc rc, ← ha, ← mul_assoc, ← hc, mul_assoc, mul_assoc, hb]

Result:
no goals