internlm/Lean-Github huggingface dataset:
Theorem: binomial_theorem
Proof state before:
case succ
x y n : ℕ
ih : (x + y) ^ n = ∑ k in Finset.range (n + 1), Nat.choose n k * x ^ (n - k) * y ^ k
⊢ (x + y) ^ Nat.succ n = ∑ k in Finset.range (Nat.succ n + 1), Nat.choose (Nat.succ n) k * x ^ (Nat.succ n - k) * y ^ k
Tactic:
rw [Finset.sum_range_succ,
    Nat.succ_eq_add_one,
    Nat.choose_self,
    Nat.sub_self,
    pow_zero,
    mul_one,
    one_mul,
    Finset.sum_range_succ',
    Nat.choose_zero_right,
    one_mul,
    Nat.sub_zero,
    pow_zero,
    mul_one]
Proof state after:
case succ
x y n : ℕ
ih : (x + y) ^ n = ∑ k in Finset.range (n + 1), Nat.choose n k * x ^ (n - k) * y ^ k
⊢ (x + y) ^ (n + 1) =
    ∑ k in Finset.range n, Nat.choose (n + 1) (k + 1) * x ^ (n + 1 - (k + 1)) * y ^ (k + 1) + x ^ (n + 1) + y ^ (n + 1)
Theorem: binomial_theorem
Proof state before:
case succ
x y n : ℕ
ih : (x + y) ^ n = ∑ k in Finset.range (n + 1), Nat.choose n k * x ^ (n - k) * y ^ k
⊢ (x + y) ^ (n + 1) =
    ∑ k in Finset.range n, Nat.choose (n + 1) (k + 1) * x ^ (n + 1 - (k + 1)) * y ^ (k + 1) + x ^ (n + 1) + y ^ (n + 1)
Tactic:
simp_rw [Nat.choose_succ_succ']
Proof state after:
case succ
x y n : ℕ
ih : (x + y) ^ n = ∑ k in Finset.range (n + 1), Nat.choose n k * x ^ (n - k) * y ^ k
⊢ (x + y) ^ (n + 1) =
    ∑ x_1 in Finset.range n, (Nat.choose n x_1 + Nat.choose n (x_1 + 1)) * x ^ (n + 1 - (x_1 + 1)) * y ^ (x_1 + 1) +
        x ^ (n + 1) +
      y ^ (n + 1)
Theorem: cons_le_is_ordered
Proof state before:
α : Type
inst✝ : LE α
a : α
xs : List α
h : IsOrdered xs
hle : ∀ x ∈ xs, a ≤ x
⊢ IsOrdered (a :: xs)
Tactic:
simp only [IsOrdered, List.pairwise_cons] at *
Proof state after:
α : Type
inst✝ : LE α
a : α
xs : List α
h : List.Pairwise LE.le xs
hle : ∀ x ∈ xs, a ≤ x
⊢ (∀ a' ∈ xs, a ≤ a') ∧ List.Pairwise LE.le xs
Theorem: cons_le_is_ordered
Proof state before:
α : Type
inst✝ : LE α
a : α
xs : List α
h : List.Pairwise LE.le xs
hle : ∀ x ∈ xs, a ≤ x
⊢ (∀ a' ∈ xs, a ≤ a') ∧ List.Pairwise LE.le xs
Tactic:
exact ⟨hle, h⟩
Proof state after:
no goals
Theorem: insert_mem
Proof state before:
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
⊢ x ∈ insert' a l ↔ x = a ∨ x ∈ l
Tactic:
constructor
Proof state after:
case mp
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
⊢ x ∈ insert' a l → x = a ∨ x ∈ l

case mpr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
⊢ x = a ∨ x ∈ l → x ∈ insert' a l
Theorem: insert_mem
Proof state before:
case mp
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
⊢ x ∈ insert' a l → x = a ∨ x ∈ l
Tactic:
intro hel
Proof state after:
case mp
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
hel : x ∈ insert' a l
⊢ x = a ∨ x ∈ l
Theorem: insert_mem
Proof state before:
case mp
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
hel : x ∈ insert' a l
⊢ x = a ∨ x ∈ l
Tactic:
induction' l with y ys ih
Proof state after:
case mp.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hel : x ∈ insert' a []
⊢ x = a ∨ x ∈ []

case mp.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
hel : x ∈ insert' a (y :: ys)
⊢ x = a ∨ x ∈ y :: ys
Theorem: insert_mem
Proof state before:
case mp.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hel : x ∈ insert' a []
⊢ x = a ∨ x ∈ []
Tactic:
rw [insert', List.mem_singleton] at hel
Proof state after:
case mp.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hel : x = a
⊢ x = a ∨ x ∈ []
Theorem: insert_mem
Proof state before:
case mp.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hel : x = a
⊢ x = a ∨ x ∈ []
Tactic:
left
Proof state after:
case mp.nil.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hel : x = a
⊢ x = a
Theorem: insert_mem
Proof state before:
case mp.nil.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hel : x = a
⊢ x = a
Tactic:
exact hel
Proof state after:
no goals
Theorem: insert_mem
Proof state before:
case mp.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
hel : x ∈ insert' a (y :: ys)
⊢ x = a ∨ x ∈ y :: ys
Tactic:
rw [insert'] at hel
Proof state after:
case mp.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
hel : x ∈ if a ≤ y then a :: y :: ys else y :: insert' a ys
⊢ x = a ∨ x ∈ y :: ys
Theorem: insert_mem
Proof state before:
case mp.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
hel : x ∈ if a ≤ y then a :: y :: ys else y :: insert' a ys
⊢ x = a ∨ x ∈ y :: ys
Tactic:
split_ifs at hel
Proof state after:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : a ≤ y
hel : x ∈ a :: y :: ys
⊢ x = a ∨ x ∈ y :: ys

case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hel : x ∈ y :: insert' a ys
⊢ x = a ∨ x ∈ y :: ys
Theorem: insert_mem
Proof state before:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : a ≤ y
hel : x ∈ a :: y :: ys
⊢ x = a ∨ x ∈ y :: ys
Tactic:
simp only [List.mem_cons] at hel
Proof state after:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : a ≤ y
hel : x = a ∨ x = y ∨ x ∈ ys
⊢ x = a ∨ x ∈ y :: ys
Theorem: insert_mem
Proof state before:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : a ≤ y
hel : x = a ∨ x = y ∨ x ∈ ys
⊢ x = a ∨ x ∈ y :: ys
Tactic:
simp only [List.mem_cons]
Proof state after:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : a ≤ y
hel : x = a ∨ x = y ∨ x ∈ ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Theorem: insert_mem
Proof state before:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : a ≤ y
hel : x = a ∨ x = y ∨ x ∈ ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
exact hel
Proof state after:
no goals
Theorem: insert_mem
Proof state before:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hel : x ∈ y :: insert' a ys
⊢ x = a ∨ x ∈ y :: ys
Tactic:
simp only [List.mem_cons] at hel
Proof state after:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hel : x = y ∨ x ∈ insert' a ys
⊢ x = a ∨ x ∈ y :: ys
Theorem: insert_mem
Proof state before:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hel : x = y ∨ x ∈ insert' a ys
⊢ x = a ∨ x ∈ y :: ys
Tactic:
simp only [List.mem_cons]
Proof state after:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hel : x = y ∨ x ∈ insert' a ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Theorem: insert_mem
Proof state before:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hel : x = y ∨ x ∈ insert' a ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
rcases hel with (heq | hmem)
Proof state after:
case neg.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
heq : x = y
⊢ x = a ∨ x = y ∨ x ∈ ys

case neg.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Theorem: insert_mem
Proof state before:
case neg.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
heq : x = y
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
right
Proof state after:
case neg.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
heq : x = y
⊢ x = y ∨ x ∈ ys
Theorem: insert_mem
Proof state before:
case neg.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
heq : x = y
⊢ x = y ∨ x ∈ ys
Tactic:
left
Proof state after:
case neg.inl.h.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
heq : x = y
⊢ x = y
Theorem: insert_mem
Proof state before:
case neg.inl.h.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
heq : x = y
⊢ x = y
Tactic:
exact heq
Proof state after:
no goals
Theorem: insert_mem
Proof state before:
case neg.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
rcases ih hmem with (heq' | hmem')
Proof state after:
case neg.inr.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
heq' : x = a
⊢ x = a ∨ x = y ∨ x ∈ ys

case neg.inr.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
hmem' : x ∈ ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Theorem: insert_mem
Proof state before:
case neg.inr.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
heq' : x = a
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
left
Proof state after:
case neg.inr.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
heq' : x = a
⊢ x = a
Theorem: insert_mem
Proof state before:
case neg.inr.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
heq' : x = a
⊢ x = a
Tactic:
exact heq'
Proof state after:
no goals
Theorem: insert_mem
Proof state before:
case neg.inr.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
hmem' : x ∈ ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
right
Proof state after:
case neg.inr.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
hmem' : x ∈ ys
⊢ x = y ∨ x ∈ ys
Theorem: insert_mem
Proof state before:
case neg.inr.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
hmem' : x ∈ ys
⊢ x = y ∨ x ∈ ys
Tactic:
right
Proof state after:
case neg.inr.inr.h.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
hmem' : x ∈ ys
⊢ x ∈ ys
Theorem: insert_mem
Proof state before:
case neg.inr.inr.h.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hmem : x ∈ insert' a ys
hmem' : x ∈ ys
⊢ x ∈ ys
Tactic:
exact hmem'
Proof state after:
no goals
Theorem: insert_mem
Proof state before:
case mpr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
⊢ x = a ∨ x ∈ l → x ∈ insert' a l
Tactic:
intro hor
Proof state after:
case mpr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
hor : x = a ∨ x ∈ l
⊢ x ∈ insert' a l
Theorem: insert_mem
Proof state before:
case mpr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
l : List α
hor : x = a ∨ x ∈ l
⊢ x ∈ insert' a l
Tactic:
induction' l with y ys ih
Proof state after:
case mpr.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hor : x = a ∨ x ∈ []
⊢ x ∈ insert' a []

case mpr.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
⊢ x ∈ insert' a (y :: ys)
Theorem: insert_mem
Proof state before:
case mpr.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hor : x = a ∨ x ∈ []
⊢ x ∈ insert' a []
Tactic:
rw [insert', List.mem_singleton]
Proof state after:
case mpr.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hor : x = a ∨ x ∈ []
⊢ x = a
Theorem: insert_mem
Proof state before:
case mpr.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hor : x = a ∨ x ∈ []
⊢ x = a
Tactic:
rcases hor with (heq | hmem)
Proof state after:
case mpr.nil.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
heq : x = a
⊢ x = a

case mpr.nil.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hmem : x ∈ []
⊢ x = a
Theorem: insert_mem
Proof state before:
case mpr.nil.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
heq : x = a
⊢ x = a
Tactic:
exact heq
Proof state after:
no goals
Theorem: insert_mem
Proof state before:
case mpr.nil.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hmem : x ∈ []
⊢ x = a
Tactic:
simp only [List.not_mem_nil] at hmem
Proof state after:
no goals
Theorem: insert_mem
Proof state before:
case mpr.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
⊢ x ∈ insert' a (y :: ys)
Tactic:
rw [insert']
Proof state after:
case mpr.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
⊢ x ∈ if a ≤ y then a :: y :: ys else y :: insert' a ys
Theorem: insert_mem
Proof state before:
case mpr.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
⊢ x ∈ if a ≤ y then a :: y :: ys else y :: insert' a ys
Tactic:
split_ifs
Proof state after:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : a ≤ y
⊢ x ∈ a :: y :: ys

case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : ¬a ≤ y
⊢ x ∈ y :: insert' a ys
Theorem: insert_mem
Proof state before:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : a ≤ y
⊢ x ∈ a :: y :: ys
Tactic:
simp only [List.mem_cons]
Proof state after:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : a ≤ y
⊢ x = a ∨ x = y ∨ x ∈ ys
Theorem: insert_mem
Proof state before:
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : a ≤ y
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
rcases hor with (heq | hmem)
Proof state after:
case pos.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
heq : x = a
⊢ x = a ∨ x = y ∨ x ∈ ys

case pos.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
hmem : x ∈ y :: ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Theorem: insert_mem
Proof state before:
case pos.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
heq : x = a
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
left
Proof state after:
case pos.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
heq : x = a
⊢ x = a
Theorem: insert_mem
Proof state before:
case pos.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
heq : x = a
⊢ x = a
Tactic:
exact heq
Proof state after:
no goals
Theorem: insert_mem
Proof state before:
case pos.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
hmem : x ∈ y :: ys
⊢ x = a ∨ x = y ∨ x ∈ ys
Tactic:
right
Proof state after:
case pos.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
hmem : x ∈ y :: ys
⊢ x = y ∨ x ∈ ys
Theorem: insert_mem
Proof state before:
case pos.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
hmem : x ∈ y :: ys
⊢ x = y ∨ x ∈ ys
Tactic:
simp only [List.mem_cons] at hmem
Proof state after:
case pos.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
hmem : x = y ∨ x ∈ ys
⊢ x = y ∨ x ∈ ys
Theorem: insert_mem
Proof state before:
case pos.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : a ≤ y
hmem : x = y ∨ x ∈ ys
⊢ x = y ∨ x ∈ ys
Tactic:
exact hmem
Proof state after:
no goals
Theorem: insert_mem
Proof state before:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : ¬a ≤ y
⊢ x ∈ y :: insert' a ys
Tactic:
simp only [List.mem_cons]
Proof state after:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : ¬a ≤ y
⊢ x = y ∨ x ∈ insert' a ys
Theorem: insert_mem
Proof state before:
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : ¬a ≤ y
⊢ x = y ∨ x ∈ insert' a ys
Tactic:
rcases hor with (heq | hmem)
Proof state after:
case neg.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq : x = a
⊢ x = y ∨ x ∈ insert' a ys

case neg.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem : x ∈ y :: ys
⊢ x = y ∨ x ∈ insert' a ys
Theorem: insert_mem
Proof state before:
case neg.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq : x = a
⊢ x = y ∨ x ∈ insert' a ys
Tactic:
right
Proof state after:
case neg.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq : x = a
⊢ x ∈ insert' a ys
Theorem: insert_mem
Proof state before:
case neg.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq : x = a
⊢ x ∈ insert' a ys
Tactic:
exact ih (Or.inl heq)
Proof state after:
no goals
Theorem: insert_mem
Proof state before:
case neg.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem : x ∈ y :: ys
⊢ x = y ∨ x ∈ insert' a ys
Tactic:
simp only [List.mem_cons] at hmem
Proof state after:
case neg.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem : x = y ∨ x ∈ ys
⊢ x = y ∨ x ∈ insert' a ys
Theorem: insert_mem
Proof state before:
case neg.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem : x = y ∨ x ∈ ys
⊢ x = y ∨ x ∈ insert' a ys
Tactic:
rcases hmem with (heq' | hmem')
Proof state after:
case neg.inr.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq' : x = y
⊢ x = y ∨ x ∈ insert' a ys

case neg.inr.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem' : x ∈ ys
⊢ x = y ∨ x ∈ insert' a ys
Theorem: insert_mem
Proof state before:
case neg.inr.inl
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq' : x = y
⊢ x = y ∨ x ∈ insert' a ys
Tactic:
left
Proof state after:
case neg.inr.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq' : x = y
⊢ x = y
Theorem: insert_mem
Proof state before:
case neg.inr.inl.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
heq' : x = y
⊢ x = y
Tactic:
exact heq'
Proof state after:
no goals
Theorem: insert_mem
Proof state before:
case neg.inr.inr
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem' : x ∈ ys
⊢ x = y ∨ x ∈ insert' a ys
Tactic:
right
Proof state after:
case neg.inr.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem' : x ∈ ys
⊢ x ∈ insert' a ys
Theorem: insert_mem
Proof state before:
case neg.inr.inr.h
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
h✝ : ¬a ≤ y
hmem' : x ∈ ys
⊢ x ∈ insert' a ys
Tactic:
exact ih (Or.inr hmem')
Proof state after:
no goals
Theorem: ordered_insert_is_ordered
Proof state before:
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
l : List α
ordered : IsOrdered l
⊢ IsOrdered (insert' a l)
Tactic:
simp at *
Proof state after:
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
l : List α
ordered : List.Pairwise LE.le l
⊢ List.Pairwise LE.le (insert' a l)
Theorem: ordered_insert_is_ordered
Proof state before:
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
l : List α
ordered : List.Pairwise LE.le l
⊢ List.Pairwise LE.le (insert' a l)
Tactic:
induction' l with x xs ih
Proof state after:
case nil
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ List.Pairwise LE.le (insert' a [])

case cons
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
⊢ List.Pairwise LE.le (insert' a (x :: xs))
Theorem: ordered_insert_is_ordered
Proof state before:
case nil
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ List.Pairwise LE.le (insert' a [])
Tactic:
rw [insert', List.pairwise_cons]
Proof state after:
case nil
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ (∀ a' ∈ [], a ≤ a') ∧ List.Pairwise LE.le []
Theorem: ordered_insert_is_ordered
Proof state before:
case nil
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ (∀ a' ∈ [], a ≤ a') ∧ List.Pairwise LE.le []
Tactic:
constructor
Proof state after:
case nil.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ ∀ a' ∈ [], a ≤ a'

case nil.right
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ List.Pairwise LE.le []
Theorem: ordered_insert_is_ordered
Proof state before:
case nil.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ ∀ a' ∈ [], a ≤ a'
Tactic:
intros y hy
Proof state after:
case nil.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
y : α
hy : y ∈ []
⊢ a ≤ y
Theorem: ordered_insert_is_ordered
Proof state before:
case nil.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
y : α
hy : y ∈ []
⊢ a ≤ y
Tactic:
simp only [List.find?_nil, List.not_mem_nil] at hy
Proof state after:
no goals
Theorem: ordered_insert_is_ordered
Proof state before:
case nil.right
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ List.Pairwise LE.le []
Tactic:
exact ordered
Proof state after:
no goals