-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem eq_of_num_factor_eq {r r' r₁ r₂ : R} {s t : S} (h : t * r = t * r') :
    r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁' * (↑t * r') * r₂ = r₁' * ↑t * r' * r₂

Tactic:
simp [← mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁' * ↑t * r' * r₂ = ↑t' * r₁ * r' * r₂

Tactic:
rw [hr₁]

Result:
no goals

Proof state:
case mk.mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ t' • (r₁ * r * r₂) /ₒ (t' * s) = t' • (r₁ * r' * r₂) /ₒ (t' * s)

Tactic:
congr 1

Result:
case mk.mk.e_r
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ t' • (r₁ * r * r₂) = t' • (r₁ * r' * r₂)

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ ↑t' * (r₁ * r * r₂) = ↑t' * r₁ * r * r₂

Tactic:
simp [← mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ ↑t' * r₁ * r * r₂ = r₁' * ↑t * r * r₂

Tactic:
rw [hr₁]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
⊢ r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s

Tactic:
rcases oreCondition r₁ t with ⟨r₁', t', hr₁⟩

Result:
case mk.mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s

Proof state:
case mk.mk.e_r
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ t' • (r₁ * r * r₂) = t' • (r₁ * r' * r₂)

Tactic:
calc (t' : R) * (r₁ * r * r₂)
    = t' * r₁ * r * r₂ := by simp [← mul_assoc]
  _ = r₁' * t * r * r₂ := by rw [hr₁]
  _ = r₁' * (t * r) * r₂ := by simp [← mul_assoc]
  _ = r₁' * (t * r') * r₂ := by rw [h]
  _ = r₁' * t * r' * r₂ := by simp [← mul_assoc]
  _ = t' * r₁ * r' * r₂ := by rw [hr₁]
  _ = t' * (r₁ * r' * r₂) := by simp [← mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ ↑t' * r₁ * r' * r₂ = ↑t' * (r₁ * r' * r₂)

Tactic:
simp [← mul_assoc]

Result:
no goals

Proof state:
case mk.mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s

Tactic:
rw [OreLocalization.expand' _ s t', OreLocalization.expand' _ s t']

Result:
case mk.mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ t' • (r₁ * r * r₂) /ₒ (t' * s) = t' • (r₁ * r' * r₂) /ₒ (t' * s)

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁' * (↑t * r) * r₂ = r₁' * (↑t * r') * r₂

Tactic:
rw [h]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁' * ↑t * r * r₂ = r₁' * (↑t * r) * r₂

Tactic:
simp [← mul_assoc]

Result:
no goals