-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem sublist_filterMap_iff {l₁ : List β} {f : α → Option β} :
    l₁ <+ l₂.filterMap f ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.filterMap f

Proof state:
case cons.h_2.mpr.intro.intro
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
l' : List α
h : filterMap f l' <+ filterMap f (a :: l₂)
⊢ f a = some b✝

Tactic:
assumption

Result:
no goals

Proof state:
case cons.h_2.mp
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
l₁ : List β
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
⊢ l₁ <+ b✝ :: filterMap f l₂ → ∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l'

Tactic:
intro w

Result:
case cons.h_2.mp
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
l₁ : List β
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
w : l₁ <+ b✝ :: filterMap f l₂
⊢ ∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l'

Proof state:
case cons.h_2.mp
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
l₁ : List β
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
w : l₁ <+ b✝ :: filterMap f l₂
⊢ ∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l'

Tactic:
cases w with
| cons _ h =>
  obtain ⟨l', s, rfl⟩ := ih.1 h
  exact ⟨l', Sublist.cons a s, rfl⟩
| cons₂ _ h =>
  rename_i l'
  obtain ⟨l', s, rfl⟩ := ih.1 h
  refine ⟨a :: l', Sublist.cons₂ a s, ?_⟩
  rwa [filterMap_cons_some]

Result:
no goals

Proof state:
case cons.h_2.mpr
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
l₁ : List β
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
⊢ (∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l') → l₁ <+ b✝ :: filterMap f l₂

Tactic:
rintro ⟨l', h, rfl⟩

Result:
case cons.h_2.mpr.intro.intro
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
l' : List α
h : l' <+ a :: l₂
⊢ filterMap f l' <+ b✝ :: filterMap f l₂

Proof state:
case cons.h_1
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
l₁ : List β
x✝ : Option β
heq✝ : f a = none
⊢ l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l'

Tactic:
simp only [ih]

Result:
case cons.h_1
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
l₁ : List β
x✝ : Option β
heq✝ : f a = none
⊢ (∃ l', l' <+ l₂ ∧ l₁ = filterMap f l') ↔ ∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l'

Proof state:
case nil
β : Type u_1
α : Type u_2
f : α → Option β
l₁ : List β
⊢ l₁ <+ filterMap f [] ↔ ∃ l', l' <+ [] ∧ l₁ = filterMap f l'

Tactic:
simp

Result:
no goals

Proof state:
case cons.h_2.mp.cons₂.intro.intro
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
l' : List α
s : l' <+ l₂
h : filterMap f l' <+ filterMap f l₂
⊢ ∃ l'_1, l'_1 <+ a :: l₂ ∧ b✝ :: filterMap f l' = filterMap f l'_1

Tactic:
refine ⟨a :: l', Sublist.cons₂ a s, ?_⟩

Result:
case cons.h_2.mp.cons₂.intro.intro
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
l' : List α
s : l' <+ l₂
h : filterMap f l' <+ filterMap f l₂
⊢ b✝ :: filterMap f l' = filterMap f (a :: l')

Proof state:
case cons.h_2.mp.cons.intro.intro
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
l' : List α
s : l' <+ l₂
h : filterMap f l' <+ filterMap f l₂
⊢ ∃ l'_1, l'_1 <+ a :: l₂ ∧ filterMap f l' = filterMap f l'_1

Tactic:
exact ⟨l', Sublist.cons a s, rfl⟩

Result:
no goals

Proof state:
case cons.h_2.mp.cons₂
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
l₁✝ : List β
h : l₁✝ <+ filterMap f l₂
⊢ ∃ l', l' <+ a :: l₂ ∧ b✝ :: l₁✝ = filterMap f l'

Tactic:
rename_i l'

Result:
case cons.h_2.mp.cons₂
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
l' : List β
h : l' <+ filterMap f l₂
⊢ ∃ l'_1, l'_1 <+ a :: l₂ ∧ b✝ :: l' = filterMap f l'_1

Proof state:
case cons.h_1.mpr.intro.intro
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
x✝ : Option β
heq✝ : f a = none
l' : List α
h : l' <+ a :: l₂
⊢ ∃ l'_1, l'_1 <+ l₂ ∧ filterMap f l' = filterMap f l'_1

Tactic:
cases h with
| cons _ h =>
  exact ⟨l', h, rfl⟩
| cons₂ _ h =>
  rename_i l'
  exact ⟨l', h, by simp_all⟩

Result:
no goals

Proof state:
case cons.h_2.mp.cons₂.intro.intro
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
l' : List α
s : l' <+ l₂
h : filterMap f l' <+ filterMap f l₂
⊢ b✝ :: filterMap f l' = filterMap f (a :: l')

Tactic:
rwa [filterMap_cons_some]

Result:
no goals

Proof state:
case cons.h_1.mpr.intro.intro.cons
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
x✝ : Option β
heq✝ : f a = none
l' : List α
h : l' <+ l₂
⊢ ∃ l'_1, l'_1 <+ l₂ ∧ filterMap f l' = filterMap f l'_1

Tactic:
exact ⟨l', h, rfl⟩

Result:
no goals

Proof state:
case cons.h_2.mp.cons₂
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
l' : List β
h : l' <+ filterMap f l₂
⊢ ∃ l'_1, l'_1 <+ a :: l₂ ∧ b✝ :: l' = filterMap f l'_1

Tactic:
obtain ⟨l', s, rfl⟩ := ih.1 h

Result:
case cons.h_2.mp.cons₂.intro.intro
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
l' : List α
s : l' <+ l₂
h : filterMap f l' <+ filterMap f l₂
⊢ ∃ l'_1, l'_1 <+ a :: l₂ ∧ b✝ :: filterMap f l' = filterMap f l'_1

Proof state:
case cons.h_1.mpr.intro.intro.cons₂
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
x✝ : Option β
heq✝ : f a = none
l' : List α
h : l' <+ l₂
⊢ ∃ l'_1, l'_1 <+ l₂ ∧ filterMap f (a :: l') = filterMap f l'_1

Tactic:
exact ⟨l', h, by simp_all⟩

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
f : α → Option β
a : α
l₂ : List α
ih : ∀ {l₁ : List β}, l₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'
x✝ : Option β
heq✝ : f a = none
l' : List α
h : l' <+ l₂
⊢ filterMap f (a :: l') = filterMap f l'

Tactic:
simp_all

Result:
no goals