internlm/Lean-Github huggingface dataset:
Theorem: Smt.Reconstruct.Int.sum_ub₅
Proof state before:
a b c d : Int
h₁ : a ≤ b
h₂ : c ≤ d
⊢ a + c ≤ b + d
Tactic:
have r₁ : a + c ≤ a + d := Int.add_le_add_left h₂ a
Proof state after:
a b c d : Int
h₁ : a ≤ b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
⊢ a + c ≤ b + d
Theorem: Smt.Reconstruct.Int.sum_ub₅
Proof state before:
a b c d : Int
h₁ : a ≤ b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
⊢ a + c ≤ b + d
Tactic:
have r₂ : a + d ≤ b + d := Int.add_le_add_right h₁ d
Proof state after:
a b c d : Int
h₁ : a ≤ b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
r₂ : a + d ≤ b + d
⊢ a + c ≤ b + d
Theorem: Smt.Reconstruct.Int.sum_ub₅
Proof state before:
a b c d : Int
h₁ : a ≤ b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
r₂ : a + d ≤ b + d
⊢ a + c ≤ b + d
Tactic:
exact Int.le_trans r₁ r₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.sum_ub₆
Proof state before:
a b c d : Int
h₁ : a ≤ b
h₂ : c = d
⊢ a + c ≤ b + d
Tactic:
rewrite [h₂]
Proof state after:
a b c d : Int
h₁ : a ≤ b
h₂ : c = d
⊢ a + d ≤ b + d
Theorem: Smt.Reconstruct.Int.sum_ub₆
Proof state before:
a b c d : Int
h₁ : a ≤ b
h₂ : c = d
⊢ a + d ≤ b + d
Tactic:
exact Int.add_le_add_right h₁ d
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.sum_ub₇
Proof state before:
a b c d : Int
h₁ : a = b
h₂ : c < d
⊢ a + c < b + d
Tactic:
rewrite [h₁]
Proof state after:
a b c d : Int
h₁ : a = b
h₂ : c < d
⊢ b + c < b + d
Theorem: Smt.Reconstruct.Int.sum_ub₇
Proof state before:
a b c d : Int
h₁ : a = b
h₂ : c < d
⊢ b + c < b + d
Tactic:
exact Int.add_lt_add_left h₂ b
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.sum_ub₈
Proof state before:
a b c d : Int
h₁ : a = b
h₂ : c ≤ d
⊢ a + c ≤ b + d
Tactic:
rewrite [h₁]
Proof state after:
a b c d : Int
h₁ : a = b
h₂ : c ≤ d
⊢ b + c ≤ b + d
Theorem: Smt.Reconstruct.Int.sum_ub₈
Proof state before:
a b c d : Int
h₁ : a = b
h₂ : c ≤ d
⊢ b + c ≤ b + d
Tactic:
exact Int.add_le_add_left h₂ b
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.sum_ub₉
Proof state before:
a b c d : Int
h₁ : a = b
h₂ : c = d
⊢ a + c ≤ b + d
Tactic:
rewrite [h₁, h₂]
Proof state after:
a b c d : Int
h₁ : a = b
h₂ : c = d
⊢ b + d ≤ b + d
Theorem: Smt.Reconstruct.Int.sum_ub₉
Proof state before:
a b c d : Int
h₁ : a = b
h₂ : c = d
⊢ b + d ≤ b + d
Tactic:
exact Int.le_refl (b + d)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.trichotomy₁
Proof state before:
a b c d : Int
h₁ : a ≥ b
h₂ : a ≠ b
⊢ a > b
Tactic:
have tr := Int.lt_trichotomy a b
Proof state after:
a b c d : Int
h₁ : a ≥ b
h₂ : a ≠ b
tr : a < b ∨ a = b ∨ b < a
⊢ a > b
Theorem: Smt.Reconstruct.Int.trichotomy₁
Proof state before:
a b c d : Int
h₁ : a ≥ b
h₂ : a ≠ b
tr : a < b ∨ a = b ∨ b < a
⊢ a > b
Tactic:
exact or_implies_right (or_implies_right tr (Int.not_lt.mpr h₁)) h₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.trichotomy₂
Proof state before:
a b c d : Int
h₁ : a ≠ b
h₂ : a ≥ b
⊢ a > b
Tactic:
have tr := Int.lt_trichotomy a b
Proof state after:
a b c d : Int
h₁ : a ≠ b
h₂ : a ≥ b
tr : a < b ∨ a = b ∨ b < a
⊢ a > b
Theorem: Smt.Reconstruct.Int.trichotomy₂
Proof state before:
a b c d : Int
h₁ : a ≠ b
h₂ : a ≥ b
tr : a < b ∨ a = b ∨ b < a
⊢ a > b
Tactic:
exact or_implies_right (or_implies_right tr (Int.not_lt.mpr h₂)) h₁
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.trichotomy₃
Proof state before:
a b c d : Int
h₁ : a ≥ b
h₂ : a ≤ b
⊢ a = b
Tactic:
have tr := Int.lt_trichotomy a b
Proof state after:
a b c d : Int
h₁ : a ≥ b
h₂ : a ≤ b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b
Theorem: Smt.Reconstruct.Int.trichotomy₃
Proof state before:
a b c d : Int
h₁ : a ≥ b
h₂ : a ≤ b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b
Tactic:
exact or_implies_left (or_implies_right tr (Int.not_lt.mpr h₁)) (Int.not_lt.mpr h₂)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.trichotomy₄
Proof state before:
a b c d : Int
h₁ : a ≤ b
h₂ : a ≥ b
⊢ a = b
Tactic:
have tr := Int.lt_trichotomy a b
Proof state after:
a b c d : Int
h₁ : a ≤ b
h₂ : a ≥ b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b
Theorem: Smt.Reconstruct.Int.trichotomy₄
Proof state before:
a b c d : Int
h₁ : a ≤ b
h₂ : a ≥ b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b
Tactic:
exact or_implies_left (or_implies_right tr (Int.not_lt.mpr h₂)) (Int.not_lt.mpr h₁)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.trichotomy₅
Proof state before:
a b c d : Int
h₁ : a ≠ b
h₂ : a ≤ b
⊢ a < b
Tactic:
have tr := Int.lt_trichotomy a b
Proof state after:
a b c d : Int
h₁ : a ≠ b
h₂ : a ≤ b
tr : a < b ∨ a = b ∨ b < a
⊢ a < b
Theorem: Smt.Reconstruct.Int.trichotomy₅
Proof state before:
a b c d : Int
h₁ : a ≠ b
h₂ : a ≤ b
tr : a < b ∨ a = b ∨ b < a
⊢ a < b
Tactic:
exact or_implies_left (or_implies_left (or_assoc.mpr tr) (Int.not_lt.mpr h₂)) h₁
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.trichotomy₆
Proof state before:
a b c d : Int
h₁ : a ≤ b
h₂ : a ≠ b
⊢ a < b
Tactic:
have tr := Int.lt_trichotomy a b
Proof state after:
a b c d : Int
h₁ : a ≤ b
h₂ : a ≠ b
tr : a < b ∨ a = b ∨ b < a
⊢ a < b
Theorem: Smt.Reconstruct.Int.trichotomy₆
Proof state before:
a b c d : Int
h₁ : a ≤ b
h₂ : a ≠ b
tr : a < b ∨ a = b ∨ b < a
⊢ a < b
Tactic:
exact or_implies_left (or_implies_left (or_assoc.mpr tr) (Int.not_lt.mpr h₁)) h₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.lt_eq_sub_lt_zero
Proof state before:
a b c d : Int
⊢ (a < b) = (a - b < 0)
Tactic:
apply propext
Proof state after:
case a
a b c d : Int
⊢ a < b ↔ a - b < 0
Theorem: Smt.Reconstruct.Int.lt_eq_sub_lt_zero
Proof state before:
case a
a b c d : Int
⊢ a < b ↔ a - b < 0
Tactic:
constructor
Proof state after:
case a.mp
a b c d : Int
⊢ a < b → a - b < 0

case a.mpr
a b c d : Int
⊢ a - b < 0 → a < b
Theorem: Smt.Reconstruct.Int.lt_eq_sub_lt_zero
Proof state before:
case a.mp
a b c d : Int
⊢ a < b → a - b < 0
Tactic:
apply Int.sub_neg_of_lt
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.lt_eq_sub_lt_zero
Proof state before:
case a.mpr
a b c d : Int
⊢ a - b < 0 → a < b
Tactic:
apply Int.lt_of_sub_neg
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.le_eq_sub_le_zero
Proof state before:
a b c d : Int
⊢ (a ≤ b) = (a - b ≤ 0)
Tactic:
apply propext
Proof state after:
case a
a b c d : Int
⊢ a ≤ b ↔ a - b ≤ 0
Theorem: Smt.Reconstruct.Int.le_eq_sub_le_zero
Proof state before:
case a
a b c d : Int
⊢ a ≤ b ↔ a - b ≤ 0
Tactic:
constructor
Proof state after:
case a.mp
a b c d : Int
⊢ a ≤ b → a - b ≤ 0

case a.mpr
a b c d : Int
⊢ a - b ≤ 0 → a ≤ b
Theorem: Smt.Reconstruct.Int.le_eq_sub_le_zero
Proof state before:
case a.mp
a b c d : Int
⊢ a ≤ b → a - b ≤ 0
Tactic:
exact Int.sub_nonpos_of_le
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.le_eq_sub_le_zero
Proof state before:
case a.mpr
a b c d : Int
⊢ a - b ≤ 0 → a ≤ b
Tactic:
exact Int.le_of_sub_nonpos
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.eq_eq_sub_eq_zero
Proof state before:
a b c d : Int
⊢ (a = b) = (a - b = 0)
Tactic:
simp only [Int.sub_eq_zero]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.ge_eq_sub_ge_zero
Proof state before:
a b c d : Int
⊢ (a ≥ b) = (a - b ≥ 0)
Tactic:
simp only [ge_iff_le, eq_iff_iff]
Proof state after:
a b c d : Int
⊢ b ≤ a ↔ 0 ≤ a - b
Theorem: Smt.Reconstruct.Int.ge_eq_sub_ge_zero
Proof state before:
a b c d : Int
⊢ b ≤ a ↔ 0 ≤ a - b
Tactic:
constructor
Proof state after:
case mp
a b c d : Int
⊢ b ≤ a → 0 ≤ a - b

case mpr
a b c d : Int
⊢ 0 ≤ a - b → b ≤ a
Theorem: Smt.Reconstruct.Int.ge_eq_sub_ge_zero
Proof state before:
case mp
a b c d : Int
⊢ b ≤ a → 0 ≤ a - b
Tactic:
exact Int.sub_nonneg_of_le
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.ge_eq_sub_ge_zero
Proof state before:
case mpr
a b c d : Int
⊢ 0 ≤ a - b → b ≤ a
Tactic:
exact Int.le_of_sub_nonneg
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.gt_eq_sub_gt_zero
Proof state before:
a b c d : Int
⊢ (a > b) = (a - b > 0)
Tactic:
simp only [gt_iff_lt, eq_iff_iff]
Proof state after:
a b c d : Int
⊢ b < a ↔ 0 < a - b
Theorem: Smt.Reconstruct.Int.gt_eq_sub_gt_zero
Proof state before:
a b c d : Int
⊢ b < a ↔ 0 < a - b
Tactic:
constructor
Proof state after:
case mp
a b c d : Int
⊢ b < a → 0 < a - b

case mpr
a b c d : Int
⊢ 0 < a - b → b < a
Theorem: Smt.Reconstruct.Int.gt_eq_sub_gt_zero
Proof state before:
case mp
a b c d : Int
⊢ b < a → 0 < a - b
Tactic:
exact Int.sub_pos_of_lt
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.gt_eq_sub_gt_zero
Proof state before:
case mpr
a b c d : Int
⊢ 0 < a - b → b < a
Tactic:
exact Int.lt_of_sub_pos
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.lt_of_sub_eq
Proof 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₂)
⊢ (a₁ < a₂) = (b₁ < b₂)
Tactic:
have {c x y : Int} (hc : c > 0) : (c * (x - y) < 0) = (x - y < 0) := by
  rw (config := { occs := .pos [1] }) [← Int.mul_zero c, Int.mul_lt_mul_left hc]
Proof state after:
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₂)
Theorem: Smt.Reconstruct.Int.lt_of_sub_eq
Proof 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 [lt_eq_sub_lt_zero, @lt_eq_sub_lt_zero b₁, ← this hc₁, ← this hc₂, h]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.lt_of_sub_eq
Proof 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:
rw (config := { occs := .pos [1] }) [← Int.mul_zero c, Int.mul_lt_mul_left hc]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.le_of_sub_eq
Proof 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₂)
⊢ (a₁ ≤ a₂) = (b₁ ≤ b₂)
Tactic:
have {c x y : Int} (hc : c > 0) : (c * (x - y) ≤ 0) = (x - y ≤ 0) := by
  rw (config := { occs := .pos [1] }) [← Int.mul_zero c, Int.mul_le_mul_left hc]
Proof state after:
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₂)
Theorem: Smt.Reconstruct.Int.le_of_sub_eq
Proof 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 [le_eq_sub_le_zero, @le_eq_sub_le_zero b₁, ← this hc₁, ← this hc₂, h]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.le_of_sub_eq
Proof 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:
rw (config := { occs := .pos [1] }) [← Int.mul_zero c, Int.mul_le_mul_left hc]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.eq_of_sub_eq
Proof 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]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.eq_of_sub_eq
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Int.eq_of_sub_eq
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Int.eq_of_sub_eq
Proof 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)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.eq_of_sub_eq
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Int.eq_of_sub_eq
Proof 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]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.ge_of_sub_eq
Proof 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₂)
⊢ (a₁ ≥ a₂) = (b₁ ≥ b₂)
Tactic:
have {c x y : Int} (hc : c > 0) : (c * (x - y) ≥ 0) = (x - y ≥ 0) := by
  rw (config := { occs := .pos [1] }) [← Int.mul_zero c, ge_iff_le, Int.mul_le_mul_left hc]
Proof state after:
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₂)
Theorem: Smt.Reconstruct.Int.ge_of_sub_eq
Proof 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 [ge_eq_sub_ge_zero, @ge_eq_sub_ge_zero b₁, ← this hc₁, ← this hc₂, h]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.ge_of_sub_eq
Proof 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:
rw (config := { occs := .pos [1] }) [← Int.mul_zero c, ge_iff_le, Int.mul_le_mul_left hc]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.gt_of_sub_eq
Proof 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₂)
⊢ (a₁ > a₂) = (b₁ > b₂)
Tactic:
have {c x y : Int} (hc : c > 0) : (c * (x - y) > 0) = (x - y > 0) := by
  rw (config := { occs := .pos [1] }) [← Int.mul_zero c, gt_iff_lt, Int.mul_lt_mul_left hc]
Proof state after:
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₂)
Theorem: Smt.Reconstruct.Int.gt_of_sub_eq
Proof 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 [gt_eq_sub_gt_zero, @gt_eq_sub_gt_zero b₁, ← this hc₁, ← this hc₂, h]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.gt_of_sub_eq
Proof 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:
rw (config := { occs := .pos [1] }) [← Int.mul_zero c, gt_iff_lt, Int.mul_lt_mul_left hc]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.pow_neg_even
Proof state before:
a b c d : Int
k : Nat
z : Int
h₁ : z < 0
h₂ : k % 2 = 0
⊢ z ^ k > 0
Tactic:
cases k with
| zero    => simp [Int.pow_zero]
| succ k =>
  have hodd := Nat.even_add_one.mp h₂
  have mulZ : z * z ^ k > z * 0 := Int.mul_lt_mul_of_neg_left (pow_neg_odd h₁ (Nat.mod_two_ne_zero.mp hodd)) h₁
  simp at mulZ
  rw [Int.pow_succ, Int.mul_comm]
  exact mulZ
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.pow_neg_even
Proof state before:
case zero
a b c d z : Int
h₁ : z < 0
h₂ : 0 % 2 = 0
⊢ z ^ 0 > 0
Tactic:
simp [Int.pow_zero]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.pow_neg_even
Proof state before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
⊢ z ^ (k + 1) > 0
Tactic:
have hodd := Nat.even_add_one.mp h₂
Proof state after:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
⊢ z ^ (k + 1) > 0
Theorem: Smt.Reconstruct.Int.pow_neg_even
Proof state before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
⊢ z ^ (k + 1) > 0
Tactic:
have mulZ : z * z ^ k > z * 0 := Int.mul_lt_mul_of_neg_left (pow_neg_odd h₁ (Nat.mod_two_ne_zero.mp hodd)) h₁
Proof state after:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
mulZ : z * z ^ k > z * 0
⊢ z ^ (k + 1) > 0
Theorem: Smt.Reconstruct.Int.pow_neg_even
Proof state before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
mulZ : z * z ^ k > z * 0
⊢ z ^ (k + 1) > 0
Tactic:
simp at mulZ
Proof state after:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
mulZ : 0 < z * z ^ k
⊢ z ^ (k + 1) > 0
Theorem: Smt.Reconstruct.Int.pow_neg_even
Proof state before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
mulZ : 0 < z * z ^ k
⊢ z ^ (k + 1) > 0
Tactic:
rw [Int.pow_succ, Int.mul_comm]
Proof state after:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
mulZ : 0 < z * z ^ k
⊢ z * z ^ k > 0
Theorem: Smt.Reconstruct.Int.pow_neg_even
Proof state before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
mulZ : 0 < z * z ^ k
⊢ z * z ^ k > 0
Tactic:
exact mulZ
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.pow_neg_odd
Proof state before:
a b c d : Int
k : Nat
z : Int
h₁ : z < 0
h₂ : k % 2 = 1
⊢ z ^ k < 0
Tactic:
cases k with
| zero    => simp at h₂
| succ k =>
  have heven : k % 2 = 0 := Classical.not_not.mp (mt Nat.even_add_one.mpr (Eq.symm h₂ ▸ nofun))
  have mulZ : z * 0 > z * z ^ k := Int.mul_lt_mul_of_neg_left (pow_neg_even h₁ heven) h₁
  simp at mulZ
  rw [Int.pow_succ, Int.mul_comm]
  exact mulZ
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.pow_neg_odd
Proof state before:
case zero
a b c d z : Int
h₁ : z < 0
h₂ : 0 % 2 = 1
⊢ z ^ 0 < 0
Tactic:
simp at h₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.pow_neg_odd
Proof state before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
⊢ z ^ (k + 1) < 0
Tactic:
have heven : k % 2 = 0 := Classical.not_not.mp (mt Nat.even_add_one.mpr (Eq.symm h₂ ▸ nofun))
Proof state after:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
heven : k % 2 = 0
⊢ z ^ (k + 1) < 0
Theorem: Smt.Reconstruct.Int.pow_neg_odd
Proof state before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
heven : k % 2 = 0
⊢ z ^ (k + 1) < 0
Tactic:
have mulZ : z * 0 > z * z ^ k := Int.mul_lt_mul_of_neg_left (pow_neg_even h₁ heven) h₁
Proof state after:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
heven : k % 2 = 0
mulZ : z * 0 > z * z ^ k
⊢ z ^ (k + 1) < 0
Theorem: Smt.Reconstruct.Int.pow_neg_odd
Proof state before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
heven : k % 2 = 0
mulZ : z * 0 > z * z ^ k
⊢ z ^ (k + 1) < 0
Tactic:
simp at mulZ
Proof state after:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
heven : k % 2 = 0
mulZ : z * z ^ k < 0
⊢ z ^ (k + 1) < 0
Theorem: Smt.Reconstruct.Int.pow_neg_odd
Proof state before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
heven : k % 2 = 0
mulZ : z * z ^ k < 0
⊢ z ^ (k + 1) < 0
Tactic:
rw [Int.pow_succ, Int.mul_comm]
Proof state after:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
heven : k % 2 = 0
mulZ : z * z ^ k < 0
⊢ z * z ^ k < 0
Theorem: Smt.Reconstruct.Int.pow_neg_odd
Proof state before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
heven : k % 2 = 0
mulZ : z * z ^ k < 0
⊢ z * z ^ k < 0
Tactic:
exact mulZ
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.pow_pos
Proof state before:
a b c d : Int
k : Nat
z : Int
h : z > 0
⊢ z ^ k > 0
Tactic:
induction k with
| zero    => simp [Int.pow_zero]
| succ k ih =>
  rw [Int.pow_succ]
  have h₂ := Int.mul_lt_mul_of_pos_left h ih
  simp at h₂
  exact h₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.pow_pos
Proof state before:
case zero
a b c d z : Int
h : z > 0
⊢ z ^ 0 > 0
Tactic:
simp [Int.pow_zero]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.pow_pos
Proof state before:
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
⊢ z ^ (k + 1) > 0
Tactic:
rw [Int.pow_succ]
Proof state after:
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
⊢ z ^ k * z > 0
Theorem: Smt.Reconstruct.Int.pow_pos
Proof state before:
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
⊢ z ^ k * z > 0
Tactic:
have h₂ := Int.mul_lt_mul_of_pos_left h ih
Proof state after:
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
h₂ : z ^ k * 0 < z ^ k * z
⊢ z ^ k * z > 0
Theorem: Smt.Reconstruct.Int.pow_pos
Proof state before:
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
h₂ : z ^ k * 0 < z ^ k * z
⊢ z ^ k * z > 0
Tactic:
simp at h₂
Proof state after:
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
h₂ : 0 < z ^ k * z
⊢ z ^ k * z > 0
Theorem: Smt.Reconstruct.Int.pow_pos
Proof state before:
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
h₂ : 0 < z ^ k * z
⊢ z ^ k * z > 0
Tactic:
exact h₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.non_zero_even_pow
Proof state before:
a b c d : Int
k : Nat
z : Int
h₁ : z ≠ 0
h₂ : k % 2 = 0
⊢ z ^ k > 0
Tactic:
match Int.lt_trichotomy z 0 with
| Or.inl hneg => exact pow_neg_even hneg h₂
| Or.inr (Or.inl hzero) => rw [hzero] at h₁; simp at h₁
| Or.inr (Or.inr hpos)  => exact pow_pos hpos
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.non_zero_even_pow
Proof state before:
a b c d : Int
k : Nat
z : Int
h₁ : z ≠ 0
h₂ : k % 2 = 0
hneg : z < 0
⊢ z ^ k > 0
Tactic:
exact pow_neg_even hneg h₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.non_zero_even_pow
Proof state before:
a b c d : Int
k : Nat
z : Int
h₁ : z ≠ 0
h₂ : k % 2 = 0
hzero : z = 0
⊢ z ^ k > 0
Tactic:
rw [hzero] at h₁
Proof state after:
a b c d : Int
k : Nat
z : Int
h₁ : 0 ≠ 0
h₂ : k % 2 = 0
hzero : z = 0
⊢ z ^ k > 0
Theorem: Smt.Reconstruct.Int.non_zero_even_pow
Proof state before:
a b c d : Int
k : Nat
z : Int
h₁ : 0 ≠ 0
h₂ : k % 2 = 0
hzero : z = 0
⊢ z ^ k > 0
Tactic:
simp at h₁
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.non_zero_even_pow
Proof state before:
a b c d : Int
k : Nat
z : Int
h₁ : z ≠ 0
h₂ : k % 2 = 0
hpos : 0 < z
⊢ z ^ k > 0
Tactic:
exact pow_pos hpos
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.combine_signs₁
Proof state before:
a b c d : Int
⊢ a > 0 → b > 0 → b * a > 0
Tactic:
intros h₁ h₂
Proof state after:
a b c d : Int
h₁ : a > 0
h₂ : b > 0
⊢ b * a > 0
Theorem: Smt.Reconstruct.Int.combine_signs₁
Proof state before:
a b c d : Int
h₁ : a > 0
h₂ : b > 0
⊢ b * a > 0
Tactic:
have h := Int.mul_lt_mul_of_pos_left h₁ h₂
Proof state after:
a b c d : Int
h₁ : a > 0
h₂ : b > 0
h : b * 0 < b * a
⊢ b * a > 0
Theorem: Smt.Reconstruct.Int.combine_signs₁
Proof state before:
a b c d : Int
h₁ : a > 0
h₂ : b > 0
h : b * 0 < b * a
⊢ b * a > 0
Tactic:
simp at h
Proof state after:
a b c d : Int
h₁ : a > 0
h₂ : b > 0
h : 0 < b * a
⊢ b * a > 0
Theorem: Smt.Reconstruct.Int.combine_signs₁
Proof state before:
a b c d : Int
h₁ : a > 0
h₂ : b > 0
h : 0 < b * a
⊢ b * a > 0
Tactic:
exact h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.combine_signs₂
Proof state before:
a b c d : Int
⊢ a > 0 → b < 0 → b * a < 0
Tactic:
intros h₁ h₂
Proof state after:
a b c d : Int
h₁ : a > 0
h₂ : b < 0
⊢ b * a < 0
Theorem: Smt.Reconstruct.Int.combine_signs₂
Proof state before:
a b c d : Int
h₁ : a > 0
h₂ : b < 0
⊢ b * a < 0
Tactic:
have h := Int.mul_lt_mul_of_pos_right h₂ h₁
Proof state after:
a b c d : Int
h₁ : a > 0
h₂ : b < 0
h : b * a < 0 * a
⊢ b * a < 0