/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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 L
mem_sections {L: List (List α)
L : List: Type ?u.14 → Type ?u.14
List (List: Type ?u.15 → Type ?u.15
List α: Type ?u.8
α)} {f: List α
f} : f: ?m.18
f ∈ sections: {α : Type ?u.26} → List (List α) → List (List α)
sections L: List (List α)
L ↔ Forall₂: {α : Type ?u.42} → {β : Type ?u.41} → (α → β → Prop) → List α → List β → Prop
Forall₂ (· ∈ ·): α → List α → Prop
(· ∈ ·) f: ?m.18
f L: List (List α)
L := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

f ∈ sections L ↔ Forall₂ (fun x x_1 => x ∈ x_1) f Lrefine' ⟨fun h: ?m.103
h => _: ?m.99
_, fun h: ?m.110
h => _: ?m.98
_⟩α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

h: f ∈ sections L

refine'_1Forall₂ (fun x x_1 => x ∈ x_1) f L
α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

h: Forall₂ (fun x x_1 => x ∈ x_1) f L

refine'_2f ∈ 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·α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

h: f ∈ sections L

refine'_1Forall₂ (fun x x_1 => x ∈ x_1) f L α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

h: f ∈ sections L

refine'_1Forall₂ (fun x x_1 => x ∈ x_1) f L
α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

h: Forall₂ (fun x x_1 => x ∈ x_1) f L

refine'_2f ∈ sections Linduction L: List (List α)
L generalizing f: List α
fα: Type u_1

β: Type ?u.11

f: List α

h: f ∈ sections []

refine'_1.nilForall₂ (fun x x_1 => x ∈ x_1) f []
α: 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✝)

refine'_1.consForall₂ (fun x x_1 => x ∈ x_1) f (head✝ :: tail✝)
    α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

h: f ∈ sections L

refine'_1Forall₂ (fun x x_1 => x ∈ x_1) f L·α: Type u_1

β: Type ?u.11

f: List α

h: f ∈ sections []

refine'_1.nilForall₂ (fun x x_1 => x ∈ x_1) f [] α: Type u_1

β: Type ?u.11

f: List α

h: f ∈ sections []

refine'_1.nilForall₂ (fun x x_1 => x ∈ x_1) f []
α: 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✝)

refine'_1.consForall₂ (fun x x_1 => x ∈ x_1) f (head✝ :: tail✝)cases mem_singleton: ∀ {α : Type ?u.159} {a b : α}, a ∈ [b] ↔ a = b
mem_singleton.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 h: f ∈ sections []
hα: Type u_1

β: Type ?u.11

h: [] ∈ sections []

refine'_1.nil.reflForall₂ (fun x x_1 => x ∈ x_1) [] []
      α: Type u_1

β: Type ?u.11

f: 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₂.nil
Goals accomplished! 🐙
    α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

h: f ∈ sections L

refine'_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 f
bind_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 a
mem_bind, mem_map: ∀ {α : Type ?u.631} {β : Type ?u.632} {b : β} {f : α → β} {l : List α}, b ∈ map f l ↔ ∃ a, a ∈ l ∧ f a = b
mem_map] at h: f ∈ sections (head✝ :: tail✝)
hα: 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

refine'_1.consForall₂ (fun x x_1 => x ∈ x_1) f (head✝ :: tail✝)
    α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

h: f ∈ sections L

refine'_1Forall₂ (fun x x_1 => x ∈ x_1) f Lrcases h: ∃ a, a ∈ sections tail✝ ∧ ∃ a_1, a_1 ∈ head✝ ∧ a_1 :: a = f
h with ⟨_, _, _, _, rfl⟩: w✝ ∈ head✝ ∧ w✝ :: w✝¹ = f
⟨_: List α
_⟨_, _, _, _, rfl⟩: w✝ ∈ head✝ ∧ w✝ :: w✝¹ = f
, _: w✝ ∈ sections tail✝
_⟨_, _, _, _, rfl⟩: w✝ ∈ head✝ ∧ w✝ :: w✝¹ = f
, _: α
_⟨_, _, _, _, rfl⟩: w✝ ∈ head✝ ∧ w✝ :: w✝¹ = f
, _: w✝ ∈ head✝
_⟨_, _, _, _, rfl⟩: w✝ ∈ head✝ ∧ w✝ :: w✝¹ = f
, rfl: w✝ :: w✝¹ = f
rfl⟨_, _, _, _, rfl⟩: w✝ ∈ head✝ ∧ w✝ :: w✝¹ = f
⟩α: 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✝

refine'_1.cons.intro.intro.intro.introForall₂ (fun x x_1 => x ∈ x_1) (w✝ :: w✝¹) (head✝ :: tail✝)
    α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

h: f ∈ sections L

refine'_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 ↔ p
true_and_iff]
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

f ∈ sections L ↔ Forall₂ (fun x x_1 => x ∈ x_1) f L·α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

h: Forall₂ (fun x x_1 => x ∈ x_1) f L

refine'_2f ∈ sections L α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

h: Forall₂ (fun x x_1 => x ∈ x_1) f L

refine'_2f ∈ sections Linduction' h: ?m.110
h with a: ?m.1304
a l: ?m.1305
l f: List ?m.1304
f L: List ?m.1305
L al: ?m.1306 a l
al fL: Forall₂ ?m.1306 f L
fL fs: ?m.1307 f L fL
fsα: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

refine'_2.nil[] ∈ sections []
α: 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

refine'_2.consa :: f ∈ sections (l :: L)
    α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

h: Forall₂ (fun x x_1 => x ∈ x_1) f L

refine'_2f ∈ sections L·α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

refine'_2.nil[] ∈ sections [] α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

refine'_2.nil[] ∈ sections []
α: 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

refine'_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 = b
mem_singleton]
Goals accomplished! 🐙
    α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

h: Forall₂ (fun x x_1 => x ∈ x_1) f L

refine'_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 f
bind_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 a
mem_bind, mem_map: ∀ {α : Type ?u.1511} {β : Type ?u.1512} {b : β} {f : α → β} {l : List α}, b ∈ map f l ↔ ∃ a, a ∈ l ∧ f a = b
mem_map]α: 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

refine'_2.cons∃ a_1, a_1 ∈ sections L ∧ ∃ a_2, a_2 ∈ l ∧ a_2 :: a_1 = a :: f
    α: Type u_1

β: Type ?u.11

L: List (List α)

f: List α

h: Forall₂ (fun x x_1 => x ∈ x_1) f L

refine'_2f ∈ sections Lexact ⟨f: List ?m.1304
f, fs: ?m.1307 f L fL
fs, a: ?m.1304
a, al: ?m.1306 a l
al, rfl: ∀ {α : Sort ?u.1783} {a : α}, a = a
rfl⟩
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 L
List.mem_sections

theorem mem_sections_length: ∀ {L : List (List α)} {f : List α}, f ∈ sections L → length f = length L
mem_sections_length {L: List (List α)
L : List: Type ?u.1884 → Type ?u.1884
List (List: Type ?u.1885 → Type ?u.1885
List α: Type ?u.1878
α)} {f: ?m.1888
f} (h: f ∈ sections L
h : f: ?m.1888
f ∈ sections: {α : Type ?u.1906} → List (List α) → List (List α)
sections L: List (List α)
L) : length: {α : Type ?u.1924} → List α → ℕ
length f: ?m.1888
f = 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 L
mem_sections.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 h: f ∈ sections L
h).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 L
List.mem_sections_length

theorem rel_sections: ∀ {r : α → β → Prop}, (Forall₂ (Forall₂ r) ⇒ Forall₂ (Forall₂ r)) sections sections
rel_sections {r: α → β → Prop
r : α: Type ?u.1987
α → β: Type ?u.1990
β → Prop: Type
Prop} :
    (Forall₂: {α : Type ?u.2008} → {β : Type ?u.2007} → (α → β → Prop) → List α → List β → Prop
Forall₂ (Forall₂: {α : Type ?u.2016} → {β : Type ?u.2015} → (α → β → Prop) → List α → List β → Prop
Forall₂ r: α → β → Prop
r) ⇒ Forall₂: {α : Type ?u.2044} → {β : Type ?u.2043} → (α → β → Prop) → List α → List β → Prop
Forall₂ (Forall₂: {α : Type ?u.2052} → {β : Type ?u.2051} → (α → β → Prop) → List α → List β → Prop
Forall₂ r: α → β → Prop
r)) 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.bind
rel_bind (rel_sections: ∀ {r : α → β → Prop}, (Forall₂ (Forall₂ r) ⇒ Forall₂ (Forall₂ r)) sections sections
rel_sections h₁: Forall₂ (Forall₂ r) l₁✝ l₂✝
h₁) fun _: ?m.2342
_ _: ?m.2345
_ hl: ?m.2348
hl => 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 map
rel_map (fun _: ?m.2363
_ _: ?m.2366
_ ha: ?m.2369
ha => 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.2369
ha hl: ?m.2348
hl) 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 sections
List.rel_sections

end List