internlm/Lean-Github huggingface dataset:
Theorem: Smt.Reconstruct.Arith.sumBounds₆
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
⊢ a ≤ b → c = d → a + c ≤ b + d
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c = d
⊢ a + c ≤ b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₆
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c = d
⊢ a + c ≤ b + d
Tactic:
rewrite [h₂]
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c = d
⊢ a + d ≤ b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₆
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c = d
⊢ a + d ≤ b + d
Tactic:
exact add_le_add_right h₁ d
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.sumBounds₇
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
⊢ a = b → c < d → a + c < b + d
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a = b
h₂ : c < d
⊢ a + c < b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₇
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a = b
h₂ : c < d
⊢ a + c < b + d
Tactic:
rewrite [h₁]
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a = b
h₂ : c < d
⊢ b + c < b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₇
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a = b
h₂ : c < d
⊢ b + c < b + d
Tactic:
exact add_lt_add_left h₂ b
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.sumBounds₈
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
⊢ a = b → c ≤ d → a + c ≤ b + d
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a = b
h₂ : c ≤ d
⊢ a + c ≤ b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₈
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a = b
h₂ : c ≤ d
⊢ a + c ≤ b + d
Tactic:
rewrite [h₁]
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a = b
h₂ : c ≤ d
⊢ b + c ≤ b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₈
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a = b
h₂ : c ≤ d
⊢ b + c ≤ b + d
Tactic:
exact add_le_add_left h₂ b
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.sumBounds₉
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
⊢ a = b → c = d → a + c ≤ b + d
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a = b
h₂ : c = d
⊢ a + c ≤ b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₉
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a = b
h₂ : c = d
⊢ a + c ≤ b + d
Tactic:
rewrite [h₁, h₂]
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a = b
h₂ : c = d
⊢ b + d ≤ b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₉
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a = b
h₂ : c = d
⊢ b + d ≤ b + d
Tactic:
exact le_refl (b + d)
Proof state after:
no goals
Theorem: neq_zero
Proof state before:
⊢ ∀ (x : ℕ), x ≠ 0
Tactic:
admit
Proof state after:
no goals
Theorem: succ_neq_zero
Proof state before:
⊢ ∀ (x : ℕ), x + 1 ≠ 0
Tactic:
admit
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castEQ
Proof state before:
⊢ ∀ {a b : ℤ}, a = b → ↑a = ↑b
Tactic:
intros a b h
Proof state after:
a b : ℤ
h : a = b
⊢ ↑a = ↑b
Theorem: Smt.Reconstruct.Arith.castEQ
Proof state before:
a b : ℤ
h : a = b
⊢ ↑a = ↑b
Tactic:
rw [h]
Proof state after:
no goals
Theorem: empty
Proof state before:
⊢ "" = ""
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.max'_ge
Proof state before:
⊢ ∀ (x y : ℕ), x ≤ x.max' y ∧ y ≤ x.max' y
Tactic:
intro x y
Proof state after:
x y : ℕ
⊢ x ≤ x.max' y ∧ y ≤ x.max' y
Theorem: Nat.max'_ge
Proof state before:
x y : ℕ
⊢ x ≤ x.max' y ∧ y ≤ x.max' y
Tactic:
by_cases h : x ≤ y <;> simp [max', h]
Proof state after:
case neg
x y : ℕ
h : ¬x ≤ y
⊢ y ≤ x
Theorem: Nat.max'_ge
Proof state before:
case neg
x y : ℕ
h : ¬x ≤ y
⊢ y ≤ x
Tactic:
apply not_le_of_reverse_le h
Proof state after:
no goals
Theorem: Nat.max'_ge'
Proof state before:
⊢ ∀ (x y : ℕ), x ≤ x.max' y ∧ y ≤ x.max' y
Tactic:
intro x y
Proof state after:
x y : ℕ
⊢ x ≤ x.max' y ∧ y ≤ x.max' y
Theorem: Nat.max'_ge'
Proof state before:
x y : ℕ
⊢ x ≤ x.max' y ∧ y ≤ x.max' y
Tactic:
by_cases h : x ≤ y <;> simp [max', h]
Proof state after:
case neg
x y : ℕ
h : ¬x ≤ y
⊢ y ≤ x
Theorem: Nat.max'_ge'
Proof state before:
case neg
x y : ℕ
h : ¬x ≤ y
⊢ y ≤ x
Tactic:
apply not_le_of_reverse_le h
Proof state after:
no goals
Theorem: append
Proof state before:
⊢ "a" ++ "b" = "ab"
Tactic:
rfl
Proof state after:
no goals
Theorem: cong
Proof state before:
x y : ℕ
f : ℕ → ℕ
⊢ x = y → f x = f y
Tactic:
simp_all
Proof state after:
no goals
Theorem: append_eq_shl_or_2
Proof state before:
x y : BitVec 2
⊢ x ++ y = zeroExtend 4 x <<< 2#2 ||| zeroExtend 4 y
Tactic:
sorry
Proof state after:
no goals
Theorem: append_eq_shl_or_3
Proof state before:
x y : BitVec 3
⊢ x ++ y = zeroExtend 6 x <<< 3#2 ||| zeroExtend 6 y
Tactic:
sorry
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arith_mul_pos_eq
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
⊢ c > 0 ∧ a = b → c * a = c * b
Tactic:
intros h
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
h : c > 0 ∧ a = b
⊢ c * a = c * b
Theorem: Smt.Reconstruct.Arith.arith_mul_pos_eq
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
h : c > 0 ∧ a = b
⊢ c * a = c * b
Tactic:
rw [h.2]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arith_mul_neg_eq
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
⊢ c < 0 ∧ a = b → c * a = c * b
Tactic:
intros h
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
h : c < 0 ∧ a = b
⊢ c * a = c * b
Theorem: Smt.Reconstruct.Arith.arith_mul_neg_eq
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
h : c < 0 ∧ a = b
⊢ c * a = c * b
Tactic:
rw [h.2]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castLT
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
⊢ ∀ {a b : ℤ}, a < b → zToR a < zToR b
Tactic:
simp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castGTZero
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
⊢ ∀ {a : ℤ}, 0 > a → 0 > zToR a
Tactic:
simp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castLE
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
⊢ ∀ {a b : ℤ}, a ≤ b → zToR a ≤ zToR b
Tactic:
simp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castGEZero
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
⊢ ∀ {a : ℤ}, a ≤ 0 → zToR a ≤ 0
Tactic:
simp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castLTZero
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
⊢ ∀ {a : ℤ}, a > 0 → zToR a > 0
Tactic:
simp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castLEZero
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
⊢ ∀ {a : ℤ}, a ≥ 0 → zToR a ≥ 0
Tactic:
simp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castFstLT
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
⊢ 0 < a ∧ p → 0 < zToR a ∧ p
Tactic:
rintro ⟨h₁, h₂⟩
Proof state after:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
h₁ : 0 < a
h₂ : p
⊢ 0 < zToR a ∧ p
Theorem: Smt.Reconstruct.Arith.castFstLT
Proof state before:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
h₁ : 0 < a
h₂ : p
⊢ 0 < zToR a ∧ p
Tactic:
exact ⟨castLTZero h₁, h₂⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castFstLE
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
⊢ 0 ≤ a ∧ p → 0 ≤ zToR a ∧ p
Tactic:
rintro ⟨h₁, h₂⟩
Proof state after:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
h₁ : 0 ≤ a
h₂ : p
⊢ 0 ≤ zToR a ∧ p
Theorem: Smt.Reconstruct.Arith.castFstLE
Proof state before:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
h₁ : 0 ≤ a
h₂ : p
⊢ 0 ≤ zToR a ∧ p
Tactic:
exact ⟨castLEZero h₁, h₂⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castFstGT
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
⊢ 0 > a ∧ p → 0 > zToR a ∧ p
Tactic:
rintro ⟨h₁, h₂⟩
Proof state after:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
h₁ : 0 > a
h₂ : p
⊢ 0 > zToR a ∧ p
Theorem: Smt.Reconstruct.Arith.castFstGT
Proof state before:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
h₁ : 0 > a
h₂ : p
⊢ 0 > zToR a ∧ p
Tactic:
exact ⟨castGTZero h₁, h₂⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castFstGE
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
⊢ 0 ≥ a ∧ p → 0 ≥ zToR a ∧ p
Tactic:
rintro ⟨h₁, h₂⟩
Proof state after:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
h₁ : 0 ≥ a
h₂ : p
⊢ 0 ≥ zToR a ∧ p
Theorem: Smt.Reconstruct.Arith.castFstGE
Proof state before:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
h₁ : 0 ≥ a
h₂ : p
⊢ 0 ≥ zToR a ∧ p
Tactic:
exact ⟨castGEZero h₁, h₂⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castFstEQ
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
⊢ 0 = a ∧ p → 0 = zToR a ∧ p
Tactic:
rintro ⟨h₁, h₂⟩
Proof state after:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
h₁ : 0 = a
h₂ : p
⊢ 0 = zToR a ∧ p
Theorem: Smt.Reconstruct.Arith.castFstEQ
Proof state before:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
h₁ : 0 = a
h₂ : p
⊢ 0 = zToR a ∧ p
Tactic:
exact ⟨by rw [← h₁]; simp, h₂⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castFstEQ
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
h₁ : 0 = a
h₂ : p
⊢ 0 = zToR a
Tactic:
rw [← h₁]
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
h₁ : 0 = a
h₂ : p
⊢ 0 = zToR 0
Theorem: Smt.Reconstruct.Arith.castFstEQ
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b c : α
p : Prop
a : ℤ
h₁ : 0 = a
h₂ : p
⊢ 0 = zToR 0
Tactic:
simp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castSndLT
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
⊢ p ∧ a < b → p ∧ zToR a < zToR b
Tactic:
rintro ⟨h₁, h₂⟩
Proof state after:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a < b
⊢ p ∧ zToR a < zToR b
Theorem: Smt.Reconstruct.Arith.castSndLT
Proof state before:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a < b
⊢ p ∧ zToR a < zToR b
Tactic:
exact ⟨h₁, castLT h₂⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castSndLE
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
⊢ p ∧ a ≤ b → p ∧ zToR a ≤ zToR b
Tactic:
rintro ⟨h₁, h₂⟩
Proof state after:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a ≤ b
⊢ p ∧ zToR a ≤ zToR b
Theorem: Smt.Reconstruct.Arith.castSndLE
Proof state before:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a ≤ b
⊢ p ∧ zToR a ≤ zToR b
Tactic:
exact ⟨h₁, castLE h₂⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castSndGT
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
⊢ p ∧ a > b → p ∧ zToR a > zToR b
Tactic:
rintro ⟨h₁, h₂⟩
Proof state after:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a > b
⊢ p ∧ zToR a > zToR b
Theorem: Smt.Reconstruct.Arith.castSndGT
Proof state before:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a > b
⊢ p ∧ zToR a > zToR b
Tactic:
exact ⟨h₁, castLT h₂⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castSndGE
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
⊢ p ∧ a ≥ b → p ∧ zToR a ≥ zToR b
Tactic:
rintro ⟨h₁, h₂⟩
Proof state after:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a ≥ b
⊢ p ∧ zToR a ≥ zToR b
Theorem: Smt.Reconstruct.Arith.castSndGE
Proof state before:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a ≥ b
⊢ p ∧ zToR a ≥ zToR b
Tactic:
exact ⟨h₁, castLE h₂⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castSndEQ
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
⊢ p ∧ a = b → p ∧ zToR a = zToR b
Tactic:
rintro ⟨h₁, h₂⟩
Proof state after:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a = b
⊢ p ∧ zToR a = zToR b
Theorem: Smt.Reconstruct.Arith.castSndEQ
Proof state before:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a = b
⊢ p ∧ zToR a = zToR b
Tactic:
exact ⟨h₁, by rw [h₂]⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castSndEQ
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a = b
⊢ zToR a = zToR b
Tactic:
rw [h₂]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithTransExpSuperLin
Proof state before:
t : ℝ
⊢ t ≤ 0 ∨ t.exp > t + 1
Tactic:
apply orImplies
Proof state after:
case a
t : ℝ
⊢ ¬t ≤ 0 → t.exp > t + 1
Theorem: Smt.Reconstruct.Arith.arithTransExpSuperLin
Proof state before:
case a
t : ℝ
⊢ ¬t ≤ 0 → t.exp > t + 1
Tactic:
intro h
Proof state after:
case a
t : ℝ
h : ¬t ≤ 0
⊢ t.exp > t + 1
Theorem: Smt.Reconstruct.Arith.arithTransExpSuperLin
Proof state before:
case a
t : ℝ
h : ¬t ≤ 0
⊢ t.exp > t + 1
Tactic:
simp at h
Proof state after:
case a
t : ℝ
h : 0 < t
⊢ t.exp > t + 1
Theorem: Smt.Reconstruct.Arith.arithTransExpSuperLin
Proof state before:
case a
t : ℝ
h : 0 < t
⊢ t.exp > t + 1
Tactic:
exact arithTransExpSuperLin' t h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.and_assoc_eq
Proof state before:
p q r : Prop
⊢ ((p ∧ q) ∧ r) = (p ∧ q ∧ r)
Tactic:
simp [and_assoc]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.and_comm_eq
Proof state before:
p q : Prop
⊢ (p ∧ q) = (q ∧ p)
Tactic:
simp [and_comm]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.or_assoc_eq
Proof state before:
a b c : Prop
⊢ ((a ∨ b) ∨ c) = (a ∨ b ∨ c)
Tactic:
simp [or_assoc]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.or_comm_eq
Proof state before:
p q : Prop
⊢ (p ∨ q) = (q ∨ p)
Tactic:
simp [or_comm]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.exp_contDiffOn
Proof state before:
⊢ ∀ (d : ℕ) (l r : ℝ), ContDiffOn ℝ (↑d) Real.exp (Set.Icc l r)
Tactic:
intros d l r
Proof state after:
d : ℕ
l r : ℝ
⊢ ContDiffOn ℝ (↑d) Real.exp (Set.Icc l r)
Theorem: Smt.Reconstruct.Arith.exp_contDiffOn
Proof state before:
d : ℕ
l r : ℝ
⊢ ContDiffOn ℝ (↑d) Real.exp (Set.Icc l r)
Tactic:
apply ContDiff.contDiffOn
Proof state after:
case h
d : ℕ
l r : ℝ
⊢ ContDiff ℝ (↑d) Real.exp
Theorem: Smt.Reconstruct.Arith.exp_contDiffOn
Proof state before:
case h
d : ℕ
l r : ℝ
⊢ ContDiff ℝ (↑d) Real.exp
Tactic:
exact Real.contDiff_exp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.t2
Proof state before:
⊢ ∀ (l r : ℝ), l < r → UniqueDiffOn ℝ (Set.Icc l r)
Tactic:
intros l r h
Proof state after:
l r : ℝ
h : l < r
⊢ UniqueDiffOn ℝ (Set.Icc l r)
Theorem: Smt.Reconstruct.Arith.t2
Proof state before:
l r : ℝ
h : l < r
⊢ UniqueDiffOn ℝ (Set.Icc l r)
Tactic:
refine uniqueDiffOn_Icc ?hab
Proof state after:
case hab
l r : ℝ
h : l < r
⊢ l < r
Theorem: Smt.Reconstruct.Arith.t2
Proof state before:
case hab
l r : ℝ
h : l < r
⊢ l < r
Tactic:
exact h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.t1
Proof state before:
⊢ ∀ (n : ℕ) (l r : ℝ), ContDiffOn ℝ (↑n) Real.exp (Set.Icc l r)
Tactic:
intros n l r
Proof state after:
n : ℕ
l r : ℝ
⊢ ContDiffOn ℝ (↑n) Real.exp (Set.Icc l r)
Theorem: Smt.Reconstruct.Arith.t1
Proof state before:
n : ℕ
l r : ℝ
⊢ ContDiffOn ℝ (↑n) Real.exp (Set.Icc l r)
Tactic:
exact exp_contDiffOn n l r
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.exp_DiffOn
Proof state before:
⊢ ∀ (d : ℕ) (l r : ℝ), l < r → DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
Tactic:
intros d l r h
Proof state after:
d : ℕ
l r : ℝ
h : l < r
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
Theorem: Smt.Reconstruct.Arith.exp_DiffOn
Proof state before:
d : ℕ
l r : ℝ
h : l < r
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
Tactic:
have d_lt_succ_d := Nat.lt.base d
Proof state after:
d : ℕ
l r : ℝ
h : l < r
d_lt_succ_d : d < d.succ
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
Theorem: Smt.Reconstruct.Arith.exp_DiffOn
Proof state before:
d : ℕ
l r : ℝ
h : l < r
d_lt_succ_d : d < d.succ
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
Tactic:
have h' := ContDiffOn.differentiableOn_iteratedDerivWithin (m := d) (n := d + 1) (t1 (d + 1) l r) (StrictMono.imp Nat.strictMono_cast d_lt_succ_d) (t2 l r h)
Proof state after:
d : ℕ
l r : ℝ
h : l < r
d_lt_succ_d : d < d.succ
h' : DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Icc l r)
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
Theorem: Smt.Reconstruct.Arith.exp_DiffOn
Proof state before:
d : ℕ
l r : ℝ
h : l < r
d_lt_succ_d : d < d.succ
h' : DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Icc l r)
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
Tactic:
have o : Set.Ioo l r ⊆ Set.Icc l r := Set.Ioo_subset_Icc_self
Proof state after:
d : ℕ
l r : ℝ
h : l < r
d_lt_succ_d : d < d.succ
h' : DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Icc l r)
o : Set.Ioo l r ⊆ Set.Icc l r
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
Theorem: Smt.Reconstruct.Arith.exp_DiffOn
Proof state before:
d : ℕ
l r : ℝ
h : l < r
d_lt_succ_d : d < d.succ
h' : DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Icc l r)
o : Set.Ioo l r ⊆ Set.Icc l r
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
Tactic:
exact DifferentiableOn.mono h' o
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithTransExpApproxAboveNeg
Proof state before:
d : ℕ
l u t : ℝ
⊢ let p := taylorWithinEval Real.exp d (Set.Ioo l u) 0;
  let secant := (p l - p u) / (l - u) * (t - l) + p l;
  StrictConvexOn ℝ (Set.Icc l u) p → t < 0 → t > l ∧ t < u → t.exp ≤ secant
Tactic:
rintro p secant p_conv t_neg ⟨l_bound, u_bound⟩
Proof state after:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
⊢ t.exp ≤ secant
Theorem: Smt.Reconstruct.Arith.arithTransExpApproxAboveNeg
Proof state before:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
⊢ t.exp ≤ secant
Tactic:
have lLeT : l ≤ t := LT.lt.le l_bound
Proof state after:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
⊢ t.exp ≤ secant
Theorem: Smt.Reconstruct.Arith.arithTransExpApproxAboveNeg
Proof state before:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
⊢ t.exp ≤ secant
Tactic:
have tLeU : t ≤ u := LT.lt.le u_bound
Proof state after:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
⊢ t.exp ≤ secant
Theorem: Smt.Reconstruct.Arith.arithTransExpApproxAboveNeg
Proof state before:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
⊢ t.exp ≤ secant
Tactic:
have lLeU : l ≤ u := LE.le.trans lLeT tLeU
Proof state after:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
⊢ t.exp ≤ secant
Theorem: Smt.Reconstruct.Arith.arithTransExpApproxAboveNeg
Proof state before:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
⊢ t.exp ≤ secant
Tactic:
have lLtU : l < u := LT.lt.trans l_bound u_bound
Proof state after:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
lLtU : l < u
⊢ t.exp ≤ secant
Theorem: Smt.Reconstruct.Arith.arithTransExpApproxAboveNeg
Proof state before:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
lLtU : l < u
⊢ t.exp ≤ secant
Tactic:
have conv_imples: (p l - p t) / (l - t) < (p u - p t) / (u - t) :=
  StrictConvexOn.secant_strict_mono p_conv (a := t) (x := l) (y := u)
    (Set.mem_Icc.mpr ⟨lLeT, tLeU⟩)
    (Set.left_mem_Icc.mpr lLeU)
    (Set.right_mem_Icc.mpr lLeU)
    (ne_of_lt l_bound) (Ne.symm (ne_of_lt u_bound)) lLtU
Proof state after:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
lLtU : l < u
conv_imples : (p l - p t) / (l - t) < (p u - p t) / (u - t)
⊢ t.exp ≤ secant
Theorem: Smt.Reconstruct.Arith.arithTransExpApproxAboveNeg
Proof state before:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
lLtU : l < u
conv_imples : (p l - p t) / (l - t) < (p u - p t) / (u - t)
⊢ t.exp ≤ secant
Tactic:
admit
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.sin_neg'
Proof state before:
⊢ ∀ (t : ℝ), t.sin = -(-t).sin
Tactic:
intro t
Proof state after:
t : ℝ
⊢ t.sin = -(-t).sin
Theorem: Smt.Reconstruct.Arith.sin_neg'
Proof state before:
t : ℝ
⊢ t.sin = -(-t).sin
Tactic:
rw [sin_neg t]
Proof state after:
t : ℝ
⊢ t.sin = - -t.sin
Theorem: Smt.Reconstruct.Arith.sin_neg'
Proof state before:
t : ℝ
⊢ t.sin = - -t.sin
Tactic:
simp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithTransSineBounds
Proof state before:
⊢ ∀ (t : ℝ), (t > 0 → t.sin < t) ∧ (t < 0 → t.sin > t)
Tactic:
intro t
Proof state after:
t : ℝ
⊢ (t > 0 → t.sin < t) ∧ (t < 0 → t.sin > t)
Theorem: Smt.Reconstruct.Arith.arithTransSineBounds
Proof state before:
t : ℝ
⊢ (t > 0 → t.sin < t) ∧ (t < 0 → t.sin > t)
Tactic:
apply And.intro
Proof state after:
case left
t : ℝ
⊢ t > 0 → t.sin < t

case right
t : ℝ
⊢ t < 0 → t.sin > t
Theorem: Smt.Reconstruct.Arith.arithTransSineBounds
Proof state before:
case left
t : ℝ
⊢ t > 0 → t.sin < t
Tactic:
exact sin_lt
Proof state after:
no goals