English
Fractions r/s and r'/s' that differ by a factor r or s can be shown equal by expanding the numerator by a common factor.
Русский
Дроби r/s и r'/s', различающиеся множителем числителя, равны после разложения числителя на общий множитель.
LaTeX
$$Eq (r s r') → Eq (r s r')$$
Lean4
/-- Fractions which differ by a factor of the numerator can be proven equal if
those factors expand to equal elements of `R`. -/
@[to_additive /-- Differences whose minuends differ by a common summand can be proven equal if
those summands expand to equal elements of `R`. -/
]
protected 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 :=
by
rcases oreCondition r₁ t with ⟨r₁', t', hr₁⟩
rw [OreLocalization.expand' _ s t', OreLocalization.expand' _ s t']
congr 1
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: use `assoc_rw`?
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]
