case refine'_1
α : Type u_1
β : Type ?u.11
L : List (List α)
f : List α
h : f ∈ sections L
⊢ Forall₂ (fun x x_1 => x ∈ x_1) f L

case refine'_2
α : Type u_1
β : Type ?u.11
L : List (List α)
f : List α
h : Forall₂ (fun x x_1 => x ∈ x_1) f L
⊢ f ∈ sections L
α : Type u_1
β : Type ?u.11
L : List (List α)
f : List α
⊢ f ∈ sections L ↔ Forall₂ (fun x x_1 => x ∈ x_1) f L
refine' ⟨fun h => _, fun h => _⟩
case refine'_1.nil
α : Type u_1
β : Type ?u.11
f : List α
h : f ∈ sections []
⊢ Forall₂ (fun x x_1 => x ∈ x_1) f []

case refine'_1.cons
α : Type u_1
β : Type ?u.11
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✝)
case refine'_1
α : Type u_1
β : Type ?u.11
L : List (List α)
f : List α
h : f ∈ sections L
⊢ Forall₂ (fun x x_1 => x ∈ x_1) f L
induction L generalizing f
case refine'_1.cons
α : Type u_1
β : Type ?u.11
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✝)
case refine'_1.cons
α : Type u_1
β : Type ?u.11
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✝)
simp only [sections, bind_eq_bind, mem_bind, mem_map] at h
case refine'_1.cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.11
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✝)
case refine'_1.cons
α : Type u_1
β : Type ?u.11
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✝)
rcases h with ⟨_, _, _, _, rfl⟩
no goals
case refine'_1.cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.11
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✝)
simp only [*, forall₂_cons, true_and_iff]
case refine'_1.nil.refl
α : Type u_1
β : Type ?u.11
h : [] ∈ sections []
⊢ Forall₂ (fun x x_1 => x ∈ x_1) [] []
case refine'_1.nil
α : Type u_1
β : Type ?u.11
f : List α
h : f ∈ sections []
⊢ Forall₂ (fun x x_1 => x ∈ x_1) f []
cases mem_singleton.1 h
no goals
case refine'_1.nil.refl
α : Type u_1
β : Type ?u.11
h : [] ∈ sections []
⊢ Forall₂ (fun x x_1 => x ∈ x_1) [] []
exact Forall₂.nil
case refine'_2.nil
α : Type u_1
β : Type ?u.11
L : List (List α)
f : List α
⊢ [] ∈ sections []

case refine'_2.cons
α : Type u_1
β : Type ?u.11
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)
case refine'_2
α : Type u_1
β : Type ?u.11
L : List (List α)
f : List α
h : Forall₂ (fun x x_1 => x ∈ x_1) f L
⊢ f ∈ sections L
induction' h with a l f L al fL fs
case refine'_2.cons
α : Type u_1
β : Type ?u.11
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
case refine'_2.cons
α : Type u_1
β : Type ?u.11
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)
simp only [sections, bind_eq_bind, mem_bind, mem_map]
no goals
case refine'_2.cons
α : Type u_1
β : Type ?u.11
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
exact ⟨f, fs, a, al, rfl⟩
no goals
case refine'_2.nil
α : Type u_1
β : Type ?u.11
L : List (List α)
f : List α
⊢ [] ∈ sections []
simp only [sections, mem_singleton]