Theorem: Smt.Arith.eq_of_sub_eq (Smt/Reconstruct/Arith/ArithPolyNorm.lean)

State before:
α : Type u_1
inst✝ : LinearOrderedRing α
c₁ c₂ a₁ a₂ b₁ b₂ : α
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
⊢ (a₁ = a₂) = (b₁ = b₂)
Tactic:
have {c x y : α} (hc : c > 0) : (c * (x - y) = 0) = (x - y = 0) := by
  rw (config := { occs := .pos [1] }) [← mul_zero c, mul_right_inj' (ne_of_gt hc)]
State after:
α : Type u_1
inst✝ : LinearOrderedRing α
c₁ c₂ a₁ a₂ b₁ b₂ : α
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
this : ∀ {c x y : α}, c > 0 → (c * (x - y) = 0) = (x - y = 0)
⊢ (a₁ = a₂) = (b₁ = b₂)

State before:
α : Type u_1
inst✝ : LinearOrderedRing α
c₁ c₂ a₁ a₂ b₁ b₂ : α
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
this : ∀ {c x y : α}, c > 0 → (c * (x - y) = 0) = (x - y = 0)
⊢ (a₁ = a₂) = (b₁ = b₂)
Tactic:
rw [@eq_eq_sub_eq_zero _ _ a₁, @eq_eq_sub_eq_zero _ _ b₁, ← this hc₁, ← this hc₂, h]
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearOrderedRing α
c₁ c₂ a₁ a₂ b₁ b₂ : α
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
c x y : α
hc : c > 0
⊢ (c * (x - y) = 0) = (x - y = 0)
Tactic:
rw (config := { occs := .pos [1] }) [← mul_zero c, mul_right_inj' (ne_of_gt hc)]
State after:
no goals