/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel, Floris van Doorn, Mario Carneiro, Martin Dvorak

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

/-!
# Join of a list of lists

This file proves basic properties of `List.join`, which concatenates a list of lists. It is defined
in `Init.Data.List.Basic`.
-/


variable {
α: Type ?u.6447
α 
β: Type ?u.281
β : 
Type _: Type (?u.18732+1)
Type _}

namespace List

attribute [simp] 
join: {α : Type u} → List (List α) → List α
join

-- Porting note: simp can prove this
-- @[simp]
theorem 
join_singleton: ∀ {α : Type u_1} (l : List α), join [l] = l
join_singleton (
l: List α
l : 
List: Type ?u.284 → Type ?u.284
List 
α: Type ?u.278
α) : [
l: List α
l].
join: {α : Type ?u.293} → List (List α) → List α
join = 
l: List α
l := by
Goals accomplished! 🐙 
α: Type u_1

β: Type ?u.281

l: List α

join [l] = lrw [
α: Type u_1

β: Type ?u.281

l: List α

join [l] = l
join: {α : Type ?u.320} → List (List α) → List α
join,
α: Type u_1

β: Type ?u.281

l: List α

l ++ join [] = l 
α: Type u_1

β: Type ?u.281

l: List α

join [l] = l
join: {α : Type ?u.327} → List (List α) → List α
join,
α: Type u_1

β: Type ?u.281

l: List α

l ++ [] = l 
α: Type u_1

β: Type ?u.281

l: List α

join [l] = l
append_nil: ∀ {α : Type ?u.328} (as : List α), as ++ [] = as
append_nil
α: Type u_1

β: Type ?u.281

l: List α

l = l]
Goals accomplished! 🐙
#align list.join_singleton 
List.join_singleton: ∀ {α : Type u_1} (l : List α), join [l] = l
List.join_singleton

@[simp]
theorem 
join_eq_nil: ∀ {α : Type u_1} {L : List (List α)}, join L = [] ↔ ∀ (l : List α), l ∈ L → l = []
join_eq_nil : ∀ {
L: List (List α)
L : 
List: Type ?u.361 → Type ?u.361
List (
List: Type ?u.362 → Type ?u.362
List 
α: Type ?u.354
α)}, 
join: {α : Type ?u.366} → List (List α) → List α
join 
L: List (List α)
L = 
[]: List ?m.371
[] ↔ ∀ 
l: ?m.401
l ∈ 
L: List (List α)
L, 
l: ?m.401
l = 
[]: List ?m.433
[]
  | [] => 
iff_of_true: ∀ {a b : Prop}, a → b → (a ↔ b)
iff_of_true 
rfl: ∀ {α : Sort ?u.488} {a : α}, a = a
rfl (
forall_mem_nil: ∀ {α : Type ?u.503} (p : α → Prop) (x : α), x ∈ [] → p x
forall_mem_nil 
_: ?m.504 → Prop
_)
  | 
l: List α
l :: 
L: List (List α)
L => by
Goals accomplished! 🐙 
α: Type u_1

β: Type ?u.357

l: List α

L: List (List α)

join (l :: L) = [] ↔ ∀ (l_1 : List α), l_1 ∈ l :: L → l_1 = []simp only [
join: {α : Type ?u.618} → List (List α) → List α
join, 
append_eq_nil: ∀ {α : Type ?u.635} {p q : List α}, p ++ q = [] ↔ p = [] ∧ q = []
append_eq_nil, 
join_eq_nil: ∀ {L : List (List α)}, join L = [] ↔ ∀ (l : List α), l ∈ L → l = []
join_eq_nil, 
forall_mem_cons: ∀ {α : Type ?u.671} {p : α → Prop} {a : α} {l : List α}, (∀ (x : α), x ∈ a :: l → p x) ↔ p a ∧ ∀ (x : α), x ∈ l → p x
forall_mem_cons]
Goals accomplished! 🐙
#align list.join_eq_nil 
List.join_eq_nil: ∀ {α : Type u_1} {L : List (List α)}, join L = [] ↔ ∀ (l : List α), l ∈ L → l = []
List.join_eq_nil

@[simp]
theorem 
join_append: ∀ {α : Type u_1} (L₁ L₂ : List (List α)), join (L₁ ++ L₂) = join L₁ ++ join L₂
join_append (
L₁: List (List α)
L₁ 
L₂: List (List α)
L₂ : 
List: Type ?u.1003 → Type ?u.1003
List (
List: Type ?u.1000 → Type ?u.1000
List 
α: Type ?u.993
α)) : 
join: {α : Type ?u.1008} → List (List α) → List α
join (
L₁: List (List α)
L₁ ++ 
L₂: List (List α)
L₂) = 
join: {α : Type ?u.1066} → List (List α) → List α
join 
L₁: List (List α)
L₁ ++ 
join: {α : Type ?u.1069} → List (List α) → List α
join 
L₂: List (List α)
L₂ := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.996

L₁, L₂: List (List α)

join (L₁ ++ L₂) = join L₁ ++ join L₂induction 
L₁: List (List α)
L₁
α: Type u_1

β: Type ?u.996

L₂: List (List α)

nil
join ([] ++ L₂) = join [] ++ join L₂
α: Type u_1

β: Type ?u.996

L₂: List (List α)

head✝: List α

tail✝: List (List α)

tail_ih✝: join (tail✝ ++ L₂) = join tail✝ ++ join L₂

cons
join (head✝ :: tail✝ ++ L₂) = join (head✝ :: tail✝) ++ join L₂
  
α: Type u_1

β: Type ?u.996

L₁, L₂: List (List α)

join (L₁ ++ L₂) = join L₁ ++ join L₂·
α: Type u_1

β: Type ?u.996

L₂: List (List α)

nil
join ([] ++ L₂) = join [] ++ join L₂ 
α: Type u_1

β: Type ?u.996

L₂: List (List α)

nil
join ([] ++ L₂) = join [] ++ join L₂
α: Type u_1

β: Type ?u.996

L₂: List (List α)

head✝: List α

tail✝: List (List α)

tail_ih✝: join (tail✝ ++ L₂) = join tail✝ ++ join L₂

cons
join (head✝ :: tail✝ ++ L₂) = join (head✝ :: tail✝) ++ join L₂rfl
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.996

L₁, L₂: List (List α)

join (L₁ ++ L₂) = join L₁ ++ join L₂·
α: Type u_1

β: Type ?u.996

L₂: List (List α)

head✝: List α

tail✝: List (List α)

tail_ih✝: join (tail✝ ++ L₂) = join tail✝ ++ join L₂

cons
join (head✝ :: tail✝ ++ L₂) = join (head✝ :: tail✝) ++ join L₂ 
α: Type u_1

β: Type ?u.996

L₂: List (List α)

head✝: List α

tail✝: List (List α)

tail_ih✝: join (tail✝ ++ L₂) = join tail✝ ++ join L₂

cons
join (head✝ :: tail✝ ++ L₂) = join (head✝ :: tail✝) ++ join L₂simp [*]
Goals accomplished! 🐙
#align list.join_append 
List.join_append: ∀ {α : Type u_1} (L₁ L₂ : List (List α)), join (L₁ ++ L₂) = join L₁ ++ join L₂
List.join_append

theorem 
join_concat: ∀ {α : Type u_1} (L : List (List α)) (l : List α), join (concat L l) = join L ++ l
join_concat (
L: List (List α)
L : 
List: Type ?u.1309 → Type ?u.1309
List (
List: Type ?u.1310 → Type ?u.1310
List 
α: Type ?u.1303
α)) (
l: List α
l : 
List: Type ?u.1313 → Type ?u.1313
List 
α: Type ?u.1303
α) : 
join: {α : Type ?u.1317} → List (List α) → List α
join (
L: List (List α)
L.
concat: {α : Type ?u.1319} → List α → α → List α
concat 
l: List α
l) = 
join: {α : Type ?u.1329} → List (List α) → List α
join 
L: List (List α)
L ++ 
l: List α
l := by
Goals accomplished! 🐙 
α: Type u_1

β: Type ?u.1306

L: List (List α)

l: List α

join (concat L l) = join L ++ lsimp
Goals accomplished! 🐙
#align list.join_concat 
List.join_concat: ∀ {α : Type u_1} (L : List (List α)) (l : List α), join (concat L l) = join L ++ l
List.join_concat

-- Porting note: `ff/tt` should be translated to `false/true`.
-- Porting note: `List.filter` now takes a `Bool` not a `Prop`.
--     Should the correct spelling now be `== false` instead?
@[simp]
theorem 
join_filter_isEmpty_eq_false: ∀ [inst : DecidablePred fun l => isEmpty l = false] {L : List (List α)},
  join (filter (fun l => decide (isEmpty l = false)) L) = join L
join_filter_isEmpty_eq_false [
DecidablePred: {α : Sort ?u.1510} → (α → Prop) → Sort (max1?u.1510)
DecidablePred fun 
l: List α
l : 
List: Type ?u.1513 → Type ?u.1513
List 
α: Type ?u.1504
α => 
l: List α
l.
isEmpty: {α : Type ?u.1516} → List α → Bool
isEmpty = 
false: Bool
false] :
    ∀ {
L: List (List α)
L : 
List: Type ?u.1530 → Type ?u.1530
List (
List: Type ?u.1531 → Type ?u.1531
List 
α: Type ?u.1504
α)}, 
join: {α : Type ?u.1535} → List (List α) → List α
join (
L: List (List α)
L.
filter: {α : Type ?u.1537} → (α → Bool) → List α → List α
filter fun 
l: ?m.1544
l => 
l: ?m.1544
l.
isEmpty: {α : Type ?u.1547} → List α → Bool
isEmpty = 
false: Bool
false) = 
L: List (List α)
L.
join: {α : Type ?u.1613} → List (List α) → List α
join
  | [] => 
rfl: ∀ {α : Sort ?u.1639} {a : α}, a = a
rfl
  | [] :: 
L: List (List α)
L => by
Goals accomplished! 🐙
      
α: Type u_1

β: Type ?u.1507

inst✝: DecidablePred fun l => isEmpty l = false

L: List (List α)

join (filter (fun l => decide (isEmpty l = false)) ([] :: L)) = join ([] :: L)simp [
join_filter_isEmpty_eq_false: ∀ [inst : DecidablePred fun l => isEmpty l = false] {L : List (List α)},
  join (filter (fun l => decide (isEmpty l = false)) L) = join L
join_filter_isEmpty_eq_false (L := 
L: List (List α)
L), 
isEmpty_iff_eq_nil: ∀ {α : Type ?u.1849} {l : List α}, isEmpty l = true ↔ l = []
isEmpty_iff_eq_nil]
Goals accomplished! 🐙
  | (
a: α
a :: 
l: List α
l) :: 
L: List (List α)
L => by
Goals accomplished! 🐙
      
α: Type u_1

β: Type ?u.1507

inst✝: DecidablePred fun l => isEmpty l = false

a: α

l: List α

L: List (List α)

join (filter (fun l => decide (isEmpty l = false)) ((a :: l) :: L)) = join ((a :: l) :: L)have 
cons_not_empty: isEmpty (a :: l) = false
cons_not_empty : 
isEmpty: {α : Type ?u.2363} → List α → Bool
isEmpty (
a: α
a :: 
l: List α
l) = 
false: Bool
false := 
rfl: ∀ {α : Sort ?u.2369} {a : α}, a = a
rfl
α: Type u_1

β: Type ?u.1507

inst✝: DecidablePred fun l => isEmpty l = false

a: α

l: List α

L: List (List α)

cons_not_empty: isEmpty (a :: l) = false

join (filter (fun l => decide (isEmpty l = false)) ((a :: l) :: L)) = join ((a :: l) :: L)
      
α: Type u_1

β: Type ?u.1507

inst✝: DecidablePred fun l => isEmpty l = false

a: α

l: List α

L: List (List α)

join (filter (fun l => decide (isEmpty l = false)) ((a :: l) :: L)) = join ((a :: l) :: L)simp [
join_filter_isEmpty_eq_false: ∀ [inst : DecidablePred fun l => isEmpty l = false] {L : List (List α)},
  join (filter (fun l => decide (isEmpty l = false)) L) = join L
join_filter_isEmpty_eq_false (L := 
L: List (List α)
L), 
cons_not_empty: isEmpty (a :: l) = false
cons_not_empty]
Goals accomplished! 🐙
#align list.join_filter_empty_eq_ff 
List.join_filter_isEmpty_eq_false: ∀ {α : Type u_1} [inst : DecidablePred fun l => isEmpty l = false] {L : List (List α)},
  join (filter (fun l => decide (isEmpty l = false)) L) = join L
List.join_filter_isEmpty_eq_false

@[simp]
theorem 
join_filter_ne_nil: ∀ {α : Type u_1} [inst : DecidablePred fun l => l ≠ []] {L : List (List α)},
  join (filter (fun l => decide (l ≠ [])) L) = join L
join_filter_ne_nil [
DecidablePred: {α : Sort ?u.2832} → (α → Prop) → Sort (max1?u.2832)
DecidablePred fun 
l: List α
l : 
List: Type ?u.2835 → Type ?u.2835
List 
α: Type ?u.2826
α => 
l: List α
l ≠ 
[]: List ?m.2841
[]] {
L: List (List α)
L : 
List: Type ?u.2849 → Type ?u.2849
List (
List: Type ?u.2850 → Type ?u.2850
List 
α: Type ?u.2826
α)} :
    
join: {α : Type ?u.2854} → List (List α) → List α
join (
L: List (List α)
L.
filter: {α : Type ?u.2856} → (α → Bool) → List α → List α
filter fun 
l: ?m.2863
l => 
l: ?m.2863
l ≠ 
[]: List ?m.2868
[]) = 
L: List (List α)
L.
join: {α : Type ?u.2925} → List (List α) → List α
join := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.2829

inst✝: DecidablePred fun l => l ≠ []

L: List (List α)

join (filter (fun l => decide (l ≠ [])) L) = join Lsimp [
join_filter_isEmpty_eq_false: ∀ {α : Type ?u.2937} [inst : DecidablePred fun l => isEmpty l = false] {L : List (List α)},
  join (filter (fun l => decide (isEmpty l = false)) L) = join L
join_filter_isEmpty_eq_false, ← 
isEmpty_iff_eq_nil: ∀ {α : Type ?u.2953} {l : List α}, isEmpty l = true ↔ l = []
isEmpty_iff_eq_nil]
Goals accomplished! 🐙
#align list.join_filter_ne_nil 
List.join_filter_ne_nil: ∀ {α : Type u_1} [inst : DecidablePred fun l => l ≠ []] {L : List (List α)},
  join (filter (fun l => decide (l ≠ [])) L) = join L
List.join_filter_ne_nil

theorem 
join_join: ∀ (l : List (List (List α))), join (join l) = join (map join l)
join_join (
l: List (List (List α))
l : 
List: Type ?u.3809 → Type ?u.3809
List (
List: Type ?u.3810 → Type ?u.3810
List (
List: Type ?u.3811 → Type ?u.3811
List 
α: Type ?u.3803
α))) : 
l: List (List (List α))
l.
join: {α : Type ?u.3815} → List (List α) → List α
join.
join: {α : Type ?u.3818} → List (List α) → List α
join = (
l: List (List (List α))
l.
map: {α : Type ?u.3823} → {β : Type ?u.3822} → (α → β) → List α → List β
map 
join: {α : Type ?u.3830} → List (List α) → List α
join).
join: {α : Type ?u.3835} → List (List α) → List α
join := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.3806

l: List (List (List α))

join (join l) = join (map join l)induction 
l: List (List (List α))
l
α: Type u_1

β: Type ?u.3806

nil
join (join []) = join (map join [])
α: Type u_1

β: Type ?u.3806

head✝: List (List α)

tail✝: List (List (List α))

tail_ih✝: join (join tail✝) = join (map join tail✝)

cons
join (join (head✝ :: tail✝)) = join (map join (head✝ :: tail✝)) 
α: Type u_1

β: Type ?u.3806

l: List (List (List α))

join (join l) = join (map join l)<;>
α: Type u_1

β: Type ?u.3806

nil
join (join []) = join (map join [])
α: Type u_1

β: Type ?u.3806

head✝: List (List α)

tail✝: List (List (List α))

tail_ih✝: join (join tail✝) = join (map join tail✝)

cons
join (join (head✝ :: tail✝)) = join (map join (head✝ :: tail✝)) 
α: Type u_1

β: Type ?u.3806

l: List (List (List α))

join (join l) = join (map join l)simp [*]
Goals accomplished! 🐙
#align list.join_join 
List.join_join: ∀ {α : Type u_1} (l : List (List (List α))), join (join l) = join (map join l)
List.join_join

@[simp]
theorem 
length_join: ∀ {α : Type u_1} (L : List (List α)), length (join L) = sum (map length L)
length_join (
L: List (List α)
L : 
List: Type ?u.4051 → Type ?u.4051
List (
List: Type ?u.4052 → Type ?u.4052
List 
α: Type ?u.4045
α)) : 
length: {α : Type ?u.4056} → List α → ℕ
length (
join: {α : Type ?u.4058} → List (List α) → List α
join 
L: List (List α)
L) = 
sum: {α : Type ?u.4063} → [inst : Add α] → [inst : Zero α] → List α → α
sum (
map: {α : Type ?u.4068} → {β : Type ?u.4067} → (α → β) → List α → List β
map 
length: {α : Type ?u.4072} → List α → ℕ
length 
L: List (List α)
L) := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.4048

L: List (List α)

length (join L) = sum (map length L)induction 
L: List (List α)
L
α: Type u_1

β: Type ?u.4048

nil
length (join []) = sum (map length [])
α: Type u_1

β: Type ?u.4048

head✝: List α

tail✝: List (List α)

tail_ih✝: length (join tail✝) = sum (map length tail✝)

cons
length (join (head✝ :: tail✝)) = sum (map length (head✝ :: tail✝)) <;> [
α: Type u_1

β: Type ?u.4048

L: List (List α)

length (join L) = sum (map length L)rfl
Goals accomplished! 🐙; 
α: Type u_1

β: Type ?u.4048

L: List (List α)

length (join L) = sum (map length L)simp only [*, 
join: {α : Type ?u.4189} → List (List α) → List α
join, 
map: {α : Type ?u.4207} → {β : Type ?u.4206} → (α → β) → List α → List β
map, 
sum_cons: ∀ {M : Type ?u.4505} [inst : AddMonoid M] {l : List M} {a : M}, sum (a :: l) = a + sum l
sum_cons, 
length_append: ∀ {α : Type ?u.4522} (as bs : List α), length (as ++ bs) = length as + length bs
length_append]
Goals accomplished! 🐙]
Goals accomplished! 🐙
#align list.length_join 
List.length_join: ∀ {α : Type u_1} (L : List (List α)), length (join L) = sum (map length L)
List.length_join

@[simp]
theorem 
length_bind: ∀ {α : Type u_1} {β : Type u_2} (l : List α) (f : α → List β), length (List.bind l f) = sum (map (length ∘ f) l)
length_bind (
l: List α
l : 
List: Type ?u.4752 → Type ?u.4752
List 
α: Type ?u.4746
α) (
f: α → List β
f : 
α: Type ?u.4746
α → 
List: Type ?u.4757 → Type ?u.4757
List 
β: Type ?u.4749
β) :
    
length: {α : Type ?u.4761} → List α → ℕ
length (
List.bind: {α : Type ?u.4764} → {β : Type ?u.4763} → List α → (α → List β) → List β
List.bind 
l: List α
l 
f: α → List β
f) = 
sum: {α : Type ?u.4775} → [inst : Add α] → [inst : Zero α] → List α → α
sum (
map: {α : Type ?u.4780} → {β : Type ?u.4779} → (α → β) → List α → List β
map (
length: {α : Type ?u.4792} → List α → ℕ
length ∘ 
f: α → List β
f) 
l: List α
l) := by
Goals accomplished! 🐙 
α: Type u_1

β: Type u_2

l: List α

f: α → List β

length (List.bind l f) = sum (map (length ∘ f) l)rw [
α: Type u_1

β: Type u_2

l: List α

f: α → List β

length (List.bind l f) = sum (map (length ∘ f) l)
List.bind: {α : Type ?u.4860} → {β : Type ?u.4859} → List α → (α → List β) → List β
List.bind,
α: Type u_1

β: Type u_2

l: List α

f: α → List β

length (join (map f l)) = sum (map (length ∘ f) l) 
α: Type u_1

β: Type u_2

l: List α

f: α → List β

length (List.bind l f) = sum (map (length ∘ f) l)
length_join: ∀ {α : Type ?u.4861} (L : List (List α)), length (join L) = sum (map length L)
length_join,
α: Type u_1

β: Type u_2

l: List α

f: α → List β

sum (map length (map f l)) = sum (map (length ∘ f) l) 
α: Type u_1

β: Type u_2

l: List α

f: α → List β

length (List.bind l f) = sum (map (length ∘ f) l)
map_map: ∀ {β : Type ?u.4872} {γ : Type ?u.4873} {α : Type ?u.4874} (g : β → γ) (f : α → β) (l : List α),
  map g (map f l) = map (g ∘ f) l
map_map
α: Type u_1

β: Type u_2

l: List α

f: α → List β

sum (map (length ∘ f) l) = sum (map (length ∘ f) l)]
Goals accomplished! 🐙
#align list.length_bind 
List.length_bind: ∀ {α : Type u_1} {β : Type u_2} (l : List α) (f : α → List β), length (List.bind l f) = sum (map (length ∘ f) l)
List.length_bind

@[simp]
theorem 
bind_eq_nil: ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β}, List.bind l f = [] ↔ ∀ (x : α), x ∈ l → f x = []
bind_eq_nil {
l: List α
l : 
List: Type ?u.4947 → Type ?u.4947
List 
α: Type ?u.4941
α} {
f: α → List β
f : 
α: Type ?u.4941
α → 
List: Type ?u.4952 → Type ?u.4952
List 
β: Type ?u.4944
β} : 
List.bind: {α : Type ?u.4957} → {β : Type ?u.4956} → List α → (α → List β) → List β
List.bind 
l: List α
l 
f: α → List β
f = 
[]: List ?m.4968
[] ↔ ∀ 
x: ?m.4998
x ∈ 
l: List α
l, 
f: α → List β
f 
x: ?m.4998
x = 
[]: List ?m.5031
[] :=
  
join_eq_nil: ∀ {α : Type ?u.5064} {L : List (List α)}, join L = [] ↔ ∀ (l : List α), l ∈ L → l = []
join_eq_nil.
trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans <| by
Goals accomplished! 🐙
    
α: Type u_1

β: Type u_2

l: List α

f: α → List β

(∀ (l_1 : List β), l_1 ∈ map f l → l_1 = []) ↔ ∀ (x : α), x ∈ l → f x = []simp only [
mem_map: ∀ {α : Type ?u.5123} {β : Type ?u.5124} {b : β} {f : α → β} {l : List α}, b ∈ map f l ↔ ∃ a, a ∈ l ∧ f a = b
mem_map, 
forall_exists_index: ∀ {α : Sort ?u.5154} {p : α → Prop} {q : (∃ x, p x) → Prop},
  (∀ (h : ∃ x, p x), q h) ↔ ∀ (x : α) (h : p x), q (_ : ∃ x, p x)
forall_exists_index, 
and_imp: ∀ {a b c : Prop}, a ∧ b → c ↔ a → b → c
and_imp, 
forall_apply_eq_imp_iff₂: ∀ {α : Sort ?u.5191} {β : Sort ?u.5192} {f : α → β} {p : α → Prop} {q : β → Prop},
  (∀ (b : β) (a : α), p a → f a = b → q b) ↔ ∀ (a : α), p a → q (f a)
forall_apply_eq_imp_iff₂]
Goals accomplished! 🐙
#align list.bind_eq_nil 
List.bind_eq_nil: ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β}, List.bind l f = [] ↔ ∀ (x : α), x ∈ l → f x = []
List.bind_eq_nil

/-- In a join, taking the first elements up to an index which is the sum of the lengths of the
first `i` sublists, is the same as taking the join of the first `i` sublists. -/
theorem 
take_sum_join: ∀ (L : List (List α)) (i : ℕ), take (sum (take i (map length L))) (join L) = join (take i L)
take_sum_join (
L: List (List α)
L : 
List: Type ?u.5742 → Type ?u.5742
List (
List: Type ?u.5743 → Type ?u.5743
List 
α: Type ?u.5736
α)) (
i: ℕ
i : 
ℕ: Type
ℕ) :
    
L: List (List α)
L.
join: {α : Type ?u.5749} → List (List α) → List α
join.
take: {α : Type ?u.5752} → ℕ → List α → List α
take ((
L: List (List α)
L.
map: {α : Type ?u.5758} → {β : Type ?u.5757} → (α → β) → List α → List β
map 
length: {α : Type ?u.5765} → List α → ℕ
length).
take: {α : Type ?u.5770} → ℕ → List α → List α
take 
i: ℕ
i).
sum: {α : Type ?u.5776} → [inst : Add α] → [inst : Zero α] → List α → α
sum = (
L: List (List α)
L.
take: {α : Type ?u.5808} → ℕ → List α → List α
take 
i: ℕ
i).
join: {α : Type ?u.5813} → List (List α) → List α
join := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.5739

L: List (List α)

i: ℕ

take (sum (take i (map length L))) (join L) = join (take i L)induction 
L: List (List α)
L generalizing 
i: ℕ
i
α: Type u_1

β: Type ?u.5739

i: ℕ

nil
take (sum (take i (map length []))) (join []) = join (take i [])
α: Type u_1

β: Type ?u.5739

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)

i: ℕ

cons
take (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (take i (head✝ :: tail✝))
  
α: Type u_1

β: Type ?u.5739

L: List (List α)

i: ℕ

take (sum (take i (map length L))) (join L) = join (take i L)·
α: Type u_1

β: Type ?u.5739

i: ℕ

nil
take (sum (take i (map length []))) (join []) = join (take i []) 
α: Type u_1

β: Type ?u.5739

i: ℕ

nil
take (sum (take i (map length []))) (join []) = join (take i [])
α: Type u_1

β: Type ?u.5739

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)

i: ℕ

cons
take (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (take i (head✝ :: tail✝))simp
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.5739

L: List (List α)

i: ℕ

take (sum (take i (map length L))) (join L) = join (take i L)·
α: Type u_1

β: Type ?u.5739

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)

i: ℕ

cons
take (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (take i (head✝ :: tail✝)) 
α: Type u_1

β: Type ?u.5739

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)

i: ℕ

cons
take (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (take i (head✝ :: tail✝))cases 
i: ℕ
i
α: Type u_1

β: Type ?u.5739

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)

cons.zero
take (sum (take Nat.zero (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (take Nat.zero (head✝ :: tail✝))
α: Type u_1

β: Type ?u.5739

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)

n✝: ℕ

cons.succ
take (sum (take (Nat.succ n✝) (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) =   join (take (Nat.succ n✝) (head✝ :: tail✝)) 
α: Type u_1

β: Type ?u.5739

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)

i: ℕ

cons
take (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (take i (head✝ :: tail✝))<;>
α: Type u_1

β: Type ?u.5739

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)

cons.zero
take (sum (take Nat.zero (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (take Nat.zero (head✝ :: tail✝))
α: Type u_1

β: Type ?u.5739

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)

n✝: ℕ

cons.succ
take (sum (take (Nat.succ n✝) (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) =   join (take (Nat.succ n✝) (head✝ :: tail✝)) 
α: Type u_1

β: Type ?u.5739

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)

i: ℕ

cons
take (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (take i (head✝ :: tail✝))simp [
take_append: ∀ {α : Type ?u.6107} {l₁ l₂ : List α} (i : ℕ), take (length l₁ + i) (l₁ ++ l₂) = l₁ ++ take i l₂
take_append, *]
Goals accomplished! 🐙
#align list.take_sum_join 
List.take_sum_join: ∀ {α : Type u_1} (L : List (List α)) (i : ℕ), take (sum (take i (map length L))) (join L) = join (take i L)
List.take_sum_join

/-- In a join, dropping all the elements up to an index which is the sum of the lengths of the
first `i` sublists, is the same as taking the join after dropping the first `i` sublists. -/
theorem 
drop_sum_join: ∀ {α : Type u_1} (L : List (List α)) (i : ℕ), drop (sum (take i (map length L))) (join L) = join (drop i L)
drop_sum_join (
L: List (List α)
L : 
List: Type ?u.6453 → Type ?u.6453
List (
List: Type ?u.6454 → Type ?u.6454
List 
α: Type ?u.6447
α)) (
i: ℕ
i : 
ℕ: Type
ℕ) :
    
L: List (List α)
L.
join: {α : Type ?u.6460} → List (List α) → List α
join.
drop: {α : Type ?u.6463} → ℕ → List α → List α
drop ((
L: List (List α)
L.
map: {α : Type ?u.6469} → {β : Type ?u.6468} → (α → β) → List α → List β
map 
length: {α : Type ?u.6476} → List α → ℕ
length).
take: {α : Type ?u.6481} → ℕ → List α → List α
take 
i: ℕ
i).
sum: {α : Type ?u.6487} → [inst : Add α] → [inst : Zero α] → List α → α
sum = (
L: List (List α)
L.
drop: {α : Type ?u.6519} → ℕ → List α → List α
drop 
i: ℕ
i).
join: {α : Type ?u.6524} → List (List α) → List α
join := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.6450

L: List (List α)

i: ℕ

drop (sum (take i (map length L))) (join L) = join (drop i L)induction 
L: List (List α)
L generalizing 
i: ℕ
i
α: Type u_1

β: Type ?u.6450

i: ℕ

nil
drop (sum (take i (map length []))) (join []) = join (drop i [])
α: Type u_1

β: Type ?u.6450

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)

i: ℕ

cons
drop (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (drop i (head✝ :: tail✝))
  
α: Type u_1

β: Type ?u.6450

L: List (List α)

i: ℕ

drop (sum (take i (map length L))) (join L) = join (drop i L)·
α: Type u_1

β: Type ?u.6450

i: ℕ

nil
drop (sum (take i (map length []))) (join []) = join (drop i []) 
α: Type u_1

β: Type ?u.6450

i: ℕ

nil
drop (sum (take i (map length []))) (join []) = join (drop i [])
α: Type u_1

β: Type ?u.6450

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)

i: ℕ

cons
drop (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (drop i (head✝ :: tail✝))simp
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.6450

L: List (List α)

i: ℕ

drop (sum (take i (map length L))) (join L) = join (drop i L)·
α: Type u_1

β: Type ?u.6450

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)

i: ℕ

cons
drop (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (drop i (head✝ :: tail✝)) 
α: Type u_1

β: Type ?u.6450

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)

i: ℕ

cons
drop (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (drop i (head✝ :: tail✝))cases 
i: ℕ
i
α: Type u_1

β: Type ?u.6450

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)

cons.zero
drop (sum (take Nat.zero (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (drop Nat.zero (head✝ :: tail✝))
α: Type u_1

β: Type ?u.6450

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)

n✝: ℕ

cons.succ
drop (sum (take (Nat.succ n✝) (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) =   join (drop (Nat.succ n✝) (head✝ :: tail✝)) 
α: Type u_1

β: Type ?u.6450

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)

i: ℕ

cons
drop (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (drop i (head✝ :: tail✝))<;>
α: Type u_1

β: Type ?u.6450

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)

cons.zero
drop (sum (take Nat.zero (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (drop Nat.zero (head✝ :: tail✝))
α: Type u_1

β: Type ?u.6450

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)

n✝: ℕ

cons.succ
drop (sum (take (Nat.succ n✝) (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) =   join (drop (Nat.succ n✝) (head✝ :: tail✝)) 
α: Type u_1

β: Type ?u.6450

head✝: List α

tail✝: List (List α)

tail_ih✝: ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)

i: ℕ

cons
drop (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (drop i (head✝ :: tail✝))simp [
drop_append: ∀ {α : Type ?u.6806} {l₁ l₂ : List α} (i : ℕ), drop (length l₁ + i) (l₁ ++ l₂) = drop i l₂
drop_append, *]
Goals accomplished! 🐙
#align list.drop_sum_join 
List.drop_sum_join: ∀ {α : Type u_1} (L : List (List α)) (i : ℕ), drop (sum (take i (map length L))) (join L) = join (drop i L)
List.drop_sum_join

/-- Taking only the first `i+1` elements in a list, and then dropping the first `i` ones, one is
left with a list of length `1` made of the `i`-th element of the original list. -/
theorem 
drop_take_succ_eq_cons_get: ∀ {α : Type u_1} (L : List α) (i : Fin (length L)), drop (↑i) (take (↑i + 1) L) = [get L i]
drop_take_succ_eq_cons_get (
L: List α
L : 
List: Type ?u.7171 → Type ?u.7171
List 
α: Type ?u.7165
α) (
i: Fin (length L)
i : 
Fin: ℕ → Type
Fin 
L: List α
L.
length: {α : Type ?u.7174} → List α → ℕ
length) :
    (
L: List α
L.
take: {α : Type ?u.7182} → ℕ → List α → List α
take (
i: Fin (length L)
i + 
1: ?m.7191
1)).
drop: {α : Type ?u.7433} → ℕ → List α → List α
drop 
i: Fin (length L)
i = [
get: {α : Type ?u.7448} → (as : List α) → Fin (length as) → α
get 
L: List α
L 
i: Fin (length L)
i] := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.7168

L: List α

i: Fin (length L)

drop (↑i) (take (↑i + 1) L) = [get L i]induction' 
L: List α
L with 
head: ?m.7478
head 
tail: List ?m.7478
tail 
ih: ?m.7479 tail
ih
α: Type u_1

β: Type ?u.7168

L: List α

i✝: Fin (length L)

i: Fin (length [])

nil
drop (↑i) (take (↑i + 1) []) = [get [] i]
α: Type u_1

β: Type ?u.7168

L: List α

i✝: Fin (length L)

head: α

tail: List α

ih: ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]

i: Fin (length (head :: tail))

cons
drop (↑i) (take (↑i + 1) (head :: tail)) = [get (head :: tail) i]
  
α: Type u_1

β: Type ?u.7168

L: List α

i: Fin (length L)

drop (↑i) (take (↑i + 1) L) = [get L i]·
α: Type u_1

β: Type ?u.7168

L: List α

i✝: Fin (length L)

i: Fin (length [])

nil
drop (↑i) (take (↑i + 1) []) = [get [] i] 
α: Type u_1

β: Type ?u.7168

L: List α

i✝: Fin (length L)

i: Fin (length [])

nil
drop (↑i) (take (↑i + 1) []) = [get [] i]
α: Type u_1

β: Type ?u.7168

L: List α

i✝: Fin (length L)

head: α

tail: List α

ih: ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]

i: Fin (length (head :: tail))

cons
drop (↑i) (take (↑i + 1) (head :: tail)) = [get (head :: tail) i]exact (
Nat.not_succ_le_zero: ∀ (n : ℕ), Nat.succ n ≤ 0 → False
Nat.not_succ_le_zero 
i: Fin (length [])
i 
i: Fin (length [])
i.
isLt: ∀ {n : ℕ} (self : Fin n), ↑self < n
isLt).
elim: ∀ {C : Sort ?u.7591}, False → C
elim
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.7168

L: List α

i: Fin (length L)

drop (↑i) (take (↑i + 1) L) = [get L i]rcases 
i: Fin (length (head :: tail))
i with 
⟨_ | i, hi⟩: Fin (length (head :: tail))
⟨
_ | i: ℕ
_ | 
i: ℕ
i
⟨_ | i, hi⟩: Fin (length (head :: tail))
, 
hi: unknown free variable '_uniq.7614'
hi
⟨_ | i, hi⟩: Fin (length (head :: tail))
⟩
α: Type u_1

β: Type ?u.7168

L: List α

i: Fin (length L)

head: α

tail: List α

ih: ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]

hi: Nat.zero < length (head :: tail)

cons.mk.zero
drop (↑{ val := Nat.zero, isLt := hi }) (take (↑{ val := Nat.zero, isLt := hi } + 1) (head :: tail)) =   [get (head :: tail) { val := Nat.zero, isLt := hi }]
α: Type u_1

β: Type ?u.7168

L: List α

i✝: Fin (length L)

head: α

tail: List α

ih: ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]

i: ℕ

hi: Nat.succ i < length (head :: tail)

cons.mk.succ
drop (↑{ val := Nat.succ i, isLt := hi }) (take (↑{ val := Nat.succ i, isLt := hi } + 1) (head :: tail)) =   [get (head :: tail) { val := Nat.succ i, isLt := hi }]
  
α: Type u_1

β: Type ?u.7168

L: List α

i: Fin (length L)

drop (↑i) (take (↑i + 1) L) = [get L i]·
α: Type u_1

β: Type ?u.7168

L: List α

i: Fin (length L)

head: α

tail: List α

ih: ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]

hi: Nat.zero < length (head :: tail)

cons.mk.zero
drop (↑{ val := Nat.zero, isLt := hi }) (take (↑{ val := Nat.zero, isLt := hi } + 1) (head :: tail)) =   [get (head :: tail) { val := Nat.zero, isLt := hi }] 
α: Type u_1

β: Type ?u.7168

L: List α

i: Fin (length L)

head: α

tail: List α

ih: ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]

hi: Nat.zero < length (head :: tail)

cons.mk.zero
drop (↑{ val := Nat.zero, isLt := hi }) (take (↑{ val := Nat.zero, isLt := hi } + 1) (head :: tail)) =   [get (head :: tail) { val := Nat.zero, isLt := hi }]
α: Type u_1

β: Type ?u.7168

L: List α

i✝: Fin (length L)

head: α

tail: List α

ih: ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]

i: ℕ

hi: Nat.succ i < length (head :: tail)

cons.mk.succ
drop (↑{ val := Nat.succ i, isLt := hi }) (take (↑{ val := Nat.succ i, isLt := hi } + 1) (head :: tail)) =   [get (head :: tail) { val := Nat.succ i, isLt := hi }]simp
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.7168

L: List α

i: Fin (length L)

drop (↑i) (take (↑i + 1) L) = [get L i]·
α: Type u_1

β: Type ?u.7168

L: List α

i✝: Fin (length L)

head: α

tail: List α

ih: ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]

i: ℕ

hi: Nat.succ i < length (head :: tail)

cons.mk.succ
drop (↑{ val := Nat.succ i, isLt := hi }) (take (↑{ val := Nat.succ i, isLt := hi } + 1) (head :: tail)) =   [get (head :: tail) { val := Nat.succ i, isLt := hi }] 
α: Type u_1

β: Type ?u.7168

L: List α

i✝: Fin (length L)

head: α

tail: List α

ih: ∀ (i : Fin (length tail)), drop (↑i) (take (↑i + 1) tail) = [get tail i]

i: ℕ

hi: Nat.succ i < length (head :: tail)

cons.mk.succ
drop (↑{ val := Nat.succ i, isLt := hi }) (take (↑{ val := Nat.succ i, isLt := hi } + 1) (head :: tail)) =   [get (head :: tail) { val := Nat.succ i, isLt := hi }]simpa using 
ih: ?m.7479 tail
ih ⟨
i: ℕ
i, 
Nat.lt_of_succ_lt_succ: ∀ {n m : ℕ}, Nat.succ n < Nat.succ m → n < m
Nat.lt_of_succ_lt_succ 
hi: Nat.succ i < length (head :: tail)
hi⟩
Goals accomplished! 🐙

set_option linter.deprecated false in
/-- Taking only the first `i+1` elements in a list, and then dropping the first `i` ones, one is
left with a list of length `1` made of the `i`-th element of the original list. -/
@[deprecated 
drop_take_succ_eq_cons_get: ∀ {α : Type u_1} (L : List α) (i : Fin (length L)), drop (↑i) (take (↑i + 1) L) = [get L i]
drop_take_succ_eq_cons_get]
theorem 
drop_take_succ_eq_cons_nthLe: ∀ (L : List α) {i : ℕ} (hi : i < length L), drop i (take (i + 1) L) = [nthLe L i hi]
drop_take_succ_eq_cons_nthLe (
L: List α
L : 
List: Type ?u.8051 → Type ?u.8051
List 
α: Type ?u.8045
α) {
i: ℕ
i : 
ℕ: Type
ℕ} (
hi: i < length L
hi : 
i: ℕ
i < 
L: List α
L.
length: {α : Type ?u.8057} → List α → ℕ
length) :
    (
L: List α
L.
take: {α : Type ?u.8070} → ℕ → List α → List α
take (
i: ℕ
i + 
1: ?m.8079
1)).
drop: {α : Type ?u.8131} → ℕ → List α → List α
drop 
i: ℕ
i = [
nthLe: {α : Type ?u.8146} → (l : List α) → (n : ℕ) → n < length l → α
nthLe 
L: List α
L 
i: ℕ
i 
hi: i < length L
hi] := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.8048

L: List α

i: ℕ

hi: i < length L

drop i (take (i + 1) L) = [nthLe L i hi]induction' 
L: List α
L with 
head: ?m.8177
head 
tail: List ?m.8177
tail generalizing 
i: ℕ
i
α: Type u_1

β: Type ?u.8048

L: List α

i✝: ℕ

hi✝: i✝ < length L

i: ℕ

hi: i < length []

nil
drop i (take (i + 1) []) = [nthLe [] i hi]
α: Type u_1

β: Type ?u.8048

L: List α

i✝: ℕ

hi✝: i✝ < length L

head: α

tail: List α

tail_ih✝: ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]

i: ℕ

hi: i < length (head :: tail)

cons
drop i (take (i + 1) (head :: tail)) = [nthLe (head :: tail) i hi]
  
α: Type u_1

β: Type ?u.8048

L: List α

i: ℕ

hi: i < length L

drop i (take (i + 1) L) = [nthLe L i hi]·
α: Type u_1

β: Type ?u.8048

L: List α

i✝: ℕ

hi✝: i✝ < length L

i: ℕ

hi: i < length []

nil
drop i (take (i + 1) []) = [nthLe [] i hi] 
α: Type u_1

β: Type ?u.8048

L: List α

i✝: ℕ

hi✝: i✝ < length L

i: ℕ

hi: i < length []

nil
drop i (take (i + 1) []) = [nthLe [] i hi]
α: Type u_1

β: Type ?u.8048

L: List α

i✝: ℕ

hi✝: i✝ < length L

head: α

tail: List α

tail_ih✝: ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]

i: ℕ

hi: i < length (head :: tail)

cons
drop i (take (i + 1) (head :: tail)) = [nthLe (head :: tail) i hi]simp only [
length: {α : Type ?u.8210} → List α → ℕ
length] at 
hi: i < length []
hi
α: Type u_1

β: Type ?u.8048

L: List α

i✝: ℕ

hi✝: i✝ < length L

i: ℕ

hi: i < 0

nil
drop i (take (i + 1) []) = [nthLe [] i hi]
    
α: Type u_1

β: Type ?u.8048

L: List α

i✝: ℕ

hi✝: i✝ < length L

i: ℕ

hi: i < length []

nil
drop i (take (i + 1) []) = [nthLe [] i hi]exact (
Nat.not_succ_le_zero: ∀ (n : ℕ), Nat.succ n ≤ 0 → False
Nat.not_succ_le_zero 
i: ℕ
i 
hi: i < 0
hi).
elim: ∀ {C : Sort ?u.8494}, False → C
elim
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.8048

L: List α

i: ℕ

hi: i < length L

drop i (take (i + 1) L) = [nthLe L i hi]cases' 
i: ℕ
i with 
i: ℕ
i hi
α: Type u_1

β: Type ?u.8048

L: List α

i: ℕ

hi✝: i < length L

head: α

tail: List α

tail_ih✝: ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]

hi: Nat.zero < length (head :: tail)

cons.zero
drop Nat.zero (take (Nat.zero + 1) (head :: tail)) = [nthLe (head :: tail) Nat.zero hi]
α: Type u_1

β: Type ?u.8048

L: List α

i✝: ℕ

hi✝: i✝ < length L

head: α

tail: List α

tail_ih✝: ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]

i: ℕ

hi: Nat.succ i < length (head :: tail)

cons.succ
drop (Nat.succ i) (take (Nat.succ i + 1) (head :: tail)) = [nthLe (head :: tail) (Nat.succ i) hi]
  
α: Type u_1

β: Type ?u.8048

L: List α

i: ℕ

hi: i < length L

drop i (take (i + 1) L) = [nthLe L i hi]·
α: Type u_1

β: Type ?u.8048

L: List α

i: ℕ

hi✝: i < length L

head: α

tail: List α

tail_ih✝: ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]

hi: Nat.zero < length (head :: tail)

cons.zero
drop Nat.zero (take (Nat.zero + 1) (head :: tail)) = [nthLe (head :: tail) Nat.zero hi] 
α: Type u_1

β: Type ?u.8048

L: List α

i: ℕ

hi✝: i < length L

head: α

tail: List α

tail_ih✝: ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]

hi: Nat.zero < length (head :: tail)

cons.zero
drop Nat.zero (take (Nat.zero + 1) (head :: tail)) = [nthLe (head :: tail) Nat.zero hi]
α: Type u_1

β: Type ?u.8048

L: List α

i✝: ℕ

hi✝: i✝ < length L

head: α

tail: List α

tail_ih✝: ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]

i: ℕ

hi: Nat.succ i < length (head :: tail)

cons.succ
drop (Nat.succ i) (take (Nat.succ i + 1) (head :: tail)) = [nthLe (head :: tail) (Nat.succ i) hi]simp
α: Type u_1

β: Type ?u.8048

L: List α

i: ℕ

hi✝: i < length L

head: α

tail: List α

tail_ih✝: ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]

hi: Nat.zero < length (head :: tail)

cons.zero
head = nthLe (head :: tail) 0 hi
    
α: Type u_1

β: Type ?u.8048

L: List α

i: ℕ

hi✝: i < length L

head: α

tail: List α

tail_ih✝: ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]

hi: Nat.zero < length (head :: tail)

cons.zero
drop Nat.zero (take (Nat.zero + 1) (head :: tail)) = [nthLe (head :: tail) Nat.zero hi]rfl
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.8048

L: List α

i: ℕ

hi: i < length L

drop i (take (i + 1) L) = [nthLe L i hi]have : 
i: ℕ
i < 
tail: List ?m.8177
tail.
length: {α : Type ?u.8729} → List α → ℕ
length := 
α: Type u_1

β: Type ?u.8048

L: List α

i✝: ℕ

hi✝: i✝ < length L

head: α

tail: List α

tail_ih✝: ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]

i: ℕ

hi: Nat.succ i < length (head :: tail)

cons.succ
drop (Nat.succ i) (take (Nat.succ i + 1) (head :: tail)) = [nthLe (head :: tail) (Nat.succ i) hi]by
Goals accomplished! 🐙
    
α: Type u_1

β: Type ?u.8048

L: List α

i✝: ℕ

hi✝: i✝ < length L

head: α

tail: List α

tail_ih✝: ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]

i: ℕ

hi: Nat.succ i < length (head :: tail)

i < length tailsimp at 
hi: Nat.succ i < length (head :: tail)
hi
α: Type u_1

β: Type ?u.8048

L: List α

i✝: ℕ

hi✝: i✝ < length L

head: α

tail: List α

tail_ih✝: ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]

i: ℕ

hi: Nat.succ i < Nat.succ (length tail)

i < length tail
    
α: Type u_1

β: Type ?u.8048

L: List α

i✝: ℕ

hi✝: i✝ < length L

head: α

tail: List α

tail_ih✝: ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]

i: ℕ

hi: Nat.succ i < length (head :: tail)

i < length tailexact 
Nat.lt_of_succ_lt_succ: ∀ {n m : ℕ}, Nat.succ n < Nat.succ m → n < m
Nat.lt_of_succ_lt_succ 
hi: Nat.succ i < Nat.succ (length tail)
hi
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.8048

L: List α

i: ℕ

hi: i < length L

drop i (take (i + 1) L) = [nthLe L i hi]simp [*]
α: Type u_1

β: Type ?u.8048

L: List α

i✝: ℕ

hi✝: i✝ < length L

head: α

tail: List α

tail_ih✝: ∀ {i : ℕ} (hi : i < length tail), drop i (take (i + 1) tail) = [nthLe tail i hi]

i: ℕ

hi: Nat.succ i < length (head :: tail)

this: i < length tail

cons.succ
nthLe tail i (_ : i < length tail) = nthLe (head :: tail) (Nat.succ i) hi
  
α: Type u_1

β: Type ?u.8048

L: List α

i: ℕ

hi: i < length L

drop i (take (i + 1) L) = [nthLe L i hi]rfl
Goals accomplished! 🐙
#align list.drop_take_succ_eq_cons_nth_le 
List.drop_take_succ_eq_cons_nthLe: ∀ {α : Type u_1} (L : List α) {i : ℕ} (hi : i < length L), drop i (take (i + 1) L) = [nthLe L i hi]
List.drop_take_succ_eq_cons_nthLe

/-- In a join of sublists, taking the slice between the indices `A` and `B - 1` gives back the
original sublist of index `i` if `A` is the sum of the lengths of sublists of index `< i`, and
`B` is the sum of the lengths of sublists of index `≤ i`. -/
theorem 
drop_take_succ_join_eq_get: ∀ {α : Type u_1} (L : List (List α)) (i : Fin (length L)),
  drop (sum (take (↑i) (map length L))) (take (sum (take (↑i + 1) (map length L))) (join L)) = get L i
drop_take_succ_join_eq_get (
L: List (List α)
L : 
List: Type ?u.9240 → Type ?u.9240
List (
List: Type ?u.9241 → Type ?u.9241
List 
α: Type ?u.9234
α)) (
i: Fin (length L)
i : 
Fin: ℕ → Type
Fin 
L: List (List α)
L.
length: {α : Type ?u.9244} → List α → ℕ
length) :
    (
L: List (List α)
L.
join: {α : Type ?u.9252} → List (List α) → List α
join.
take: {α : Type ?u.9254} → ℕ → List α → List α
take ((
L: List (List α)
L.
map: {α : Type ?u.9260} → {β : Type ?u.9259} → (α → β) → List α → List β
map 
length: {α : Type ?u.9267} → List α → ℕ
length).
take: {α : Type ?u.9272} → ℕ → List α → List α
take (
i: Fin (length L)
i + 
1: ?m.9281
1)).
sum: {α : Type ?u.9524} → [inst : Add α] → [inst : Zero α] → List α → α
sum).
drop: {α : Type ?u.9555} → ℕ → List α → List α
drop ((
L: List (List α)
L.
map: {α : Type ?u.9561} → {β : Type ?u.9560} → (α → β) → List α → List β
map 
length: {α : Type ?u.9568} → List α → ℕ
length).
take: {α : Type ?u.9573} → ℕ → List α → List α
take 
i: Fin (length L)
i).
sum: {α : Type ?u.9578} → [inst : Add α] → [inst : Zero α] → List α → α
sum =
      
get: {α : Type ?u.9594} → (as : List α) → Fin (length as) → α
get 
L: List (List α)
L 
i: Fin (length L)
i := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.9237

L: List (List α)

i: Fin (length L)

drop (sum (take (↑i) (map length L))) (take (sum (take (↑i + 1) (map length L))) (join L)) = get L ihave : (
L: List (List α)
L.
map: {α : Type ?u.9606} → {β : Type ?u.9605} → (α → β) → List α → List β
map 
length: {α : Type ?u.9613} → List α → ℕ
length).
take: {α : Type ?u.9619} → ℕ → List α → List α
take 
i: Fin (length L)
i = ((
L: List (List α)
L.
take: {α : Type ?u.9706} → ℕ → List α → List α
take (
i: Fin (length L)
i + 
1: ?m.9715
1)).
map: {α : Type ?u.9835} → {β : Type ?u.9834} → (α → β) → List α → List β
map 
length: {α : Type ?u.9842} → List α → ℕ
length).
take: {α : Type ?u.9847} → ℕ → List α → List α
take 
i: Fin (length L)
i := 
α: Type u_1

β: Type ?u.9237

L: List (List α)

i: Fin (length L)

drop (sum (take (↑i) (map length L))) (take (sum (take (↑i + 1) (map length L))) (join L)) = get L iby
Goals accomplished! 🐙
    
α: Type u_1

β: Type ?u.9237

L: List (List α)

i: Fin (length L)

take (↑i) (map length L) = take (↑i) (map length (take (↑i + 1) L))simp [
map_take: ∀ {α : Type ?u.9857} {β : Type ?u.9858} (f : α → β) (L : List α) (i : ℕ), map f (take i L) = take i (map f L)
map_take, 
take_take: ∀ {α : Type ?u.9878} (n m : ℕ) (l : List α), take n (take m l) = take (min n m) l
take_take]
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.9237

L: List (List α)

i: Fin (length L)

drop (sum (take (↑i) (map length L))) (take (sum (take (↑i + 1) (map length L))) (join L)) = get L isimp [
take_sum_join: ∀ {α : Type ?u.10677} (L : List (List α)) (i : ℕ), take (sum (take i (map length L))) (join L) = join (take i L)
take_sum_join, 
this: take (↑i) (map length L) = take (↑i) (map length (take (↑i + 1) L))
this, 
drop_sum_join: ∀ {α : Type ?u.10693} (L : List (List α)) (i : ℕ), drop (sum (take i (map length L))) (join L) = join (drop i L)
drop_sum_join, 
drop_take_succ_eq_cons_get: ∀ {α : Type ?u.10704} (L : List α) (i : Fin (length L)), drop (↑i) (take (↑i + 1) L) = [get L i]
drop_take_succ_eq_cons_get]
Goals accomplished! 🐙

set_option linter.deprecated false in
/-- In a join of sublists, taking the slice between the indices `A` and `B - 1` gives back the
original sublist of index `i` if `A` is the sum of the lengths of sublists of index `< i`, and
`B` is the sum of the lengths of sublists of index `≤ i`. -/
@[deprecated 
drop_take_succ_join_eq_get: ∀ {α : Type u_1} (L : List (List α)) (i : Fin (length L)),
  drop (sum (take (↑i) (map length L))) (take (sum (take (↑i + 1) (map length L))) (join L)) = get L i
drop_take_succ_join_eq_get]
theorem 
drop_take_succ_join_eq_nthLe: ∀ (L : List (List α)) {i : ℕ} (hi : i < length L),
  drop (sum (take i (map length L))) (take (sum (take (i + 1) (map length L))) (join L)) = nthLe L i hi
drop_take_succ_join_eq_nthLe (
L: List (List α)
L : 
List: Type ?u.11185 → Type ?u.11185
List (
List: Type ?u.11186 → Type ?u.11186
List 
α: Type ?u.11179
α)) {
i: ℕ
i : 
ℕ: Type
ℕ} (
hi: i < length L
hi : 
i: ℕ
i < 
L: List (List α)
L.
length: {α : Type ?u.11192} → List α → ℕ
length) :
    (
L: List (List α)
L.
join: {α : Type ?u.11205} → List (List α) → List α
join.
take: {α : Type ?u.11207} → ℕ → List α → List α
take ((
L: List (List α)
L.
map: {α : Type ?u.11213} → {β : Type ?u.11212} → (α → β) → List α → List β
map 
length: {α : Type ?u.11220} → List α → ℕ
length).
take: {α : Type ?u.11225} → ℕ → List α → List α
take (
i: ℕ
i + 
1: ?m.11234
1)).
sum: {α : Type ?u.11287} → [inst : Add α] → [inst : Zero α] → List α → α
sum).
drop: {α : Type ?u.11318} → ℕ → List α → List α
drop ((
L: List (List α)
L.
map: {α : Type ?u.11324} → {β : Type ?u.11323} → (α → β) → List α → List β
map 
length: {α : Type ?u.11331} → List α → ℕ
length).
take: {α : Type ?u.11336} → ℕ → List α → List α
take 
i: ℕ
i).
sum: {α : Type ?u.11341} → [inst : Add α] → [inst : Zero α] → List α → α
sum =
      
nthLe: {α : Type ?u.11357} → (l : List α) → (n : ℕ) → n < length l → α
nthLe 
L: List (List α)
L 
i: ℕ
i 
hi: i < length L
hi := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.11182

L: List (List α)

i: ℕ

hi: i < length L

drop (sum (take i (map length L))) (take (sum (take (i + 1) (map length L))) (join L)) = nthLe L i hihave : (
L: List (List α)
L.
map: {α : Type ?u.11370} → {β : Type ?u.11369} → (α → β) → List α → List β
map 
length: {α : Type ?u.11377} → List α → ℕ
length).
take: {α : Type ?u.11383} → ℕ → List α → List α
take 
i: ℕ
i = ((
L: List (List α)
L.
take: {α : Type ?u.11388} → ℕ → List α → List α
take (
i: ℕ
i + 
1: ?m.11397
1)).
map: {α : Type ?u.11434} → {β : Type ?u.11433} → (α → β) → List α → List β
map 
length: {α : Type ?u.11441} → List α → ℕ
length).
take: {α : Type ?u.11446} → ℕ → List α → List α
take 
i: ℕ
i := 
α: Type u_1

β: Type ?u.11182

L: List (List α)

i: ℕ

hi: i < length L

drop (sum (take i (map length L))) (take (sum (take (i + 1) (map length L))) (join L)) = nthLe L i hiby
Goals accomplished! 🐙
    
α: Type u_1

β: Type ?u.11182

L: List (List α)

i: ℕ

hi: i < length L

take i (map length L) = take i (map length (take (i + 1) L))simp [
map_take: ∀ {α : Type ?u.11456} {β : Type ?u.11457} (f : α → β) (L : List α) (i : ℕ), map f (take i L) = take i (map f L)
map_take, 
take_take: ∀ {α : Type ?u.11477} (n m : ℕ) (l : List α), take n (take m l) = take (min n m) l
take_take]
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.11182

L: List (List α)

i: ℕ

hi: i < length L

drop (sum (take i (map length L))) (take (sum (take (i + 1) (map length L))) (join L)) = nthLe L i hisimp [
take_sum_join: ∀ {α : Type ?u.12270} (L : List (List α)) (i : ℕ), take (sum (take i (map length L))) (join L) = join (take i L)
take_sum_join, 
this: take i (map length L) = take i (map length (take (i + 1) L))
this, 
drop_sum_join: ∀ {α : Type ?u.12286} (L : List (List α)) (i : ℕ), drop (sum (take i (map length L))) (join L) = join (drop i L)
drop_sum_join, 
drop_take_succ_eq_cons_nthLe: ∀ {α : Type ?u.12298} (L : List α) {i : ℕ} (hi : i < length L), drop i (take (i + 1) L) = [nthLe L i hi]
drop_take_succ_eq_cons_nthLe 
_: List ?m.12299
_ 
hi: i < length L
hi]
Goals accomplished! 🐙
#align list.drop_take_succ_join_eq_nth_le 
List.drop_take_succ_join_eq_nthLe: ∀ {α : Type u_1} (L : List (List α)) {i : ℕ} (hi : i < length L),
  drop (sum (take i (map length L))) (take (sum (take (i + 1) (map length L))) (join L)) = nthLe L i hi
List.drop_take_succ_join_eq_nthLe

set_option linter.deprecated false in
/-- Auxiliary lemma to control elements in a join. -/
@[deprecated]
theorem 
sum_take_map_length_lt1: ∀ (L : List (List α)) {i j : ℕ} (hi : i < length L),
  j < length (nthLe L i hi) → sum (take i (map length L)) + j < sum (take (i + 1) (map length L))
sum_take_map_length_lt1 (
L: List (List α)
L : 
List: Type ?u.12786 → Type ?u.12786
List (
List: Type ?u.12787 → Type ?u.12787
List 
α: Type ?u.12780
α)) {
i: ℕ
i 
j: ℕ
j : 
ℕ: Type
ℕ} (
hi: i < length L
hi : 
i: ℕ
i < 
L: List (List α)
L.
length: {α : Type ?u.12795} → List α → ℕ
length)
    (
hj: j < length (nthLe L i hi)
hj : 
j: ℕ
j < (
nthLe: {α : Type ?u.12808} → (l : List α) → (n : ℕ) → n < length l → α
nthLe 
L: List (List α)
L 
i: ℕ
i 
hi: i < length L
hi).
length: {α : Type ?u.12811} → List α → ℕ
length) :
    ((
L: List (List α)
L.
map: {α : Type ?u.12824} → {β : Type ?u.12823} → (α → β) → List α → List β
map 
length: {α : Type ?u.12831} → List α → ℕ
length).
take: {α : Type ?u.12836} → ℕ → List α → List α
take 
i: ℕ
i).
sum: {α : Type ?u.12842} → [inst : Add α] → [inst : Zero α] → List α → α
sum + 
j: ℕ
j < ((
L: List (List α)
L.
map: {α : Type ?u.12875} → {β : Type ?u.12874} → (α → β) → List α → List β
map 
length: {α : Type ?u.12882} → List α → ℕ
length).
take: {α : Type ?u.12887} → ℕ → List α → List α
take (
i: ℕ
i + 
1: ?m.12896
1)).
sum: {α : Type ?u.12947} → [inst : Add α] → [inst : Zero α] → List α → α
sum := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.12783

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

sum (take i (map length L)) + j < sum (take (i + 1) (map length L))simp [
hi: i < length L
hi, 
sum_take_succ: ∀ {M : Type ?u.13008} [inst : AddMonoid M] (L : List M) (i : ℕ) (p : i < length L),
  sum (take (i + 1) L) = sum (take i L) + nthLe L i p
sum_take_succ, 
hj: j < length (nthLe L i hi)
hj]
Goals accomplished! 🐙
#align list.sum_take_map_length_lt1 
List.sum_take_map_length_lt1: ∀ {α : Type u_1} (L : List (List α)) {i j : ℕ} (hi : i < length L),
  j < length (nthLe L i hi) → sum (take i (map length L)) + j < sum (take (i + 1) (map length L))
List.sum_take_map_length_lt1

set_option linter.deprecated false in
/-- Auxiliary lemma to control elements in a join. -/
@[deprecated]
theorem 
sum_take_map_length_lt2: ∀ (L : List (List α)) {i j : ℕ} (hi : i < length L),
  j < length (nthLe L i hi) → sum (take i (map length L)) + j < length (join L)
sum_take_map_length_lt2 (
L: List (List α)
L : 
List: Type ?u.13933 → Type ?u.13933
List (
List: Type ?u.13934 → Type ?u.13934
List 
α: Type ?u.13927
α)) {
i: ℕ
i 
j: ℕ
j : 
ℕ: Type
ℕ} (
hi: i < length L
hi : 
i: ℕ
i < 
L: List (List α)
L.
length: {α : Type ?u.13942} → List α → ℕ
length)
    (
hj: j < length (nthLe L i hi)
hj : 
j: ℕ
j < (
nthLe: {α : Type ?u.13955} → (l : List α) → (n : ℕ) → n < length l → α
nthLe 
L: List (List α)
L 
i: ℕ
i 
hi: i < length L
hi).
length: {α : Type ?u.13958} → List α → ℕ
length) : ((
L: List (List α)
L.
map: {α : Type ?u.13971} → {β : Type ?u.13970} → (α → β) → List α → List β
map 
length: {α : Type ?u.13978} → List α → ℕ
length).
take: {α : Type ?u.13983} → ℕ → List α → List α
take 
i: ℕ
i).
sum: {α : Type ?u.13989} → [inst : Add α] → [inst : Zero α] → List α → α
sum + 
j: ℕ
j < 
L: List (List α)
L.
join: {α : Type ?u.14021} → List (List α) → List α
join.
length: {α : Type ?u.14023} → List α → ℕ
length := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.13930

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

sum (take i (map length L)) + j < length (join L)convert 
lt_of_lt_of_le: ∀ {α : Type ?u.14079} [inst : Preorder α] {a b c : α}, a < b → b ≤ c → a < c
lt_of_lt_of_le (
sum_take_map_length_lt1: ∀ {α : Type ?u.14101} (L : List (List α)) {i j : ℕ} (hi : i < length L),
  j < length (nthLe L i hi) → sum (take i (map length L)) + j < sum (take (i + 1) (map length L))
sum_take_map_length_lt1 
L: List (List α)
L 
hi: i < length L
hi 
hj: j < length (nthLe L i hi)
hj) (
monotone_sum_take: ∀ {M : Type ?u.14162} [inst : CanonicallyOrderedAddMonoid M] (L : List M), Monotone fun i => sum (take i L)
monotone_sum_take 
_: List ?m.14163
_ 
hi: i < length L
hi)
α: Type u_1

β: Type ?u.13930

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

h.e'_4
length (join L) = (fun i => sum (take i (map length L))) (length L)
  
α: Type u_1

β: Type ?u.13930

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

sum (take i (map length L)) + j < length (join L)have : 
L: List (List α)
L.
length: {α : Type ?u.15356} → List α → ℕ
length = (
L: List (List α)
L.
map: {α : Type ?u.15361} → {β : Type ?u.15360} → (α → β) → List α → List β
map 
length: {α : Type ?u.15368} → List α → ℕ
length).
length: {α : Type ?u.15373} → List α → ℕ
length := 
α: Type u_1

β: Type ?u.13930

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

h.e'_4
length (join L) = (fun i => sum (take i (map length L))) (length L)by
Goals accomplished! 🐙 
α: Type u_1

β: Type ?u.13930

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

length L = length (map length L)simp
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.13930

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

sum (take i (map length L)) + j < length (join L)simp [
this: length L = length (map length L)
this, -
length_map: ∀ {α : Type u} {β : Type v} (as : List α) (f : α → β), length (map f as) = length as
length_map]
Goals accomplished! 🐙
#align list.sum_take_map_length_lt2 
List.sum_take_map_length_lt2: ∀ {α : Type u_1} (L : List (List α)) {i j : ℕ} (hi : i < length L),
  j < length (nthLe L i hi) → sum (take i (map length L)) + j < length (join L)
List.sum_take_map_length_lt2

set_option linter.deprecated false in
/-- The `n`-th element in a join of sublists is the `j`-th element of the `i`th sublist,
where `n` can be obtained in terms of `i` and `j` by adding the lengths of all the sublists
of index `< i`, and adding `j`. -/
@[deprecated]
theorem 
nthLe_join: ∀ (L : List (List α)) {i j : ℕ} (hi : i < length L) (hj : j < length (nthLe L i hi)),
  nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =     nthLe (nthLe L i hi) j hj
nthLe_join (
L: List (List α)
L : 
List: Type ?u.15599 → Type ?u.15599
List (
List: Type ?u.15600 → Type ?u.15600
List 
α: Type ?u.15593
α)) {
i: ℕ
i 
j: ℕ
j : 
ℕ: Type
ℕ} (
hi: i < length L
hi : 
i: ℕ
i < 
L: List (List α)
L.
length: {α : Type ?u.15608} → List α → ℕ
length)
    (
hj: j < length (nthLe L i hi)
hj : 
j: ℕ
j < (
nthLe: {α : Type ?u.15621} → (l : List α) → (n : ℕ) → n < length l → α
nthLe 
L: List (List α)
L 
i: ℕ
i 
hi: i < length L
hi).
length: {α : Type ?u.15624} → List α → ℕ
length) :
    
nthLe: {α : Type ?u.15633} → (l : List α) → (n : ℕ) → n < length l → α
nthLe 
L: List (List α)
L.
join: {α : Type ?u.15635} → List (List α) → List α
join (((
L: List (List α)
L.
map: {α : Type ?u.15644} → {β : Type ?u.15643} → (α → β) → List α → List β
map 
length: {α : Type ?u.15651} → List α → ℕ
length).
take: {α : Type ?u.15656} → ℕ → List α → List α
take 
i: ℕ
i).
sum: {α : Type ?u.15662} → [inst : Add α] → [inst : Zero α] → List α → α
sum + 
j: ℕ
j) (
sum_take_map_length_lt2: ∀ {α : Type ?u.15730} (L : List (List α)) {i j : ℕ} (hi : i < length L),
  j < length (nthLe L i hi) → sum (take i (map length L)) + j < length (join L)
sum_take_map_length_lt2 
L: List (List α)
L 
hi: i < length L
hi 
hj: j < length (nthLe L i hi)
hj) =
      
nthLe: {α : Type ?u.15752} → (l : List α) → (n : ℕ) → n < length l → α
nthLe (
nthLe: {α : Type ?u.15754} → (l : List α) → (n : ℕ) → n < length l → α
nthLe 
L: List (List α)
L 
i: ℕ
i 
hi: i < length L
hi) 
j: ℕ
j 
hj: j < length (nthLe L i hi)
hj := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.15596

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =   nthLe (nthLe L i hi) j hjhave := 
nthLe_take: ∀ {α : Type ?u.15768} (L : List α) {i j : ℕ} (hi : i < length L) (hj : i < j),
  nthLe L i hi = nthLe (take j L) i (_ : i < length (take j L))
nthLe_take 
L: List (List α)
L.
join: {α : Type ?u.15770} → List (List α) → List α
join (
sum_take_map_length_lt2: ∀ {α : Type ?u.15778} (L : List (List α)) {i j : ℕ} (hi : i < length L),
  j < length (nthLe L i hi) → sum (take i (map length L)) + j < length (join L)
sum_take_map_length_lt2 
L: List (List α)
L 
hi: i < length L
hi 
hj: j < length (nthLe L i hi)
hj) (
sum_take_map_length_lt1: ∀ {α : Type ?u.15783} (L : List (List α)) {i j : ℕ} (hi : i < length L),
  j < length (nthLe L i hi) → sum (take i (map length L)) + j < sum (take (i + 1) (map length L))
sum_take_map_length_lt1 
L: List (List α)
L 
hi: i < length L
hi 
hj: j < length (nthLe L i hi)
hj)
α: Type u_1

β: Type ?u.15596

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

this: nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =   nthLe (take (sum (take (i + 1) (map length L))) (join L)) (sum (take i (map length L)) + j)
    (_ : sum (take i (map length L)) + j < length (take (sum (take (i + 1) (map length L))) (join L)))

nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =   nthLe (nthLe L i hi) j hj
  
α: Type u_1

β: Type ?u.15596

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =   nthLe (nthLe L i hi) j hjrw [
α: Type u_1

β: Type ?u.15596

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

this: nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =   nthLe (take (sum (take (i + 1) (map length L))) (join L)) (sum (take i (map length L)) + j)
    (_ : sum (take i (map length L)) + j < length (take (sum (take (i + 1) (map length L))) (join L)))

nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =   nthLe (nthLe L i hi) j hj
this: ?m.15767
this,
α: Type u_1

β: Type ?u.15596

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

this: nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =   nthLe (take (sum (take (i + 1) (map length L))) (join L)) (sum (take i (map length L)) + j)
    (_ : sum (take i (map length L)) + j < length (take (sum (take (i + 1) (map length L))) (join L)))

nthLe (take (sum (take (i + 1) (map length L))) (join L)) (sum (take i (map length L)) + j)
    (_ : sum (take i (map length L)) + j < length (take (sum (take (i + 1) (map length L))) (join L))) =   nthLe (nthLe L i hi) j hj 
α: Type u_1

β: Type ?u.15596

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

this: nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =   nthLe (take (sum (take (i + 1) (map length L))) (join L)) (sum (take i (map length L)) + j)
    (_ : sum (take i (map length L)) + j < length (take (sum (take (i + 1) (map length L))) (join L)))

nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =   nthLe (nthLe L i hi) j hj
nthLe_drop: ∀ {α : Type ?u.15806} (L : List α) {i j : ℕ} (h : i + j < length L),
  nthLe L (i + j) h = nthLe (drop i L) j (_ : j < length (drop i L))
nthLe_drop,
α: Type u_1

β: Type ?u.15596

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

this: nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =   nthLe (take (sum (take (i + 1) (map length L))) (join L)) (sum (take i (map length L)) + j)
    (_ : sum (take i (map length L)) + j < length (take (sum (take (i + 1) (map length L))) (join L)))

nthLe (drop (sum (take i (map length L))) (take (sum (take (i + 1) (map length L))) (join L))) j
    (_ : j < length (drop (sum (take i (map length L))) (take (sum (take (i + 1) (map length L))) (join L)))) =   nthLe (nthLe L i hi) j hj 
α: Type u_1

β: Type ?u.15596

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

this: nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =   nthLe (take (sum (take (i + 1) (map length L))) (join L)) (sum (take i (map length L)) + j)
    (_ : sum (take i (map length L)) + j < length (take (sum (take (i + 1) (map length L))) (join L)))

nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =   nthLe (nthLe L i hi) j hj
nthLe_of_eq: ∀ {α : Type ?u.15831} {L L' : List α} (h : L = L') {i : ℕ} (hi : i < length L),
  nthLe L i hi = nthLe L' i (_ : i < length L')
nthLe_of_eq (
drop_take_succ_join_eq_nthLe: ∀ {α : Type ?u.15835} (L : List (List α)) {i : ℕ} (hi : i < length L),
  drop (sum (take i (map length L))) (take (sum (take (i + 1) (map length L))) (join L)) = nthLe L i hi
drop_take_succ_join_eq_nthLe 
L: List (List α)
L 
hi: i < length L
hi)
α: Type u_1

β: Type ?u.15596

L: List (List α)

i, j: ℕ

hi: i < length L

hj: j < length (nthLe L i hi)

this: nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =   nthLe (take (sum (take (i + 1) (map length L))) (join L)) (sum (take i (map length L)) + j)
    (_ : sum (take i (map length L)) + j < length (take (sum (take (i + 1) (map length L))) (join L)))

nthLe (nthLe L i hi) j (_ : j < length (nthLe L i hi)) = nthLe (nthLe L i hi) j hj]
Goals accomplished! 🐙
#align list.nth_le_join 
List.nthLe_join: ∀ {α : Type u_1} (L : List (List α)) {i j : ℕ} (hi : i < length L) (hj : j < length (nthLe L i hi)),
  nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =     nthLe (nthLe L i hi) j hj
List.nthLe_join

/-- Two lists of sublists are equal iff their joins coincide, as well as the lengths of the
sublists. -/
theorem 
eq_iff_join_eq: ∀ (L L' : List (List α)), L = L' ↔ join L = join L' ∧ map length L = map length L'
eq_iff_join_eq (
L: List (List α)
L 
L': List (List α)
L' : 
List: Type ?u.15923 → Type ?u.15923
List (
List: Type ?u.15920 → Type ?u.15920
List 
α: Type ?u.15913
α)) :
    
L: List (List α)
L = 
L': List (List α)
L' ↔ 
L: List (List α)
L.
join: {α : Type ?u.15931} → List (List α) → List α
join = 
L': List (List α)
L'.
join: {α : Type ?u.15935} → List (List α) → List α
join ∧ 
map: {α : Type ?u.15942} → {β : Type ?u.15941} → (α → β) → List α → List β
map 
length: {α : Type ?u.15945} → List α → ℕ
length 
L: List (List α)
L = 
map: {α : Type ?u.15952} → {β : Type ?u.15951} → (α → β) → List α → List β
map 
length: {α : Type ?u.15955} → List α → ℕ
length 
L': List (List α)
L' := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

L = L' ↔ join L = join L' ∧ map length L = map length L'refine' ⟨fun 
H: ?m.15977
H => 
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

L = L' ↔ join L = join L' ∧ map length L = map length L'by
Goals accomplished! 🐙 
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

H: L = L'

join L = join L' ∧ map length L = map length L'simp [
H: L = L'
H]
Goals accomplished! 🐙, 
_: ?m.15973 → ?m.15972
_⟩
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join L = join L' ∧ map length L = map length L' → L = L'
  
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

L = L' ↔ join L = join L' ∧ map length L = map length L'rintro 
⟨join_eq, length_eq⟩: ?m.15973
⟨
join_eq: join L = join L'
join_eq
⟨join_eq, length_eq⟩: ?m.15973
, 
length_eq: map length L = map length L'
length_eq
⟨join_eq, length_eq⟩: ?m.15973
⟩
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

intro
L = L'
  
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

L = L' ↔ join L = join L' ∧ map length L = map length L'apply 
ext_get: ∀ {α : Type ?u.16104} {l₁ l₂ : List α},
  length l₁ = length l₂ →
    (∀ (n : ℕ) (h₁ : n < length l₁) (h₂ : n < length l₂),
        get l₁ { val := n, isLt := h₁ } = get l₂ { val := n, isLt := h₂ }) →
      l₁ = l₂
ext_get
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

intro.hl
length L = length L'
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

intro.h
∀ (n : ℕ) (h₁ : n < length L) (h₂ : n < length L'), get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }
  
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

L = L' ↔ join L = join L' ∧ map length L = map length L'·
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

intro.hl
length L = length L' 
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

intro.hl
length L = length L'
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

intro.h
∀ (n : ℕ) (h₁ : n < length L) (h₂ : n < length L'), get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }have : 
length: {α : Type ?u.16121} → List α → ℕ
length (
map: {α : Type ?u.16124} → {β : Type ?u.16123} → (α → β) → List α → List β
map 
length: {α : Type ?u.16128} → List α → ℕ
length 
L: List (List α)
L) = 
length: {α : Type ?u.16135} → List α → ℕ
length (
map: {α : Type ?u.16138} → {β : Type ?u.16137} → (α → β) → List α → List β
map 
length: {α : Type ?u.16142} → List α → ℕ
length 
L': List (List α)
L') := 
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

intro.hl
length L = length L'by
Goals accomplished! 🐙 
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

length (map length L) = length (map length L')rw [
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

length (map length L) = length (map length L')
length_eq: map length L = map length L'
length_eq
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

length (map length L') = length (map length L')]
Goals accomplished! 🐙
    
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

intro.hl
length L = length L'simpa using 
this: length (map length L) = length (map length L')
this
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

L = L' ↔ join L = join L' ∧ map length L = map length L'·
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

intro.h
∀ (n : ℕ) (h₁ : n < length L) (h₂ : n < length L'), get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ } 
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

intro.h
∀ (n : ℕ) (h₁ : n < length L) (h₂ : n < length L'), get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }intro 
n: ℕ
n 
h₁: n < length ?l₁
h₁ 
h₂: n < length ?l₂
h₂
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

n: ℕ

h₁: n < length L

h₂: n < length L'

intro.h
get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }
    
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

intro.h
∀ (n : ℕ) (h₁ : n < length L) (h₂ : n < length L'), get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }rw [
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

n: ℕ

h₁: n < length L

h₂: n < length L'

intro.h
get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }← 
drop_take_succ_join_eq_get: ∀ {α : Type ?u.16300} (L : List (List α)) (i : Fin (length L)),
  drop (sum (take (↑i) (map length L))) (take (sum (take (↑i + 1) (map length L))) (join L)) = get L i
drop_take_succ_join_eq_get,
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

n: ℕ

h₁: n < length L

h₂: n < length L'

intro.h
drop (sum (take (↑{ val := n, isLt := h₁ }) (map length L)))
    (take (sum (take (↑{ val := n, isLt := h₁ } + 1) (map length L))) (join L)) =   get L' { val := n, isLt := h₂ } 
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

n: ℕ

h₁: n < length L

h₂: n < length L'

intro.h
get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }← 
drop_take_succ_join_eq_get: ∀ {α : Type ?u.16315} (L : List (List α)) (i : Fin (length L)),
  drop (sum (take (↑i) (map length L))) (take (sum (take (↑i + 1) (map length L))) (join L)) = get L i
drop_take_succ_join_eq_get,
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

n: ℕ

h₁: n < length L

h₂: n < length L'

intro.h
drop (sum (take (↑{ val := n, isLt := h₁ }) (map length L)))
    (take (sum (take (↑{ val := n, isLt := h₁ } + 1) (map length L))) (join L)) =   drop (sum (take (↑{ val := n, isLt := h₂ }) (map length L')))
    (take (sum (take (↑{ val := n, isLt := h₂ } + 1) (map length L'))) (join L')) 
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

n: ℕ

h₁: n < length L

h₂: n < length L'

intro.h
get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }
join_eq: join L = join L'
join_eq,
α: Type u_1

β: Type ?u.15916

L, L': List (List α)

join_eq: join L = join L'

length_eq: map length L = map length L'

n: ℕ

h₁: n < length L

h₂: n < length L'

intro.h
drop (sum (take (↑{ val := n, isLt := h₁ }) (map length L)))
    (take (sum (take (↑{ val := n, isLt := h₁ } + 1) (map length L))) (join L')) =   drop (sum (take (↑{ val :=