internlm/Lean-Github huggingface dataset:
Theorem: Smt.Reconstruct.Int.combine_signs₂
Proof state before:
a b c d : Int
h₁ : a > 0
h₂ : b < 0
h : b * a < 0 * a
⊢ b * a < 0
Tactic:
simp at h
Proof state after:
a b c d : Int
h₁ : a > 0
h₂ : b < 0
h : b * a < 0
⊢ 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 * a < 0
⊢ 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_left h₁ h₂
Proof state after:
a b c d : Int
h₁ : a < 0
h₂ : b > 0
h : b * a < 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
h : b * a < b * 0
⊢ b * a < 0
Tactic:
simp at h
Proof state after:
a b c d : Int
h₁ : a < 0
h₂ : b > 0
h : b * a < 0
⊢ 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 * a < 0
⊢ 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_neg_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.arith_mul_pos_eq
Proof state before:
a b c d : Int
⊢ c > 0 ∧ a = b → c * a = c * b
Tactic:
intros h
Proof state after:
a b c d : Int
h : c > 0 ∧ a = b
⊢ c * a = c * b
Theorem: Smt.Reconstruct.Int.arith_mul_pos_eq
Proof state before:
a b c d : Int
h : c > 0 ∧ a = b
⊢ c * a = c * b
Tactic:
rw [h.2]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Int.arith_mul_neg_eq
Proof state before:
a b c d : Int
⊢ c < 0 ∧ a = b → c * a = c * b
Tactic:
intros h
Proof state after:
a b c d : Int
h : c < 0 ∧ a = b
⊢ c * a = c * b
Theorem: Smt.Reconstruct.Int.arith_mul_neg_eq
Proof state before:
a b c d : Int
h : c < 0 ∧ a = b
⊢ c * a = c * b
Tactic:
rw [h.2]
Proof state after:
no goals
Theorem: cong
Proof state before:
p q : Bool
f : Bool → Bool
⊢ (p == q) = true → (f p == f q) = true
Tactic:
cases p <;> cases q <;> cases f true <;> cases f false <;> simp_all
Proof state after:
no goals
Theorem: conjunction
Proof state before:
p q : Bool
⊢ p = true → q = true → (p && q) = true
Tactic:
simp_all
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithTransSineSymmetry
Proof state before:
⊢ ∀ (t : ℝ), t.sin + (-t).sin = 0
Tactic:
intro t
Proof state after:
t : ℝ
⊢ t.sin + (-t).sin = 0
Theorem: Smt.Reconstruct.Arith.arithTransSineSymmetry
Proof state before:
t : ℝ
⊢ t.sin + (-t).sin = 0
Tactic:
rw [sin_neg]
Proof state after:
t : ℝ
⊢ t.sin + -t.sin = 0
Theorem: Smt.Reconstruct.Arith.arithTransSineSymmetry
Proof state before:
t : ℝ
⊢ t.sin + -t.sin = 0
Tactic:
simp
Proof state after:
no goals
Theorem: falsum
Proof state before:
⊢ (!false) = true
Tactic:
simp_all
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithTransSineTangentPi
Proof state before:
pi : ℝ
⊢ ∀ (t : ℝ), (t > -pi → t.sin > -pi - t) ∧ (t < pi → t.sin < pi - t)
Tactic:
intro t
Proof state after:
pi t : ℝ
⊢ (t > -pi → t.sin > -pi - t) ∧ (t < pi → t.sin < pi - t)
Theorem: Smt.Reconstruct.Arith.arithTransSineTangentPi
Proof state before:
pi t : ℝ
⊢ (t > -pi → t.sin > -pi - t) ∧ (t < pi → t.sin < pi - t)
Tactic:
apply And.intro
Proof state after:
case left
pi t : ℝ
⊢ t > -pi → t.sin > -pi - t

case right
pi t : ℝ
⊢ t < pi → t.sin < pi - t
Theorem: Smt.Reconstruct.Arith.arithTransSineTangentPi
Proof state before:
case left
pi t : ℝ
⊢ t > -pi → t.sin > -pi - t
Tactic:
intro ht
Proof state after:
case left
pi t : ℝ
ht : t > -pi
⊢ t.sin > -pi - t
Theorem: Smt.Reconstruct.Arith.arithTransSineTangentPi
Proof state before:
case left
pi t : ℝ
ht : t > -pi
⊢ t.sin > -pi - t
Tactic:
admit
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithTransSineTangentPi
Proof state before:
case right
pi t : ℝ
⊢ t < pi → t.sin < pi - t
Tactic:
intro ht
Proof state after:
case right
pi t : ℝ
ht : t < pi
⊢ t.sin < pi - t
Theorem: Smt.Reconstruct.Arith.arithTransSineTangentPi
Proof state before:
case right
pi t : ℝ
ht : t < pi
⊢ t.sin < pi - t
Tactic:
admit
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithTransExpZero
Proof state before:
t : ℝ
⊢ t = 0 ↔ t.exp = 1
Tactic:
apply Iff.intro
Proof state after:
case mp
t : ℝ
⊢ t = 0 → t.exp = 1

case mpr
t : ℝ
⊢ t.exp = 1 → t = 0
Theorem: Smt.Reconstruct.Arith.arithTransExpZero
Proof state before:
case mp
t : ℝ
⊢ t = 0 → t.exp = 1
Tactic:
intro h
Proof state after:
case mp
t : ℝ
h : t = 0
⊢ t.exp = 1
Theorem: Smt.Reconstruct.Arith.arithTransExpZero
Proof state before:
case mp
t : ℝ
h : t = 0
⊢ t.exp = 1
Tactic:
rw [h]
Proof state after:
case mp
t : ℝ
h : t = 0
⊢ Real.exp 0 = 1
Theorem: Smt.Reconstruct.Arith.arithTransExpZero
Proof state before:
case mp
t : ℝ
h : t = 0
⊢ Real.exp 0 = 1
Tactic:
simp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithTransExpZero
Proof state before:
case mpr
t : ℝ
⊢ t.exp = 1 → t = 0
Tactic:
intro h
Proof state after:
case mpr
t : ℝ
h : t.exp = 1
⊢ t = 0
Theorem: Smt.Reconstruct.Arith.arithTransExpZero
Proof state before:
case mpr
t : ℝ
h : t.exp = 1
⊢ t = 0
Tactic:
simp at h
Proof state after:
case mpr
t : ℝ
h : t = 0
⊢ t = 0
Theorem: Smt.Reconstruct.Arith.arithTransExpZero
Proof state before:
case mpr
t : ℝ
h : t = 0
⊢ t = 0
Tactic:
assumption
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orFalse
Proof state before:
⊢ ∀ {A : Prop}, A ∨ False → A
Tactic:
intros a h
Proof state after:
a : Prop
h : a ∨ False
⊢ a
Theorem: Smt.Reconstruct.Prop.orFalse
Proof state before:
a : Prop
h : a ∨ False
⊢ a
Tactic:
cases h with
| inl ha => exact ha
| inr ff => exact False.elim ff
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orFalse
Proof state before:
case inl
a : Prop
ha : a
⊢ a
Tactic:
exact ha
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orFalse
Proof state before:
case inr
a : Prop
ff : False
⊢ a
Tactic:
exact False.elim ff
Proof state after:
no goals
Theorem: disjunctive_syllogism
Proof state before:
p q : Bool
⊢ (p || q) = true → (!p) = true → q = true
Tactic:
intro hpq hnp
Proof state after:
p q : Bool
hpq : (p || q) = true
hnp : (!p) = true
⊢ q = true
Theorem: disjunctive_syllogism
Proof state before:
p q : Bool
hpq : (p || q) = true
hnp : (!p) = true
⊢ q = true
Tactic:
cases p <;> simp_all
Proof state after:
no goals
Theorem: triv
Proof state before:
⊢ Nat.zero + Nat.zero.succ = Nat.zero.succ
Tactic:
simp_all
Proof state after:
no goals
Theorem: contains
Proof state before:
⊢ "a".contains 'a' = true
Tactic:
sorry
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.trichotomy₁
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
⊢ ¬a < b → ¬a = b → a > b
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
⊢ a > b
Theorem: Smt.Reconstruct.Arith.trichotomy₁
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
⊢ a > b
Tactic:
have tr := lt_trichotomy a b
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
tr : a < b ∨ a = b ∨ b < a
⊢ a > b
Theorem: Smt.Reconstruct.Arith.trichotomy₁
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
tr : a < b ∨ a = b ∨ b < a
⊢ a > b
Tactic:
exact (orImplies₃ ((orImplies₃ tr) h₁)) h₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.trichotomy₂
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
⊢ ¬a = b → ¬a < b → a > b
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a = b
h₂ : ¬a < b
⊢ a > b
Theorem: Smt.Reconstruct.Arith.trichotomy₂
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a = b
h₂ : ¬a < b
⊢ a > b
Tactic:
have tr := lt_trichotomy a b
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a = b
h₂ : ¬a < b
tr : a < b ∨ a = b ∨ b < a
⊢ a > b
Theorem: Smt.Reconstruct.Arith.trichotomy₂
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a = b
h₂ : ¬a < b
tr : a < b ∨ a = b ∨ b < a
⊢ a > b
Tactic:
exact (orImplies₃ ((orImplies₃ tr) h₂)) h₁
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.trichotomy₃
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
⊢ ¬a < b → ¬a > b → a = b
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
⊢ a = b
Theorem: Smt.Reconstruct.Arith.trichotomy₃
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
⊢ a = b
Tactic:
have tr := lt_trichotomy a b
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b
Theorem: Smt.Reconstruct.Arith.trichotomy₃
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b
Tactic:
have tr': a < b ∨ b < a ∨ a = b  := by permutateOr tr, [0, 2, 1]
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
tr' : a < b ∨ b < a ∨ a = b
⊢ a = b
Theorem: Smt.Reconstruct.Arith.trichotomy₃
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
tr' : a < b ∨ b < a ∨ a = b
⊢ a = b
Tactic:
exact (orImplies₃ ((orImplies₃ tr') h₁)) h₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.trichotomy₃
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
⊢ a < b ∨ b < a ∨ a = b
Tactic:
permutateOr tr, [0, 2, 1]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.trichotomy₄
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
⊢ ¬a > b → ¬a < b → a = b
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a < b
⊢ a = b
Theorem: Smt.Reconstruct.Arith.trichotomy₄
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a < b
⊢ a = b
Tactic:
have tr := lt_trichotomy a b
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a < b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b
Theorem: Smt.Reconstruct.Arith.trichotomy₄
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a < b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b
Tactic:
have tr': a < b ∨ b < a ∨ a = b  := by permutateOr tr, [0, 2, 1]
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a < b
tr : a < b ∨ a = b ∨ b < a
tr' : a < b ∨ b < a ∨ a = b
⊢ a = b
Theorem: Smt.Reconstruct.Arith.trichotomy₄
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a < b
tr : a < b ∨ a = b ∨ b < a
tr' : a < b ∨ b < a ∨ a = b
⊢ a = b
Tactic:
exact (orImplies₃ ((orImplies₃ tr') h₂)) h₁
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.trichotomy₄
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a < b
tr : a < b ∨ a = b ∨ b < a
⊢ a < b ∨ b < a ∨ a = b
Tactic:
permutateOr tr, [0, 2, 1]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.trichotomy₅
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
⊢ ¬a = b → ¬a > b → a < b
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a = b
h₂ : ¬a > b
⊢ a < b
Theorem: Smt.Reconstruct.Arith.trichotomy₅
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a = b
h₂ : ¬a > b
⊢ a < b
Tactic:
have tr := lt_trichotomy a b
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a = b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
⊢ a < b
Theorem: Smt.Reconstruct.Arith.trichotomy₅
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a = b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
⊢ a < b
Tactic:
have tr': a = b ∨ b < a ∨ a < b  := by permutateOr tr, [1, 2, 0]
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a = b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
tr' : a = b ∨ b < a ∨ a < b
⊢ a < b
Theorem: Smt.Reconstruct.Arith.trichotomy₅
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a = b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
tr' : a = b ∨ b < a ∨ a < b
⊢ a < b
Tactic:
exact (orImplies₃ ((orImplies₃ tr') h₁)) h₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.trichotomy₅
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a = b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b ∨ b < a ∨ a < b
Tactic:
permutateOr tr, [1, 2, 0]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.trichotomy₆
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
⊢ ¬a > b → ¬a = b → a < b
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a = b
⊢ a < b
Theorem: Smt.Reconstruct.Arith.trichotomy₆
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a = b
⊢ a < b
Tactic:
have tr := lt_trichotomy a b
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a = b
tr : a < b ∨ a = b ∨ b < a
⊢ a < b
Theorem: Smt.Reconstruct.Arith.trichotomy₆
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a = b
tr : a < b ∨ a = b ∨ b < a
⊢ a < b
Tactic:
have tr' : a = b ∨ b < a ∨ a < b := by permutateOr tr, [1, 2, 0]
Proof state after:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a = b
tr : a < b ∨ a = b ∨ b < a
tr' : a = b ∨ b < a ∨ a < b
⊢ a < b
Theorem: Smt.Reconstruct.Arith.trichotomy₆
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a = b
tr : a < b ∨ a = b ∨ b < a
tr' : a = b ∨ b < a ∨ a < b
⊢ a < b
Tactic:
exact (orImplies₃ ((orImplies₃ tr') h₂)) h₁
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.trichotomy₆
Proof state before:
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a > b
h₂ : ¬a = b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b ∨ b < a ∨ a < b
Tactic:
permutateOr tr, [1, 2, 0]
Proof state after:
no goals
Theorem: BitVec.adcb_eq_adcb'
Proof state before:
⊢ adcb = adcb'
Tactic:
funext x y c
Proof state after:
case h.h.h
x y c : Bool
⊢ adcb x y c = adcb' x y c
Theorem: BitVec.adcb_eq_adcb'
Proof state before:
case h.h.h
x y c : Bool
⊢ adcb x y c = adcb' x y c
Tactic:
cases x <;> cases y <;> cases c <;> rfl
Proof state after:
no goals
Theorem: BitVec.adc_eq_adc'
Proof state before:
⊢ @adc = @adc'
Tactic:
funext x y c
Proof state after:
case h.h.h
x : Nat
y c : BitVec x
⊢ y.adc c = y.adc' c
Theorem: BitVec.adc_eq_adc'
Proof state before:
case h.h.h
x : Nat
y c : BitVec x
⊢ y.adc c = y.adc' c
Tactic:
simp only [adc, adc', adcb_eq_adcb']
Proof state after:
no goals
Theorem: BitVec.add_eq_adc'
Proof state before:
w : Nat
x y : BitVec w
⊢ x + y = (x.adc' y false).snd
Tactic:
rw [add_eq_adc, adc_eq_adc']
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithTransSineBounds
Proof state before:
⊢ ∀ (t : ℝ), t.sin ≤ 1 ∧ t.sin ≥ -1
Tactic:
intro t
Proof state after:
t : ℝ
⊢ t.sin ≤ 1 ∧ t.sin ≥ -1
Theorem: Smt.Reconstruct.Arith.arithTransSineBounds
Proof state before:
t : ℝ
⊢ t.sin ≤ 1 ∧ t.sin ≥ -1
Tactic:
apply And.intro
Proof state after:
case left
t : ℝ
⊢ t.sin ≤ 1

case right
t : ℝ
⊢ t.sin ≥ -1
Theorem: Smt.Reconstruct.Arith.arithTransSineBounds
Proof state before:
case left
t : ℝ
⊢ t.sin ≤ 1
Tactic:
exact sin_le_one t
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithTransSineBounds
Proof state before:
case right
t : ℝ
⊢ t.sin ≥ -1
Tactic:
exact neg_one_le_sin t
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.iteElim1
Proof state before:
c a b : Prop
hc : Decidable c
⊢ (if c then a else b) → ¬c ∨ a
Tactic:
intros h
Proof state after:
c a b : Prop
hc : Decidable c
h : if c then a else b
⊢ ¬c ∨ a
Theorem: Smt.Reconstruct.Builtin.iteElim1
Proof state before:
c a b : Prop
hc : Decidable c
h : if c then a else b
⊢ ¬c ∨ a
Tactic:
cases hc with
| isTrue hc   => exact Or.inr h
| isFalse hnc => exact Or.inl hnc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.iteElim1
Proof state before:
case isTrue
c a b : Prop
hc : c
h : if c then a else b
⊢ ¬c ∨ a
Tactic:
exact Or.inr h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.iteElim1
Proof state before:
case isFalse
c a b : Prop
hnc : ¬c
h : if c then a else b
⊢ ¬c ∨ a
Tactic:
exact Or.inl hnc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.iteElim2
Proof state before:
c a b : Prop
hc : Decidable c
⊢ (if c then a else b) → c ∨ b
Tactic:
intros h
Proof state after:
c a b : Prop
hc : Decidable c
h : if c then a else b
⊢ c ∨ b
Theorem: Smt.Reconstruct.Builtin.iteElim2
Proof state before:
c a b : Prop
hc : Decidable c
h : if c then a else b
⊢ c ∨ b
Tactic:
cases hc with
| isTrue hc   => exact Or.inl hc
| isFalse hnc => exact Or.inr h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.iteElim2
Proof state before:
case isTrue
c a b : Prop
hc : c
h : if c then a else b
⊢ c ∨ b
Tactic:
exact Or.inl hc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.iteElim2
Proof state before:
case isFalse
c a b : Prop
hnc : ¬c
h : if c then a else b
⊢ c ∨ b
Tactic:
exact Or.inr h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.notIteElim1
Proof state before:
c a b : Prop
hc : Decidable c
⊢ (¬if c then a else b) → ¬c ∨ ¬a
Tactic:
intros h
Proof state after:
c a b : Prop
hc : Decidable c
h : ¬if c then a else b
⊢ ¬c ∨ ¬a
Theorem: Smt.Reconstruct.Builtin.notIteElim1
Proof state before:
c a b : Prop
hc : Decidable c
h : ¬if c then a else b
⊢ ¬c ∨ ¬a
Tactic:
cases hc with
| isTrue hc   => exact Or.inr h
| isFalse hnc => exact Or.inl hnc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.notIteElim1
Proof state before:
case isTrue
c a b : Prop
hc : c
h : ¬if c then a else b
⊢ ¬c ∨ ¬a
Tactic:
exact Or.inr h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.notIteElim1
Proof state before:
case isFalse
c a b : Prop
hnc : ¬c
h : ¬if c then a else b
⊢ ¬c ∨ ¬a
Tactic:
exact Or.inl hnc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.notIteElim2
Proof state before:
c a b : Prop
hc : Decidable c
⊢ (¬if c then a else b) → c ∨ ¬b
Tactic:
intros h
Proof state after:
c a b : Prop
hc : Decidable c
h : ¬if c then a else b
⊢ c ∨ ¬b
Theorem: Smt.Reconstruct.Builtin.notIteElim2
Proof state before:
c a b : Prop
hc : Decidable c
h : ¬if c then a else b
⊢ c ∨ ¬b
Tactic:
cases hc with
| isTrue hc   => exact Or.inl hc
| isFalse hnc => exact Or.inr h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.notIteElim2
Proof state before:
case isTrue
c a b : Prop
hc : c
h : ¬if c then a else b
⊢ c ∨ ¬b
Tactic:
exact Or.inl hc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.notIteElim2
Proof state before:
case isFalse
c a b : Prop
hnc : ¬c
h : ¬if c then a else b
⊢ c ∨ ¬b
Tactic:
exact Or.inr h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.orImplies
Proof state before:
⊢ ∀ {p q : Prop}, (¬p → q) → p ∨ q
Tactic:
intros p q h
Proof state after:
p q : Prop
h : ¬p → q
⊢ p ∨ q
Theorem: Smt.Reconstruct.Builtin.orImplies
Proof state before:
p q : Prop
h : ¬p → q
⊢ p ∨ q
Tactic:
exact match Classical.em p with
| Or.inl pp => Or.inl pp
| Or.inr npp => match Classical.em q with
                | Or.inl pq => Or.inr pq
                | Or.inr npq => False.elim (npq (h npp))
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.notNotElim
Proof state before:
⊢ ∀ {p : Prop}, ¬¬p → p
Tactic:
intros p h
Proof state after:
p : Prop
h : ¬¬p
⊢ p
Theorem: Smt.Reconstruct.Builtin.notNotElim
Proof state before:
p : Prop
h : ¬¬p
⊢ p
Tactic:
exact match Classical.em p with
| Or.inl pp => pp
| Or.inr np => False.elim (h (λ p => np p))
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfItePos1
Proof state before:
c a b : Prop
h : Decidable c
⊢ (¬if c then a else b) ∨ ¬c ∨ a
Tactic:
apply orImplies
Proof state after:
case a
c a b : Prop
h : Decidable c
⊢ (¬¬if c then a else b) → ¬c ∨ a
Theorem: Smt.Reconstruct.Builtin.cnfItePos1
Proof state before:
case a
c a b : Prop
h : Decidable c
⊢ (¬¬if c then a else b) → ¬c ∨ a
Tactic:
intro hite
Proof state after:
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
⊢ ¬c ∨ a
Theorem: Smt.Reconstruct.Builtin.cnfItePos1
Proof state before:
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
⊢ ¬c ∨ a
Tactic:
have hite' := notNotElim hite
Proof state after:
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ ¬c ∨ a
Theorem: Smt.Reconstruct.Builtin.cnfItePos1
Proof state before:
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ ¬c ∨ a
Tactic:
match h with
| isTrue _    => exact Or.inr hite'
| isFalse hnc => exact Or.inl hnc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfItePos1
Proof state before:
c a b : Prop
h : Decidable c
h✝ : c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ ¬c ∨ a
Tactic:
exact Or.inr hite'
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfItePos1
Proof state before:
c a b : Prop
h : Decidable c
hnc : ¬c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ ¬c ∨ a
Tactic:
exact Or.inl hnc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfItePos2
Proof state before:
c a b : Prop
h : Decidable c
⊢ (¬if c then a else b) ∨ c ∨ b
Tactic:
apply orImplies
Proof state after:
case a
c a b : Prop
h : Decidable c
⊢ (¬¬if c then a else b) → c ∨ b
Theorem: Smt.Reconstruct.Builtin.cnfItePos2
Proof state before:
case a
c a b : Prop
h : Decidable c
⊢ (¬¬if c then a else b) → c ∨ b
Tactic:
intro hite
Proof state after:
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
⊢ c ∨ b
Theorem: Smt.Reconstruct.Builtin.cnfItePos2
Proof state before:
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
⊢ c ∨ b
Tactic:
have hite' := notNotElim hite
Proof state after:
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ c ∨ b
Theorem: Smt.Reconstruct.Builtin.cnfItePos2
Proof state before:
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ c ∨ b
Tactic:
match h with
| isFalse _ => exact Or.inr hite'
| isTrue hc => exact Or.inl hc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfItePos2
Proof state before:
c a b : Prop
h : Decidable c
h✝ : ¬c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ c ∨ b
Tactic:
exact Or.inr hite'
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfItePos2
Proof state before:
c a b : Prop
h : Decidable c
hc : c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ c ∨ b
Tactic:
exact Or.inl hc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfItePos3
Proof state before:
c a b : Prop
h : Decidable c
⊢ (¬if c then a else b) ∨ a ∨ b
Tactic:
apply orImplies
Proof state after:
case a
c a b : Prop
h : Decidable c
⊢ (¬¬if c then a else b) → a ∨ b
Theorem: Smt.Reconstruct.Builtin.cnfItePos3
Proof state before:
case a
c a b : Prop
h : Decidable c
⊢ (¬¬if c then a else b) → a ∨ b
Tactic:
intro hite
Proof state after:
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
⊢ a ∨ b
Theorem: Smt.Reconstruct.Builtin.cnfItePos3
Proof state before:
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
⊢ a ∨ b
Tactic:
have hite' := notNotElim hite
Proof state after:
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ a ∨ b
Theorem: Smt.Reconstruct.Builtin.cnfItePos3
Proof state before:
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ a ∨ b
Tactic:
match h with
| isFalse _ => exact Or.inr hite'
| isTrue _  => exact Or.inl hite'
Proof state after:
no goals