sub_eq_eval — Mathlib

Lean4
theorem sub_eq_eval {R₁ R₂ S₁ S₂ : Type*} [AddCommGroup M] [Ring R] [Module R M] [Semiring R₁] [Module R₁ M]
    [Semiring R₂] [Module R₂ M] [Semiring S₁] [Module S₁ M] [Semiring S₂] [Module S₂ M] {l₁ l₂ l : NF R M}
    {l₁' : NF R₁ M} {l₂' : NF R₂ M} {l₁'' : NF S₁ M} {l₂'' : NF S₂ M} {x₁ x₂ : M} (hx₁ : x₁ = l₁''.eval)
    (hx₂ : x₂ = l₂''.eval) (h₁' : l₁'.eval = l₁''.eval) (h₂' : l₂'.eval = l₂''.eval) (h₁ : l₁.eval = l₁'.eval)
    (h₂ : l₂.eval = l₂'.eval) (h : l₁.eval - l₂.eval = l.eval) : x₁ - x₂ = l.eval := by
  rw [hx₁, hx₂, ← h₁', ← h₂', ← h₁, ← h₂, h]
Похожие утверждения