internlm/Lean-Github huggingface dataset:
Theorem: Smt.Reconstruct.Arith.powPos
Proof state before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
h₂ : 0 < z * z ^ k'
⊢ z * z ^ k' > 0
Tactic:
exact h₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.nonZeroEvenPow
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
⊢ ∀ {k : ℕ} {z : α}, z ≠ 0 → Even k → z ^ k > 0
Tactic:
intros k z h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z ≠ 0
h₂ : Even k
⊢ z ^ k > 0
Theorem: Smt.Reconstruct.Arith.nonZeroEvenPow
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z ≠ 0
h₂ : Even k
⊢ z ^ k > 0
Tactic:
match lt_trichotomy z 0 with
| Or.inl zNeg => exact powNegEven zNeg h₂
| Or.inr (Or.inl zZero) => rw [zZero] at h₁; simp at h₁
| Or.inr (Or.inr zPos)  => exact powPos zPos
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.nonZeroEvenPow
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z ≠ 0
h₂ : Even k
zNeg : z < 0
⊢ z ^ k > 0
Tactic:
exact powNegEven zNeg h₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.nonZeroEvenPow
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z ≠ 0
h₂ : Even k
zZero : z = 0
⊢ z ^ k > 0
Tactic:
rw [zZero] at h₁
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : 0 ≠ 0
h₂ : Even k
zZero : z = 0
⊢ z ^ k > 0
Theorem: Smt.Reconstruct.Arith.nonZeroEvenPow
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : 0 ≠ 0
h₂ : Even k
zZero : z = 0
⊢ z ^ k > 0
Tactic:
simp at h₁
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.nonZeroEvenPow
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z ≠ 0
h₂ : Even k
zPos : 0 < z
⊢ z ^ k > 0
Tactic:
exact powPos zPos
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.combineSigns₁
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
⊢ a > 0 → b > 0 → b * a > 0
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b > 0
⊢ b * a > 0
Theorem: Smt.Reconstruct.Arith.combineSigns₁
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b > 0
⊢ b * a > 0
Tactic:
have h := mul_lt_mul_of_pos_left h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b > 0
h : b * 0 < b * a
⊢ b * a > 0
Theorem: Smt.Reconstruct.Arith.combineSigns₁
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b > 0
h : b * 0 < b * a
⊢ b * a > 0
Tactic:
simp at h
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b > 0
h : 0 < b * a
⊢ b * a > 0
Theorem: Smt.Reconstruct.Arith.combineSigns₁
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b > 0
h : 0 < b * a
⊢ b * a > 0
Tactic:
exact h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.combineSigns₂
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
⊢ a > 0 → b < 0 → b * a < 0
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b < 0
⊢ b * a < 0
Theorem: Smt.Reconstruct.Arith.combineSigns₂
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b < 0
⊢ b * a < 0
Tactic:
have h := mul_lt_mul_of_pos_right h₂ h₁
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b < 0
h : b * a < 0 * a
⊢ b * a < 0
Theorem: Smt.Reconstruct.Arith.combineSigns₂
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b < 0
h : b * a < 0 * a
⊢ b * a < 0
Tactic:
simp at h
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b < 0
h : b * a < 0
⊢ b * a < 0
Theorem: Smt.Reconstruct.Arith.combineSigns₂
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b < 0
h : b * a < 0
⊢ b * a < 0
Tactic:
exact h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.combineSigns₃
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
⊢ a < 0 → b > 0 → b * a < 0
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a < 0
h₂ : b > 0
⊢ b * a < 0
Theorem: Smt.Reconstruct.Arith.combineSigns₃
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a < 0
h₂ : b > 0
⊢ b * a < 0
Tactic:
have h := mul_lt_mul_of_pos_left h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a < 0
h₂ : b > 0
h : b * a < b * 0
⊢ b * a < 0
Theorem: Smt.Reconstruct.Arith.combineSigns₃
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a < 0
h₂ : b > 0
h : b * a < b * 0
⊢ b * a < 0
Tactic:
simp at h
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a < 0
h₂ : b > 0
h : b * a < 0
⊢ b * a < 0
Theorem: Smt.Reconstruct.Arith.combineSigns₃
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a < 0
h₂ : b > 0
h : b * a < 0
⊢ b * a < 0
Tactic:
exact h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.combineSigns₄
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
⊢ a < 0 → b < 0 → b * a > 0
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a < 0
h₂ : b < 0
⊢ b * a > 0
Theorem: Smt.Reconstruct.Arith.combineSigns₄
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a < 0
h₂ : b < 0
⊢ b * a > 0
Tactic:
have h := mul_lt_mul_of_neg_left h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a < 0
h₂ : b < 0
h : b * 0 < b * a
⊢ b * a > 0
Theorem: Smt.Reconstruct.Arith.combineSigns₄
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a < 0
h₂ : b < 0
h : b * 0 < b * a
⊢ b * a > 0
Tactic:
simp at h
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a < 0
h₂ : b < 0
h : 0 < b * a
⊢ b * a > 0
Theorem: Smt.Reconstruct.Arith.combineSigns₄
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a < 0
h₂ : b < 0
h : 0 < b * a
⊢ b * a > 0
Tactic:
exact h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castPos
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
⊢ ∀ a > 0, a > 0
Tactic:
intros a h
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a✝ b : α
a : ℤ
h : a > 0
⊢ a > 0
Theorem: Smt.Reconstruct.Arith.castPos
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a✝ b : α
a : ℤ
h : a > 0
⊢ a > 0
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castNeg
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
⊢ ∀ a < 0, a < 0
Tactic:
intros a h
Proof state after:
α : Type
inst✝ : LinearOrderedCommRing α
a✝ b : α
a : ℤ
h : a < 0
⊢ a < 0
Theorem: Smt.Reconstruct.Arith.castNeg
Proof state before:
α : Type
inst✝ : LinearOrderedCommRing α
a✝ b : α
a : ℤ
h : a < 0
⊢ a < 0
Tactic:
simp [h]
Proof state after:
no goals
Theorem: density
Proof state before:
x z : ℝ
⊢ x < z → ∃ y, x < y ∧ y < z
Tactic:
sorry
Proof state after:
no goals
Theorem: Smt.Arith.lt_eq_sub_lt_zero
Proof state before:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ (a < b) = (a - b < 0)
Tactic:
simp only [sub_neg]
Proof state after:
no goals
Theorem: Smt.Arith.le_eq_sub_le_zero
Proof state before:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ (a ≤ b) = (a - b ≤ 0)
Tactic:
simp only [tsub_le_iff_right, zero_add]
Proof state after:
no goals
Theorem: Smt.Arith.eq_eq_sub_eq_zero
Proof state before:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ (a = b) = (a - b = 0)
Tactic:
simp only [sub_eq_zero]
Proof state after:
no goals
Theorem: Smt.Arith.ge_eq_sub_ge_zero
Proof state before:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ (a ≥ b) = (a - b ≥ 0)
Tactic:
simp only [ge_iff_le, sub_nonneg]
Proof state after:
no goals
Theorem: Smt.Arith.gt_eq_sub_gt_zero
Proof state before:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ (a > b) = (a - b > 0)
Tactic:
simp only [gt_iff_lt, sub_pos]
Proof state after:
no goals
Theorem: Smt.Arith.lt_of_sub_eq
Proof 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_lt_mul_left hc]
Proof 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₂)
Theorem: Smt.Arith.lt_of_sub_eq
Proof 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 [lt_eq_sub_lt_zero, @lt_eq_sub_lt_zero _ _ b₁, ← this hc₁, ← this hc₂, h]
Proof state after:
no goals
Theorem: Smt.Arith.lt_of_sub_eq
Proof 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_lt_mul_left hc]
Proof state after:
no goals
Theorem: Smt.Arith.le_of_sub_eq
Proof 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_le_mul_left hc]
Proof 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₂)
Theorem: Smt.Arith.le_of_sub_eq
Proof 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 [le_eq_sub_le_zero, @le_eq_sub_le_zero _ _ b₁, ← this hc₁, ← this hc₂, h]
Proof state after:
no goals
Theorem: Smt.Arith.le_of_sub_eq
Proof 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_le_mul_left hc]
Proof state after:
no goals
Theorem: Smt.Arith.eq_of_sub_eq
Proof 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)]
Proof 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₂)
Theorem: Smt.Arith.eq_of_sub_eq
Proof 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]
Proof state after:
no goals
Theorem: Smt.Arith.eq_of_sub_eq
Proof 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)]
Proof state after:
no goals
Theorem: Smt.Arith.ge_of_sub_eq
Proof 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, ge_iff_le, mul_le_mul_left hc]
Proof 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₂)
Theorem: Smt.Arith.ge_of_sub_eq
Proof 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 [ge_eq_sub_ge_zero, @ge_eq_sub_ge_zero _ _ b₁, ← this hc₁, ← this hc₂, h]
Proof state after:
no goals
Theorem: Smt.Arith.ge_of_sub_eq
Proof 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, ge_iff_le, mul_le_mul_left hc]
Proof state after:
no goals
Theorem: Smt.Arith.gt_of_sub_eq
Proof 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, gt_iff_lt, mul_lt_mul_left hc]
Proof 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₂)
Theorem: Smt.Arith.gt_of_sub_eq
Proof 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 [gt_eq_sub_gt_zero, @gt_eq_sub_gt_zero _ _ b₁, ← this hc₁, ← this hc₂, h]
Proof state after:
no goals
Theorem: Smt.Arith.gt_of_sub_eq
Proof 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, gt_iff_lt, mul_lt_mul_left hc]
Proof state after:
no goals
Theorem: inverse
Proof state before:
x : ℝ
⊢ x ≠ 0 → ∃ y, x * y = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: modus_tollens
Proof state before:
p q : Bool
⊢ (!q) = true → (p = true → q = true) → (!p) = true
Tactic:
intro hnq hpq
Proof state after:
p q : Bool
hnq : (!q) = true
hpq : p = true → q = true
⊢ (!p) = true
Theorem: modus_tollens
Proof state before:
p q : Bool
hnq : (!q) = true
hpq : p = true → q = true
⊢ (!p) = true
Tactic:
cases p <;> simp_all
Proof state after:
no goals
Theorem: verum
Proof state before:
⊢ true = true
Tactic:
simp_all
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.resolution_thm
Proof state before:
⊢ ∀ {A B C : Prop}, A ∨ B → ¬A ∨ C → B ∨ C
Tactic:
intros A B C h₁ h₂
Proof state after:
A B C : Prop
h₁ : A ∨ B
h₂ : ¬A ∨ C
⊢ B ∨ C
Theorem: Smt.Reconstruct.Prop.resolution_thm
Proof state before:
A B C : Prop
h₁ : A ∨ B
h₂ : ¬A ∨ C
⊢ B ∨ C
Tactic:
cases h₁ with
| inl ap => cases h₂ with
            | inl nap => exact (False.elim (nap ap))
            | inr cp  => exact (Or.inr cp)
| inr bp => exact (Or.inl bp)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.resolution_thm
Proof state before:
case inl
A B C : Prop
h₂ : ¬A ∨ C
ap : A
⊢ B ∨ C
Tactic:
cases h₂ with
| inl nap => exact (False.elim (nap ap))
| inr cp  => exact (Or.inr cp)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.resolution_thm
Proof state before:
case inl.inl
A B C : Prop
ap : A
nap : ¬A
⊢ B ∨ C
Tactic:
exact (False.elim (nap ap))
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.resolution_thm
Proof state before:
case inl.inr
A B C : Prop
ap : A
cp : C
⊢ B ∨ C
Tactic:
exact (Or.inr cp)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.resolution_thm
Proof state before:
case inr
A B C : Prop
h₂ : ¬A ∨ C
bp : B
⊢ B ∨ C
Tactic:
exact (Or.inl bp)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.flipped_resolution_thm
Proof state before:
⊢ ∀ {A B C : Prop}, ¬A ∨ B → A ∨ C → B ∨ C
Tactic:
intros A B C h₁ h₂
Proof state after:
A B C : Prop
h₁ : ¬A ∨ B
h₂ : A ∨ C
⊢ B ∨ C
Theorem: Smt.Reconstruct.Prop.flipped_resolution_thm
Proof state before:
A B C : Prop
h₁ : ¬A ∨ B
h₂ : A ∨ C
⊢ B ∨ C
Tactic:
cases h₁ with
| inl nap => cases h₂ with
             | inl ap => exact False.elim (nap ap)
             | inr cp => exact (Or.inr cp)
| inr bp => exact (Or.inl bp)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.flipped_resolution_thm
Proof state before:
case inl
A B C : Prop
h₂ : A ∨ C
nap : ¬A
⊢ B ∨ C
Tactic:
cases h₂ with
| inl ap => exact False.elim (nap ap)
| inr cp => exact (Or.inr cp)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.flipped_resolution_thm
Proof state before:
case inl.inl
A B C : Prop
nap : ¬A
ap : A
⊢ B ∨ C
Tactic:
exact False.elim (nap ap)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.flipped_resolution_thm
Proof state before:
case inl.inr
A B C : Prop
nap : ¬A
cp : C
⊢ B ∨ C
Tactic:
exact (Or.inr cp)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.flipped_resolution_thm
Proof state before:
case inr
A B C : Prop
h₂ : A ∨ C
bp : B
⊢ B ∨ C
Tactic:
exact (Or.inl bp)
Proof state after:
no goals
Theorem: Nat.mod_two_ne_zero
Proof state before:
n : Nat
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Tactic:
cases Nat.mod_two_eq_zero_or_one n <;> rename_i h <;> simp [h]
Proof state after:
no goals
Theorem: Nat.even_add
Proof state before:
m n : Nat
⊢ (m + n) % 2 = 0 ↔ (m % 2 = 0 ↔ n % 2 = 0)
Tactic:
cases Nat.mod_two_eq_zero_or_one m <;> rename_i h₁ <;> cases Nat.mod_two_eq_zero_or_one n <;> rename_i h₂ <;>
  simp [h₁, h₂, Nat.add_mod]
Proof state after:
no goals
Theorem: Nat.even_add_one
Proof state before:
n : Nat
⊢ (n + 1) % 2 = 0 ↔ n % 2 ≠ 0
Tactic:
simp [Nat.even_add]
Proof state after:
no goals
Theorem: Int.mul_lt_mul_left
Proof state before:
c x y : Int
hc : c > 0
⊢ (c * x < c * y) = (x < y)
Tactic:
apply propext
Proof state after:
case a
c x y : Int
hc : c > 0
⊢ c * x < c * y ↔ x < y
Theorem: Int.mul_lt_mul_left
Proof state before:
case a
c x y : Int
hc : c > 0
⊢ c * x < c * y ↔ x < y
Tactic:
constructor
Proof state after:
case a.mp
c x y : Int
hc : c > 0
⊢ c * x < c * y → x < y

case a.mpr
c x y : Int
hc : c > 0
⊢ x < y → c * x < c * y
Theorem: Int.mul_lt_mul_left
Proof state before:
case a.mp
c x y : Int
hc : c > 0
⊢ c * x < c * y → x < y
Tactic:
apply Int.lt_of_mul_lt_mul_left (h := Int.le_of_lt hc)
Proof state after:
no goals
Theorem: Int.mul_lt_mul_left
Proof state before:
case a.mpr
c x y : Int
hc : c > 0
⊢ x < y → c * x < c * y
Tactic:
apply Int.mul_lt_mul_of_pos_left (h₂ := hc)
Proof state after:
no goals
Theorem: Int.mul_le_mul_left
Proof state before:
c x y : Int
hc : c > 0
⊢ (c * x ≤ c * y) = (x ≤ y)
Tactic:
apply propext
Proof state after:
case a
c x y : Int
hc : c > 0
⊢ c * x ≤ c * y ↔ x ≤ y
Theorem: Int.mul_le_mul_left
Proof state before:
case a
c x y : Int
hc : c > 0
⊢ c * x ≤ c * y ↔ x ≤ y
Tactic:
constructor
Proof state after:
case a.mp
c x y : Int
hc : c > 0
⊢ c * x ≤ c * y → x ≤ y

case a.mpr
c x y : Int
hc : c > 0
⊢ x ≤ y → c * x ≤ c * y
Theorem: Int.mul_le_mul_left
Proof state before:
case a.mp
c x y : Int
hc : c > 0
⊢ c * x ≤ c * y → x ≤ y
Tactic:
apply le_of_mul_le_mul_left (h := hc)
Proof state after:
no goals
Theorem: Int.mul_le_mul_left
Proof state before:
case a.mpr
c x y : Int
hc : c > 0
⊢ x ≤ y → c * x ≤ c * y
Tactic:
apply Int.mul_le_mul_of_nonneg_left (h₂ := Int.le_of_lt hc)
Proof state after:
no goals
Theorem: Int.mul_eq_zero_left
Proof state before:
x y : Int
hx : x ≠ 0
hxy : x * y = 0
⊢ y = 0
Tactic:
rewrite [Int.mul_eq_zero] at hxy
Proof state after:
x y : Int
hx : x ≠ 0
hxy : x = 0 ∨ y = 0
⊢ y = 0
Theorem: Int.mul_eq_zero_left
Proof state before:
x y : Int
hx : x ≠ 0
hxy : x = 0 ∨ y = 0
⊢ y = 0
Tactic:
exact hxy.resolve_left hx
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.or_implies_left
Proof state before:
a b c d : Int
p q : Prop
hpq : p ∨ q
hnq : ¬q
⊢ p
Tactic:
cases hpq with
| inl hp => exact hp
| inr hq => exact False.elim (hnq hq)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.or_implies_left
Proof state before:
case inl
a b c d : Int
p q : Prop
hnq : ¬q
hp : p
⊢ p
Tactic:
exact hp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.or_implies_left
Proof state before:
case inr
a b c d : Int
p q : Prop
hnq : ¬q
hq : q
⊢ p
Tactic:
exact False.elim (hnq hq)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.or_implies_right
Proof state before:
a b c d : Int
p q : Prop
hpq : p ∨ q
hnp : ¬p
⊢ q
Tactic:
cases hpq with
| inl hp => exact False.elim (hnp hp)
| inr hq => exact hq
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.or_implies_right
Proof state before:
case inl
a b c d : Int
p q : Prop
hnp : ¬p
hp : p
⊢ q
Tactic:
exact False.elim (hnp hp)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.or_implies_right
Proof state before:
case inr
a b c d : Int
p q : Prop
hnp : ¬p
hq : q
⊢ q
Tactic:
exact hq
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:
have r₁: a + c < a + d := Int.add_lt_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_lt_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.lt_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:
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_lt_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.lt_of_le_of_lt 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_lt_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:
have r₁ : a + c < a + d := Int.add_lt_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.lt_of_lt_of_le r₁ r₂
Proof state after:
no goals