-- 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
β : 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 β
⊢ (l₁ <+
      match f a with
      | none => filterMap f l₂
      | some b => b :: filterMap f l₂) ↔
    ∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l'

Tactic:
split

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₁ <+ filterMap f l₂ ↔ ∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l'

case cons.h_2
β : 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'

Proof state:
case cons.h_2
β : 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:
constructor

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✝
⊢ l₁ <+ b✝ :: filterMap f l₂ → ∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l'

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₂

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', l' <+ l₂ ∧ filterMap f (a :: l₁✝) = filterMap f l'

Tactic:
rename_i l'

Result:
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

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₂)
⊢ filterMap f l' <+ b✝ :: filterMap f l₂

Tactic:
rwa [filterMap_cons_some] at h

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 : filterMap f l' <+ filterMap f (a :: l₂)
⊢ f a = some b✝

Proof state:
case cons.h_1.mp.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' <+ l₂
⊢ ∃ l'_1, l'_1 <+ a :: l₂ ∧ filterMap f l' = filterMap f l'_1

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

Result:
no goals

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', l' <+ l₂ ∧ l₁ = filterMap f l') ↔ ∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l'

Tactic:
constructor

Result:
case cons.h_1.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 β
heq✝ : f a = none
⊢ (∃ l', l' <+ l₂ ∧ l₁ = filterMap f l') → ∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l'

case cons.h_1.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 β
heq✝ : f a = none
⊢ (∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l') → ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'

Proof state:
case cons.h_1.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 β
heq✝ : f a = none
⊢ (∃ l', l' <+ l₂ ∧ l₁ = filterMap f l') → ∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l'

Tactic:
rintro ⟨l', h, rfl⟩

Result:
case cons.h_1.mp.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' <+ l₂
⊢ ∃ l'_1, l'_1 <+ a :: l₂ ∧ filterMap f l' = filterMap f l'_1

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'
l₁ : List β
x✝ : Option β
b✝ : β
heq✝ : f a = some b✝
h : l₁ <+ filterMap f l₂
⊢ ∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l'

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₂ ∧ filterMap f l' = filterMap f l'_1

Proof state:
case 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'
l₁ : List β
⊢ l₁ <+ filterMap f (a :: l₂) ↔ ∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l'

Tactic:
simp only [filterMap_cons]

Result:
case 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'
l₁ : List β
⊢ (l₁ <+
      match f a with
      | none => filterMap f l₂
      | some b => b :: filterMap f l₂) ↔
    ∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l'

Proof state:
case cons.h_1.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 β
heq✝ : f a = none
⊢ (∃ l', l' <+ a :: l₂ ∧ l₁ = filterMap f l') → ∃ l', l' <+ l₂ ∧ l₁ = filterMap f l'

Tactic:
rintro ⟨l', h, rfl⟩

Result:
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

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 : l' <+ a :: l₂
⊢ filterMap f l' <+ b✝ :: filterMap f l₂

Tactic:
replace h := h.filterMap f

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 : filterMap f l' <+ filterMap f (a :: l₂)
⊢ filterMap f l' <+ b✝ :: filterMap f l₂