internlm/Lean-Github huggingface dataset:
Theorem: Waffle.le_trans
Proof state before:
a c : Answer
h₁ : a ≤ Answer.yes
h₂ : Answer.yes ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c
Tactic:
case le_yes => 
  cases c₂:h₂
  case le_yes => apply Answer.le.le_yes
  case refl => assumption
Proof state after:
no goals
Theorem: Waffle.le_trans
Proof state before:
a c : Answer
h₁ : a ≤ a
h₂ : a ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c
Tactic:
case refl => assumption
Proof state after:
no goals
Theorem: Waffle.le_trans
Proof state before:
b c : Answer
h₂ : b ≤ c
h₁ : Answer.no ≤ b
c₁ : h₁ = ⋯
⊢ Answer.no ≤ c
Tactic:
apply Answer.le.no_le
Proof state after:
no goals
Theorem: Waffle.le_trans
Proof state before:
a c : Answer
h₁ : a ≤ Answer.yes
h₂ : Answer.yes ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c
Tactic:
cases c₂:h₂
Proof state after:
case le_yes
a : Answer
h₁ : a ≤ Answer.yes
c₁ : h₁ = ⋯
h₂ : Answer.yes ≤ Answer.yes
c₂ : h₂ = ⋯
⊢ a ≤ Answer.yes

case refl
a : Answer
h₁ : a ≤ Answer.yes
c₁ : h₁ = ⋯
h₂ : Answer.yes ≤ Answer.yes
c₂ : h₂ = ⋯
⊢ a ≤ Answer.yes
Theorem: Waffle.le_trans
Proof state before:
a : Answer
h₁ : a ≤ Answer.yes
c₁ : h₁ = ⋯
h₂ : Answer.yes ≤ Answer.yes
c₂ : h₂ = ⋯
⊢ a ≤ Answer.yes
Tactic:
case le_yes => apply Answer.le.le_yes
Proof state after:
no goals
Theorem: Waffle.le_trans
Proof state before:
a : Answer
h₁ : a ≤ Answer.yes
c₁ : h₁ = ⋯
h₂ : Answer.yes ≤ Answer.yes
c₂ : h₂ = ⋯
⊢ a ≤ Answer.yes
Tactic:
case refl => assumption
Proof state after:
no goals
Theorem: Waffle.le_trans
Proof state before:
a : Answer
h₁ : a ≤ Answer.yes
c₁ : h₁ = ⋯
h₂ : Answer.yes ≤ Answer.yes
c₂ : h₂ = ⋯
⊢ a ≤ Answer.yes
Tactic:
apply Answer.le.le_yes
Proof state after:
no goals
Theorem: Waffle.le_trans
Proof state before:
a : Answer
h₁ : a ≤ Answer.yes
c₁ : h₁ = ⋯
h₂ : Answer.yes ≤ Answer.yes
c₂ : h₂ = ⋯
⊢ a ≤ Answer.yes
Tactic:
assumption
Proof state after:
no goals
Theorem: Waffle.le_trans
Proof state before:
a c : Answer
h₁ : a ≤ a
h₂ : a ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c
Tactic:
assumption
Proof state after:
no goals
Theorem: remove_length_le
Proof state before:
case nil
α : Type u
inst✝ : DecidableEq α
a : α
⊢ List.length (List.remove a []) ≤ List.length []
Tactic:
simp [List.remove]
Proof state after:
no goals
Theorem: remove_length_le
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
⊢ List.length (List.remove a (h' :: t)) ≤ List.length (h' :: t)
Tactic:
simp [List.remove]
Proof state after:
case cons
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
⊢ List.length (if a = h' then List.remove a t else h' :: List.remove a t) ≤ Nat.succ (List.length t)
Theorem: remove_length_le
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
⊢ List.length (if a = h' then List.remove a t else h' :: List.remove a t) ≤ Nat.succ (List.length t)
Tactic:
split
Proof state after:
case cons.inl
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : a = h'
⊢ List.length (List.remove a t) ≤ Nat.succ (List.length t)

case cons.inr
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : ¬a = h'
⊢ List.length (h' :: List.remove a t) ≤ Nat.succ (List.length t)
Theorem: remove_length_le
Proof state before:
case cons.inl
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : a = h'
⊢ List.length (List.remove a t) ≤ Nat.succ (List.length t)
Tactic:
apply Nat.le_step
Proof state after:
case cons.inl.h
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : a = h'
⊢ List.length (List.remove a t) ≤ List.length t
Theorem: remove_length_le
Proof state before:
case cons.inl.h
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : a = h'
⊢ List.length (List.remove a t) ≤ List.length t
Tactic:
assumption
Proof state after:
no goals
Theorem: remove_length_le
Proof state before:
case cons.inr
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : ¬a = h'
⊢ List.length (h' :: List.remove a t) ≤ Nat.succ (List.length t)
Tactic:
rw [List.length_cons]
Proof state after:
case cons.inr
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : ¬a = h'
⊢ Nat.succ (List.length (List.remove a t)) ≤ Nat.succ (List.length t)
Theorem: remove_length_le
Proof state before:
case cons.inr
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : ¬a = h'
⊢ Nat.succ (List.length (List.remove a t)) ≤ Nat.succ (List.length t)
Tactic:
apply Nat.succ_le_succ
Proof state after:
case cons.inr.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : ¬a = h'
⊢ List.length (List.remove a t) ≤ List.length t
Theorem: remove_length_le
Proof state before:
case cons.inr.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : List.length (List.remove a t) ≤ List.length t
h✝ : ¬a = h'
⊢ List.length (List.remove a t) ≤ List.length t
Tactic:
exact ih
Proof state after:
no goals
Theorem: remove_mem_length
Proof state before:
case nil
α : Type u
inst✝ : DecidableEq α
a : α
hyp : a ∈ []
⊢ List.length (List.remove a []) < List.length []
Tactic:
contradiction
Proof state after:
no goals
Theorem: remove_mem_length
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
⊢ List.length (List.remove a (h' :: t)) < List.length (h' :: t)
Tactic:
simp [List.remove]
Proof state after:
case cons
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
⊢ List.length (if a = h' then List.remove a t else h' :: List.remove a t) < Nat.succ (List.length t)
Theorem: remove_mem_length
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
⊢ List.length (if a = h' then List.remove a t else h' :: List.remove a t) < Nat.succ (List.length t)
Tactic:
split
Proof state after:
case cons.inl
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : a = h'
⊢ List.length (List.remove a t) < Nat.succ (List.length t)

case cons.inr
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
⊢ List.length (h' :: List.remove a t) < Nat.succ (List.length t)
Theorem: remove_mem_length
Proof state before:
case cons.inl
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : a = h'
⊢ List.length (List.remove a t) < Nat.succ (List.length t)
Tactic:
apply Nat.lt_succ_of_le
Proof state after:
case cons.inl.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : a = h'
⊢ List.length (List.remove a t) ≤ List.length t
Theorem: remove_mem_length
Proof state before:
case cons.inl.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : a = h'
⊢ List.length (List.remove a t) ≤ List.length t
Tactic:
apply remove_length_le
Proof state after:
no goals
Theorem: remove_mem_length
Proof state before:
case cons.inr
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
⊢ List.length (h' :: List.remove a t) < Nat.succ (List.length t)
Tactic:
rw [List.length_cons]
Proof state after:
case cons.inr
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
⊢ Nat.succ (List.length (List.remove a t)) < Nat.succ (List.length t)
Theorem: remove_mem_length
Proof state before:
case cons.inr
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
⊢ Nat.succ (List.length (List.remove a t)) < Nat.succ (List.length t)
Tactic:
apply Nat.succ_lt_succ
Proof state after:
case cons.inr.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
⊢ List.length (List.remove a t) < List.length t
Theorem: remove_mem_length
Proof state before:
case cons.inr.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
⊢ List.length (List.remove a t) < List.length t
Tactic:
have in_tail: a ∈ t := by
  have : ¬ a = h' := by assumption
  simp [List.mem_cons, this] at hyp
  assumption
Proof state after:
case cons.inr.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
in_tail : a ∈ t
⊢ List.length (List.remove a t) < List.length t
Theorem: remove_mem_length
Proof state before:
case cons.inr.a
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
in_tail : a ∈ t
⊢ List.length (List.remove a t) < List.length t
Tactic:
exact ih in_tail
Proof state after:
no goals
Theorem: remove_mem_length
Proof state before:
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
⊢ a ∈ t
Tactic:
have : ¬ a = h' := by assumption
Proof state after:
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ this : ¬a = h'
⊢ a ∈ t
Theorem: remove_mem_length
Proof state before:
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ this : ¬a = h'
⊢ a ∈ t
Tactic:
simp [List.mem_cons, this] at hyp
Proof state after:
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
h✝ this : ¬a = h'
hyp : a ∈ t
⊢ a ∈ t
Theorem: remove_mem_length
Proof state before:
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
h✝ this : ¬a = h'
hyp : a ∈ t
⊢ a ∈ t
Tactic:
assumption
Proof state after:
no goals
Theorem: remove_mem_length
Proof state before:
α : Type u
inst✝ : DecidableEq α
a h' : α
t : List α
ih : a ∈ t → List.length (List.remove a t) < List.length t
hyp : a ∈ h' :: t
h✝ : ¬a = h'
⊢ ¬a = h'
Tactic:
assumption
Proof state after:
no goals
Theorem: Waffle.Answer.eq_of_le_le
Proof state before:
a b : Answer
⊢ a ≤ b → b ≤ a → a = b
Tactic:
sorry
Proof state after:
no goals
Theorem: smallest_in_list
Proof state before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ smallest (head :: tail) hyp ∈ head :: tail
Tactic:
by_cases c:tail = []
Proof state after:
case pos
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : tail = []
⊢ smallest (head :: tail) hyp ∈ head :: tail

case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
⊢ smallest (head :: tail) hyp ∈ head :: tail
Theorem: smallest_in_list
Proof state before:
case pos
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : tail = []
⊢ smallest (head :: tail) hyp ∈ head :: tail
Tactic:
simp [smallest, c]
Proof state after:
no goals
Theorem: smallest_in_list
Proof state before:
case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
⊢ smallest (head :: tail) hyp ∈ head :: tail
Tactic:
simp [smallest, c]
Proof state after:
case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
⊢ head ≤ smallest tail ⋯ ∨ Nat.min head (smallest tail ⋯) ∈ tail
Theorem: smallest_in_list
Proof state before:
case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
⊢ head ≤ smallest tail ⋯ ∨ Nat.min head (smallest tail ⋯) ∈ tail
Tactic:
by_cases c':head ≤ smallest tail (by simp [c])
Proof state after:
case pos
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : head ≤ smallest tail ⋯
⊢ head ≤ smallest tail ⋯ ∨ Nat.min head (smallest tail ⋯) ∈ tail

case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ head ≤ smallest tail ⋯ ∨ Nat.min head (smallest tail ⋯) ∈ tail
Theorem: smallest_in_list
Proof state before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
⊢ tail ≠ []
Tactic:
simp [c]
Proof state after:
no goals
Theorem: smallest_in_list
Proof state before:
case pos
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : head ≤ smallest tail ⋯
⊢ head ≤ smallest tail ⋯ ∨ Nat.min head (smallest tail ⋯) ∈ tail
Tactic:
left
Proof state after:
case pos.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : head ≤ smallest tail ⋯
⊢ head ≤ smallest tail ⋯
Theorem: smallest_in_list
Proof state before:
case pos.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : head ≤ smallest tail ⋯
⊢ head ≤ smallest tail ⋯
Tactic:
assumption
Proof state after:
no goals
Theorem: smallest_in_list
Proof state before:
case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ head ≤ smallest tail ⋯ ∨ Nat.min head (smallest tail ⋯) ∈ tail
Tactic:
right
Proof state after:
case neg.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ Nat.min head (smallest tail ⋯) ∈ tail
Theorem: smallest_in_list
Proof state before:
case neg.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ Nat.min head (smallest tail ⋯) ∈ tail
Tactic:
have lem : 
  Nat.min head (smallest tail (by simp [c])) = smallest tail (by simp [c]) := by
    apply Nat.min_eq_right
    apply Nat.le_of_not_le 
    assumption
Proof state after:
case neg.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
lem : Nat.min head (smallest tail ⋯) = smallest tail ⋯
⊢ Nat.min head (smallest tail ⋯) ∈ tail
Theorem: smallest_in_list
Proof state before:
case neg.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
lem : Nat.min head (smallest tail ⋯) = smallest tail ⋯
⊢ Nat.min head (smallest tail ⋯) ∈ tail
Tactic:
rw [lem]
Proof state after:
case neg.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
lem : Nat.min head (smallest tail ⋯) = smallest tail ⋯
⊢ smallest tail ⋯ ∈ tail
Theorem: smallest_in_list
Proof state before:
case neg.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
lem : Nat.min head (smallest tail ⋯) = smallest tail ⋯
⊢ smallest tail ⋯ ∈ tail
Tactic:
simp [smallest_in_list]
Proof state after:
no goals
Theorem: smallest_in_list
Proof state before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ tail ≠ []
Tactic:
simp [c]
Proof state after:
no goals
Theorem: smallest_in_list
Proof state before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ Nat.min head (smallest tail ⋯) = smallest tail ⋯
Tactic:
apply Nat.min_eq_right
Proof state after:
case h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ smallest tail ⋯ ≤ head
Theorem: smallest_in_list
Proof state before:
case h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ smallest tail ⋯ ≤ head
Tactic:
apply Nat.le_of_not_le
Proof state after:
case h.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ ¬head ≤ smallest tail ⋯
Theorem: smallest_in_list
Proof state before:
case h.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ ¬head ≤ smallest tail ⋯
Tactic:
assumption
Proof state after:
no goals
Theorem: smallest_le
Proof state before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ ∀ m ∈ head :: tail, smallest (head :: tail) hyp ≤ m
Tactic:
simp [smallest, hyp]
Proof state after:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ head ∧
    ∀ a ∈ tail, (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a
Theorem: smallest_le
Proof state before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ head ∧
    ∀ a ∈ tail, (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a
Tactic:
apply And.intro
Proof state after:
case left
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ head

case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ ∀ a ∈ tail, (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a
Theorem: smallest_le
Proof state before:
case left
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ head
Tactic:
split  <;> simp
Proof state after:
no goals
Theorem: smallest_le
Proof state before:
case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ ∀ a ∈ tail, (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a
Tactic:
intro a hyp'
Proof state after:
case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a
Theorem: smallest_le
Proof state before:
case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a
Tactic:
have c'' : tail ≠ [] := by
  intro contra
  rw [contra] at hyp'
  contradiction
Proof state after:
case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a
Theorem: smallest_le
Proof state before:
case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a
Tactic:
simp [c'']
Proof state after:
case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ head ≤ a ∨ smallest tail ⋯ ≤ a
Theorem: smallest_le
Proof state before:
case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ head ≤ a ∨ smallest tail ⋯ ≤ a
Tactic:
right
Proof state after:
case right.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ smallest tail ⋯ ≤ a
Theorem: smallest_le
Proof state before:
case right.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
c'' : tail ≠ []
⊢ smallest tail ⋯ ≤ a
Tactic:
exact smallest_le tail c'' a hyp'
Proof state after:
no goals
Theorem: smallest_le
Proof state before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
⊢ tail ≠ []
Tactic:
intro contra
Proof state after:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
contra : tail = []
⊢ False
Theorem: smallest_le
Proof state before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ tail
contra : tail = []
⊢ False
Tactic:
rw [contra] at hyp'
Proof state after:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ []
contra : tail = []
⊢ False
Theorem: smallest_le
Proof state before:
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
a : ℕ
hyp' : a ∈ []
contra : tail = []
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: remove_length_le
Proof state before:
a : ℕ
l : List ℕ
⊢ List.length (List.remove a l) ≤ List.length l
Tactic:
sorry
Proof state after:
no goals
Theorem: remove_mem_length
Proof state before:
a : ℕ
l : List ℕ
hyp : a ∈ l
⊢ List.length (List.remove a l) < List.length l
Tactic:
sorry
Proof state after:
no goals
Theorem: integral_point
Proof state before:
f : ℝ → ℝ
int : Integrable f
a : ℝ
⊢ integral f a a = 0
Tactic:
unfold integral
Proof state after:
f : ℝ → ℝ
int : Integrable f
a : ℝ
⊢ Integrable.integral f a a = 0
Theorem: integral_point
Proof state before:
f : ℝ → ℝ
int : Integrable f
a : ℝ
⊢ Integrable.integral f a a = 0
Tactic:
have l := int.interval_union a a a
Proof state after:
f : ℝ → ℝ
int : Integrable f
a : ℝ
l : Integrable.integral f a a = Integrable.integral f a a + Integrable.integral f a a
⊢ Integrable.integral f a a = 0
Theorem: integral_point
Proof state before:
f : ℝ → ℝ
int : Integrable f
a : ℝ
l : Integrable.integral f a a = Integrable.integral f a a + Integrable.integral f a a
⊢ Integrable.integral f a a = 0
Tactic:
simp  at l
Proof state after:
f : ℝ → ℝ
int : Integrable f
a : ℝ
l : Integrable.integral f a a = 0
⊢ Integrable.integral f a a = 0
Theorem: integral_point
Proof state before:
f : ℝ → ℝ
int : Integrable f
a : ℝ
l : Integrable.integral f a a = 0
⊢ Integrable.integral f a a = 0
Tactic:
assumption
Proof state after:
no goals
Theorem: sum_formula
Proof state before:
n : ℕ
⊢ 2 * sumTo n = n * (n + 1)
Tactic:
induction n with
| zero => rfl
| succ n ih => 
  simp [sumTo] simp [left_distrib, ih] 
  linarith
Proof state after:
no goals
Theorem: sum_formula
Proof state before:
case zero

⊢ 2 * sumTo Nat.zero = Nat.zero * (Nat.zero + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: sum_formula
Proof state before:
case succ
n : ℕ
ih : 2 * sumTo n = n * (n + 1)
⊢ 2 * sumTo (Nat.succ n) = Nat.succ n * (Nat.succ n + 1)
Tactic:
simp [sumTo]
Proof state after:
case succ
n : ℕ
ih : 2 * sumTo n = n * (n + 1)
⊢ 2 * (n + 1 + sumTo n) = Nat.succ n * (Nat.succ n + 1)
Theorem: sum_formula
Proof state before:
case succ
n : ℕ
ih : 2 * sumTo n = n * (n + 1)
⊢ 2 * (n + 1 + sumTo n) = Nat.succ n * (Nat.succ n + 1)
Tactic:
simp [left_distrib, ih]
Proof state after:
case succ
n : ℕ
ih : 2 * sumTo n = n * (n + 1)
⊢ 2 * n + 2 + (n * n + n) = Nat.succ n * Nat.succ n + Nat.succ n
Theorem: sum_formula
Proof state before:
case succ
n : ℕ
ih : 2 * sumTo n = n * (n + 1)
⊢ 2 * n + 2 + (n * n + n) = Nat.succ n * Nat.succ n + Nat.succ n
Tactic:
linarith
Proof state after:
no goals
Theorem: gradebook_schema_is_quiz_schema
Proof state before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema (schema gradebook)
Tactic:
repeat (first | apply IsQuizSchema.consQuiz (by decide)
              | apply IsQuizSchema.consNonQuiz (by decide)
              | apply IsQuizSchema.nil)
Proof state after:
no goals
Theorem: gradebook_schema_is_quiz_schema
Proof state before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema []
Tactic:
(first | apply IsQuizSchema.consQuiz (by decide)
       | apply IsQuizSchema.consNonQuiz (by decide)
       | apply IsQuizSchema.nil)
Proof state after:
no goals
Theorem: gradebook_schema_is_quiz_schema
Proof state before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema []
Tactic:
first | apply IsQuizSchema.consQuiz (by decide)
      | apply IsQuizSchema.consNonQuiz (by decide)
      | apply IsQuizSchema.nil
Proof state after:
no goals
Theorem: gradebook_schema_is_quiz_schema
Proof state before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema [("final", Nat)]
Tactic:
apply IsQuizSchema.consQuiz (by decide)
Proof state after:
no goals
Theorem: gradebook_schema_is_quiz_schema
Proof state before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ String.startsWith "quiz4" "quiz" = true
Tactic:
decide
Proof state after:
no goals