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

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
⊢ ∀ (as : List (α × Nat)), ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
Tactic:
intros as h
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
as : List (α × Nat)
h : ¬x ∈ map Prod.fst as
⊢ map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
as : List (α × Nat)
h : ¬x ∈ map Prod.fst as
⊢ map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
Tactic:
induction as with
| nil =>
  simp only [incrCounts, map, HAppend.hAppend, Append.append, List.append]
| cons a as ih =>
  simp only [map, incrCounts]
  cases Decidable.em (a.1 = x) with
  | inl heq =>
    apply absurd h
    apply not_not
    simp only [map, heq]
    apply List.Mem.head
  | inr hneq =>
    simp only [hneq, ite_false, map]
    apply congrArg
    apply ih
    . intros hneg
      apply h
      apply List.Mem.tail _ hneg
State after:
no goals

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : ¬x ∈ map Prod.fst []
⊢ map Prod.fst (incrCounts [] x) = map Prod.fst [] ++ [x]
Tactic:
simp only [incrCounts, map, HAppend.hAppend, Append.append, List.append]
State after:
no goals

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
⊢ map Prod.fst (incrCounts (a :: as) x) = map Prod.fst (a :: as) ++ [x]
Tactic:
simp only [map, incrCounts]
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
⊢ map Prod.fst (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) =
    a.fst :: map Prod.fst as ++ [x]

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
⊢ map Prod.fst (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) =
    a.fst :: map Prod.fst as ++ [x]
Tactic:
cases Decidable.em (a.1 = x) with
| inl heq =>
  apply absurd h
  apply not_not
  simp only [map, heq]
  apply List.Mem.head
| inr hneq =>
  simp only [hneq, ite_false, map]
  apply congrArg
  apply ih
  . intros hneg
    apply h
    apply List.Mem.tail _ hneg
State after:
no goals

State before:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ map Prod.fst (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) =
    a.fst :: map Prod.fst as ++ [x]
Tactic:
apply absurd h
State after:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ ¬¬x ∈ map Prod.fst (a :: as)

State before:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ ¬¬x ∈ map Prod.fst (a :: as)
Tactic:
apply not_not
State after:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ x ∈ map Prod.fst (a :: as)

State before:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ x ∈ map Prod.fst (a :: as)
Tactic:
simp only [map, heq]
State after:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ x ∈ x :: map Prod.fst as

State before:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
heq : a.fst = x
⊢ x ∈ x :: map Prod.fst as
Tactic:
apply List.Mem.head
State after:
no goals

State before:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ map Prod.fst (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) =
    a.fst :: map Prod.fst as ++ [x]
Tactic:
simp only [hneq, ite_false, map]
State after:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ a.fst :: map Prod.fst (incrCounts as x) = a.fst :: map Prod.fst as ++ [x]

State before:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ a.fst :: map Prod.fst (incrCounts as x) = a.fst :: map Prod.fst as ++ [x]
Tactic:
apply congrArg
State after:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ map Prod.fst (incrCounts as x) = List.append (map Prod.fst as) [x]

State before:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ map Prod.fst (incrCounts as x) = List.append (map Prod.fst as) [x]
Tactic:
apply ih
State after:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ ¬x ∈ map Prod.fst as

State before:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ ¬x ∈ map Prod.fst as
Tactic:
. intros hneg
  apply h
  apply List.Mem.tail _ hneg
State after:
no goals

State before:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
⊢ ¬x ∈ map Prod.fst as
Tactic:
intros hneg
State after:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
hneg : x ∈ map Prod.fst as
⊢ False

State before:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
hneg : x ∈ map Prod.fst as
⊢ False
Tactic:
apply h
State after:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
hneg : x ∈ map Prod.fst as
⊢ x ∈ map Prod.fst (a :: as)

State before:
case cons.inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
hneq : ¬a.fst = x
hneg : x ∈ map Prod.fst as
⊢ x ∈ map Prod.fst (a :: as)
Tactic:
apply List.Mem.tail _ hneg
State after:
no goals