R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂) /ₒ (s₁ * oreDenom (↑s₁) s₂) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
⊢ OreLocalization.add'' r₁ s₁ r₂ s₂ = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
simp only [add'']
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂) /ₒ (s₁ * oreDenom (↑s₁) s₂) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂) /ₒ (s₁ * oreDenom (↑s₁) s₂) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
have ha := ore_eq (s₁ : R) s₂
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
h : ra = oreNum (↑s₁) s₂
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂) /ₒ (s₁ * oreDenom (↑s₁) s₂) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂) /ₒ (s₁ * oreDenom (↑s₁) s₂) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
set! ra := oreNum (s₁ : R) s₂ with h
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
h : ra = ra
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * ra) /ₒ (s₁ * oreDenom (↑s₁) s₂) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
h : ra = oreNum (↑s₁) s₂
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂) /ₒ (s₁ * oreDenom (↑s₁) s₂) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
rw [← h] at *
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * ra) /ₒ (s₁ * oreDenom (↑s₁) s₂) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
h : ra = ra
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * ra) /ₒ (s₁ * oreDenom (↑s₁) s₂) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
clear h
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
h : sa = oreDenom (↑s₁) s₂
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * ra) /ₒ (s₁ * oreDenom (↑s₁) s₂) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * ra) /ₒ (s₁ * oreDenom (↑s₁) s₂) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
set! sa := oreDenom (s₁ : R) s₂ with h
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
h : sa = sa
⊢ (r₁ * ↑sa + r₂ * ra) /ₒ (s₁ * sa) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
h : sa = oreDenom (↑s₁) s₂
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * ra) /ₒ (s₁ * oreDenom (↑s₁) s₂) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
rw [← h] at *
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
⊢ (r₁ * ↑sa + r₂ * ra) /ₒ (s₁ * sa) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
h : sa = sa
⊢ (r₁ * ↑sa + r₂ * ra) /ₒ (s₁ * sa) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
clear h
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
rc : R
sc : { x // x ∈ S }
hc : ↑sa * ↑sc = ↑sb * rc
⊢ (r₁ * ↑sa + r₂ * ra) /ₒ (s₁ * sa) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
⊢ (r₁ * ↑sa + r₂ * ra) /ₒ (s₁ * sa) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
rcases oreCondition (sa : R) sb with ⟨rc, sc, hc⟩
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
rc : R
sc : { x // x ∈ S }
hc : ↑sa * ↑sc = ↑sb * rc
this : ↑s₂ * (rb * rc) = ↑s₂ * (ra * ↑sc)
⊢ (r₁ * ↑sa + r₂ * ra) /ₒ (s₁ * sa) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
rc : R
sc : { x // x ∈ S }
hc : ↑sa * ↑sc = ↑sb * rc
⊢ (r₁ * ↑sa + r₂ * ra) /ₒ (s₁ * sa) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
have : (s₂ : R) * (rb * rc) = s₂ * (ra * sc) := by
  rw [← mul_assoc, ← hb, mul_assoc, ← hc, ← mul_assoc, ← mul_assoc, ha]
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
rc : R
sc : { x // x ∈ S }
hc : ↑sa * ↑sc = ↑sb * rc
this : ↑s₂ * (rb * rc) = ↑s₂ * (ra * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ra * ↑sc * ↑sd
⊢ (r₁ * ↑sa + r₂ * ra) /ₒ (s₁ * sa) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
rc : R
sc : { x // x ∈ S }
hc : ↑sa * ↑sc = ↑sb * rc
this : ↑s₂ * (rb * rc) = ↑s₂ * (ra * ↑sc)
⊢ (r₁ * ↑sa + r₂ * ra) /ₒ (s₁ * sa) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
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
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
rc : R
sc : { x // x ∈ S }
hc : ↑sa * ↑sc = ↑sb * rc
this : ↑s₂ * (rb * rc) = ↑s₂ * (ra * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ra * ↑sc * ↑sd
⊢ (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb) = (r₁ * ↑sa + r₂ * ra) /ₒ (s₁ * sa)
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
rc : R
sc : { x // x ∈ S }
hc : ↑sa * ↑sc = ↑sb * rc
this : ↑s₂ * (rb * rc) = ↑s₂ * (ra * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ra * ↑sc * ↑sd
⊢ (r₁ * ↑sa + r₂ * ra) /ₒ (s₁ * sa) = (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb)
symm
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
rc : R
sc : { x // x ∈ S }
hc : ↑sa * ↑sc = ↑sb * rc
this : ↑s₂ * (rb * rc) = ↑s₂ * (ra * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ra * ↑sc * ↑sd
⊢ ∃ u v, (r₁ * ↑sa + r₂ * ra) * ↑u = (r₁ * ↑sb + r₂ * rb) * v ∧ ↑(s₁ * sa) * ↑u = ↑(s₁ * sb) * v
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
rc : R
sc : { x // x ∈ S }
hc : ↑sa * ↑sc = ↑sb * rc
this : ↑s₂ * (rb * rc) = ↑s₂ * (ra * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ra * ↑sc * ↑sd
⊢ (r₁ * ↑sb + r₂ * rb) /ₒ (s₁ * sb) = (r₁ * ↑sa + r₂ * ra) /ₒ (s₁ * sa)
rw [oreDiv_eq_iff]
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
rc : R
sc : { x // x ∈ S }
hc : ↑sa * ↑sc = ↑sb * rc
this : ↑s₂ * (rb * rc) = ↑s₂ * (ra * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ra * ↑sc * ↑sd
⊢ ∃ v, (r₁ * ↑sa + r₂ * ra) * ↑(sc * sd) = (r₁ * ↑sb + r₂ * rb) * v ∧ ↑(s₁ * sa) * ↑(sc * sd) = ↑(s₁ * sb) * v
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
rc : R
sc : { x // x ∈ S }
hc : ↑sa * ↑sc = ↑sb * rc
this : ↑s₂ * (rb * rc) = ↑s₂ * (ra * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ra * ↑sc * ↑sd
⊢ ∃ u v, (r₁ * ↑sa + r₂ * ra) * ↑u = (r₁ * ↑sb + r₂ * rb) * v ∧ ↑(s₁ * sa) * ↑u = ↑(s₁ * sb) * v
use sc * sd
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
rc : R
sc : { x // x ∈ S }
hc : ↑sa * ↑sc = ↑sb * rc
this : ↑s₂ * (rb * rc) = ↑s₂ * (ra * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ra * ↑sc * ↑sd
⊢ (r₁ * ↑sa + r₂ * ra) * ↑(sc * sd) = (r₁ * ↑sb + r₂ * rb) * (rc * ↑sd) ∧
    ↑(s₁ * sa) * ↑(sc * sd) = ↑(s₁ * sb) * (rc * ↑sd)
case mk.mk.intro
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
rc : R
sc : { x // x ∈ S }
hc : ↑sa * ↑sc = ↑sb * rc
this : ↑s₂ * (rb * rc) = ↑s₂ * (ra * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ra * ↑sc * ↑sd
⊢ ∃ v, (r₁ * ↑sa + r₂ * ra) * ↑(sc * sd) = (r₁ * ↑sb + r₂ * rb) * v ∧ ↑(s₁ * sa) * ↑(sc * sd) = ↑(s₁ * sb) * v
use rc * sd
case mk.mk.intro.left
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
rb : R
sb : { x // x ∈ S }
hb : ↑s₁ * ↑sb = ↑s₂ * rb
ha : ↑s₁ * ↑(oreDenom (↑s₁) s₂) = ↑s₂ * oreNum (↑s₁) s₂
ra : R := oreNum (↑s₁) s₂
sa : { x // x ∈ S } := oreDenom (↑s₁) s₂
rc : R
sc : { x // x ∈ S }
hc : ↑sa * ↑sc = ↑sb * rc
this : ↑s₂ * (rb * rc) = ↑s₂ * (ra * ↑sc)
sd : { x // x ∈ S }
hd : rb * rc * ↑sd = ra * ↑sc * ↑sd
⊢ (r₁ * ↑(oreDenom (↑s₁) s₂) + r₂ * oreNum (↑s₁) s₂) * (↑sc * ↑sd) = (r₁ * ↑sb + r₂ * rb) * (rc * ↑sd)

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