case c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
y z : OreLocalization R S
r₁ : R
s₁ : { x // x ∈ S }
⊢ r₁ /ₒ s₁ * (y + z) = r₁ /ₒ s₁ * y + r₁ /ₒ s₁ * z
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
x y z : OreLocalization R S
⊢ x * (y + z) = x * y + x * z
induction' x using OreLocalization.ind with r₁ s₁
case c.c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
z : OreLocalization R S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂ + z) = r₁ /ₒ s₁ * (r₂ /ₒ s₂) + r₁ /ₒ s₁ * z
case c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
y z : OreLocalization R S
r₁ : R
s₁ : { x // x ∈ S }
⊢ r₁ /ₒ s₁ * (y + z) = r₁ /ₒ s₁ * y + r₁ /ₒ s₁ * z
induction' y using OreLocalization.ind with r₂ s₂
case c.c.c
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 }
r₃ : R
s₃ : { x // x ∈ S }
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂ + r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ /ₒ s₂) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
case c.c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
z : OreLocalization R S
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂ + z) = r₁ /ₒ s₁ * (r₂ /ₒ s₂) + r₁ /ₒ s₁ * z
induction' z using OreLocalization.ind with r₃ s₃
case c.c.c.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
q : r₂ /ₒ s₂ + r₃ /ₒ s₃ = (r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂ + r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ /ₒ s₂) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
case c.c.c
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 }
r₃ : R
s₃ : { x // x ∈ S }
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂ + r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ /ₒ s₂) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
rcases oreDivAddChar' r₂ r₃ s₂ s₃ with ⟨ra, sa, ha, q⟩
case c.c.c.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
q : r₂ /ₒ s₂ + r₃ /ₒ s₃ = (r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ /ₒ s₁ * (r₂ /ₒ s₂) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
case c.c.c.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
q : r₂ /ₒ s₂ + r₃ /ₒ s₃ = (r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂ + r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ /ₒ s₂) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
rw [q]
case c.c.c.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ /ₒ s₁ * (r₂ /ₒ s₂) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
case c.c.c.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
q : r₂ /ₒ s₂ + r₃ /ₒ s₃ = (r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ /ₒ s₁ * (r₂ /ₒ s₂) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
clear q
case c.c.c.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ /ₒ s₁ * (r₂ * ↑sa /ₒ (s₂ * sa)) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
case c.c.c.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ /ₒ s₁ * (r₂ /ₒ s₂) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
rw [OreLocalization.expand' r₂ s₂ sa]
case c.c.c.mk.mk.intro.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
q : r₁ /ₒ s₁ * (r₂ * ↑sa /ₒ (s₂ * sa)) = r₁ * rb /ₒ (s₂ * sa * sb)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ /ₒ s₁ * (r₂ * ↑sa /ₒ (s₂ * sa)) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
case c.c.c.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ /ₒ s₁ * (r₂ * ↑sa /ₒ (s₂ * sa)) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
rcases oreDivMulChar' r₁ (r₂ * sa) s₁ (s₂ * sa) with ⟨rb, sb, hb, q⟩
case c.c.c.mk.mk.intro.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
q : r₁ /ₒ s₁ * (r₂ * ↑sa /ₒ (s₂ * sa)) = r₁ * rb /ₒ (s₂ * sa * sb)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ * rb /ₒ (s₂ * sa * sb) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
case c.c.c.mk.mk.intro.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
q : r₁ /ₒ s₁ * (r₂ * ↑sa /ₒ (s₂ * sa)) = r₁ * rb /ₒ (s₂ * sa * sb)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ /ₒ s₁ * (r₂ * ↑sa /ₒ (s₂ * sa)) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
rw [q]
case c.c.c.mk.mk.intro.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ * rb /ₒ (s₂ * sa * sb) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
case c.c.c.mk.mk.intro.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
q : r₁ /ₒ s₁ * (r₂ * ↑sa /ₒ (s₂ * sa)) = r₁ * rb /ₒ (s₂ * sa * sb)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ * rb /ₒ (s₂ * sa * sb) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
clear q
case c.c.c.mk.mk.intro.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ * rb /ₒ (s₂ * sa * sb) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
case c.c.c.mk.mk.intro.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ * rb /ₒ (s₂ * sa * sb) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
have hs₃rasb : ↑s₃ * (ra * sb) ∈ S := by
  rw [← mul_assoc, ← ha]
  norm_cast
  apply SetLike.coe_mem
case c.c.c.mk.mk.intro.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) =
    r₁ * rb /ₒ (s₂ * sa * sb) + r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ { val := ↑s₃ * (ra * ↑sb), property := hs₃rasb })
case c.c.c.mk.mk.intro.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ * rb /ₒ (s₂ * sa * sb) + r₁ /ₒ s₁ * (r₃ /ₒ s₃)
rw [OreLocalization.expand _ _ _ hs₃rasb]
case c.c.c.mk.mk.intro.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) =
    r₁ * rb /ₒ (s₂ * sa * sb) + r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ { val := ↑s₃ * (ra * ↑sb), property := hs₃rasb })
case c.c.c.mk.mk.intro.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) =
    r₁ * rb /ₒ (s₂ * sa * sb) + r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ { val := ↑s₃ * (ra * ↑sb), property := hs₃rasb })
have ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * sb) := by simp [ha, ← mul_assoc]
case c.c.c.mk.mk.intro.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) =
    r₁ * rb /ₒ (s₂ * sa * sb) + r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb))
case c.c.c.mk.mk.intro.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) =
    r₁ * rb /ₒ (s₂ * sa * sb) + r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ { val := ↑s₃ * (ra * ↑sb), property := hs₃rasb })
rw [← Subtype.coe_eq_of_eq_mk ha']
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
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
rc : R
sc : { x // x ∈ S }
hc : r₃ * (ra * ↑sb) * ↑sc = ↑s₁ * rc
hc' : r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb)) = r₁ * rc /ₒ (s₂ * sa * sb * sc)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) =
    r₁ * rb /ₒ (s₂ * sa * sb) + r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb))
case c.c.c.mk.mk.intro.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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) =
    r₁ * rb /ₒ (s₂ * sa * sb) + r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb))
rcases oreDivMulChar' r₁ (r₃ * (ra * sb)) s₁ (s₂ * sa * sb) with ⟨rc, sc, hc, hc'⟩
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
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
rc : R
sc : { x // x ∈ S }
hc : r₃ * (ra * ↑sb) * ↑sc = ↑s₁ * rc
hc' : r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb)) = r₁ * rc /ₒ (s₂ * sa * sb * sc)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ * rb /ₒ (s₂ * sa * sb) + r₁ * rc /ₒ (s₂ * sa * sb * sc)
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
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
rc : R
sc : { x // x ∈ S }
hc : r₃ * (ra * ↑sb) * ↑sc = ↑s₁ * rc
hc' : r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb)) = r₁ * rc /ₒ (s₂ * sa * sb * sc)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) =
    r₁ * rb /ₒ (s₂ * sa * sb) + r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb))
rw [hc']
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
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
rc : R
sc : { x // x ∈ S }
hc : r₃ * (ra * ↑sb) * ↑sc = ↑s₁ * rc
hc' : r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb)) = r₁ * rc /ₒ (s₂ * sa * sb * sc)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = (r₁ * rb * ↑sc + r₁ * rc * 1) /ₒ (s₂ * sa * sb * sc)
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
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
rc : R
sc : { x // x ∈ S }
hc : r₃ * (ra * ↑sb) * ↑sc = ↑s₁ * rc
hc' : r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb)) = r₁ * rc /ₒ (s₂ * sa * sb * sc)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = r₁ * rb /ₒ (s₂ * sa * sb) + r₁ * rc /ₒ (s₂ * sa * sb * sc)
rw [oreDiv_add_char (s₂ * sa * sb) (s₂ * sa * sb * sc) 1 sc (by simp)]
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
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
rc : R
sc : { x // x ∈ S }
hc : r₃ * (ra * ↑sb) * ↑sc = ↑s₁ * rc
hc' : r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb)) = r₁ * rc /ₒ (s₂ * sa * sb * sc)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) * ↑(sb * sc) /ₒ (s₂ * sa * (sb * sc))) =
    (r₁ * rb * ↑sc + r₁ * rc * 1) /ₒ (s₂ * sa * sb * sc)
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
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
rc : R
sc : { x // x ∈ S }
hc : r₃ * (ra * ↑sb) * ↑sc = ↑s₁ * rc
hc' : r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb)) = r₁ * rc /ₒ (s₂ * sa * sb * sc)
⊢ r₁ /ₒ s₁ * ((r₂ * ↑sa + r₃ * ra) /ₒ (s₂ * sa)) = (r₁ * rb * ↑sc + r₁ * rc * 1) /ₒ (s₂ * sa * sb * sc)
rw [OreLocalization.expand' (r₂ * ↑sa + r₃ * ra) (s₂ * sa) (sb * sc)]
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
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
rc : R
sc : { x // x ∈ S }
hc : r₃ * (ra * ↑sb) * ↑sc = ↑s₁ * rc
hc' : r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb)) = r₁ * rc /ₒ (s₂ * sa * sb * sc)
⊢ r₁ * (rb * ↑sc + rc) /ₒ (s₂ * sa * (sb * sc)) = (r₁ * rb * ↑sc + r₁ * rc * 1) /ₒ (s₂ * sa * sb * sc)
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
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
rc : R
sc : { x // x ∈ S }
hc : r₃ * (ra * ↑sb) * ↑sc = ↑s₁ * rc
hc' : r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb)) = r₁ * rc /ₒ (s₂ * sa * sb * sc)
⊢ r₁ /ₒ s₁ * (↑s₁ * (rb * ↑sc + rc) /ₒ (s₂ * sa * (sb * sc))) = (r₁ * rb * ↑sc + r₁ * rc * 1) /ₒ (s₂ * sa * sb * sc)
rw [OreLocalization.mul_cancel']
no goals
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
r₁ : R
s₁ : { x // x ∈ S }
r₂ : R
s₂ : { x // x ∈ S }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
rc : R
sc : { x // x ∈ S }
hc : r₃ * (ra * ↑sb) * ↑sc = ↑s₁ * rc
hc' : r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb)) = r₁ * rc /ₒ (s₂ * sa * sb * sc)
⊢ r₁ * (rb * ↑sc + rc) /ₒ (s₂ * sa * (sb * sc)) = (r₁ * rb * ↑sc + r₁ * rc * 1) /ₒ (s₂ * sa * sb * sc)
simp only [mul_one, Submonoid.coe_mul, mul_add, ← mul_assoc]
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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
⊢ ↑s₂ * ↑sa * ↑sb ∈ 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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
⊢ ↑s₃ * (ra * ↑sb) ∈ S
rw [← mul_assoc, ← ha]
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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
⊢ ↑(s₂ * sa * sb) ∈ 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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
⊢ ↑s₂ * ↑sa * ↑sb ∈ S
norm_cast
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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
⊢ ↑(s₂ * sa * sb) ∈ S
apply SetLike.coe_mem
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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
⊢ ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
simp [ha, ← mul_assoc]
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 }
r₃ : R
s₃ : { x // x ∈ S }
ra : R
sa : { x // x ∈ S }
ha : ↑s₂ * ↑sa = ↑s₃ * ra
rb : R
sb : { x // x ∈ S }
hb : r₂ * ↑sa * ↑sb = ↑s₁ * rb
hs₃rasb : ↑s₃ * (ra * ↑sb) ∈ S
ha' : ↑(s₂ * sa * sb) = ↑s₃ * (ra * ↑sb)
rc : R
sc : { x // x ∈ S }
hc : r₃ * (ra * ↑sb) * ↑sc = ↑s₁ * rc
hc' : r₁ /ₒ s₁ * (r₃ * (ra * ↑sb) /ₒ (s₂ * sa * sb)) = r₁ * rc /ₒ (s₂ * sa * sb * sc)
⊢ ↑(s₂ * sa * sb) * ↑sc = ↑(s₂ * sa * sb * sc) * 1
simp