-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_length_eq_length {l} :
    (filterMap f l).length = l.length ↔ ∀ a ∈ l, (f a).isSome

Proof state:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (filterMap f l).length = l.length ↔ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true
⊢ (filterMap f (a :: l)).length = (a :: l).length ↔ ∀ (a_1 : α✝¹), a_1 ∈ a :: l → (f a_1).isSome = true

Tactic:
simp only [filterMap_cons, length_cons, succ_eq_add_one, mem_cons, forall_eq_or_imp]

Result:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (filterMap f l).length = l.length ↔ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true
⊢ (match f a with
        | none => filterMap f l
        | some b => b :: filterMap f l).length =
      l.length + 1 ↔
    (f a).isSome = true ∧ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true

Proof state:
case nil
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
⊢ (filterMap f []).length = [].length ↔ ∀ (a : α✝¹), a ∈ [] → (f a).isSome = true

Tactic:
simp

Result:
no goals

Proof state:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (filterMap f l).length = l.length ↔ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true
⊢ (match f a with
        | none => filterMap f l
        | some b => b :: filterMap f l).length =
      l.length + 1 ↔
    (f a).isSome = true ∧ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true

Tactic:
split <;> rename_i h

Result:
case cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (filterMap f l).length = l.length ↔ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true
x✝ : Option α✝
h : f a = none
⊢ (filterMap f l).length = l.length + 1 ↔ (f a).isSome = true ∧ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true

case cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (filterMap f l).length = l.length ↔ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true
x✝ : Option α✝
b✝ : α✝
h : f a = some b✝
⊢ (b✝ :: filterMap f l).length = l.length + 1 ↔ (f a).isSome = true ∧ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true

Proof state:
case cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (filterMap f l).length = l.length ↔ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true
x✝ : Option α✝
h : f a = none
⊢ (filterMap f l).length = l.length + 1 ↔ (f a).isSome = true ∧ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true

Tactic:
have := Nat.ne_of_lt (Nat.lt_succ.mpr (length_filterMap_le f l))

Result:
case cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (filterMap f l).length = l.length ↔ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true
x✝ : Option α✝
h : f a = none
this : (filterMap f l).length ≠ l.length.succ
⊢ (filterMap f l).length = l.length + 1 ↔ (f a).isSome = true ∧ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true

Proof state:
case cons.h_2
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (filterMap f l).length = l.length ↔ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true
x✝ : Option α✝
b✝ : α✝
h : f a = some b✝
⊢ (b✝ :: filterMap f l).length = l.length + 1 ↔ (f a).isSome = true ∧ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true

Tactic:
simp_all [Nat.add_one_inj]

Result:
no goals

Proof state:
case cons.h_1
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
ih : (filterMap f l).length = l.length ↔ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true
x✝ : Option α✝
h : f a = none
this : (filterMap f l).length ≠ l.length.succ
⊢ (filterMap f l).length = l.length + 1 ↔ (f a).isSome = true ∧ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true

Tactic:
simp_all

Result:
no goals