-- 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 nil
α : 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 })
⊢ (List.map (fun a => a.fst)
        (List.filterMap
          (fun x =>
            match x with
            | (a, b) => Option.map (fun x => (a, x)) (f a b))
          [])).Sublist
    (List.map (fun x => x.fst) [])

Tactic:
exact .slnil

Result:
no goals

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
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 })

Tactic:
induction l generalizing n acc with simp only [filterMap.go, AssocList.toList,
  List.filterMap_nil, List.reverse_nil, List.nil_append, AssocList.toList_toAssocList,
  List.length_nil, Nat.add_zero, List.filterMap_cons, g₁, *]
| cons a b l => match f a b with
  | none => rfl
  | some c =>
    simp only [Option.map_some', List.reverse_cons, List.append_assoc, List.singleton_append,
      List.length_cons, Nat.succ_eq_add_one, Prod.mk.injEq, true_and]
    rw [Nat.add_right_comm]
    rfl

Result:
no goals

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 : γ
⊢ (match some c with
    | none =>
      (((List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).reverse ++
            acc.toList).toAssocList,
        {
          down :=
            n.down + (List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).length })
    | some c =>
      (((List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).reverse ++
            (a, c) :: acc.toList).toAssocList,
        {
          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 })) =
    (((match Option.map (fun x => (a, x)) (some c) with
            | none => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList
            | some b =>
              b :: List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).reverse ++
          acc.toList).toAssocList,
      {
        down :=
          n.down +
            (match Option.map (fun x => (a, x)) (some c) with
              | none => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList
              | some b =>
                b :: List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).length })

Tactic:
simp only [Option.map_some', List.reverse_cons, List.append_assoc, List.singleton_append,
  List.length_cons, Nat.succ_eq_add_one, Prod.mk.injEq, true_and]

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 + 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) }

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 α γ
⊢ (match none with
    | none =>
      (((List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).reverse ++
            acc.toList).toAssocList,
        {
          down :=
            n.down + (List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).length })
    | some c =>
      (((List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).reverse ++
            (a, c) :: acc.toList).toAssocList,
        {
          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 })) =
    (((match Option.map (fun x => (a, x)) none with
            | none => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList
            | some b =>
              b :: List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).reverse ++
          acc.toList).toAssocList,
      {
        down :=
          n.down +
            (match Option.map (fun x => (a, x)) none with
              | none => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList
              | some b =>
                b :: List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList).length })

Tactic:
rfl

Result:
no goals