internlm/Lean-Github huggingface dataset:
Theorem: List.getLast_intercalate
Proof state before:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast (intercalate delim (head :: mid :: mid₂ :: tail)) h₂ =
    getLast (getLast (head :: mid :: mid₂ :: tail) (_ : head :: mid :: mid₂ :: tail = [] → False))
      (_ : getLast (head :: mid :: mid₂ :: tail) (_ : head :: mid :: mid₂ :: tail = [] → False) = [] → False)
Tactic:
simp [intercalate]
Proof state after:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast (head ++ (delim ++ (mid ++ (delim ++ join (intersperse delim (mid₂ :: tail))))))
      (_ : head ++ (delim ++ (mid ++ (delim ++ join (intersperse delim (mid₂ :: tail))))) ≠ []) =
    getLast (getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = [])) (_ : getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = []) ≠ [])
Theorem: List.getLast_intercalate
Proof state before:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast (head ++ (delim ++ (mid ++ (delim ++ join (intersperse delim (mid₂ :: tail))))))
      (_ : head ++ (delim ++ (mid ++ (delim ++ join (intersperse delim (mid₂ :: tail))))) ≠ []) =
    getLast (getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = [])) (_ : getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = []) ≠ [])
Tactic:
simp [← intercalate._eq_1]
Proof state after:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast (head ++ (delim ++ (mid ++ (delim ++ intercalate delim (mid₂ :: tail)))))
      (_ : head ++ (delim ++ (mid ++ (delim ++ intercalate delim (mid₂ :: tail)))) ≠ []) =
    getLast (getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = [])) (_ : getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = []) ≠ [])
Theorem: List.getLast_intercalate
Proof state before:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast (head ++ (delim ++ (mid ++ (delim ++ intercalate delim (mid₂ :: tail)))))
      (_ : head ++ (delim ++ (mid ++ (delim ++ intercalate delim (mid₂ :: tail)))) ≠ []) =
    getLast (getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = [])) (_ : getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = []) ≠ [])
Tactic:
simp only [← append_assoc]
Proof state after:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast (head ++ delim ++ mid ++ delim ++ intercalate delim (mid₂ :: tail))
      (_ : head ++ delim ++ mid ++ delim ++ intercalate delim (mid₂ :: tail) ≠ []) =
    getLast (getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = [])) (_ : getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = []) ≠ [])
Theorem: List.getLast_intercalate
Proof state before:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast (head ++ delim ++ mid ++ delim ++ intercalate delim (mid₂ :: tail))
      (_ : head ++ delim ++ mid ++ delim ++ intercalate delim (mid₂ :: tail) ≠ []) =
    getLast (getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = [])) (_ : getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = []) ≠ [])
Tactic:
rw [getLast_append', getLast_intercalate (mid₂::tail)]
Proof state after:
case h₂
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ intercalate delim (mid₂ :: tail) ≠ []

case not_nil
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast? (mid₂ :: tail) ≠ some []

α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ α
Theorem: List.getLast_intercalate
Proof state before:
case h₂
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ intercalate delim (mid₂ :: tail) ≠ []

case not_nil
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast? (mid₂ :: tail) ≠ some []

α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ α
Tactic:
. intro contr
  apply not_nil
  rw [List.getLast?_eq_getLast]
  simp only [ne_eq, not_false_iff, getLast_cons, Option.some.injEq]
  generalize_proofs hp
  apply List.intercalate_eq_nil contr (getLast (mid₂ :: tail) hp)
  apply List.getLast_mem
  simp only [ne_eq, not_false_iff]
Proof state after:
case not_nil
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast? (mid₂ :: tail) ≠ some []

α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ α
Theorem: List.getLast_intercalate
Proof state before:
case not_nil
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast? (mid₂ :: tail) ≠ some []

α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ α
Tactic:
. intro contr
  apply not_nil
  simp only [getLast?_cons_cons, contr]
Proof state after:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ α
Theorem: List.getLast_intercalate
Proof state before:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ α
Tactic:
. exact a
Proof state after:
no goals
Theorem: List.mem_of_mem_take
Proof state before:
α✝ : Type u_1
a : α✝
l : List α✝
n : ℕ
h : a ∈ take n l
⊢ a ∈ l
Tactic:
rw [← take_append_drop n l]
Proof state after:
α✝ : Type u_1
a : α✝
l : List α✝
n : ℕ
h : a ∈ take n l
⊢ a ∈ take n l ++ drop n l
Theorem: List.mem_of_mem_take
Proof state before:
α✝ : Type u_1
a : α✝
l : List α✝
n : ℕ
h : a ∈ take n l
⊢ a ∈ take n l ++ drop n l
Tactic:
apply mem_append_left _ h
Proof state after:
no goals
Theorem: List.countp_nil
Proof state before:
α✝ : Type u_1
p : α✝ → Bool
⊢ countp p [] = 0
Tactic:
unfold countp countp.go
Proof state after:
α✝ : Type u_1
p : α✝ → Bool
⊢ 0 = 0
Theorem: List.countp_nil
Proof state before:
α✝ : Type u_1
p : α✝ → Bool
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: List.countp.go_acc
Proof state before:
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
acc : ℕ
⊢ go p l acc = acc + go p l 0
Tactic:
induction l generalizing acc with
| nil => unfold go; simp
| cons head tail ih =>
  unfold go
  cases p head with
  | true => simp only [@ih (acc + 1), add_assoc, zero_le, ge_iff_le, nonpos_iff_eq_zero, cond_true, zero_add, @ih 1]
  | false => simp only [@ih acc, zero_le, ge_iff_le, nonpos_iff_eq_zero, cond_false, zero_add]
Proof state after:
no goals
Theorem: List.countp.go_acc
Proof state before:
case nil
α✝ : Type u_1
p : α✝ → Bool
acc : ℕ
⊢ go p [] acc = acc + go p [] 0
Tactic:
unfold go
Proof state after:
case nil
α✝ : Type u_1
p : α✝ → Bool
acc : ℕ
⊢ acc = acc + 0
Theorem: List.countp.go_acc
Proof state before:
case nil
α✝ : Type u_1
p : α✝ → Bool
acc : ℕ
⊢ acc = acc + 0
Tactic:
simp
Proof state after:
no goals
Theorem: List.countp.go_acc
Proof state before:
case cons
α✝ : Type u_1
p : α✝ → Bool
head : α✝
tail : List α✝
ih : ∀ {acc : ℕ}, go p tail acc = acc + go p tail 0
acc : ℕ
⊢ go p (head :: tail) acc = acc + go p (head :: tail) 0
Tactic:
unfold go
Proof state after:
case cons
α✝ : Type u_1
p : α✝ → Bool
head : α✝
tail : List α✝
ih : ∀ {acc : ℕ}, go p tail acc = acc + go p tail 0
acc : ℕ
⊢ (bif p head then go p tail (acc + 1) else go p tail acc) = acc + bif p head then go p tail (0 + 1) else go p tail 0
Theorem: List.countp.go_acc
Proof state before:
case cons
α✝ : Type u_1
p : α✝ → Bool
head : α✝
tail : List α✝
ih : ∀ {acc : ℕ}, go p tail acc = acc + go p tail 0
acc : ℕ
⊢ (bif p head then go p tail (acc + 1) else go p tail acc) = acc + bif p head then go p tail (0 + 1) else go p tail 0
Tactic:
cases p head with
| true => simp only [@ih (acc + 1), add_assoc, zero_le, ge_iff_le, nonpos_iff_eq_zero, cond_true, zero_add, @ih 1]
| false => simp only [@ih acc, zero_le, ge_iff_le, nonpos_iff_eq_zero, cond_false, zero_add]
Proof state after:
no goals
Theorem: List.countp.go_acc
Proof state before:
case cons.true
α✝ : Type u_1
p : α✝ → Bool
head : α✝
tail : List α✝
ih : ∀ {acc : ℕ}, go p tail acc = acc + go p tail 0
acc : ℕ
⊢ (bif true then go p tail (acc + 1) else go p tail acc) = acc + bif true then go p tail (0 + 1) else go p tail 0
Tactic:
simp only [@ih (acc + 1), add_assoc, zero_le, ge_iff_le, nonpos_iff_eq_zero, cond_true, zero_add, @ih 1]
Proof state after:
no goals
Theorem: List.countp.go_acc
Proof state before:
case cons.false
α✝ : Type u_1
p : α✝ → Bool
head : α✝
tail : List α✝
ih : ∀ {acc : ℕ}, go p tail acc = acc + go p tail 0
acc : ℕ
⊢ (bif false then go p tail (acc + 1) else go p tail acc) = acc + bif false then go p tail (0 + 1) else go p tail 0
Tactic:
simp only [@ih acc, zero_le, ge_iff_le, nonpos_iff_eq_zero, cond_false, zero_add]
Proof state after:
no goals
Theorem: List.countp_cons
Proof state before:
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ countp p (head :: tail) = (if p head = true then 1 else 0) + countp p tail
Tactic:
rw [countp, countp.go]
Proof state after:
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ (bif p head then countp.go p tail (0 + 1) else countp.go p tail 0) = (if p head = true then 1 else 0) + countp p tail
Theorem: List.countp_cons
Proof state before:
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ (bif p head then countp.go p tail (0 + 1) else countp.go p tail 0) = (if p head = true then 1 else 0) + countp p tail
Tactic:
cases p head with
| true => simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_add, cond_true, ite_true]; rw [List.countp.go_acc, ← countp]
| false => simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_add, cond_false, ite_false]; rw [← countp]
Proof state after:
no goals
Theorem: List.countp_cons
Proof state before:
case true
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ (bif true then countp.go p tail (0 + 1) else countp.go p tail 0) = (if true = true then 1 else 0) + countp p tail
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_add, cond_true, ite_true]
Proof state after:
case true
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ countp.go p tail 1 = 1 + countp p tail
Theorem: List.countp_cons
Proof state before:
case true
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ countp.go p tail 1 = 1 + countp p tail
Tactic:
rw [List.countp.go_acc, ← countp]
Proof state after:
no goals
Theorem: List.countp_cons
Proof state before:
case false
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ (bif false then countp.go p tail (0 + 1) else countp.go p tail 0) = (if false = true then 1 else 0) + countp p tail
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_add, cond_false, ite_false]
Proof state after:
case false
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ countp.go p tail 0 = countp p tail
Theorem: List.countp_cons
Proof state before:
case false
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ countp.go p tail 0 = countp p tail
Tactic:
rw [← countp]
Proof state after:
no goals
Theorem: List.count_nil
Proof state before:
α : Type u_1
inst✝ : BEq α
a : α
⊢ count a [] = 0
Tactic:
unfold count
Proof state after:
α : Type u_1
inst✝ : BEq α
a : α
⊢ countp (fun x => x == a) [] = 0
Theorem: List.count_nil
Proof state before:
α : Type u_1
inst✝ : BEq α
a : α
⊢ countp (fun x => x == a) [] = 0
Tactic:
apply countp_nil
Proof state after:
no goals
Theorem: List.count_cons
Proof state before:
α : Type u_1
a : α
inst✝ : BEq α
head : α
tail : List α
⊢ count a (head :: tail) = (if (head == a) = true then 1 else 0) + count a tail
Tactic:
unfold count
Proof state after:
α : Type u_1
a : α
inst✝ : BEq α
head : α
tail : List α
⊢ countp (fun x => x == a) (head :: tail) = (if (head == a) = true then 1 else 0) + countp (fun x => x == a) tail
Theorem: List.count_cons
Proof state before:
α : Type u_1
a : α
inst✝ : BEq α
head : α
tail : List α
⊢ countp (fun x => x == a) (head :: tail) = (if (head == a) = true then 1 else 0) + countp (fun x => x == a) tail
Tactic:
apply countp_cons
Proof state after:
no goals
Theorem: List.countp_append
Proof state before:
α✝ : Type u_1
p : α✝ → Bool
l₁ l₂ : List α✝
⊢ countp p (l₁ ++ l₂) = countp p l₁ + countp p l₂
Tactic:
induction l₁ with
| nil => simp only [nil_append, countp_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_add]
| cons head tail ih => simp only [cons_append, countp_cons, ih, zero_le, ge_iff_le, nonpos_iff_eq_zero, add_assoc]
Proof state after:
no goals
Theorem: List.countp_append
Proof state before:
case nil
α✝ : Type u_1
p : α✝ → Bool
l₂ : List α✝
⊢ countp p ([] ++ l₂) = countp p [] + countp p l₂
Tactic:
simp only [nil_append, countp_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_add]
Proof state after:
no goals
Theorem: List.countp_append
Proof state before:
case cons
α✝ : Type u_1
p : α✝ → Bool
l₂ : List α✝
head : α✝
tail : List α✝
ih : countp p (tail ++ l₂) = countp p tail + countp p l₂
⊢ countp p (head :: tail ++ l₂) = countp p (head :: tail) + countp p l₂
Tactic:
simp only [cons_append, countp_cons, ih, zero_le, ge_iff_le, nonpos_iff_eq_zero, add_assoc]
Proof state after:
no goals
Theorem: List.count_append
Proof state before:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
⊢ count a (l₁ ++ l₂) = count a l₁ + count a l₂
Tactic:
unfold count
Proof state after:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
⊢ countp (fun x => x == a) (l₁ ++ l₂) = countp (fun x => x == a) l₁ + countp (fun x => x == a) l₂
Theorem: List.count_append
Proof state before:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
⊢ countp (fun x => x == a) (l₁ ++ l₂) = countp (fun x => x == a) l₁ + countp (fun x => x == a) l₂
Tactic:
apply List.countp_append
Proof state after:
no goals
Theorem: List.isInfix_countp_le
Proof state before:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
⊢ countp p l₁ ≤ countp p l₂
Tactic:
have ⟨s,t,heq⟩ := h
Proof state after:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ countp p l₁ ≤ countp p l₂
Theorem: List.isInfix_countp_le
Proof state before:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ countp p l₁ ≤ countp p l₂
Tactic:
apply_fun countp p at heq
Proof state after:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : countp p (s ++ l₁ ++ t) = countp p l₂
⊢ countp p l₁ ≤ countp p l₂
Theorem: List.isInfix_countp_le
Proof state before:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : countp p (s ++ l₁ ++ t) = countp p l₂
⊢ countp p l₁ ≤ countp p l₂
Tactic:
simp only [append_assoc, countp_append] at heq
Proof state after:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : countp p s + (countp p l₁ + countp p t) = countp p l₂
⊢ countp p l₁ ≤ countp p l₂
Theorem: List.isInfix_countp_le
Proof state before:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : countp p s + (countp p l₁ + countp p t) = countp p l₂
⊢ countp p l₁ ≤ countp p l₂
Tactic:
rw [← heq]
Proof state after:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : countp p s + (countp p l₁ + countp p t) = countp p l₂
⊢ countp p l₁ ≤ countp p s + (countp p l₁ + countp p t)
Theorem: List.isInfix_countp_le
Proof state before:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <:+: l₂
s t : List α✝
heq : countp p s + (countp p l₁ + countp p t) = countp p l₂
⊢ countp p l₁ ≤ countp p s + (countp p l₁ + countp p t)
Tactic:
linarith
Proof state after:
no goals
Theorem: List.isInfix_count_le
Proof state before:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
h : l₁ <:+: l₂
⊢ count a l₁ ≤ count a l₂
Tactic:
unfold count
Proof state after:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
h : l₁ <:+: l₂
⊢ countp (fun x => x == a) l₁ ≤ countp (fun x => x == a) l₂
Theorem: List.isInfix_count_le
Proof state before:
α : Type u_1
inst✝ : BEq α
a : α
l₁ l₂ : List α
h : l₁ <:+: l₂
⊢ countp (fun x => x == a) l₁ ≤ countp (fun x => x == a) l₂
Tactic:
apply List.isInfix_countp_le h
Proof state after:
no goals
Theorem: List.count_pos_iff_mem
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ count a l > 0 ↔ a ∈ l
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ count a l > 0 → a ∈ l

case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ a ∈ l → count a l > 0
Theorem: List.count_pos_iff_mem
Proof state before:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ count a l > 0 → a ∈ l

case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ a ∈ l → count a l > 0
Tactic:
. intro count_pos
  induction l with
  | nil => simp only [count_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, lt_self_iff_false] at count_pos
  | cons head tail ih=>
    simp only [count_cons, beq_iff_eq, zero_le, ge_iff_le, nonpos_iff_eq_zero, gt_iff_lt, add_pos_iff] at count_pos
    cases count_pos with
    | inl hlt =>
      split at hlt
      case inl heq => simp at heq;  simp [heq]
      case inr heq => simp only at hlt
    | inr hlt =>
      apply mem_cons.2; right
      apply ih hlt
Proof state after:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ a ∈ l → count a l > 0
Theorem: List.count_pos_iff_mem
Proof state before:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ a ∈ l → count a l > 0
Tactic:
. intro ain
  induction l with
  | nil => simp only [not_mem_nil] at ain
  | cons head tail ih => 
    cases mem_cons.1 ain with
    | inl heq =>
      simp only [heq, count_cons, beq_self_eq_true, ite_true, zero_le, ge_iff_le, nonpos_iff_eq_zero, gt_iff_lt,
        add_pos_iff, true_or]
    | inr hin =>
      simp only [count_cons, beq_iff_eq, zero_le, ge_iff_le, nonpos_iff_eq_zero, gt_iff_lt, add_pos_iff, ih hin, or_true]
Proof state after:
no goals
Theorem: List.count_pos_iff_mem
Proof state before:
case mp.nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
count_pos : count a [] > 0
⊢ a ∈ []
Tactic:
simp only [count_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, lt_self_iff_false] at count_pos
Proof state after:
no goals
Theorem: List.count_pos_iff_mem
Proof state before:
case mp.cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
count_pos : count a (head :: tail) > 0
⊢ a ∈ head :: tail
Tactic:
simp only [count_cons, beq_iff_eq, zero_le, ge_iff_le, nonpos_iff_eq_zero, gt_iff_lt, add_pos_iff] at count_pos
Proof state after:
case mp.cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
count_pos : (0 < if (head == a) = true then 1 else 0) ∨ 0 < count a tail
⊢ a ∈ head :: tail
Theorem: List.count_pos_iff_mem
Proof state before:
case mp.cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
count_pos : (0 < if (head == a) = true then 1 else 0) ∨ 0 < count a tail
⊢ a ∈ head :: tail
Tactic:
cases count_pos with
| inl hlt =>
  split at hlt
  case inl heq => simp at heq;  simp [heq]
  case inr heq => simp only at hlt
| inr hlt =>
  apply mem_cons.2; right
  apply ih hlt
Proof state after:
no goals
Theorem: List.count_pos_iff_mem
Proof state before:
case mp.cons.inl
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
hlt : 0 < if (head == a) = true then 1 else 0
⊢ a ∈ head :: tail
Tactic:
split at hlt
Proof state after:
case mp.cons.inl.inl
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
h✝ : (head == a) = true
hlt : 0 < 1
⊢ a ∈ head :: tail

case mp.cons.inl.inr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
h✝ : ¬(head == a) = true
hlt : 0 < 0
⊢ a ∈ head :: tail
Theorem: List.count_pos_iff_mem
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
heq : (head == a) = true
hlt : 0 < 1
⊢ a ∈ head :: tail
Tactic:
case inl heq => simp at heq;  simp [heq]
Proof state after:
no goals
Theorem: List.count_pos_iff_mem
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
heq : ¬(head == a) = true
hlt : 0 < 0
⊢ a ∈ head :: tail
Tactic:
case inr heq => simp only at hlt
Proof state after:
no goals
Theorem: List.count_pos_iff_mem
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
heq : (head == a) = true
hlt : 0 < 1
⊢ a ∈ head :: tail
Tactic:
simp at heq
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
hlt : 0 < 1
heq : head = a
⊢ a ∈ head :: tail
Theorem: List.count_pos_iff_mem
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
hlt : 0 < 1
heq : head = a
⊢ a ∈ head :: tail
Tactic:
simp [heq]
Proof state after:
no goals
Theorem: List.count_pos_iff_mem
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
heq : ¬(head == a) = true
hlt : 0 < 0
⊢ a ∈ head :: tail
Tactic:
simp only at hlt
Proof state after:
no goals
Theorem: List.count_pos_iff_mem
Proof state before:
case mp.cons.inr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
hlt : 0 < count a tail
⊢ a ∈ head :: tail
Tactic:
apply mem_cons.2
Proof state after:
case mp.cons.inr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
hlt : 0 < count a tail
⊢ a = head ∨ a ∈ tail
Theorem: List.count_pos_iff_mem
Proof state before:
case mp.cons.inr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
hlt : 0 < count a tail
⊢ a = head ∨ a ∈ tail
Tactic:
right
Proof state after:
case mp.cons.inr.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : count a tail > 0 → a ∈ tail
hlt : 0 < count a tail
⊢ a ∈ tail