Theorem: List.length_counts_aux (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
acc : List (α × Nat)
⊢ length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
Tactic:
induction xs generalizing acc with
| nil => simp [foldl, uniqueAux]
| cons x xs ih =>
  simp only [uniqueAux, foldl]
  cases acc with
  | nil =>
    simp only [incrCounts, map, List.not_mem_nil, ite_false]
    apply ih
  | cons a as =>
    simp only [incrCounts]
    cases Decidable.em (a.1 = x) with
    | inl htrue =>
      simp only [htrue, ite_true, incrCounts, map]
      rw [if_pos]
      . apply ih
      . exact List.Mem.head _
    | inr hfalse =>
      simp only [hfalse, ite_false, incrCounts, map]
      rw [ih]
      cases Decidable.em (x ∈ map Prod.fst as) with
      | inl hin =>
        have : x ∈ a.1 :: map Prod.fst as := List.Mem.tail _ hin
        simp only [this, ite_true, map, uniqueAux]
        apply congrArg
        apply congrArg
        apply congrArg
        exact map_fst_incrCounts_eq_map_fst x as hin
      | inr hout =>
        have : ¬ (x ∈ a.1 :: map Prod.fst as) := by
          intros hneg; cases hneg; repeat contradiction
        simp only [this, ite_false, map]
        rw [map_fst_incrCounts_eq_cons_fst _ _ hout]
        apply List.length_uniqueAux_congr_append_cons_acc _ _ _ _ []
State after:
no goals

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
acc : List (α × Nat)
⊢ length (foldl (fun acc v => incrCounts acc v) acc []) = length (uniqueAux [] (map Prod.fst acc))
Tactic:
simp [foldl, uniqueAux]
State after:
no goals

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
acc : List (α × Nat)
⊢ length (foldl (fun acc v => incrCounts acc v) acc (x :: xs)) = length (uniqueAux (x :: xs) (map Prod.fst acc))
Tactic:
simp only [uniqueAux, foldl]
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
acc : List (α × Nat)
⊢ length (foldl (fun acc v => incrCounts acc v) (incrCounts acc x) xs) =
    length (if x ∈ map Prod.fst acc then uniqueAux xs (map Prod.fst acc) else uniqueAux xs (x :: map Prod.fst acc))

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
acc : List (α × Nat)
⊢ length (foldl (fun acc v => incrCounts acc v) (incrCounts acc x) xs) =
    length (if x ∈ map Prod.fst acc then uniqueAux xs (map Prod.fst acc) else uniqueAux xs (x :: map Prod.fst acc))
Tactic:
cases acc with
| nil =>
  simp only [incrCounts, map, List.not_mem_nil, ite_false]
  apply ih
| cons a as =>
  simp only [incrCounts]
  cases Decidable.em (a.1 = x) with
  | inl htrue =>
    simp only [htrue, ite_true, incrCounts, map]
    rw [if_pos]
    . apply ih
    . exact List.Mem.head _
  | inr hfalse =>
    simp only [hfalse, ite_false, incrCounts, map]
    rw [ih]
    cases Decidable.em (x ∈ map Prod.fst as) with
    | inl hin =>
      have : x ∈ a.1 :: map Prod.fst as := List.Mem.tail _ hin
      simp only [this, ite_true, map, uniqueAux]
      apply congrArg
      apply congrArg
      apply congrArg
      exact map_fst_incrCounts_eq_map_fst x as hin
    | inr hout =>
      have : ¬ (x ∈ a.1 :: map Prod.fst as) := by
        intros hneg; cases hneg; repeat contradiction
      simp only [this, ite_false, map]
      rw [map_fst_incrCounts_eq_cons_fst _ _ hout]
      apply List.length_uniqueAux_congr_append_cons_acc _ _ _ _ []
State after:
no goals

State before:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
⊢ length (foldl (fun acc v => incrCounts acc v) (incrCounts [] x) xs) =
    length (if x ∈ map Prod.fst [] then uniqueAux xs (map Prod.fst []) else uniqueAux xs (x :: map Prod.fst []))
Tactic:
simp only [incrCounts, map, List.not_mem_nil, ite_false]
State after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
⊢ length (foldl (fun acc v => incrCounts acc v) [(x, 1)] xs) = length (uniqueAux xs [x])

State before:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
⊢ length (foldl (fun acc v => incrCounts acc v) [(x, 1)] xs) = length (uniqueAux xs [x])
Tactic:
apply ih
State after:
no goals

State before:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
⊢ length (foldl (fun acc v => incrCounts acc v) (incrCounts (a :: as) x) xs) =
    length
      (if x ∈ map Prod.fst (a :: as) then uniqueAux xs (map Prod.fst (a :: as))
      else uniqueAux xs (x :: map Prod.fst (a :: as)))
Tactic:
simp only [incrCounts]
State after:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
⊢ length
      (foldl (fun acc v => incrCounts acc v)
        (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) xs) =
    length
      (if x ∈ map Prod.fst (a :: as) then uniqueAux xs (map Prod.fst (a :: as))
      else uniqueAux xs (x :: map Prod.fst (a :: as)))

State before:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
⊢ length
      (foldl (fun acc v => incrCounts acc v)
        (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) xs) =
    length
      (if x ∈ map Prod.fst (a :: as) then uniqueAux xs (map Prod.fst (a :: as))
      else uniqueAux xs (x :: map Prod.fst (a :: as)))
Tactic:
cases Decidable.em (a.1 = x) with
| inl htrue =>
  simp only [htrue, ite_true, incrCounts, map]
  rw [if_pos]
  . apply ih
  . exact List.Mem.head _
| inr hfalse =>
  simp only [hfalse, ite_false, incrCounts, map]
  rw [ih]
  cases Decidable.em (x ∈ map Prod.fst as) with
  | inl hin =>
    have : x ∈ a.1 :: map Prod.fst as := List.Mem.tail _ hin
    simp only [this, ite_true, map, uniqueAux]
    apply congrArg
    apply congrArg
    apply congrArg
    exact map_fst_incrCounts_eq_map_fst x as hin
  | inr hout =>
    have : ¬ (x ∈ a.1 :: map Prod.fst as) := by
      intros hneg; cases hneg; repeat contradiction
    simp only [this, ite_false, map]
    rw [map_fst_incrCounts_eq_cons_fst _ _ hout]
    apply List.length_uniqueAux_congr_append_cons_acc _ _ _ _ []
State after:
no goals

State before:
case cons.cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
htrue : a.fst = x
⊢ length
      (foldl (fun acc v => incrCounts acc v)
        (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) xs) =
    length
      (if x ∈ map Prod.fst (a :: as) then uniqueAux xs (map Prod.fst (a :: as))
      else uniqueAux xs (x :: map Prod.fst (a :: as)))
Tactic:
simp only [htrue, ite_true, incrCounts, map]
State after:
case cons.cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
htrue : a.fst = x
⊢ length (foldl (fun acc v => incrCounts acc v) ((x, a.snd + 1) :: as) xs) =
    length
      (if x ∈ x :: map Prod.fst as then uniqueAux xs (x :: map Prod.fst as)
      else uniqueAux xs (x :: x :: map Prod.fst as))

State before:
case cons.cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
htrue : a.fst = x
⊢ length (foldl (fun acc v => incrCounts acc v) ((x, a.snd + 1) :: as) xs) =
    length
      (if x ∈ x :: map Prod.fst as then uniqueAux xs (x :: map Prod.fst as)
      else uniqueAux xs (x :: x :: map Prod.fst as))
Tactic:
rw [if_pos]
State after:
case cons.cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
htrue : a.fst = x
⊢ length (foldl (fun acc v => incrCounts acc v) ((x, a.snd + 1) :: as) xs) =
    length (uniqueAux xs (x :: map Prod.fst as))

case cons.cons.inl.hc
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
htrue : a.fst = x
⊢ x ∈ x :: map Prod.fst as

State before:
case cons.cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
htrue : a.fst = x
⊢ length (foldl (fun acc v => incrCounts acc v) ((x, a.snd + 1) :: as) xs) =
    length (uniqueAux xs (x :: map Prod.fst as))

case cons.cons.inl.hc
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
htrue : a.fst = x
⊢ x ∈ x :: map Prod.fst as
Tactic:
. apply ih
State after:
case cons.cons.inl.hc
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
htrue : a.fst = x
⊢ x ∈ x :: map Prod.fst as

State before:
case cons.cons.inl.hc
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
htrue : a.fst = x
⊢ x ∈ x :: map Prod.fst as
Tactic:
. exact List.Mem.head _
State after:
no goals

State before:
case cons.cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
htrue : a.fst = x
⊢ length (foldl (fun acc v => incrCounts acc v) ((x, a.snd + 1) :: as) xs) =
    length (uniqueAux xs (x :: map Prod.fst as))
Tactic:
apply ih
State after:
no goals

State before:
case cons.cons.inl.hc
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
htrue : a.fst = x
⊢ x ∈ x :: map Prod.fst as
Tactic:
exact List.Mem.head _
State after:
no goals

State before:
case cons.cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
⊢ length
      (foldl (fun acc v => incrCounts acc v)
        (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) xs) =
    length
      (if x ∈ map Prod.fst (a :: as) then uniqueAux xs (map Prod.fst (a :: as))
      else uniqueAux xs (x :: map Prod.fst (a :: as)))
Tactic:
simp only [hfalse, ite_false, incrCounts, map]
State after:
case cons.cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
⊢ length (foldl (fun acc v => incrCounts acc v) ((a.fst, a.snd) :: incrCounts as x) xs) =
    length
      (if x ∈ a.fst :: map Prod.fst as then uniqueAux xs (a.fst :: map Prod.fst as)
      else uniqueAux xs (x :: a.fst :: map Prod.fst as))

State before:
case cons.cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
⊢ length (foldl (fun acc v => incrCounts acc v) ((a.fst, a.snd) :: incrCounts as x) xs) =
    length
      (if x ∈ a.fst :: map Prod.fst as then uniqueAux xs (a.fst :: map Prod.fst as)
      else uniqueAux xs (x :: a.fst :: map Prod.fst as))
Tactic:
rw [ih]
State after:
case cons.cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
⊢ length (uniqueAux xs (map Prod.fst ((a.fst, a.snd) :: incrCounts as x))) =
    length
      (if x ∈ a.fst :: map Prod.fst as then uniqueAux xs (a.fst :: map Prod.fst as)
      else uniqueAux xs (x :: a.fst :: map Prod.fst as))

State before:
case cons.cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
⊢ length (uniqueAux xs (map Prod.fst ((a.fst, a.snd) :: incrCounts as x))) =
    length
      (if x ∈ a.fst :: map Prod.fst as then uniqueAux xs (a.fst :: map Prod.fst as)
      else uniqueAux xs (x :: a.fst :: map Prod.fst as))
Tactic:
cases Decidable.em (x ∈ map Prod.fst as) with
| inl hin =>
  have : x ∈ a.1 :: map Prod.fst as := List.Mem.tail _ hin
  simp only [this, ite_true, map, uniqueAux]
  apply congrArg
  apply congrArg
  apply congrArg
  exact map_fst_incrCounts_eq_map_fst x as hin
| inr hout =>
  have : ¬ (x ∈ a.1 :: map Prod.fst as) := by
    intros hneg; cases hneg; repeat contradiction
  simp only [this, ite_false, map]
  rw [map_fst_incrCounts_eq_cons_fst _ _ hout]
  apply List.length_uniqueAux_congr_append_cons_acc _ _ _ _ []
State after:
no goals

State before:
case cons.cons.inr.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hin : x ∈ map Prod.fst as
⊢ length (uniqueAux xs (map Prod.fst ((a.fst, a.snd) :: incrCounts as x))) =
    length
      (if x ∈ a.fst :: map Prod.fst as then uniqueAux xs (a.fst :: map Prod.fst as)
      else uniqueAux xs (x :: a.fst :: map Prod.fst as))
Tactic:
have : x ∈ a.1 :: map Prod.fst as := List.Mem.tail _ hin
State after:
case cons.cons.inr.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hin : x ∈ map Prod.fst as
this : x ∈ a.fst :: map Prod.fst as
⊢ length (uniqueAux xs (map Prod.fst ((a.fst, a.snd) :: incrCounts as x))) =
    length
      (if x ∈ a.fst :: map Prod.fst as then uniqueAux xs (a.fst :: map Prod.fst as)
      else uniqueAux xs (x :: a.fst :: map Prod.fst as))

State before:
case cons.cons.inr.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hin : x ∈ map Prod.fst as
this : x ∈ a.fst :: map Prod.fst as
⊢ length (uniqueAux xs (map Prod.fst ((a.fst, a.snd) :: incrCounts as x))) =
    length
      (if x ∈ a.fst :: map Prod.fst as then uniqueAux xs (a.fst :: map Prod.fst as)
      else uniqueAux xs (x :: a.fst :: map Prod.fst as))
Tactic:
simp only [this, ite_true, map, uniqueAux]
State after:
case cons.cons.inr.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hin : x ∈ map Prod.fst as
this : x ∈ a.fst :: map Prod.fst as
⊢ length (uniqueAux xs (a.fst :: map Prod.fst (incrCounts as x))) = length (uniqueAux xs (a.fst :: map Prod.fst as))

State before:
case cons.cons.inr.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hin : x ∈ map Prod.fst as
this : x ∈ a.fst :: map Prod.fst as
⊢ length (uniqueAux xs (a.fst :: map Prod.fst (incrCounts as x))) = length (uniqueAux xs (a.fst :: map Prod.fst as))
Tactic:
apply congrArg
State after:
case cons.cons.inr.inl.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hin : x ∈ map Prod.fst as
this : x ∈ a.fst :: map Prod.fst as
⊢ uniqueAux xs (a.fst :: map Prod.fst (incrCounts as x)) = uniqueAux xs (a.fst :: map Prod.fst as)

State before:
case cons.cons.inr.inl.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hin : x ∈ map Prod.fst as
this : x ∈ a.fst :: map Prod.fst as
⊢ uniqueAux xs (a.fst :: map Prod.fst (incrCounts as x)) = uniqueAux xs (a.fst :: map Prod.fst as)
Tactic:
apply congrArg
State after:
case cons.cons.inr.inl.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hin : x ∈ map Prod.fst as
this : x ∈ a.fst :: map Prod.fst as
⊢ a.fst :: map Prod.fst (incrCounts as x) = a.fst :: map Prod.fst as

State before:
case cons.cons.inr.inl.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hin : x ∈ map Prod.fst as
this : x ∈ a.fst :: map Prod.fst as
⊢ a.fst :: map Prod.fst (incrCounts as x) = a.fst :: map Prod.fst as
Tactic:
apply congrArg
State after:
case cons.cons.inr.inl.h.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hin : x ∈ map Prod.fst as
this : x ∈ a.fst :: map Prod.fst as
⊢ map Prod.fst (incrCounts as x) = map Prod.fst as

State before:
case cons.cons.inr.inl.h.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hin : x ∈ map Prod.fst as
this : x ∈ a.fst :: map Prod.fst as
⊢ map Prod.fst (incrCounts as x) = map Prod.fst as
Tactic:
exact map_fst_incrCounts_eq_map_fst x as hin
State after:
no goals

State before:
case cons.cons.inr.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
⊢ length (uniqueAux xs (map Prod.fst ((a.fst, a.snd) :: incrCounts as x))) =
    length
      (if x ∈ a.fst :: map Prod.fst as then uniqueAux xs (a.fst :: map Prod.fst as)
      else uniqueAux xs (x :: a.fst :: map Prod.fst as))
Tactic:
have : ¬ (x ∈ a.1 :: map Prod.fst as) := by
  intros hneg; cases hneg; repeat contradiction
State after:
case cons.cons.inr.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
this : ¬x ∈ a.fst :: map Prod.fst as
⊢ length (uniqueAux xs (map Prod.fst ((a.fst, a.snd) :: incrCounts as x))) =
    length
      (if x ∈ a.fst :: map Prod.fst as then uniqueAux xs (a.fst :: map Prod.fst as)
      else uniqueAux xs (x :: a.fst :: map Prod.fst as))

State before:
case cons.cons.inr.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
this : ¬x ∈ a.fst :: map Prod.fst as
⊢ length (uniqueAux xs (map Prod.fst ((a.fst, a.snd) :: incrCounts as x))) =
    length
      (if x ∈ a.fst :: map Prod.fst as then uniqueAux xs (a.fst :: map Prod.fst as)
      else uniqueAux xs (x :: a.fst :: map Prod.fst as))
Tactic:
simp only [this, ite_false, map]
State after:
case cons.cons.inr.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
this : ¬x ∈ a.fst :: map Prod.fst as
⊢ length (uniqueAux xs (a.fst :: map Prod.fst (incrCounts as x))) =
    length (uniqueAux xs (x :: a.fst :: map Prod.fst as))

State before:
case cons.cons.inr.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
this : ¬x ∈ a.fst :: map Prod.fst as
⊢ length (uniqueAux xs (a.fst :: map Prod.fst (incrCounts as x))) =
    length (uniqueAux xs (x :: a.fst :: map Prod.fst as))
Tactic:
rw [map_fst_incrCounts_eq_cons_fst _ _ hout]
State after:
case cons.cons.inr.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
this : ¬x ∈ a.fst :: map Prod.fst as
⊢ length (uniqueAux xs (a.fst :: (map Prod.fst as ++ [x]))) = length (uniqueAux xs (x :: a.fst :: map Prod.fst as))

State before:
case cons.cons.inr.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
this : ¬x ∈ a.fst :: map Prod.fst as
⊢ length (uniqueAux xs (a.fst :: (map Prod.fst as ++ [x]))) = length (uniqueAux xs (x :: a.fst :: map Prod.fst as))
Tactic:
apply List.length_uniqueAux_congr_append_cons_acc _ _ _ _ []
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
⊢ ¬x ∈ a.fst :: map Prod.fst as
Tactic:
intros hneg
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
hneg : x ∈ a.fst :: map Prod.fst as
⊢ False

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
hneg : x ∈ a.fst :: map Prod.fst as
⊢ False
Tactic:
cases hneg
State after:
case head
α : Type u_1
inst✝ : DecidableEq α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = a.fst
hout : ¬a.fst ∈ map Prod.fst as
⊢ False

case tail
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
a✝ : Mem x (map Prod.fst as)
⊢ False

State before:
case head
α : Type u_1
inst✝ : DecidableEq α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = a.fst
hout : ¬a.fst ∈ map Prod.fst as
⊢ False

case tail
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
a✝ : Mem x (map Prod.fst as)
⊢ False
Tactic:
repeat contradiction
State after:
no goals

State before:
case tail
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
a✝ : Mem x (map Prod.fst as)
⊢ False
Tactic:
contradiction
State after:
no goals