Theorem: Smt.Reconstruct.Int.eq_of_sub_eq (Smt/Reconstruct/Int/Lemmas.lean)

State before:
a b c d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
this : ∀ {c x y : Int}, 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:
a b c✝ d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
c x y : Int
hc : c > 0
⊢ (c * (x - y) = 0) = (x - y = 0)
Tactic:
apply propext
State after:
case a
a b c✝ d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
c x y : Int
hc : c > 0
⊢ c * (x - y) = 0 ↔ x - y = 0

State before:
case a
a b c✝ d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
c x y : Int
hc : c > 0
⊢ c * (x - y) = 0 ↔ x - y = 0
Tactic:
constructor
State after:
case a.mp
a b c✝ d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
c x y : Int
hc : c > 0
⊢ c * (x - y) = 0 → x - y = 0

case a.mpr
a b c✝ d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
c x y : Int
hc : c > 0
⊢ x - y = 0 → c * (x - y) = 0

State before:
case a.mp
a b c✝ d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
c x y : Int
hc : c > 0
⊢ c * (x - y) = 0 → x - y = 0
Tactic:
apply Int.mul_eq_zero_left (Int.ne_of_gt hc)
State after:
no goals

State before:
case a.mpr
a b c✝ d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
c x y : Int
hc : c > 0
⊢ x - y = 0 → c * (x - y) = 0
Tactic:
intro hxy
State after:
case a.mpr
a b c✝ d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
c x y : Int
hc : c > 0
hxy : x - y = 0
⊢ c * (x - y) = 0

State before:
case a.mpr
a b c✝ d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
c x y : Int
hc : c > 0
hxy : x - y = 0
⊢ c * (x - y) = 0
Tactic:
rw [hxy, Int.mul_zero]
State after:
no goals