-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable α]
    {m : Imp α β} (H : WF m) : WF (filterMap f m)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → Option γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
g₁ : AssocList α β → List (α × γ) :=
  fun l => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList
a : α
b : β
l : AssocList α β
tail_ih✝ :
  ∀ (n : ULift Nat) (acc : AssocList α γ),
    filterMap.go f acc l n = (((g₁ l).reverse ++ acc.toList).toAssocList, { down := n.down + (g₁ l).length })
n : ULift Nat
acc : AssocList α γ
c : γ
⊢ {
      down :=
        n.down + (List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).length +
          1 } =
    {
      down :=
        n.down +
          ((List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).length + 1) }

Tactic:
rfl

Result:
no goals

Proof state:
case refl.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → Option γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
g₁ : AssocList α β → List (α × γ) :=
  fun l => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList
H1 :
  ∀ (l : AssocList α β) (n : ULift Nat) (acc : AssocList α γ),
    filterMap.go f acc l n = (((g₁ l).reverse ++ acc.toList).toAssocList, { down := n.down + (g₁ l).length })
g : AssocList α β → AssocList α γ := fun l => (g₁ l).reverse.toAssocList
M : Type (max u_3 u_1) → Type (max u_3 u_1) := StateT (ULift Nat) Id
H2 :
  ∀ (l : List (AssocList α β)) (n : ULift Nat),
    List.mapM (filterMap.go f AssocList.nil) l n =
      (List.map g l, { down := n.down + (List.map (fun x => x.toList.length) (List.map g l)).sum })
H3 :
  ∀ (l : List (α × β)),
    (List.map (fun a => a.fst)
          (List.filterMap
            (fun x =>
              match x with
              | (a, b) => Option.map (fun x => (a, x)) (f a b))
            l)).Sublist
      (List.map (fun x => x.fst) l)
h✝¹ :
  0 <
    (List.map (fun l => (g₁ l).reverse.toAssocList) m.buckets.val.toList,
          {
            down :=
              (List.map ((fun x => x.toList.length) ∘ fun l => (g₁ l).reverse.toAssocList)
                  m.buckets.val.toList).sum }).fst.length
i : Nat
h✝ :
  i <
    { size := (List.map ((fun x => x.toList.length) ∘ fun l => (g₁ l).reverse.toAssocList) m.buckets.val.toList).sum,
            buckets :=
              ⟨{
                  toList :=
                    (List.map (fun l => (g₁ l).reverse.toAssocList) m.buckets.val.toList,
                        {
                          down :=
                            (List.map ((fun x => x.toList.length) ∘ fun l => (g₁ l).reverse.toAssocList)
                                m.buckets.val.toList).sum }).fst },
                h✝¹⟩ }.buckets.val.size
h : i < m.buckets.val.size
this : ∀ (a : α × β), a ∈ m.buckets.val[i].toList → ((hash a.fst).toUSize % USize.ofNat m.buckets.val.size).toNat = i
⊢ ∀ (a : α × γ) (x : α × β),
    x ∈ m.buckets.val.toList[i].toList →
      ∀ (x_1 : γ),
        f x.fst x.snd = some x_1 → (x.fst, x_1) = a → ((hash a.fst).toUSize % USize.ofNat m.buckets.val.size).toNat = i

Tactic:
rintro _ _ h' _ _ rfl

Result:
case refl.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → Option γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
g₁ : AssocList α β → List (α × γ) :=
  fun l => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList
H1 :
  ∀ (l : AssocList α β) (n : ULift Nat) (acc : AssocList α γ),
    filterMap.go f acc l n = (((g₁ l).reverse ++ acc.toList).toAssocList, { down := n.down + (g₁ l).length })
g : AssocList α β → AssocList α γ := fun l => (g₁ l).reverse.toAssocList
M : Type (max u_3 u_1) → Type (max u_3 u_1) := StateT (ULift Nat) Id
H2 :
  ∀ (l : List (AssocList α β)) (n : ULift Nat),
    List.mapM (filterMap.go f AssocList.nil) l n =
      (List.map g l, { down := n.down + (List.map (fun x => x.toList.length) (List.map g l)).sum })
H3 :
  ∀ (l : List (α × β)),
    (List.map (fun a => a.fst)
          (List.filterMap
            (fun x =>
              match x with
              | (a, b) => Option.map (fun x => (a, x)) (f a b))
            l)).Sublist
      (List.map (fun x => x.fst) l)
h✝¹ :
  0 <
    (List.map (fun l => (g₁ l).reverse.toAssocList) m.buckets.val.toList,
          {
            down :=
              (List.map ((fun x => x.toList.length) ∘ fun l => (g₁ l).reverse.toAssocList)
                  m.buckets.val.toList).sum }).fst.length
i : Nat
h✝ :
  i <
    { size := (List.map ((fun x => x.toList.length) ∘ fun l => (g₁ l).reverse.toAssocList) m.buckets.val.toList).sum,
            buckets :=
              ⟨{
                  toList :=
                    (List.map (fun l => (g₁ l).reverse.toAssocList) m.buckets.val.toList,
                        {
                          down :=
                            (List.map ((fun x => x.toList.length) ∘ fun l => (g₁ l).reverse.toAssocList)
                                m.buckets.val.toList).sum }).fst },
                h✝¹⟩ }.buckets.val.size
h : i < m.buckets.val.size
this : ∀ (a : α × β), a ∈ m.buckets.val[i].toList → ((hash a.fst).toUSize % USize.ofNat m.buckets.val.size).toNat = i
x✝¹ : α × β
h' : x✝¹ ∈ m.buckets.val.toList[i].toList
x✝ : γ
a✝ : f x✝¹.fst x✝¹.snd = some x✝
⊢ ((hash (x✝¹.fst, x✝).fst).toUSize % USize.ofNat m.buckets.val.size).toNat = i

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → Option γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
g₁ : AssocList α β → List (α × γ) :=
  fun l => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList
a : α
b : β
l : AssocList α β
tail_ih✝ :
  ∀ (n : ULift Nat) (acc : AssocList α γ),
    filterMap.go f acc l n = (((g₁ l).reverse ++ acc.toList).toAssocList, { down := n.down + (g₁ l).length })
n : ULift Nat
acc : AssocList α γ
c : γ
⊢ {
      down :=
        n.down + 1 +
          (List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).length } =
    {
      down :=
        n.down +
          ((List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).length + 1) }

Tactic:
rw [Nat.add_right_comm]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → Option γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
g₁ : AssocList α β → List (α × γ) :=
  fun l => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList
a : α
b : β
l : AssocList α β
tail_ih✝ :
  ∀ (n : ULift Nat) (acc : AssocList α γ),
    filterMap.go f acc l n = (((g₁ l).reverse ++ acc.toList).toAssocList, { down := n.down + (g₁ l).length })
n : ULift Nat
acc : AssocList α γ
c : γ
⊢ {
      down :=
        n.down + (List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).length +
          1 } =
    {
      down :=
        n.down +
          ((List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).length + 1) }