Theorem: List.count_pos_iff_mem (One.lean)

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ count a l > 0 ↔ a ∈ l
Tactic:
apply Iff.intro
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

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
State after:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ a ∈ l → count a l > 0

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]
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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]
State after:
no goals

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
State after:
no goals

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
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

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]
State after:
no goals

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
State after:
no goals

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
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

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
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

State before:
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
Tactic:
apply ih hlt
State after:
no goals

State before:
case mpr.nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
ain : a ∈ []
⊢ count a [] > 0
Tactic:
simp only [not_mem_nil] at ain
State after:
no goals

State before:
case mpr.cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : a ∈ tail → count a tail > 0
ain : a ∈ head :: tail
⊢ count a (head :: tail) > 0
Tactic:
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]
State after:
no goals

State before:
case mpr.cons.inl
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : a ∈ tail → count a tail > 0
ain : a ∈ head :: tail
heq : a = head
⊢ count a (head :: tail) > 0
Tactic:
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]
State after:
no goals

State before:
case mpr.cons.inr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head : α
tail : List α
ih : a ∈ tail → count a tail > 0
ain : a ∈ head :: tail
hin : a ∈ tail
⊢ count a (head :: tail) > 0
Tactic:
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]
State after:
no goals