Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.list.sections
! leanprover-community/mathlib commit 26f081a2fb920140ed5bc5cc5344e84bcc7cb2b2
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.List.Forall2
/-!
# List sections

This file proves some stuff about `List.sections` (definition in `Data.List.Defs`). A section of a
list of lists `[l₁, ..., lₙ]` is a list whose `i`-th element comes from the `i`-th list.
-/

open Nat Function

namespace List

variable {α: Type ?u.8α β: Type ?u.11β : Type _: Type (?u.5+1)Type _}

theorem mem_sections: ∀ {L : List (List α)} {f : List α}, f ∈ sections L ↔ Forall₂ (fun x x_1 => x ∈ x_1) f Lmem_sections {L: List (List α)L : List: Type ?u.14 → Type ?u.14List (List: Type ?u.15 → Type ?u.15List α: Type ?u.8α)} {f: List αf} : f: ?m.18f ∈ sections: {α : Type ?u.26} → List (List α) → List (List α)sections L: List (List α)L ↔ Forall₂: {α : Type ?u.42} → {β : Type ?u.41} → (α → β → Prop) → List α → List β → PropForall₂ (· ∈ ·): α → List α → Prop(· ∈ ·) f: ?m.18f L: List (List α)L := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.11L: List (List α)f: List αf ∈ sections L ↔ Forall₂ (fun x x_1 => x ∈ x_1) f Lrefine' ⟨fun h: ?m.103h => _: ?m.99_, fun h: ?m.110h => _: ?m.98_⟩α: Type u_1β: Type ?u.11L: List (List α)f: List αh: f ∈ sections Lrefine'_1Forall₂ (fun x x_1 => x ∈ x_1) f Lα: Type u_1β: Type ?u.11L: List (List α)f: List αh: Forall₂ (fun x x_1 => x ∈ x_1) f Lrefine'_2f ∈ sections L
α: Type u_1β: Type ?u.11L: List (List α)f: List αf ∈ sections L ↔ Forall₂ (fun x x_1 => x ∈ x_1) f L·α: Type u_1β: Type ?u.11L: List (List α)f: List αh: f ∈ sections Lrefine'_1Forall₂ (fun x x_1 => x ∈ x_1) f L α: Type u_1β: Type ?u.11L: List (List α)f: List αh: f ∈ sections Lrefine'_1Forall₂ (fun x x_1 => x ∈ x_1) f Lα: Type u_1β: Type ?u.11L: List (List α)f: List αh: Forall₂ (fun x x_1 => x ∈ x_1) f Lrefine'_2f ∈ sections Linduction L: List (List α)L generalizing f: List αfα: Type u_1β: Type ?u.11f: List αh: f ∈ sections []refine'_1.nilForall₂ (fun x x_1 => x ∈ x_1) f []α: Type u_1β: Type ?u.11head✝: 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✝)refine'_1.consForall₂ (fun x x_1 => x ∈ x_1) f (head✝ :: tail✝)
α: Type u_1β: Type ?u.11L: List (List α)f: List αh: f ∈ sections Lrefine'_1Forall₂ (fun x x_1 => x ∈ x_1) f L·α: Type u_1β: Type ?u.11f: List αh: f ∈ sections []refine'_1.nilForall₂ (fun x x_1 => x ∈ x_1) f [] α: Type u_1β: Type ?u.11f: List αh: f ∈ sections []refine'_1.nilForall₂ (fun x x_1 => x ∈ x_1) f []α: Type u_1β: Type ?u.11head✝: 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✝)refine'_1.consForall₂ (fun x x_1 => x ∈ x_1) f (head✝ :: tail✝)cases mem_singleton: ∀ {α : Type ?u.159} {a b : α}, a ∈ [b] ↔ a = bmem_singleton.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 h: f ∈ sections []hα: Type u_1β: Type ?u.11h: [] ∈ sections []refine'_1.nil.reflForall₂ (fun x x_1 => x ∈ x_1) [] []
α: Type u_1β: Type ?u.11f: List αh: f ∈ sections []refine'_1.nilForall₂ (fun x x_1 => x ∈ x_1) f []exact Forall₂.nil: ∀ {α : Type ?u.274} {β : Type ?u.273} {R : α → β → Prop}, Forall₂ R [] []Forall₂.nilGoals accomplished! 🐙
α: Type u_1β: Type ?u.11L: List (List α)f: List αh: f ∈ sections Lrefine'_1Forall₂ (fun x x_1 => x ∈ x_1) f Lsimp only [sections: {α : Type ?u.299} → List (List α) → List (List α)sections, bind_eq_bind: ∀ {α β : Type ?u.580} (f : α → List β) (l : List α), l >>= f = List.bind l fbind_eq_bind, mem_bind: ∀ {α : Type ?u.598} {β : Type ?u.599} {f : α → List β} {b : β} {l : List α}, b ∈ List.bind l f ↔ ∃ a, a ∈ l ∧ b ∈ f amem_bind, mem_map: ∀ {α : Type ?u.631} {β : Type ?u.632} {b : β} {f : α → β} {l : List α}, b ∈ map f l ↔ ∃ a, a ∈ l ∧ f a = bmem_map] at h: f ∈ sections (head✝ :: tail✝)hα: Type u_1β: Type ?u.11head✝: 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 = frefine'_1.consForall₂ (fun x x_1 => x ∈ x_1) f (head✝ :: tail✝)
α: Type u_1β: Type ?u.11L: List (List α)f: List αh: f ∈ sections Lrefine'_1Forall₂ (fun x x_1 => x ∈ x_1) f Lsimp only [*, forall₂_cons: ∀ {α : Type ?u.1109} {β : Type ?u.1110} {R : α → β → Prop} {a : α} {b : β} {l₁ : List α} {l₂ : List β},
Forall₂ R (a :: l₁) (b :: l₂) ↔ R a b ∧ Forall₂ R l₁ l₂forall₂_cons, true_and_iff: ∀ (p : Prop), True ∧ p ↔ ptrue_and_iff]Goals accomplished! 🐙
α: Type u_1β: Type ?u.11L: List (List α)f: List αf ∈ sections L ↔ Forall₂ (fun x x_1 => x ∈ x_1) f L·α: Type u_1β: Type ?u.11L: List (List α)f: List αh: Forall₂ (fun x x_1 => x ∈ x_1) f Lrefine'_2f ∈ sections L α: Type u_1β: Type ?u.11L: List (List α)f: List αh: Forall₂ (fun x x_1 => x ∈ x_1) f Lrefine'_2f ∈ sections Linduction' h: ?m.110h with a: ?m.1304a l: ?m.1305l f: List ?m.1304f L: List ?m.1305L al: ?m.1306 a lal fL: Forall₂ ?m.1306 f LfL fs: ?m.1307 f L fLfsα: Type u_1β: Type ?u.11L: List (List α)f: List αrefine'_2.nil[] ∈ sections []α: Type u_1β: Type ?u.11L✝: List (List α)f✝: List αa: αl, f: List αL: List (List α)al: a ∈ lfL: Forall₂ (fun x x_1 => x ∈ x_1) f Lfs: f ∈ sections Lrefine'_2.consa :: f ∈ sections (l :: L)
α: Type u_1β: Type ?u.11L: List (List α)f: List αh: Forall₂ (fun x x_1 => x ∈ x_1) f Lrefine'_2f ∈ sections L·α: Type u_1β: Type ?u.11L: List (List α)f: List αrefine'_2.nil[] ∈ sections [] α: Type u_1β: Type ?u.11L: List (List α)f: List αrefine'_2.nil[] ∈ sections []α: Type u_1β: Type ?u.11L✝: List (List α)f✝: List αa: αl, f: List αL: List (List α)al: a ∈ lfL: Forall₂ (fun x x_1 => x ∈ x_1) f Lfs: f ∈ sections Lrefine'_2.consa :: f ∈ sections (l :: L)simp only [sections: {α : Type ?u.1347} → List (List α) → List (List α)sections, mem_singleton: ∀ {α : Type ?u.1358} {a b : α}, a ∈ [b] ↔ a = bmem_singleton]Goals accomplished! 🐙
α: Type u_1β: Type ?u.11L: List (List α)f: List αh: Forall₂ (fun x x_1 => x ∈ x_1) f Lrefine'_2f ∈ sections Lsimp only [sections: {α : Type ?u.1450} → List (List α) → List (List α)sections, bind_eq_bind: ∀ {α β : Type ?u.1462} (f : α → List β) (l : List α), l >>= f = List.bind l fbind_eq_bind, mem_bind: ∀ {α : Type ?u.1480} {β : Type ?u.1481} {f : α → List β} {b : β} {l : List α}, b ∈ List.bind l f ↔ ∃ a, a ∈ l ∧ b ∈ f amem_bind, mem_map: ∀ {α : Type ?u.1511} {β : Type ?u.1512} {b : β} {f : α → β} {l : List α}, b ∈ map f l ↔ ∃ a, a ∈ l ∧ f a = bmem_map]α: Type u_1β: Type ?u.11L✝: List (List α)f✝: List αa: αl, f: List αL: List (List α)al: a ∈ lfL: Forall₂ (fun x x_1 => x ∈ x_1) f Lfs: f ∈ sections Lrefine'_2.cons∃ a_1, a_1 ∈ sections L ∧ ∃ a_2, a_2 ∈ l ∧ a_2 :: a_1 = a :: f
α: Type u_1β: Type ?u.11L: List (List α)f: List αh: Forall₂ (fun x x_1 => x ∈ x_1) f Lrefine'_2f ∈ sections Lexact ⟨f: List ?m.1304f, fs: ?m.1307 f L fLfs, a: ?m.1304a, al: ?m.1306 a lal, rfl: ∀ {α : Sort ?u.1783} {a : α}, a = arfl⟩Goals accomplished! 🐙
#align list.mem_sections List.mem_sections: ∀ {α : Type u_1} {L : List (List α)} {f : List α}, f ∈ sections L ↔ Forall₂ (fun x x_1 => x ∈ x_1) f LList.mem_sections

theorem mem_sections_length: ∀ {L : List (List α)} {f : List α}, f ∈ sections L → length f = length Lmem_sections_length {L: List (List α)L : List: Type ?u.1884 → Type ?u.1884List (List: Type ?u.1885 → Type ?u.1885List α: Type ?u.1878α)} {f: ?m.1888f} (h: f ∈ sections Lh : f: ?m.1888f ∈ sections: {α : Type ?u.1906} → List (List α) → List (List α)sections L: List (List α)L) : length: {α : Type ?u.1924} → List α → ℕlength f: ?m.1888f = length: {α : Type ?u.1927} → List α → ℕlength L: List (List α)L :=
(mem_sections: ∀ {α : Type ?u.1935} {L : List (List α)} {f : List α}, f ∈ sections L ↔ Forall₂ (fun x x_1 => x ∈ x_1) f Lmem_sections.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 h: f ∈ sections Lh).length_eq: ∀ {α : Type ?u.1953} {β : Type ?u.1954} {R : α → β → Prop} {l₁ : List α} {l₂ : List β},
Forall₂ R l₁ l₂ → length l₁ = length l₂length_eq
#align list.mem_sections_length List.mem_sections_length: ∀ {α : Type u_1} {L : List (List α)} {f : List α}, f ∈ sections L → length f = length LList.mem_sections_length

theorem rel_sections: ∀ {r : α → β → Prop}, (Forall₂ (Forall₂ r) ⇒ Forall₂ (Forall₂ r)) sections sectionsrel_sections {r: α → β → Propr : α: Type ?u.1987α → β: Type ?u.1990β → Prop: TypeProp} :
(Forall₂: {α : Type ?u.2008} → {β : Type ?u.2007} → (α → β → Prop) → List α → List β → PropForall₂ (Forall₂: {α : Type ?u.2016} → {β : Type ?u.2015} → (α → β → Prop) → List α → List β → PropForall₂ r: α → β → Propr) ⇒ Forall₂: {α : Type ?u.2044} → {β : Type ?u.2043} → (α → β → Prop) → List α → List β → PropForall₂ (Forall₂: {α : Type ?u.2052} → {β : Type ?u.2051} → (α → β → Prop) → List α → List β → PropForall₂ r: α → β → Propr)) sections: {α : Type ?u.2079} → List (List α) → List (List α)sections sections: {α : Type ?u.2084} → List (List α) → List (List α)sections
| _, _, Forall₂.nil: ∀ {α : Type ?u.2104} {β : Type ?u.2103} {R : α → β → Prop}, Forall₂ R [] []Forall₂.nil => Forall₂.cons: ∀ {α : Type ?u.2145} {β : Type ?u.2144} {R : α → β → Prop} {a : α} {b : β} {l₁ : List α} {l₂ : List β},
R a b → Forall₂ R l₁ l₂ → Forall₂ R (a :: l₁) (b :: l₂)Forall₂.cons Forall₂.nil: ∀ {α : Type ?u.2176} {β : Type ?u.2175} {R : α → β → Prop}, Forall₂ R [] []Forall₂.nil Forall₂.nil: ∀ {α : Type ?u.2185} {β : Type ?u.2184} {R : α → β → Prop}, Forall₂ R [] []Forall₂.nil
| _, _, Forall₂.cons: ∀ {α : Type ?u.2200} {β : Type ?u.2199} {R : α → β → Prop} {a : α} {b : β} {l₁ : List α} {l₂ : List β},
R a b → Forall₂ R l₁ l₂ → Forall₂ R (a :: l₁) (b :: l₂)Forall₂.cons h₀: Forall₂ r a✝ b✝h₀ h₁: Forall₂ (Forall₂ r) l₁✝ l₂✝h₁ =>
rel_bind: ∀ {α : Type ?u.2290} {β : Type ?u.2291} {γ : Type ?u.2292} {δ : Type ?u.2293} {R : α → β → Prop} {P : γ → δ → Prop},
(Forall₂ R ⇒ (R ⇒ Forall₂ P) ⇒ Forall₂ P) List.bind List.bindrel_bind (rel_sections: ∀ {r : α → β → Prop}, (Forall₂ (Forall₂ r) ⇒ Forall₂ (Forall₂ r)) sections sectionsrel_sections h₁: Forall₂ (Forall₂ r) l₁✝ l₂✝h₁) fun _: ?m.2342_ _: ?m.2345_ hl: ?m.2348hl => rel_map: ∀ {α : Type ?u.2350} {β : Type ?u.2352} {γ : Type ?u.2351} {δ : Type ?u.2353} {R : α → β → Prop} {P : γ → δ → Prop},
((R ⇒ P) ⇒ Forall₂ R ⇒ Forall₂ P) map maprel_map (fun _: ?m.2363_ _: ?m.2366_ ha: ?m.2369ha => Forall₂.cons: ∀ {α : Type ?u.2372} {β : Type ?u.2371} {R : α → β → Prop} {a : α} {b : β} {l₁ : List α} {l₂ : List β},
R a b → Forall₂ R l₁ l₂ → Forall₂ R (a :: l₁) (b :: l₂)Forall₂.cons ha: ?m.2369ha hl: ?m.2348hl) h₀: Forall₂ r a✝ b✝h₀
#align list.rel_sections List.rel_sections: ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop}, (Forall₂ (Forall₂ r) ⇒ Forall₂ (Forall₂ r)) sections sectionsList.rel_sections

end List
```