[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
f : List α
⊢ f ∈ sections L ↔ Forall₂ (fun x x_1 => x ∈ x_1) f L
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
L : List (List α)
f : List α
h : f ∈ sections L
⊢ Forall₂ (fun x x_1 => x ∈ x_1) f L
[PROOFSTEP]
induction L generalizing f
[GOAL]
case refine'_1.nil
α : Type u_1
β : Type u_2
f : List α
h : f ∈ sections []
⊢ Forall₂ (fun x x_1 => x ∈ x_1) f []
[PROOFSTEP]
cases mem_singleton.1 h
[GOAL]
case refine'_1.nil.refl
α : Type u_1
β : Type u_2
h : [] ∈ sections []
⊢ Forall₂ (fun x x_1 => x ∈ x_1) [] []
[PROOFSTEP]
exact Forall₂.nil
[GOAL]
case refine'_1.cons
α : Type u_1
β : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ sections tail✝ → Forall₂ (fun x x_1 => x ∈ x_1) f tail✝
f : List α
h : f ∈ sections (head✝ :: tail✝)
⊢ Forall₂ (fun x x_1 => x ∈ x_1) f (head✝ :: tail✝)
[PROOFSTEP]
simp only [sections, bind_eq_bind, mem_bind, mem_map] at h 
[GOAL]
case refine'_1.cons
α : Type u_1
β : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ sections tail✝ → Forall₂ (fun x x_1 => x ∈ x_1) f tail✝
f : List α
h : ∃ a, a ∈ sections tail✝ ∧ ∃ a_1, a_1 ∈ head✝ ∧ a_1 :: a = f
⊢ Forall₂ (fun x x_1 => x ∈ x_1) f (head✝ :: tail✝)
[PROOFSTEP]
rcases h with ⟨_, _, _, _, rfl⟩
[GOAL]
case refine'_1.cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ sections tail✝ → Forall₂ (fun x x_1 => x ∈ x_1) f tail✝
w✝¹ : List α
left✝¹ : w✝¹ ∈ sections tail✝
w✝ : α
left✝ : w✝ ∈ head✝
⊢ Forall₂ (fun x x_1 => x ∈ x_1) (w✝ :: w✝¹) (head✝ :: tail✝)
[PROOFSTEP]
simp only [*, forall₂_cons, true_and_iff]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
L : List (List α)
f : List α
h : Forall₂ (fun x x_1 => x ∈ x_1) f L
⊢ f ∈ sections L
[PROOFSTEP]
induction' h with a l f L al fL fs
[GOAL]
case refine'_2.nil
α : Type u_1
β : Type u_2
L : List (List α)
f : List α
⊢ [] ∈ sections []
[PROOFSTEP]
simp only [sections, mem_singleton]
[GOAL]
case refine'_2.cons
α : Type u_1
β : Type u_2
L✝ : List (List α)
f✝ : List α
a : α
l f : List α
L : List (List α)
al : a ∈ l
fL : Forall₂ (fun x x_1 => x ∈ x_1) f L
fs : f ∈ sections L
⊢ a :: f ∈ sections (l :: L)
[PROOFSTEP]
simp only [sections, bind_eq_bind, mem_bind, mem_map]
[GOAL]
case refine'_2.cons
α : Type u_1
β : Type u_2
L✝ : List (List α)
f✝ : List α
a : α
l f : List α
L : List (List α)
al : a ∈ l
fL : Forall₂ (fun x x_1 => x ∈ x_1) f L
fs : f ∈ sections L
⊢ ∃ a_1, a_1 ∈ sections L ∧ ∃ a_2, a_2 ∈ l ∧ a_2 :: a_1 = a :: f
[PROOFSTEP]
exact ⟨f, fs, a, al, rfl⟩
