-- 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
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
⊢ (sa • r₁ + ra • r₂) /ₒ (sa * s₁) = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩

Tactic:
rw [oreDiv_eq_iff]

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₂
⊢ ∃ u v, u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑u * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)

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)
⊢ (↑sd * ↑sc * sb) • r₁ + (↑sd * ↑sc * rb) • r₂ = (↑sd * rc * ↑sa) • r₁ + (↑sd * rc * ra) • r₂ ∧
    ↑sd * ↑sc * (sb * ↑s₁) = ↑sd * rc * (↑sa * ↑s₁)

Tactic:
constructor

Result:
case h.left
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₁ + (↑sd * ↑sc * rb) • r₂ = (↑sd * rc * ↑sa) • r₁ + (↑sd * rc * ra) • r₂

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₁)

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
⊢ (oreDenom (↑s₁) s₂ • r₁ + oreNum (↑s₁) s₂ • r₂) /ₒ (oreDenom (↑s₁) s₂ * s₁) = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩

Tactic:
have ha := ore_eq (s₁ : R) s₂

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
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⟩

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₂
⊢ ∃ u v, u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑u * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)

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

Result:
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
⊢ ∃ u v, u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑u * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)

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

Tactic:
use sd * sc

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)
⊢ ∃ v, (sd * sc) • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑(sd * sc) * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)

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
⊢ ∃ u v, u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧ ↑u * ↑⟨sb * ↑s₁, h⟩ = v * ↑(sa * s₁)

Tactic:
have : sc * rb * s₂ = rc * ra * s₂ := by
  rw [mul_assoc rc, ← ha, ← mul_assoc, ← hc, mul_assoc, mul_assoc, hb]

Result:
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₁)

Proof state:
case h.left
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₁ + (↑sd * ↑sc * rb) • r₂ = (↑sd * rc * ↑sa) • r₁ + (↑sd * rc * ra) • r₂

Tactic:
rw [mul_assoc _ _ rb, hd, mul_assoc, 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)
⊢ (sd * sc) • (sb • r₁ + rb • r₂) = (↑sd * rc) • (sa • r₁ + ra • r₂) ∧
    ↑(sd * sc) * ↑⟨sb * ↑s₁, h⟩ = ↑sd * rc * ↑(sa * s₁)

Tactic:
simp only [smul_add, smul_smul, Submonoid.smul_def, Submonoid.coe_mul]

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₁ + (↑sd * ↑sc * rb) • r₂ = (↑sd * rc * ↑sa) • r₁ + (↑sd * rc * ra) • r₂ ∧
    ↑sd * ↑sc * (sb * ↑s₁) = ↑sd * rc * (↑sa * ↑s₁)