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.
```/-
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] = ljoin_singleton (l: List αl : List: Type ?u.284 → Type ?u.284List α: Type ?u.278α) : [l: List αl].join: {α : Type ?u.293} → List (List α) → List αjoin = l: List αl := byGoals accomplished! 🐙 α: Type u_1β: Type ?u.281l: List αjoin [l] = lrw [α: Type u_1β: Type ?u.281l: List αjoin [l] = ljoin: {α : Type ?u.320} → List (List α) → List αjoin,α: Type u_1β: Type ?u.281l: List αl ++ join [] = l α: Type u_1β: Type ?u.281l: List αjoin [l] = ljoin: {α : Type ?u.327} → List (List α) → List αjoin,α: Type u_1β: Type ?u.281l: List αl ++ [] = l α: Type u_1β: Type ?u.281l: List αjoin [l] = lappend_nil: ∀ {α : Type ?u.328} (as : List α), as ++ [] = asappend_nilα: Type u_1β: Type ?u.281l: List αl = l]Goals accomplished! 🐙
#align list.join_singleton List.join_singleton: ∀ {α : Type u_1} (l : List α), join [l] = lList.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.361List (List: Type ?u.362 → Type ?u.362List α: Type ?u.354α)}, join: {α : Type ?u.366} → List (List α) → List αjoin L: List (List α)L = []: List ?m.371[] ↔ ∀ l: ?m.401l ∈ L: List (List α)L, l: ?m.401l = []: List ?m.433[]
| [] => iff_of_true: ∀ {a b : Prop}, a → b → (a ↔ b)iff_of_true rfl: ∀ {α : Sort ?u.488} {a : α}, a = arfl (forall_mem_nil: ∀ {α : Type ?u.503} (p : α → Prop) (x : α), x ∈ [] → p xforall_mem_nil _: ?m.504 → Prop_)
| l: List αl :: L: List (List α)L => byGoals accomplished! 🐙 α: Type u_1β: Type ?u.357l: 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 xforall_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.1003List (List: Type ?u.1000 → Type ?u.1000List α: 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₂ := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.996L₁, L₂: List (List α)join (L₁ ++ L₂) = join L₁ ++ join L₂induction L₁: List (List α)L₁α: Type u_1β: Type ?u.996L₂: List (List α)niljoin ([] ++ L₂) = join [] ++ join L₂α: Type u_1β: Type ?u.996L₂: List (List α)head✝: List αtail✝: List (List α)tail_ih✝: join (tail✝ ++ L₂) = join tail✝ ++ join L₂consjoin (head✝ :: tail✝ ++ L₂) = join (head✝ :: tail✝) ++ join L₂
α: Type u_1β: Type ?u.996L₁, L₂: List (List α)join (L₁ ++ L₂) = join L₁ ++ join L₂·α: Type u_1β: Type ?u.996L₂: List (List α)niljoin ([] ++ L₂) = join [] ++ join L₂ α: Type u_1β: Type ?u.996L₂: List (List α)niljoin ([] ++ L₂) = join [] ++ join L₂α: Type u_1β: Type ?u.996L₂: List (List α)head✝: List αtail✝: List (List α)tail_ih✝: join (tail✝ ++ L₂) = join tail✝ ++ join L₂consjoin (head✝ :: tail✝ ++ L₂) = join (head✝ :: tail✝) ++ join L₂rflGoals accomplished! 🐙
α: Type u_1β: Type ?u.996L₁, L₂: List (List α)join (L₁ ++ L₂) = join L₁ ++ join L₂·α: Type u_1β: Type ?u.996L₂: List (List α)head✝: List αtail✝: List (List α)tail_ih✝: join (tail✝ ++ L₂) = join tail✝ ++ join L₂consjoin (head✝ :: tail✝ ++ L₂) = join (head✝ :: tail✝) ++ join L₂ α: Type u_1β: Type ?u.996L₂: List (List α)head✝: List αtail✝: List (List α)tail_ih✝: join (tail✝ ++ L₂) = join tail✝ ++ join L₂consjoin (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 ++ ljoin_concat (L: List (List α)L : List: Type ?u.1309 → Type ?u.1309List (List: Type ?u.1310 → Type ?u.1310List α: Type ?u.1303α)) (l: List αl : List: Type ?u.1313 → Type ?u.1313List α: 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 := byGoals accomplished! 🐙 α: Type u_1β: Type ?u.1306L: List (List α)l: List αjoin (concat L l) = join L ++ lsimpGoals accomplished! 🐙
#align list.join_concat List.join_concat: ∀ {α : Type u_1} (L : List (List α)) (l : List α), join (concat L l) = join L ++ lList.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 Ljoin_filter_isEmpty_eq_false [DecidablePred: {α : Sort ?u.1510} → (α → Prop) → Sort (max1?u.1510)DecidablePred fun l: List αl : List: Type ?u.1513 → Type ?u.1513List α: Type ?u.1504α => l: List αl.isEmpty: {α : Type ?u.1516} → List α → BoolisEmpty = false: Boolfalse] :
∀ {L: List (List α)L : List: Type ?u.1530 → Type ?u.1530List (List: Type ?u.1531 → Type ?u.1531List α: 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.1544l => l: ?m.1544l.isEmpty: {α : Type ?u.1547} → List α → BoolisEmpty = false: Boolfalse) = L: List (List α)L.join: {α : Type ?u.1613} → List (List α) → List αjoin
| [] => rfl: ∀ {α : Sort ?u.1639} {a : α}, a = arfl
| [] :: L: List (List α)L => byGoals accomplished! 🐙
α: Type u_1β: Type ?u.1507inst✝: DecidablePred fun l => isEmpty l = falseL: 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 Ljoin_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 => byGoals accomplished! 🐙
α: Type u_1β: Type ?u.1507inst✝: DecidablePred fun l => isEmpty l = falsea: α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) = falsecons_not_empty : isEmpty: {α : Type ?u.2363} → List α → BoolisEmpty (a: αa :: l: List αl) = false: Boolfalse := rfl: ∀ {α : Sort ?u.2369} {a : α}, a = arflα: Type u_1β: Type ?u.1507inst✝: DecidablePred fun l => isEmpty l = falsea: αl: List αL: List (List α)cons_not_empty: isEmpty (a :: l) = falsejoin (filter (fun l => decide (isEmpty l = false)) ((a :: l) :: L)) = join ((a :: l) :: L)
α: Type u_1β: Type ?u.1507inst✝: DecidablePred fun l => isEmpty l = falsea: α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 Ljoin_filter_isEmpty_eq_false (L := L: List (List α)L), cons_not_empty: isEmpty (a :: l) = falsecons_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 LList.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 Ljoin_filter_ne_nil [DecidablePred: {α : Sort ?u.2832} → (α → Prop) → Sort (max1?u.2832)DecidablePred fun l: List αl : List: Type ?u.2835 → Type ?u.2835List α: Type ?u.2826α => l: List αl ≠ []: List ?m.2841[]] {L: List (List α)L : List: Type ?u.2849 → Type ?u.2849List (List: Type ?u.2850 → Type ?u.2850List α: 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.2863l => l: ?m.2863l ≠ []: List ?m.2868[]) = L: List (List α)L.join: {α : Type ?u.2925} → List (List α) → List αjoin := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.2829inst✝: 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 Ljoin_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 LList.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.3809List (List: Type ?u.3810 → Type ?u.3810List (List: Type ?u.3811 → Type ?u.3811List α: 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 := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.3806l: List (List (List α))join (join l) = join (map join l)induction l: List (List (List α))lα: Type u_1β: Type ?u.3806niljoin (join []) = join (map join [])α: Type u_1β: Type ?u.3806head✝: List (List α)tail✝: List (List (List α))tail_ih✝: join (join tail✝) = join (map join tail✝)consjoin (join (head✝ :: tail✝)) = join (map join (head✝ :: tail✝)) α: Type u_1β: Type ?u.3806l: List (List (List α))join (join l) = join (map join l)<;>α: Type u_1β: Type ?u.3806niljoin (join []) = join (map join [])α: Type u_1β: Type ?u.3806head✝: List (List α)tail✝: List (List (List α))tail_ih✝: join (join tail✝) = join (map join tail✝)consjoin (join (head✝ :: tail✝)) = join (map join (head✝ :: tail✝)) α: Type u_1β: Type ?u.3806l: 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.4051List (List: Type ?u.4052 → Type ?u.4052List α: 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) := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.4048L: List (List α)length (join L) = sum (map length L)induction L: List (List α)Lα: Type u_1β: Type ?u.4048nillength (join []) = sum (map length [])α: Type u_1β: Type ?u.4048head✝: List αtail✝: List (List α)tail_ih✝: length (join tail✝) = sum (map length tail✝)conslength (join (head✝ :: tail✝)) = sum (map length (head✝ :: tail✝)) <;> [α: Type u_1β: Type ?u.4048L: List (List α)length (join L) = sum (map length L)rflGoals accomplished! 🐙; α: Type u_1β: Type ?u.4048L: 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 lsum_cons, length_append: ∀ {α : Type ?u.4522} (as bs : List α), length (as ++ bs) = length as + length bslength_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.4752List α: Type ?u.4746α) (f: α → List βf : α: Type ?u.4746α → List: Type ?u.4757 → Type ?u.4757List β: 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) := byGoals accomplished! 🐙 α: Type u_1β: Type u_2l: List αf: α → List βlength (List.bind l f) = sum (map (length ∘ f) l)rw [α: Type u_1β: Type u_2l: 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_2l: List αf: α → List βlength (join (map f l)) = sum (map (length ∘ f) l) α: Type u_1β: Type u_2l: 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_2l: List αf: α → List βsum (map length (map f l)) = sum (map (length ∘ f) l) α: Type u_1β: Type u_2l: 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) lmap_mapα: Type u_1β: Type u_2l: 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.4947List α: Type ?u.4941α} {f: α → List βf : α: Type ?u.4941α → List: Type ?u.4952 → Type ?u.4952List β: 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.4998x ∈ l: List αl, f: α → List βf x: ?m.4998x = []: 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 <| byGoals accomplished! 🐙
α: Type u_1β: Type u_2l: 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 = bmem_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 → cand_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.5742List (List: Type ?u.5743 → Type ?u.5743List α: 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 := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.5739L: 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.5739i: ℕniltake (sum (take i (map length []))) (join []) = join (take i [])α: Type u_1β: Type ?u.5739head✝: List αtail✝: List (List α)tail_ih✝: ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)i: ℕconstake (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (take i (head✝ :: tail✝))
α: Type u_1β: Type ?u.5739L: List (List α)i: ℕtake (sum (take i (map length L))) (join L) = join (take i L)·α: Type u_1β: Type ?u.5739i: ℕniltake (sum (take i (map length []))) (join []) = join (take i []) α: Type u_1β: Type ?u.5739i: ℕniltake (sum (take i (map length []))) (join []) = join (take i [])α: Type u_1β: Type ?u.5739head✝: List αtail✝: List (List α)tail_ih✝: ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)i: ℕconstake (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (take i (head✝ :: tail✝))simpGoals 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.6453List (List: Type ?u.6454 → Type ?u.6454List α: 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 := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.6450L: 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.6450i: ℕnildrop (sum (take i (map length []))) (join []) = join (drop i [])α: Type u_1β: Type ?u.6450head✝: List αtail✝: List (List α)tail_ih✝: ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)i: ℕconsdrop (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (drop i (head✝ :: tail✝))
α: Type u_1β: Type ?u.6450L: List (List α)i: ℕdrop (sum (take i (map length L))) (join L) = join (drop i L)·α: Type u_1β: Type ?u.6450i: ℕnildrop (sum (take i (map length []))) (join []) = join (drop i []) α: Type u_1β: Type ?u.6450i: ℕnildrop (sum (take i (map length []))) (join []) = join (drop i [])α: Type u_1β: Type ?u.6450head✝: List αtail✝: List (List α)tail_ih✝: ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)i: ℕconsdrop (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (drop i (head✝ :: tail✝))simpGoals 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.7171List α: Type ?u.7165α) (i: Fin (length L)i : Fin: ℕ → TypeFin 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.71911)).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] := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.7168L: List αi: Fin (length L)drop (↑i) (take (↑i + 1) L) = [get L i]induction' L: List αL with head: ?m.7478head tail: List ?m.7478tail ih: ?m.7479 tailihα: Type u_1β: Type ?u.7168L: List αi✝: Fin (length L)i: Fin (length [])nildrop (↑i) (take (↑i + 1) []) = [get [] i]α: Type u_1β: Type ?u.7168L: 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))consdrop (↑i) (take (↑i + 1) (head :: tail)) = [get (head :: tail) i]
α: Type u_1β: Type ?u.7168L: List αi: Fin (length L)drop (↑i) (take (↑i + 1) L) = [get L i]·α: Type u_1β: Type ?u.7168L: List αi✝: Fin (length L)i: Fin (length [])nildrop (↑i) (take (↑i + 1) []) = [get [] i] α: Type u_1β: Type ?u.7168L: List αi✝: Fin (length L)i: Fin (length [])nildrop (↑i) (take (↑i + 1) []) = [get [] i]α: Type u_1β: Type ?u.7168L: 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))consdrop (↑i) (take (↑i + 1) (head :: tail)) = [get (head :: tail) i]exact (Nat.not_succ_le_zero: ∀ (n : ℕ), Nat.succ n ≤ 0 → FalseNat.not_succ_le_zero i: Fin (length [])i i: Fin (length [])i.isLt: ∀ {n : ℕ} (self : Fin n), ↑self < nisLt).elim: ∀ {C : Sort ?u.7591}, False → CelimGoals accomplished! 🐙
α: Type u_1β: Type ?u.7168L: List αi: Fin (length L)drop (↑i) (take (↑i + 1) L) = [get L i]·α: Type u_1β: Type ?u.7168L: 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.succdrop (↑{ 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.7168L: 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.succdrop (↑{ 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 tailih ⟨i: ℕi, Nat.lt_of_succ_lt_succ: ∀ {n m : ℕ}, Nat.succ n < Nat.succ m → n < mNat.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.8051List α: Type ?u.8045α) {i: ℕi : ℕ: Typeℕ} (hi: i < length Lhi : 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.80791)).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 Lhi] := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.8048L: List αi: ℕhi: i < length Ldrop i (take (i + 1) L) = [nthLe L i hi]induction' L: List αL with head: ?m.8177head tail: List ?m.8177tail generalizing i: ℕiα: Type u_1β: Type ?u.8048L: List αi✝: ℕhi✝: i✝ < length Li: ℕhi: i < length []nildrop i (take (i + 1) []) = [nthLe [] i hi]α: Type u_1β: Type ?u.8048L: List αi✝: ℕhi✝: i✝ < length Lhead: α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)consdrop i (take (i + 1) (head :: tail)) = [nthLe (head :: tail) i hi]
α: Type u_1β: Type ?u.8048L: List αi: ℕhi: i < length Ldrop i (take (i + 1) L) = [nthLe L i hi]·α: Type u_1β: Type ?u.8048L: List αi✝: ℕhi✝: i✝ < length Li: ℕhi: i < length []nildrop i (take (i + 1) []) = [nthLe [] i hi] α: Type u_1β: Type ?u.8048L: List αi✝: ℕhi✝: i✝ < length Li: ℕhi: i < length []nildrop i (take (i + 1) []) = [nthLe [] i hi]α: Type u_1β: Type ?u.8048L: List αi✝: ℕhi✝: i✝ < length Lhead: α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)consdrop 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.8048L: List αi✝: ℕhi✝: i✝ < length Li: ℕhi: i < 0nildrop i (take (i + 1) []) = [nthLe [] i hi]
α: Type u_1β: Type ?u.8048L: List αi✝: ℕhi✝: i✝ < length Li: ℕhi: i < length []nildrop i (take (i + 1) []) = [nthLe [] i hi]exact (Nat.not_succ_le_zero: ∀ (n : ℕ), Nat.succ n ≤ 0 → FalseNat.not_succ_le_zero i: ℕi hi: i < 0hi).elim: ∀ {C : Sort ?u.8494}, False → CelimGoals accomplished! 🐙
α: Type u_1β: Type ?u.8048L: List αi: ℕhi: i < length Ldrop i (take (i + 1) L) = [nthLe L i hi]cases' i: ℕi with i: ℕi hiα: Type u_1β: Type ?u.8048L: List αi: ℕhi✝: i < length Lhead: α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.zerodrop Nat.zero (take (Nat.zero + 1) (head :: tail)) = [nthLe (head :: tail) Nat.zero hi]α: Type u_1β: Type ?u.8048L: List αi✝: ℕhi✝: i✝ < length Lhead: α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.succdrop (Nat.succ i) (take (Nat.succ i + 1) (head :: tail)) = [nthLe (head :: tail) (Nat.succ i) hi]
α: Type u_1β: Type ?u.8048L: List αi: ℕhi✝: i < length Lhead: α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.zerodrop Nat.zero (take (Nat.zero + 1) (head :: tail)) = [nthLe (head :: tail) Nat.zero hi]rflGoals accomplished! 🐙
α: Type u_1β: Type ?u.8048L: List αi: ℕhi: i < length Ldrop i (take (i + 1) L) = [nthLe L i hi]have : i: ℕi < tail: List ?m.8177tail.length: {α : Type ?u.8729} → List α → ℕlength := α: Type u_1β: Type ?u.8048L: List αi✝: ℕhi✝: i✝ < length Lhead: α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.succdrop (Nat.succ i) (take (Nat.succ i + 1) (head :: tail)) = [nthLe (head :: tail) (Nat.succ i) hi]byGoals accomplished! 🐙
α: Type u_1β: Type ?u.8048L: List αi✝: ℕhi✝: i✝ < length Lhead: α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.8048L: List αi✝: ℕhi✝: i✝ < length Lhead: α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.8048L: List αi✝: ℕhi✝: i✝ < length Lhead: α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 < mNat.lt_of_succ_lt_succ hi: Nat.succ i < Nat.succ (length tail)hiGoals accomplished! 🐙
α: Type u_1β: Type ?u.8048L: List αi: ℕhi: i < length Ldrop i (take (i + 1) L) = [nthLe L i hi]simp [*]α: Type u_1β: Type ?u.8048L: List αi✝: ℕhi✝: i✝ < length Lhead: α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 tailcons.succnthLe tail i (_ : i < length tail) = nthLe (head :: tail) (Nat.succ i) hi
α: Type u_1β: Type ?u.8048L: List αi: ℕhi: i < length Ldrop i (take (i + 1) L) = [nthLe L i hi]rflGoals 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 idrop_take_succ_join_eq_get (L: List (List α)L : List: Type ?u.9240 → Type ?u.9240List (List: Type ?u.9241 → Type ?u.9241List α: Type ?u.9234α)) (i: Fin (length L)i : Fin: ℕ → TypeFin 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.92811)).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 := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.9237L: 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.97151)).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.9237L: 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 ibyGoals accomplished! 🐙
α: Type u_1β: Type ?u.9237L: 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) ltake_take]Goals accomplished! 🐙
α: Type u_1β: Type ?u.9237L: 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 idrop_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 hidrop_take_succ_join_eq_nthLe (L: List (List α)L : List: Type ?u.11185 → Type ?u.11185List (List: Type ?u.11186 → Type ?u.11186List α: Type ?u.11179α)) {i: ℕi : ℕ: Typeℕ} (hi: i < length Lhi : 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.112341)).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 Lhi := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.11182L: List (List α)i: ℕhi: i < length Ldrop (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.113971)).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.11182L: List (List α)i: ℕhi: i < length Ldrop (sum (take i (map length L))) (take (sum (take (i + 1) (map length L))) (join L)) = nthLe L i hibyGoals accomplished! 🐙
α: Type u_1β: Type ?u.11182L: List (List α)i: ℕhi: i < length Ltake 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) ltake_take]Goals accomplished! 🐙
α: Type u_1β: Type ?u.11182L: List (List α)i: ℕhi: i < length Ldrop (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 Lhi]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 hiList.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.12786List (List: Type ?u.12787 → Type ?u.12787List α: Type ?u.12780α)) {i: ℕi j: ℕj : ℕ: Typeℕ} (hi: i < length Lhi : 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 Lhi).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.128961)).sum: {α : Type ?u.12947} → [inst : Add α] → [inst : Zero α] → List α → αsum := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.12783L: List (List α)i, j: ℕhi: i < length Lhj: j < length (nthLe L i hi)sum (take i (map length L)) + j < sum (take (i + 1) (map length L))simp [hi: i < length Lhi, 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 psum_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.13933List (List: Type ?u.13934 → Type ?u.13934List α: Type ?u.13927α)) {i: ℕi j: ℕj : ℕ: Typeℕ} (hi: i < length Lhi : 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 Lhi).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 := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.13930L: List (List α)i, j: ℕhi: i < length Lhj: 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 < clt_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 Lhi 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 Lhi)α: Type u_1β: Type ?u.13930L: List (List α)i, j: ℕhi: i < length Lhj: j < length (nthLe L i hi)h.e'_4length (join L) = (fun i => sum (take i (map length L))) (length L)
α: Type u_1β: Type ?u.13930L: List (List α)i, j: ℕhi: i < length Lhj: 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.13930L: List (List α)i, j: ℕhi: i < length Lhj: j < length (nthLe L i hi)h.e'_4length (join L) = (fun i => sum (take i (map length L))) (length L)byGoals accomplished! 🐙 α: Type u_1β: Type ?u.13930L: List (List α)i, j: ℕhi: i < length Lhj: j < length (nthLe L i hi)length L = length (map length L)simpGoals accomplished! 🐙
α: Type u_1β: Type ?u.13930L: List (List α)i, j: ℕhi: i < length Lhj: 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 aslength_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 hjnthLe_join (L: List (List α)L : List: Type ?u.15599 → Type ?u.15599List (List: Type ?u.15600 → Type ?u.15600List α: Type ?u.15593α)) {i: ℕi j: ℕj : ℕ: Typeℕ} (hi: i < length Lhi : 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 Lhi).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 Lhi 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 Lhi) j: ℕj hj: j < length (nthLe L i hi)hj := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.15596L: List (List α)i, j: ℕhi: i < length Lhj: 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 Lhi 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 Lhi hj: j < length (nthLe L i hi)hj)α: Type u_1β: Type ?u.15596L: List (List α)i, j: ℕhi: i < length Lhj: 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.15596L: List (List α)i, j: ℕhi: i < length Lhj: 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.15596L: List (List α)i, j: ℕhi: i < length Lhj: 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 hjthis: ?m.15767this,α: Type u_1β: Type ?u.15596L: List (List α)i, j: ℕhi: i < length Lhj: 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.15596L: List (List α)i, j: ℕhi: i < length Lhj: 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 hjnthLe_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.15596L: List (List α)i, j: ℕhi: i < length Lhj: 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.15596L: List (List α)i, j: ℕhi: i < length Lhj: 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 hjnthLe_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 hidrop_take_succ_join_eq_nthLe L: List (List α)L hi: i < length Lhi)α: Type u_1β: Type ?u.15596L: List (List α)i, j: ℕhi: i < length Lhj: 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 hjList.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.15923List (List: Type ?u.15920 → Type ?u.15920List α: 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' := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.15916L, L': List (List α)L = L' ↔ join L = join L' ∧ map length L = map length L'refine' ⟨fun H: ?m.15977H => α: Type u_1β: Type ?u.15916L, L': List (List α)L = L' ↔ join L = join L' ∧ map length L = map length L'byGoals accomplished! 🐙 α: Type u_1β: Type ?u.15916L, 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.15916L, L': List (List α)join L = join L' ∧ map length L = map length L' → L = L'
α: Type u_1β: Type ?u.15916L, 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.15916L, L': List (List α)join_eq: join L = join L'length_eq: map length L = map length L'introL = L'
α: Type u_1β: Type ?u.15916L, 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.15916L, L': List (List α)join_eq: join L = join L'length_eq: map length L = map length L'intro.hllength L = length L'α: Type u_1β: Type ?u.15916L, 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.15916L, L': List (List α)L = L' ↔ join L = join L' ∧ map length L = map length L'·α: Type u_1β: Type ?u.15916L, L': List (List α)join_eq: join L = join L'length_eq: map length L = map length L'intro.hllength L = length L' α: Type u_1β: Type ?u.15916L, L': List (List α)join_eq: join L = join L'length_eq: map length L = map length L'intro.hllength L = length L'α: Type u_1β: Type ?u.15916L, 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.15916L, L': List (List α)join_eq: join L = join L'length_eq: map length L = map length L'intro.hllength L = length L'byGoals accomplished! 🐙 α: Type u_1β: Type ?u.15916L, 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.15916L, 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.15916L, 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.15916L, L': List (List α)join_eq: join L = join L'length_eq: map length L = map length L'intro.hllength L = length L'simpa using this: length (map length L) = length (map length L')thisGoals accomplished! 🐙
α: Type u_1β: Type ?u.15916L, L': List (List α)L = L' ↔ join L = join L' ∧ map length L = map length L'·α: Type u_1β: Type ?u.15916L, 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.15916L, 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.15916L, L': List (List α)join_eq: join L = join L'length_eq: map length L = map length L'n: ℕh₁: n < length Lh₂: n < length L'intro.hget L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }
α: Type u_1β: Type ?u.15916L, 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.15916L, L': List (List α)join_eq: join L = join L'length_eq: map length L = map length L'n: ℕh₁: n < length Lh₂: n < length L'intro.hget 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 idrop_take_succ_join_eq_get,α: Type u_1β: Type ?u.15916L, L': List (List α)join_eq: join L = join L'length_eq: map length L = map length L'n: ℕh₁: n < length Lh₂: n < length L'intro.hdrop (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.15916L, L': List (List α)join_eq: join L = join L'length_eq: map length L = map length L'n: ℕh₁: n < length Lh₂: n < length L'intro.hget 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 idrop_take_succ_join_eq_get,α: Type u_1β: Type ?u.15916L, L': List (List α)join_eq: join L = join L'length_eq: map length L = map length L'n: ℕh₁: n < length Lh₂: n < length L'intro.hdrop (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.15916L, L': List (List α)join_eq: join L = join L'length_eq: map length L = map length L'n: ℕh₁: n < length Lh₂: n < length L'intro.hget L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }join_eq: join L = join L'join_eq,α: Type u_1β: Type ?u.15916L, L': List (List α)join_eq: join L = join L'length_eq: map length L = map length L'n: ℕh₁: n < length Lh₂: n < length L'intro.hdrop (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 := ```