-- 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:
case cons
α : 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 })
a : α × β
l : List (α × β)
ih :
  (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)
⊢ (List.map (fun a => a.fst)
        (match Option.map (fun x => (a.fst, x)) (f a.fst a.snd) with
        | none => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l
        | some b => b :: List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l)).Sublist
    (a.fst :: List.map (fun x => x.fst) l)

Tactic:
exact match f a.1 a.2 with
| none => .cons _ ih
| some b => .cons₂ _ ih

Result:
no goals

Proof state:
case refl.refine_1
α : 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
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
l : AssocList α β
h : l ∈ m.buckets.val.toList
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (g₁ l)

Tactic:
have := H.out.2.1 _ h

Result:
case refl.refine_1
α : 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
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
l : AssocList α β
h : l ∈ m.buckets.val.toList
this : List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l.toList
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (g₁ l)

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
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)
⊢ ∀ (bk : List (AssocList α γ)) (sz : Nat) (h : 0 < bk.length),
    (do
          let __discr ←
            (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 })
          pure (__discr.fst.toArray, __discr.snd)) =
        ({ toList := bk }, { down := sz }) →
      { size := sz, buckets := ⟨{ toList := bk }, h⟩ }.WF

Tactic:
intro bk sz h e'

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
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)
bk : List (AssocList α γ)
sz : Nat
h : 0 < bk.length
e' :
  (do
      let __discr ←
        (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 })
      pure (__discr.fst.toArray, __discr.snd)) =
    ({ toList := bk }, { down := sz })
⊢ { size := sz, buckets := ⟨{ toList := bk }, h⟩ }.WF