case mk.mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : { x // x ∈ S }
h : r * ↑t = r' * ↑t
r₂' : R
t' : { x // x ∈ S }
hr₂ : r₂ * ↑t' = ↑t * r₂'
⊢ r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : { x // x ∈ S }
h : r * ↑t = r' * ↑t
⊢ r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s
rcases oreCondition r₂ t with ⟨r₂', t', hr₂⟩
no goals
case mk.mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : { x // x ∈ S }
h : r * ↑t = r' * ↑t
r₂' : R
t' : { x // x ∈ S }
hr₂ : r₂ * ↑t' = ↑t * r₂'
⊢ r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s
calc
  r₁ * r * r₂ /ₒ s = r₁ * r * r₂ * t' /ₒ (s * t') := OreLocalization.expand (r₁ * r * r₂) s t' _
  _ = r₁ * r * (r₂ * t') /ₒ (s * t') := by simp [← mul_assoc]
  _ = r₁ * r * (t * r₂') /ₒ (s * t') := by rw [hr₂]
  _ = r₁ * (r * t) * r₂' /ₒ (s * t') := by simp [← mul_assoc]
  _ = r₁ * (r' * t) * r₂' /ₒ (s * t') := by rw [h]
  _ = r₁ * r' * (t * r₂') /ₒ (s * t') := by simp [← mul_assoc]
  _ = r₁ * r' * (r₂ * t') /ₒ (s * t') := by rw [hr₂]
  _ = r₁ * r' * r₂ * t' /ₒ (s * t') := by simp [← mul_assoc]
  _ = r₁ * r' * r₂ /ₒ s := (OreLocalization.expand _ _ _ _).symm
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : { x // x ∈ S }
h : r * ↑t = r' * ↑t
r₂' : R
t' : { x // x ∈ S }
hr₂ : r₂ * ↑t' = ↑t * r₂'
⊢ r₁ * r * r₂ * ↑t' /ₒ (s * t') = r₁ * r * (r₂ * ↑t') /ₒ (s * t')
simp [← mul_assoc]
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : { x // x ∈ S }
h : r * ↑t = r' * ↑t
r₂' : R
t' : { x // x ∈ S }
hr₂ : r₂ * ↑t' = ↑t * r₂'
⊢ r₁ * r * (r₂ * ↑t') /ₒ (s * t') = r₁ * r * (↑t * r₂') /ₒ (s * t')
rw [hr₂]
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : { x // x ∈ S }
h : r * ↑t = r' * ↑t
r₂' : R
t' : { x // x ∈ S }
hr₂ : r₂ * ↑t' = ↑t * r₂'
⊢ r₁ * r * (↑t * r₂') /ₒ (s * t') = r₁ * (r * ↑t) * r₂' /ₒ (s * t')
simp [← mul_assoc]
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : { x // x ∈ S }
h : r * ↑t = r' * ↑t
r₂' : R
t' : { x // x ∈ S }
hr₂ : r₂ * ↑t' = ↑t * r₂'
⊢ r₁ * (r * ↑t) * r₂' /ₒ (s * t') = r₁ * (r' * ↑t) * r₂' /ₒ (s * t')
rw [h]
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : { x // x ∈ S }
h : r * ↑t = r' * ↑t
r₂' : R
t' : { x // x ∈ S }
hr₂ : r₂ * ↑t' = ↑t * r₂'
⊢ r₁ * (r' * ↑t) * r₂' /ₒ (s * t') = r₁ * r' * (↑t * r₂') /ₒ (s * t')
simp [← mul_assoc]
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : { x // x ∈ S }
h : r * ↑t = r' * ↑t
r₂' : R
t' : { x // x ∈ S }
hr₂ : r₂ * ↑t' = ↑t * r₂'
⊢ r₁ * r' * (↑t * r₂') /ₒ (s * t') = r₁ * r' * (r₂ * ↑t') /ₒ (s * t')
rw [hr₂]
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : { x // x ∈ S }
h : r * ↑t = r' * ↑t
r₂' : R
t' : { x // x ∈ S }
hr₂ : r₂ * ↑t' = ↑t * r₂'
⊢ r₁ * r' * (r₂ * ↑t') /ₒ (s * t') = r₁ * r' * r₂ * ↑t' /ₒ (s * t')
simp [← mul_assoc]