-- Mathlib/Data/List/Sections.lean
theorem mem_sections {L : List (List α)} {f} : f ∈ sections L ↔ Forall₂ (· ∈ ·) f L

Proof state:
case refine_1.nil
α : Type u_1
f : List α
h : f ∈ [].sections
⊢ Forall₂ (fun x1 x2 => x1 ∈ x2) f []

Tactic:
cases mem_singleton.1 h

Result:
case refine_1.nil.refl
α : Type u_1
h : [] ∈ [].sections
⊢ Forall₂ (fun x1 x2 => x1 ∈ x2) [] []

Proof state:
case refine_1.cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ tail✝.sections → Forall₂ (fun x1 x2 => x1 ∈ x2) f tail✝
f : List α
h : f ∈ (head✝ :: tail✝).sections
⊢ Forall₂ (fun x1 x2 => x1 ∈ x2) f (head✝ :: tail✝)

Tactic:
simp only [sections, bind_eq_flatMap, mem_flatMap, mem_map] at h

Result:
case refine_1.cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ tail✝.sections → Forall₂ (fun x1 x2 => x1 ∈ x2) f tail✝
f : List α
h : ∃ a, a ∈ tail✝.sections ∧ ∃ a_1, a_1 ∈ head✝ ∧ a_1 :: a = f
⊢ Forall₂ (fun x1 x2 => x1 ∈ x2) f (head✝ :: tail✝)

Proof state:
case refine_1.nil.refl
α : Type u_1
h : [] ∈ [].sections
⊢ Forall₂ (fun x1 x2 => x1 ∈ x2) [] []

Tactic:
exact Forall₂.nil

Result:
no goals

Proof state:
case refine_1
α : Type u_1
L : List (List α)
f : List α
h : f ∈ L.sections
⊢ Forall₂ (fun x1 x2 => x1 ∈ x2) f L

Tactic:
induction L generalizing f

Result:
case refine_1.nil
α : Type u_1
f : List α
h : f ∈ [].sections
⊢ Forall₂ (fun x1 x2 => x1 ∈ x2) f []

case refine_1.cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ tail✝.sections → Forall₂ (fun x1 x2 => x1 ∈ x2) f tail✝
f : List α
h : f ∈ (head✝ :: tail✝).sections
⊢ Forall₂ (fun x1 x2 => x1 ∈ x2) f (head✝ :: tail✝)

Proof state:
case refine_2.cons
α : Type u_1
L✝ : List (List α)
f✝ : List α
a : α
l f : List α
L : List (List α)
al : a ∈ l
fL : Forall₂ (fun x1 x2 => x1 ∈ x2) f L
fs : f ∈ L.sections
⊢ ∃ a_1, a_1 ∈ L.sections ∧ ∃ a_2, a_2 ∈ l ∧ a_2 :: a_1 = a :: f

Tactic:
exact ⟨f, fs, a, al, rfl⟩

Result:
no goals

Proof state:
case refine_1.cons.intro.intro.intro.intro
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ tail✝.sections → Forall₂ (fun x1 x2 => x1 ∈ x2) f tail✝
w✝¹ : List α
left✝¹ : w✝¹ ∈ tail✝.sections
w✝ : α
left✝ : w✝ ∈ head✝
⊢ Forall₂ (fun x1 x2 => x1 ∈ x2) (w✝ :: w✝¹) (head✝ :: tail✝)

Tactic:
simp only [*, forall₂_cons, true_and]

Result:
no goals

Proof state:
case refine_2.nil
α : Type u_1
L : List (List α)
f : List α
⊢ [] ∈ [].sections

Tactic:
simp only [sections, mem_singleton]

Result:
no goals

Proof state:
α : Type u_1
L : List (List α)
f : List α
⊢ f ∈ L.sections ↔ Forall₂ (fun x1 x2 => x1 ∈ x2) f L

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
α : Type u_1
L : List (List α)
f : List α
h : f ∈ L.sections
⊢ Forall₂ (fun x1 x2 => x1 ∈ x2) f L

case refine_2
α : Type u_1
L : List (List α)
f : List α
h : Forall₂ (fun x1 x2 => x1 ∈ x2) f L
⊢ f ∈ L.sections

Proof state:
case refine_2
α : Type u_1
L : List (List α)
f : List α
h : Forall₂ (fun x1 x2 => x1 ∈ x2) f L
⊢ f ∈ L.sections

Tactic:
induction' h with a l f L al fL fs

Result:
case refine_2.nil
α : Type u_1
L : List (List α)
f : List α
⊢ [] ∈ [].sections

case refine_2.cons
α : Type u_1
L✝ : List (List α)
f✝ : List α
a : α
l f : List α
L : List (List α)
al : a ∈ l
fL : Forall₂ (fun x1 x2 => x1 ∈ x2) f L
fs : f ∈ L.sections
⊢ a :: f ∈ (l :: L).sections

Proof state:
case refine_1.cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ tail✝.sections → Forall₂ (fun x1 x2 => x1 ∈ x2) f tail✝
f : List α
h : ∃ a, a ∈ tail✝.sections ∧ ∃ a_1, a_1 ∈ head✝ ∧ a_1 :: a = f
⊢ Forall₂ (fun x1 x2 => x1 ∈ x2) f (head✝ :: tail✝)

Tactic:
rcases h with ⟨_, _, _, _, rfl⟩

Result:
case refine_1.cons.intro.intro.intro.intro
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ tail✝.sections → Forall₂ (fun x1 x2 => x1 ∈ x2) f tail✝
w✝¹ : List α
left✝¹ : w✝¹ ∈ tail✝.sections
w✝ : α
left✝ : w✝ ∈ head✝
⊢ Forall₂ (fun x1 x2 => x1 ∈ x2) (w✝ :: w✝¹) (head✝ :: tail✝)

Proof state:
case refine_2.cons
α : Type u_1
L✝ : List (List α)
f✝ : List α
a : α
l f : List α
L : List (List α)
al : a ∈ l
fL : Forall₂ (fun x1 x2 => x1 ∈ x2) f L
fs : f ∈ L.sections
⊢ a :: f ∈ (l :: L).sections

Tactic:
simp only [sections, bind_eq_flatMap, mem_flatMap, mem_map]

Result:
case refine_2.cons
α : Type u_1
L✝ : List (List α)
f✝ : List α
a : α
l f : List α
L : List (List α)
al : a ∈ l
fL : Forall₂ (fun x1 x2 => x1 ∈ x2) f L
fs : f ∈ L.sections
⊢ ∃ a_1, a_1 ∈ L.sections ∧ ∃ a_2, a_2 ∈ l ∧ a_2 :: a_1 = a :: f