R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
⊢ r₁ * oreNum r₂ s₁ /ₒ (s₂ * oreDenom r₂ s₁) = r₁ * v /ₒ (s₂ * u)
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
⊢ OreLocalization.mul' r₁ s₁ r₂ s₂ = r₁ * v /ₒ (s₂ * u)
simp only [mul']
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
h₀ : r₂ * ↑(oreDenom r₂ s₁) = ↑s₁ * oreNum r₂ s₁
⊢ r₁ * oreNum r₂ s₁ /ₒ (s₂ * oreDenom r₂ s₁) = r₁ * v /ₒ (s₂ * u)
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
⊢ r₁ * oreNum r₂ s₁ /ₒ (s₂ * oreDenom r₂ s₁) = r₁ * v /ₒ (s₂ * u)
have h₀ := ore_eq r₂ s₁
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
h₀ : r₂ * ↑(oreDenom r₂ s₁) = ↑s₁ * v₀
⊢ r₁ * v₀ /ₒ (s₂ * oreDenom r₂ s₁) = r₁ * v /ₒ (s₂ * u)
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
h₀ : r₂ * ↑(oreDenom r₂ s₁) = ↑s₁ * oreNum r₂ s₁
⊢ r₁ * oreNum r₂ s₁ /ₒ (s₂ * oreDenom r₂ s₁) = r₁ * v /ₒ (s₂ * u)
set v₀ := oreNum r₂ s₁
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
⊢ r₁ * v₀ /ₒ (s₂ * u₀) = r₁ * v /ₒ (s₂ * u)
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
h₀ : r₂ * ↑(oreDenom r₂ s₁) = ↑s₁ * v₀
⊢ r₁ * v₀ /ₒ (s₂ * oreDenom r₂ s₁) = r₁ * v /ₒ (s₂ * u)
set u₀ := oreDenom r₂ s₁
case mk.mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
⊢ r₁ * v₀ /ₒ (s₂ * u₀) = r₁ * v /ₒ (s₂ * u)
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
⊢ r₁ * v₀ /ₒ (s₂ * u₀) = r₁ * v /ₒ (s₂ * u)
rcases oreCondition (u₀ : R) u with ⟨r₃, s₃, h₃⟩
case mk.mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
⊢ r₁ * v₀ /ₒ (s₂ * u₀) = r₁ * v /ₒ (s₂ * u)
case mk.mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
⊢ r₁ * v₀ /ₒ (s₂ * u₀) = r₁ * v /ₒ (s₂ * u)
have :=
  calc
    (s₁ : R) * (v * r₃) = r₂ * u * r₃ := by rw [← mul_assoc, ← huv]
    _ = r₂ * u₀ * s₃ := by rw [mul_assoc, mul_assoc, h₃]
    _ = s₁ * (v₀ * s₃) := by rw [← mul_assoc, h₀]
case mk.mk.intro
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ r₁ * v₀ /ₒ (s₂ * u₀) = r₁ * v /ₒ (s₂ * u)
case mk.mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
⊢ r₁ * v₀ /ₒ (s₂ * u₀) = r₁ * v /ₒ (s₂ * u)
rcases ore_left_cancel _ _ _ this with ⟨s₄, hs₄⟩
case mk.mk.intro
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ r₁ * v /ₒ (s₂ * u) = r₁ * v₀ /ₒ (s₂ * u₀)
case mk.mk.intro
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ r₁ * v₀ /ₒ (s₂ * u₀) = r₁ * v /ₒ (s₂ * u)
symm
case mk.mk.intro
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ ∃ u_1 v_1, r₁ * v₀ * ↑u_1 = r₁ * v * v_1 ∧ ↑(s₂ * u₀) * ↑u_1 = ↑(s₂ * u) * v_1
case mk.mk.intro
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ r₁ * v /ₒ (s₂ * u) = r₁ * v₀ /ₒ (s₂ * u₀)
rw [oreDiv_eq_iff]
case mk.mk.intro
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ ∃ v_1, r₁ * v₀ * ↑(s₃ * s₄) = r₁ * v * v_1 ∧ ↑(s₂ * u₀) * ↑(s₃ * s₄) = ↑(s₂ * u) * v_1
case mk.mk.intro
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ ∃ u_1 v_1, r₁ * v₀ * ↑u_1 = r₁ * v * v_1 ∧ ↑(s₂ * u₀) * ↑u_1 = ↑(s₂ * u) * v_1
use s₃ * s₄
case mk.mk.intro
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ r₁ * v₀ * ↑(s₃ * s₄) = r₁ * v * (r₃ * ↑s₄) ∧ ↑(s₂ * u₀) * ↑(s₃ * s₄) = ↑(s₂ * u) * (r₃ * ↑s₄)
case mk.mk.intro
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ ∃ v_1, r₁ * v₀ * ↑(s₃ * s₄) = r₁ * v * v_1 ∧ ↑(s₂ * u₀) * ↑(s₃ * s₄) = ↑(s₂ * u) * v_1
use r₃ * s₄
case mk.mk.intro
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ r₁ * oreNum r₂ s₁ * (↑s₃ * ↑s₄) = r₁ * v * (r₃ * ↑s₄) ∧ ↑s₂ * ↑(oreDenom r₂ s₁) * (↑s₃ * ↑s₄) = ↑s₂ * ↑u * (r₃ * ↑s₄)
case mk.mk.intro
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ r₁ * v₀ * ↑(s₃ * s₄) = r₁ * v * (r₃ * ↑s₄) ∧ ↑(s₂ * u₀) * ↑(s₃ * s₄) = ↑(s₂ * u) * (r₃ * ↑s₄)
simp only [Submonoid.coe_mul]
case mk.mk.intro.left
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ r₁ * oreNum r₂ s₁ * (↑s₃ * ↑s₄) = r₁ * v * (r₃ * ↑s₄)

case mk.mk.intro.right
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ ↑s₂ * ↑(oreDenom r₂ s₁) * (↑s₃ * ↑s₄) = ↑s₂ * ↑u * (r₃ * ↑s₄)
case mk.mk.intro
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ r₁ * oreNum r₂ s₁ * (↑s₃ * ↑s₄) = r₁ * v * (r₃ * ↑s₄) ∧ ↑s₂ * ↑(oreDenom r₂ s₁) * (↑s₃ * ↑s₄) = ↑s₂ * ↑u * (r₃ * ↑s₄)
constructor
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
⊢ ↑s₁ * (v * r₃) = r₂ * ↑u * r₃
rw [← mul_assoc, ← huv]
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
⊢ r₂ * ↑u * r₃ = r₂ * ↑u₀ * ↑s₃
rw [mul_assoc, mul_assoc, h₃]
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
⊢ r₂ * ↑u₀ * ↑s₃ = ↑s₁ * (v₀ * ↑s₃)
rw [← mul_assoc, h₀]
case mk.mk.intro.left
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ r₁ * (v * r₃ * ↑s₄) = r₁ * v * (r₃ * ↑s₄)
case mk.mk.intro.left
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ r₁ * oreNum r₂ s₁ * (↑s₃ * ↑s₄) = r₁ * v * (r₃ * ↑s₄)
rw [mul_assoc (b := v₀), ← mul_assoc (a := v₀), ← hs₄]
no goals
case mk.mk.intro.left
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ r₁ * (v * r₃ * ↑s₄) = r₁ * v * (r₃ * ↑s₄)
simp only [mul_assoc]
case mk.mk.intro.right
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ ↑s₂ * (↑u * r₃ * ↑s₄) = ↑s₂ * ↑u * (r₃ * ↑s₄)
case mk.mk.intro.right
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ ↑s₂ * ↑(oreDenom r₂ s₁) * (↑s₃ * ↑s₄) = ↑s₂ * ↑u * (r₃ * ↑s₄)
rw [mul_assoc (b := (u₀ : R)), ← mul_assoc (a := (u₀ : R)), h₃]
no goals
case mk.mk.intro.right
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ u : { x // x ∈ S }
v : R
huv : r₂ * ↑u = ↑s₁ * v
v₀ : R := oreNum r₂ s₁
u₀ : { x // x ∈ S } := oreDenom r₂ s₁
h₀ : r₂ * ↑u₀ = ↑s₁ * v₀
r₃ : R
s₃ : { x // x ∈ S }
h₃ : ↑u₀ * ↑s₃ = ↑u * r₃
this : ↑s₁ * (v * r₃) = ↑s₁ * (v₀ * ↑s₃)
s₄ : { x // x ∈ S }
hs₄ : v * r₃ * ↑s₄ = v₀ * ↑s₃ * ↑s₄
⊢ ↑s₂ * (↑u * r₃ * ↑s₄) = ↑s₂ * ↑u * (r₃ * ↑s₄)
simp only [mul_assoc]