R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
⊢ Quotient.mk (oreEqv R S) (r₂ * ↑(oreDenom (↑s₂) s₁) + r₁ * oreNum (↑s₂) s₁, s₂ * oreDenom (↑s₂) s₁) =
    Quotient.mk (oreEqv R S) (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂, s₁ * oreDenom (↑s₁) s₂)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
⊢ OreLocalization.add' r₁ s₁ (r₂ /ₒ s₂) = OreLocalization.add' r₂ s₂ (r₁ /ₒ s₁)
simp only [add', oreDiv, add'', Quotient.mk', Quotient.lift_mk]
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
⊢ (r₂ * ↑(oreDenom (↑s₂) s₁) + r₁ * oreNum (↑s₂) s₁, s₂ * oreDenom (↑s₂) s₁) ≈
    (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂, s₁ * oreDenom (↑s₁) s₂)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
⊢ Quotient.mk (oreEqv R S) (r₂ * ↑(oreDenom (↑s₂) s₁) + r₁ * oreNum (↑s₂) s₁, s₂ * oreDenom (↑s₂) s₁) =
    Quotient.mk (oreEqv R S) (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂, s₁ * oreDenom (↑s₁) s₂)
rw [Quotient.eq]
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
hb : ↑s₂ * ↑(oreDenom (↑s₂) s₁) = ↑s₁ * oreNum (↑s₂) s₁
⊢ (r₂ * ↑(oreDenom (↑s₂) s₁) + r₁ * oreNum (↑s₂) s₁, s₂ * oreDenom (↑s₂) s₁) ≈
    (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂, s₁ * oreDenom (↑s₁) s₂)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
⊢ (r₂ * ↑(oreDenom (↑s₂) s₁) + r₁ * oreNum (↑s₂) s₁, s₂ * oreDenom (↑s₂) s₁) ≈
    (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂, s₁ * oreDenom (↑s₁) s₂)
have hb := ore_eq (↑s₂) s₁
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
hb : ↑s₂ * ↑(oreDenom (↑s₂) s₁) = ↑s₁ * rb
⊢ (r₂ * ↑(oreDenom (↑s₂) s₁) + r₁ * rb, s₂ * oreDenom (↑s₂) s₁) ≈
    (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂, s₁ * oreDenom (↑s₁) s₂)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
hb : ↑s₂ * ↑(oreDenom (↑s₂) s₁) = ↑s₁ * oreNum (↑s₂) s₁
⊢ (r₂ * ↑(oreDenom (↑s₂) s₁) + r₁ * oreNum (↑s₂) s₁, s₂ * oreDenom (↑s₂) s₁) ≈
    (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂, s₁ * oreDenom (↑s₁) s₂)
set rb := oreNum (↑s₂) s₁
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
⊢ (r₂ * ↑sb + r₁ * rb, s₂ * sb) ≈ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂, s₁ * oreDenom (↑s₁) s₂)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
hb : ↑s₂ * ↑(oreDenom (↑s₂) s₁) = ↑s₁ * rb
⊢ (r₂ * ↑(oreDenom (↑s₂) s₁) + r₁ * rb, s₂ * oreDenom (↑s₂) s₁) ≈
    (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂, s₁ * oreDenom (↑s₁) s₂)
set sb := oreDenom (↑s₂) s₁
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
⊢ (r₂ * ↑sb + r₁ * rb, s₂ * sb) ≈ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂, s₁ * oreDenom (↑s₁) s₂)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
⊢ (r₂ * ↑sb + r₁ * rb, s₂ * sb) ≈ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂, s₁ * oreDenom (↑s₁) s₂)
have ha := ore_eq (↑s₁) s₂
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * ra
⊢ (r₂ * ↑sb + r₁ * rb, s₂ * sb) ≈ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * ra, s₁ * oreDenom (↑s₁) s₂)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
⊢ (r₂ * ↑sb + r₁ * rb, s₂ * sb) ≈ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂, s₁ * oreDenom (↑s₁) s₂)
set ra := oreNum (↑s₁) s₂
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
⊢ (r₂ * ↑sb + r₁ * rb, s₂ * sb) ≈ (r₁ * ↑sa + r₂ * ra, s₁ * sa)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * ra
⊢ (r₂ * ↑sb + r₁ * rb, s₂ * sb) ≈ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * ra, s₁ * oreDenom (↑s₁) s₂)
set sa := oreDenom (↑s₁) s₂
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
⊢ (r₂ * ↑sb + r₁ * rb, s₂ * sb) ≈ (r₁ * ↑sa + r₂ * ra, s₁ * sa)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
⊢ (r₂ * ↑sb + r₁ * rb, s₂ * sb) ≈ (r₁ * ↑sa + r₂ * ra, s₁ * sa)
rcases oreCondition ra sb with ⟨rc, sc, hc⟩
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
⊢ (r₂ * ↑sb + r₁ * rb, s₂ * sb) ≈ (r₁ * ↑sa + r₂ * ra, s₁ * sa)
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
⊢ (r₂ * ↑sb + r₁ * rb, s₂ * sb) ≈ (r₁ * ↑sa + r₂ * ra, s₁ * sa)
have : (s₁ : R) * (rb * rc) = s₁ * (sa * sc) := by
  rw [← mul_assoc, ← hb, mul_assoc, ← hc, ← mul_assoc, ← ha, mul_assoc]
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ (r₂ * ↑sb + r₁ * rb, s₂ * sb) ≈ (r₁ * ↑sa + r₂ * ra, s₁ * sa)
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
⊢ (r₂ * ↑sb + r₁ * rb, s₂ * sb) ≈ (r₁ * ↑sa + r₂ * ra, s₁ * sa)
rcases ore_left_cancel _ _ s₁ this with ⟨sd, hd⟩
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ ∃ v,
    (r₁ * ↑sa + r₂ * ra, s₁ * sa).fst * ↑(sc * sd) = (r₂ * ↑sb + r₁ * rb, s₂ * sb).fst * v ∧
      ↑(r₁ * ↑sa + r₂ * ra, s₁ * sa).snd * ↑(sc * sd) = ↑(r₂ * ↑sb + r₁ * rb, s₂ * sb).snd * v
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ (r₂ * ↑sb + r₁ * rb, s₂ * sb) ≈ (r₁ * ↑sa + r₂ * ra, s₁ * sa)
use sc * sd
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ (r₁ * ↑sa + r₂ * ra, s₁ * sa).fst * ↑(sc * sd) = (r₂ * ↑sb + r₁ * rb, s₂ * sb).fst * (rc * ↑sd) ∧
    ↑(r₁ * ↑sa + r₂ * ra, s₁ * sa).snd * ↑(sc * sd) = ↑(r₂ * ↑sb + r₁ * rb, s₂ * sb).snd * (rc * ↑sd)
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ ∃ v,
    (r₁ * ↑sa + r₂ * ra, s₁ * sa).fst * ↑(sc * sd) = (r₂ * ↑sb + r₁ * rb, s₂ * sb).fst * v ∧
      ↑(r₁ * ↑sa + r₂ * ra, s₁ * sa).snd * ↑(sc * sd) = ↑(r₂ * ↑sb + r₁ * rb, s₂ * sb).snd * v
use rc * sd
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂) * (↑sc * ↑sd) =
      (r₂ * ↑(oreDenom (↑s₂) s₁) + r₁ * oreNum (↑s₂) s₁) * (rc * ↑sd) ∧
    ↑s₁ * ↑(oreDenom (↑s₁) s₂) * (↑sc * ↑sd) = ↑s₂ * ↑(oreDenom (↑s₂) s₁) * (rc * ↑sd)
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ (r₁ * ↑sa + r₂ * ra, s₁ * sa).fst * ↑(sc * sd) = (r₂ * ↑sb + r₁ * rb, s₂ * sb).fst * (rc * ↑sd) ∧
    ↑(r₁ * ↑sa + r₂ * ra, s₁ * sa).snd * ↑(sc * sd) = ↑(r₂ * ↑sb + r₁ * rb, s₂ * sb).snd * (rc * ↑sd)
dsimp
case mk.mk.intro.left
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂) * (↑sc * ↑sd) =
    (r₂ * ↑(oreDenom (↑s₂) s₁) + r₁ * oreNum (↑s₂) s₁) * (rc * ↑sd)

case mk.mk.intro.right
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ ↑s₁ * ↑(oreDenom (↑s₁) s₂) * (↑sc * ↑sd) = ↑s₂ * ↑(oreDenom (↑s₂) s₁) * (rc * ↑sd)
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂) * (↑sc * ↑sd) =
      (r₂ * ↑(oreDenom (↑s₂) s₁) + r₁ * oreNum (↑s₂) s₁) * (rc * ↑sd) ∧
    ↑s₁ * ↑(oreDenom (↑s₁) s₂) * (↑sc * ↑sd) = ↑s₂ * ↑(oreDenom (↑s₂) s₁) * (rc * ↑sd)
constructor
no goals
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
⊢ ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
rw [← mul_assoc, ← hb, mul_assoc, ← hc, ← mul_assoc, ← ha, mul_assoc]
case mk.mk.intro.left
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ r₂ * (↑sb * rc * ↑sd) + r₁ * (rb * rc * ↑sd) =
    r₂ * ↑(oreDenom (↑s₂) s₁) * (rc * ↑sd) + r₁ * oreNum (↑s₂) s₁ * (rc * ↑sd)
case mk.mk.intro.left
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂) * (↑sc * ↑sd) =
    (r₂ * ↑(oreDenom (↑s₂) s₁) + r₁ * oreNum (↑s₂) s₁) * (rc * ↑sd)
rw [add_mul, add_mul, add_comm, mul_assoc (a := r₁) (b := (sa : R)),
  ← mul_assoc (a := (sa : R)), ← hd, mul_assoc (a := r₂) (b := ra),
  ← mul_assoc (a := ra) (b := (sc : R)), hc]
no goals
case mk.mk.intro.left
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ r₂ * (↑sb * rc * ↑sd) + r₁ * (rb * rc * ↑sd) =
    r₂ * ↑(oreDenom (↑s₂) s₁) * (rc * ↑sd) + r₁ * oreNum (↑s₂) s₁ * (rc * ↑sd)
simp only [mul_assoc]
case mk.mk.intro.right
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ ↑s₁ * (rb * rc * ↑sd) = ↑s₁ * rb * (rc * ↑sd)
case mk.mk.intro.right
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ ↑s₁ * ↑(oreDenom (↑s₁) s₂) * (↑sc * ↑sd) = ↑s₂ * ↑(oreDenom (↑s₂) s₁) * (rc * ↑sd)
rw [mul_assoc, ← mul_assoc (sa : R), ← hd, hb]
no goals
case mk.mk.intro.right
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : { x // x ∈ S }
rb : R := oreNum (↑s₂) s₁
sb : { x // x ∈ S } := oreDenom (↑s₂) s₁
hb : ↑s₂ * ↑sb = ↑s₁ * rb
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
ha : ↑s₁ * ↑sa = ↑s₂ * ra
rc : R
sc : { x // x ∈ S }
hc : ra * ↑sc = ↑sb * rc
this : ↑s₁ * (rb * rc) = ↑s₁ * (↑sa * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ↑sa * ↑sc * ↑sd
⊢ ↑s₁ * (rb * rc * ↑sd) = ↑s₁ * rb * (rc * ↑sd)
simp only [mul_assoc]