case c
R : Type u_1
inst✝¹ : Monoid 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 * z)
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x y z : OreLocalization R S
⊢ x * y * z = x * (y * z)
induction' x using OreLocalization.ind with r₁ s₁
case c.c
R : Type u_1
inst✝¹ : Monoid 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₂ * z)
case c
R : Type u_1
inst✝¹ : Monoid 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 * z)
induction' y using OreLocalization.ind with r₂ s₂
case c.c.c
R : Type u_1
inst✝¹ : Monoid 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₃))
case c.c
R : Type u_1
inst✝¹ : Monoid 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₂ * z)
induction' z using OreLocalization.ind with r₃ s₃
case c.c.c.mk.mk.intro
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * ra /ₒ (s₂ * sa)
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) * (r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ /ₒ s₂ * (r₃ /ₒ s₃))
case c.c.c
R : Type u_1
inst✝¹ : Monoid 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₃))
rcases oreDivMulChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩
case c.c.c.mk.mk.intro
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * ra /ₒ (s₂ * 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✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * ra /ₒ (s₂ * sa)
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) * (r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ /ₒ s₂ * (r₃ /ₒ s₃))
rw [ha']
case c.c.c.mk.mk.intro
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
⊢ r₁ * ra /ₒ (s₂ * sa) * (r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ /ₒ s₂ * (r₃ /ₒ s₃))
case c.c.c.mk.mk.intro
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * ra /ₒ (s₂ * sa)
⊢ r₁ * ra /ₒ (s₂ * sa) * (r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ /ₒ s₂ * (r₃ /ₒ s₃))
clear ha'
case c.c.c.mk.mk.intro.mk.mk.intro
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
hb' : r₂ /ₒ s₂ * (r₃ /ₒ s₃) = r₂ * rb /ₒ (s₃ * sb)
⊢ r₁ * ra /ₒ (s₂ * sa) * (r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ /ₒ s₂ * (r₃ /ₒ s₃))
case c.c.c.mk.mk.intro
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
⊢ r₁ * ra /ₒ (s₂ * sa) * (r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ /ₒ s₂ * (r₃ /ₒ s₃))
rcases oreDivMulChar' r₂ r₃ s₂ s₃ with ⟨rb, sb, hb, hb'⟩
case c.c.c.mk.mk.intro.mk.mk.intro
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
hb' : r₂ /ₒ s₂ * (r₃ /ₒ s₃) = r₂ * rb /ₒ (s₃ * sb)
⊢ r₁ * ra /ₒ (s₂ * sa) * (r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ * rb /ₒ (s₃ * sb))
case c.c.c.mk.mk.intro.mk.mk.intro
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
hb' : r₂ /ₒ s₂ * (r₃ /ₒ s₃) = r₂ * rb /ₒ (s₃ * sb)
⊢ r₁ * ra /ₒ (s₂ * sa) * (r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ /ₒ s₂ * (r₃ /ₒ s₃))
rw [hb']
case c.c.c.mk.mk.intro.mk.mk.intro
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
⊢ r₁ * ra /ₒ (s₂ * sa) * (r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ * rb /ₒ (s₃ * sb))
case c.c.c.mk.mk.intro.mk.mk.intro
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
hb' : r₂ /ₒ s₂ * (r₃ /ₒ s₃) = r₂ * rb /ₒ (s₃ * sb)
⊢ r₁ * ra /ₒ (s₂ * sa) * (r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ * rb /ₒ (s₃ * sb))
clear hb'
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
rc : R
sc : { x // x ∈ S }
hc : rb * ↑sc = ↑sa * rc
⊢ r₁ * ra /ₒ (s₂ * sa) * (r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ * rb /ₒ (s₃ * sb))
case c.c.c.mk.mk.intro.mk.mk.intro
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
⊢ r₁ * ra /ₒ (s₂ * sa) * (r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ * rb /ₒ (s₃ * sb))
rcases oreCondition rb sa with ⟨rc, sc, hc⟩
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
rc : R
sc : { x // x ∈ S }
hc : rb * ↑sc = ↑sa * rc
⊢ r₁ * ra * rc /ₒ (s₃ * (sb * sc)) = r₁ /ₒ s₁ * (r₂ * rb /ₒ (s₃ * sb))
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
rc : R
sc : { x // x ∈ S }
hc : rb * ↑sc = ↑sa * rc
⊢ r₁ * ra /ₒ (s₂ * sa) * (r₃ /ₒ s₃) = r₁ /ₒ s₁ * (r₂ * rb /ₒ (s₃ * sb))
rw [oreDiv_mul_char (r₁ * ra) r₃ (s₂ * sa) s₃ rc (sb * sc)
    (by
      simp only [Submonoid.coe_mul]
      rw [← mul_assoc, hb, mul_assoc, hc, ← mul_assoc])]
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
rc : R
sc : { x // x ∈ S }
hc : rb * ↑sc = ↑sa * rc
⊢ r₁ * (ra * rc) /ₒ (s₃ * sb * sc) = r₁ /ₒ s₁ * (r₂ * rb /ₒ (s₃ * sb))
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
rc : R
sc : { x // x ∈ S }
hc : rb * ↑sc = ↑sa * rc
⊢ r₁ * ra * rc /ₒ (s₃ * (sb * sc)) = r₁ /ₒ s₁ * (r₂ * rb /ₒ (s₃ * sb))
rw [mul_assoc, ← mul_assoc s₃]
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
rc : R
sc : { x // x ∈ S }
hc : rb * ↑sc = ↑sa * rc
⊢ r₁ /ₒ s₁ * (r₂ * rb /ₒ (s₃ * sb)) = r₁ * (ra * rc) /ₒ (s₃ * sb * sc)
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
rc : R
sc : { x // x ∈ S }
hc : rb * ↑sc = ↑sa * rc
⊢ r₁ * (ra * rc) /ₒ (s₃ * sb * sc) = r₁ /ₒ s₁ * (r₂ * rb /ₒ (s₃ * sb))
symm
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk.huv
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
rc : R
sc : { x // x ∈ S }
hc : rb * ↑sc = ↑sa * rc
⊢ r₂ * rb * ↑sc = ↑s₁ * (ra * rc)
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
rc : R
sc : { x // x ∈ S }
hc : rb * ↑sc = ↑sa * rc
⊢ r₁ /ₒ s₁ * (r₂ * rb /ₒ (s₃ * sb)) = r₁ * (ra * rc) /ₒ (s₃ * sb * sc)
apply oreDiv_mul_char
no goals
case c.c.c.mk.mk.intro.mk.mk.intro.mk.mk.huv
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
rc : R
sc : { x // x ∈ S }
hc : rb * ↑sc = ↑sa * rc
⊢ r₂ * rb * ↑sc = ↑s₁ * (ra * rc)
rw [mul_assoc, hc, ← mul_assoc (b := ra), ← ha, mul_assoc]
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
rc : R
sc : { x // x ∈ S }
hc : rb * ↑sc = ↑sa * rc
⊢ r₃ * (↑sb * ↑sc) = ↑s₂ * ↑sa * rc
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
rc : R
sc : { x // x ∈ S }
hc : rb * ↑sc = ↑sa * rc
⊢ r₃ * ↑(sb * sc) = ↑(s₂ * sa) * rc
simp only [Submonoid.coe_mul]
no goals
R : Type u_1
inst✝¹ : Monoid 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 : r₂ * ↑sa = ↑s₁ * ra
rb : R
sb : { x // x ∈ S }
hb : r₃ * ↑sb = ↑s₂ * rb
rc : R
sc : { x // x ∈ S }
hc : rb * ↑sc = ↑sa * rc
⊢ r₃ * (↑sb * ↑sc) = ↑s₂ * ↑sa * rc
rw [← mul_assoc, hb, mul_assoc, hc, ← mul_assoc]