-- Mathlib/Data/List/Basic.lean
theorem filterMap_eq_map_iff_forall_eq_some {f : α → Option β} {g : α → β} {l : List α} :
    l.filterMap f = l.map g ↔ ∀ x ∈ l, f x = some (g x) where
  mp

Proof state:
α : Type u
β : Type v
f : α → Option β
g : α → β
l : List α
⊢ filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)

Tactic:
induction' l with a l ih

Result:
case nil
α : Type u
β : Type v
f : α → Option β
g : α → β
⊢ filterMap f [] = map g [] → ∀ (x : α), x ∈ [] → f x = some (g x)

case cons
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)

Proof state:
case cons.none
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = none
h : filterMap f l = g a :: map g l
⊢ False

Tactic:
simpa [show (filterMap f l).length = l.length + 1 from by simp[h], Nat.add_one_le_iff]
  using List.length_filterMap_le f l

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
f : α → Option β
g : α → β
⊢ filterMap f [] = map g [] → ∀ (x : α), x ∈ [] → f x = some (g x)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = none
h : filterMap f l = g a :: map g l
⊢ (filterMap f l).length = l.length + 1

Tactic:
simp[h]

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)

Tactic:
rcases ha : f a with - | b <;> simp [ha, filterMap_cons]

Result:
case cons.none
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = none
⊢ ¬filterMap f l = g a :: map g l

case cons.some
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
b : β
ha : f a = some b
⊢ b = g a → filterMap f l = map g l → b = g a ∧ ∀ (a : α), a ∈ l → f a = some (g a)

Proof state:
case cons.none
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = none
⊢ ¬filterMap f l = g a :: map g l

Tactic:
intro h

Result:
case cons.none
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = none
h : filterMap f l = g a :: map g l
⊢ False

Proof state:
case cons.some
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = some (g a)
h : filterMap f l = map g l
⊢ g a = g a ∧ ∀ (a : α), a ∈ l → f a = some (g a)

Tactic:
exact ⟨rfl, ih h⟩

Result:
no goals

Proof state:
case cons.some
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
b : β
ha : f a = some b
⊢ b = g a → filterMap f l = map g l → b = g a ∧ ∀ (a : α), a ∈ l → f a = some (g a)

Tactic:
rintro rfl h

Result:
case cons.some
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = some (g a)
h : filterMap f l = map g l
⊢ g a = g a ∧ ∀ (a : α), a ∈ l → f a = some (g a)

Proof state:
α : Type u
β : Type v
f : α → Option β
g : α → β
l : List α
h : ∀ (x : α), x ∈ l → f x = some (g x)
⊢ ∀ (x : α), x ∈ l → f x = (some ∘ g) x

Tactic:
simpa

Result:
no goals