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

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
snd✝ : Nat
as : List (α × Nat)
⊢ map Prod.fst (incrCounts ((x, snd✝) :: as) x) = map Prod.fst ((x, snd✝) :: as)
Tactic:
simp only [map, incrCounts]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
h' : Mem x (map Prod.fst as)
ih : map Prod.fst (incrCounts as x) = map Prod.fst as
heq : a.fst = x
⊢ map Prod.fst (incrCounts (a :: as) x) = map Prod.fst (a :: as)
Tactic:
simp only [map, incrCounts, heq, ite_true, map]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
h' : Mem x (map Prod.fst as)
ih : map Prod.fst (incrCounts as x) = map Prod.fst as
hneq : ¬a.fst = x
⊢ map Prod.fst (incrCounts (a :: as) x) = map Prod.fst (a :: as)
Tactic:
simp only [hneq, ite_false, map, incrCounts]
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
h' : Mem x (map Prod.fst as)
ih : map Prod.fst (incrCounts as x) = map Prod.fst as
hneq : ¬a.fst = x
⊢ a.fst :: map Prod.fst (incrCounts as x) = a.fst :: map Prod.fst as

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
h' : Mem x (map Prod.fst as)
ih : map Prod.fst (incrCounts as x) = map Prod.fst as
hneq : ¬a.fst = x
⊢ a.fst :: map Prod.fst (incrCounts as x) = a.fst :: map Prod.fst as
Tactic:
exact congrArg _ ih
State after:
no goals