[GOAL]
α : Type u_1
β : Type u_2
l : List α
⊢ join [l] = l
[PROOFSTEP]
rw [join, join, append_nil]
[GOAL]
α : Type u_1
β : Type u_2
l : List α
L : List (List α)
⊢ join (l :: L) = [] ↔ ∀ (l_1 : List α), l_1 ∈ l :: L → l_1 = []
[PROOFSTEP]
simp only [join, append_eq_nil, join_eq_nil, forall_mem_cons]
[GOAL]
α : Type u_1
β : Type u_2
L₁ L₂ : List (List α)
⊢ join (L₁ ++ L₂) = join L₁ ++ join L₂
[PROOFSTEP]
induction L₁
[GOAL]
case nil
α : Type u_1
β : Type u_2
L₂ : List (List α)
⊢ join ([] ++ L₂) = join [] ++ join L₂
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
L₂ : List (List α)
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : join (tail✝ ++ L₂) = join tail✝ ++ join L₂
⊢ join (head✝ :: tail✝ ++ L₂) = join (head✝ :: tail✝) ++ join L₂
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
l : List α
⊢ join (concat L l) = join L ++ l
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidablePred fun l => isEmpty l = false
L : List (List α)
⊢ join (filter (fun l => decide (isEmpty l = false)) ([] :: L)) = join ([] :: L)
[PROOFSTEP]
simp [join_filter_isEmpty_eq_false (L := L), isEmpty_iff_eq_nil]
[GOAL]
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
have cons_not_empty : isEmpty (a :: l) = false := rfl
[GOAL]
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
simp [join_filter_isEmpty_eq_false (L := L), cons_not_empty]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidablePred fun l => l ≠ []
L : List (List α)
⊢ join (filter (fun l => decide (l ≠ [])) L) = join L
[PROOFSTEP]
simp [join_filter_isEmpty_eq_false, ← isEmpty_iff_eq_nil]
[GOAL]
α : Type u_1
β : Type u_2
l : List (List (List α))
⊢ join (join l) = join (map join l)
[PROOFSTEP]
induction l
[GOAL]
case nil
α : Type u_1
β : Type u_2
⊢ join (join []) = join (map join [])
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u_1
β : Type u_2
head✝ : List (List α)
tail✝ : List (List (List α))
tail_ih✝ : join (join tail✝) = join (map join tail✝)
⊢ join (join (head✝ :: tail✝)) = join (map join (head✝ :: tail✝))
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
⊢ length (join L) = sum (map length L)
[PROOFSTEP]
induction L <;> [rfl; simp only [*, join, map, sum_cons, length_append]]
[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
⊢ length (join L) = sum (map length L)
[PROOFSTEP]
induction L
[GOAL]
case nil
α : Type u_1
β : Type u_2
⊢ length (join []) = sum (map length [])
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : length (join tail✝) = sum (map length tail✝)
⊢ length (join (head✝ :: tail✝)) = sum (map length (head✝ :: tail✝))
[PROOFSTEP]
simp only [*, join, map, sum_cons, length_append]
[GOAL]
α : Type u_1
β : Type u_2
l : List α
f : α → List β
⊢ length (List.bind l f) = sum (map (length ∘ f) l)
[PROOFSTEP]
rw [List.bind, length_join, map_map]
[GOAL]
α : 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 = []
[PROOFSTEP]
simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
i : ℕ
⊢ take (sum (take i (map length L))) (join L) = join (take i L)
[PROOFSTEP]
induction L generalizing i
[GOAL]
case nil
α : Type u_1
β : Type u_2
i : ℕ
⊢ take (sum (take i (map length []))) (join []) = join (take i [])
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)
i : ℕ
⊢ take (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (take i (head✝ :: tail✝))
[PROOFSTEP]
cases i
[GOAL]
case cons.zero
α : Type u_1
β : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)
⊢ take (sum (take Nat.zero (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) =
    join (take Nat.zero (head✝ :: tail✝))
[PROOFSTEP]
simp [take_append, *]
[GOAL]
case cons.succ
α : Type u_1
β : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (sum (take i (map length tail✝))) (join tail✝) = join (take i tail✝)
n✝ : ℕ
⊢ take (sum (take (Nat.succ n✝) (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) =
    join (take (Nat.succ n✝) (head✝ :: tail✝))
[PROOFSTEP]
simp [take_append, *]
[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
i : ℕ
⊢ drop (sum (take i (map length L))) (join L) = join (drop i L)
[PROOFSTEP]
induction L generalizing i
[GOAL]
case nil
α : Type u_1
β : Type u_2
i : ℕ
⊢ drop (sum (take i (map length []))) (join []) = join (drop i [])
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)
i : ℕ
⊢ drop (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (drop i (head✝ :: tail✝))
[PROOFSTEP]
cases i
[GOAL]
case cons.zero
α : Type u_1
β : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)
⊢ drop (sum (take Nat.zero (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) =
    join (drop Nat.zero (head✝ :: tail✝))
[PROOFSTEP]
simp [drop_append, *]
[GOAL]
case cons.succ
α : Type u_1
β : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)
n✝ : ℕ
⊢ drop (sum (take (Nat.succ n✝) (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) =
    join (drop (Nat.succ n✝) (head✝ :: tail✝))
[PROOFSTEP]
simp [drop_append, *]
[GOAL]
α : Type u_1
β : Type u_2
L : List α
i : Fin (length L)
⊢ drop (↑i) (take (↑i + 1) L) = [get L i]
[PROOFSTEP]
induction' L with head tail ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
L : List α
i✝ : Fin (length L)
i : Fin (length [])
⊢ drop (↑i) (take (↑i + 1) []) = [get [] i]
[PROOFSTEP]
exact (Nat.not_succ_le_zero i i.isLt).elim
[GOAL]
case cons
α : Type u_1
β : Type u_2
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))
⊢ drop (↑i) (take (↑i + 1) (head :: tail)) = [get (head :: tail) i]
[PROOFSTEP]
rcases i with ⟨_ | i, hi⟩
[GOAL]
case cons.mk.zero
α : Type u_1
β : Type u_2
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)
⊢ drop (↑{ val := Nat.zero, isLt := hi }) (take (↑{ val := Nat.zero, isLt := hi } + 1) (head :: tail)) =
    [get (head :: tail) { val := Nat.zero, isLt := hi }]
[PROOFSTEP]
simp
[GOAL]
case cons.mk.succ
α : Type u_1
β : Type u_2
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)
⊢ 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 }]
[PROOFSTEP]
simpa using ih ⟨i, Nat.lt_of_succ_lt_succ hi⟩
[GOAL]
α : Type u_1
β : Type u_2
L : List α
i : ℕ
hi : i < length L
⊢ drop i (take (i + 1) L) = [nthLe L i hi]
[PROOFSTEP]
induction' L with head tail generalizing i
[GOAL]
case nil
α : Type u_1
β : Type u_2
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
i : ℕ
hi : i < length []
⊢ drop i (take (i + 1) []) = [nthLe [] i hi]
[PROOFSTEP]
simp only [length] at hi
[GOAL]
case nil
α : Type u_1
β : Type u_2
L : List α
i✝ : ℕ
hi✝ : i✝ < length L
i : ℕ
hi : i < 0
⊢ drop i (take (i + 1) []) = [nthLe [] i hi]
[PROOFSTEP]
exact (Nat.not_succ_le_zero i hi).elim
[GOAL]
case cons
α : Type u_1
β : Type u_2
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)
⊢ drop i (take (i + 1) (head :: tail)) = [nthLe (head :: tail) i hi]
[PROOFSTEP]
cases' i with i hi
[GOAL]
case cons.zero
α : Type u_1
β : Type u_2
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)
⊢ drop Nat.zero (take (Nat.zero + 1) (head :: tail)) = [nthLe (head :: tail) Nat.zero hi]
[PROOFSTEP]
simp
[GOAL]
case cons.zero
α : Type u_1
β : Type u_2
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)
⊢ head = nthLe (head :: tail) 0 hi
[PROOFSTEP]
rfl
[GOAL]
case cons.succ
α : Type u_1
β : Type u_2
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)
⊢ drop (Nat.succ i) (take (Nat.succ i + 1) (head :: tail)) = [nthLe (head :: tail) (Nat.succ i) hi]
[PROOFSTEP]
have : i < tail.length := by
  simp at hi
  exact Nat.lt_of_succ_lt_succ hi
[GOAL]
α : Type u_1
β : Type u_2
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 tail
[PROOFSTEP]
simp at hi
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact Nat.lt_of_succ_lt_succ hi
[GOAL]
case cons.succ
α : Type u_1
β : Type u_2
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
⊢ drop (Nat.succ i) (take (Nat.succ i + 1) (head :: tail)) = [nthLe (head :: tail) (Nat.succ i) hi]
[PROOFSTEP]
simp [*]
[GOAL]
case cons.succ
α : Type u_1
β : Type u_2
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
⊢ nthLe tail i (_ : i < length tail) = nthLe (head :: tail) (Nat.succ i) hi
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have : (L.map length).take i = ((L.take (i + 1)).map length).take i := by simp [map_take, take_take]
[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
i : Fin (length L)
⊢ take (↑i) (map length L) = take (↑i) (map length (take (↑i + 1) L))
[PROOFSTEP]
simp [map_take, take_take]
[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
i : Fin (length L)
this : take (↑i) (map length L) = take (↑i) (map length (take (↑i + 1) L))
⊢ drop (sum (take (↑i) (map length L))) (take (sum (take (↑i + 1) (map length L))) (join L)) = get L i
[PROOFSTEP]
simp only [this, length_map, take_sum_join, drop_sum_join, drop_take_succ_eq_cons_get, join, append_nil]
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have : (L.map length).take i = ((L.take (i + 1)).map length).take i := by simp [map_take, take_take]
[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
i : ℕ
hi : i < length L
⊢ take i (map length L) = take i (map length (take (i + 1) L))
[PROOFSTEP]
simp [map_take, take_take]
[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
i : ℕ
hi : i < length L
this : take i (map length L) = take i (map length (take (i + 1) L))
⊢ drop (sum (take i (map length L))) (take (sum (take (i + 1) (map length L))) (join L)) = nthLe L i hi
[PROOFSTEP]
simp [take_sum_join, this, drop_sum_join, drop_take_succ_eq_cons_nthLe _ hi]
[GOAL]
α : Type u_1
β : Type u_2
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))
[PROOFSTEP]
simp [hi, sum_take_succ, hj]
[GOAL]
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
convert lt_of_lt_of_le (sum_take_map_length_lt1 L hi hj) (monotone_sum_take _ hi)
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
L : List (List α)
i j : ℕ
hi : i < length L
hj : j < length (nthLe L i hi)
⊢ length (join L) = (fun i => sum (take i (map length L))) (length L)
[PROOFSTEP]
have : L.length = (L.map length).length := by simp
[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
i j : ℕ
hi : i < length L
hj : j < length (nthLe L i hi)
⊢ length L = length (map length L)
[PROOFSTEP]
simp
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
L : List (List α)
i j : ℕ
hi : i < length L
hj : j < length (nthLe L i hi)
this : length L = length (map length L)
⊢ length (join L) = (fun i => sum (take i (map length L))) (length L)
[PROOFSTEP]
simp [this, -length_map]
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have := nthLe_take L.join (sum_take_map_length_lt2 L hi hj) (sum_take_map_length_lt1 L hi hj)
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [this, nthLe_drop, nthLe_of_eq (drop_take_succ_join_eq_nthLe L hi)]
[GOAL]
α : Type u_1
β : Type u_2
L L' : List (List α)
⊢ L = L' ↔ join L = join L' ∧ map length L = map length L'
[PROOFSTEP]
refine' ⟨fun H => by simp [H], _⟩
[GOAL]
α : Type u_1
β : Type u_2
L L' : List (List α)
H : L = L'
⊢ join L = join L' ∧ map length L = map length L'
[PROOFSTEP]
simp [H]
[GOAL]
α : Type u_1
β : Type u_2
L L' : List (List α)
⊢ join L = join L' ∧ map length L = map length L' → L = L'
[PROOFSTEP]
rintro ⟨join_eq, length_eq⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
L L' : List (List α)
join_eq : join L = join L'
length_eq : map length L = map length L'
⊢ L = L'
[PROOFSTEP]
apply ext_get
[GOAL]
case intro.hl
α : Type u_1
β : Type u_2
L L' : List (List α)
join_eq : join L = join L'
length_eq : map length L = map length L'
⊢ length L = length L'
[PROOFSTEP]
have : length (map length L) = length (map length L') := by rw [length_eq]
[GOAL]
α : Type u_1
β : Type u_2
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')
[PROOFSTEP]
rw [length_eq]
[GOAL]
case intro.hl
α : Type u_1
β : Type u_2
L L' : List (List α)
join_eq : join L = join L'
length_eq : map length L = map length L'
this : length (map length L) = length (map length L')
⊢ length L = length L'
[PROOFSTEP]
simpa using this
[GOAL]
case intro.h
α : Type u_1
β : Type u_2
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'), get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }
[PROOFSTEP]
intro n h₁ h₂
[GOAL]
case intro.h
α : Type u_1
β : Type u_2
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'
⊢ get L { val := n, isLt := h₁ } = get L' { val := n, isLt := h₂ }
[PROOFSTEP]
rw [← drop_take_succ_join_eq_get, ← drop_take_succ_join_eq_get, join_eq, length_eq]
[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
h : L ≠ []
⊢ join (drop (length L - 1) L) = getLast L h
[PROOFSTEP]
induction L using List.reverseRecOn
[GOAL]
case H0
α : Type u_1
β : Type u_2
h : [] ≠ []
⊢ join (drop (length [] - 1) []) = getLast [] h
[PROOFSTEP]
cases h rfl
[GOAL]
case H1
α : Type u_1
β : Type u_2
l✝ : List (List α)
a✝¹ : List α
a✝ : ∀ (h : l✝ ≠ []), join (drop (length l✝ - 1) l✝) = getLast l✝ h
h : l✝ ++ [a✝¹] ≠ []
⊢ join (drop (length (l✝ ++ [a✝¹]) - 1) (l✝ ++ [a✝¹])) = getLast (l✝ ++ [a✝¹]) h
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
x : List α
⊢ x ++ join (map (fun l => l ++ x) L) = join (map (fun l => x ++ l) L) ++ x
[PROOFSTEP]
induction' L with _ _ ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
x : List α
⊢ x ++ join (map (fun l => l ++ x) []) = join (map (fun l => x ++ l) []) ++ x
[PROOFSTEP]
rw [map_nil, join, append_nil, map_nil, join, nil_append]
[GOAL]
case cons
α : Type u_1
β : Type u_2
x head✝ : List α
tail✝ : List (List α)
ih : x ++ join (map (fun l => l ++ x) tail✝) = join (map (fun l => x ++ l) tail✝) ++ x
⊢ x ++ join (map (fun l => l ++ x) (head✝ :: tail✝)) = join (map (fun l => x ++ l) (head✝ :: tail✝)) ++ x
[PROOFSTEP]
rw [map_cons, join, map_cons, join, append_assoc, ih, append_assoc, append_assoc]
[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
⊢ reverse (join L) = join (reverse (map reverse L))
[PROOFSTEP]
induction' L with _ _ ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
⊢ reverse (join []) = join (reverse (map reverse []))
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
head✝ : List α
tail✝ : List (List α)
ih : reverse (join tail✝) = join (reverse (map reverse tail✝))
⊢ reverse (join (head✝ :: tail✝)) = join (reverse (map reverse (head✝ :: tail✝)))
[PROOFSTEP]
rw [join, reverse_append, ih, map_cons, reverse_cons', join_concat]
[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
⊢ join (reverse L) = reverse (join (map reverse L))
[PROOFSTEP]
simpa [reverse_reverse, map_reverse] using congr_arg List.reverse (reverse_join L.reverse)


[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
⊢ α ≃ Fin (Nat.card α)
[PROOFSTEP]
have := (Finite.exists_equiv_fin α).choose_spec.some
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
this : α ≃ Fin (Exists.choose (_ : ∃ n, Nonempty (α ≃ Fin n)))
⊢ α ≃ Fin (Nat.card α)
[PROOFSTEP]
rwa [Nat.card_eq_of_equiv_fin this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
n : ℕ
h : Nat.card α = n
⊢ α ≃ Fin n
[PROOFSTEP]
subst h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ α ≃ Fin (Nat.card α)
[PROOFSTEP]
apply Finite.equivFin
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0
[PROOFSTEP]
cases finite_or_infinite α
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
h✝ : Finite α
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0
[PROOFSTEP]
letI := Fintype.ofFinite α
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
h✝ : Finite α
this : Fintype α := Fintype.ofFinite α
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0
[PROOFSTEP]
simp only [*, Nat.card_eq_fintype_card, dif_pos]
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
h✝ : Infinite α
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0
[PROOFSTEP]
simp only [*, card_eq_zero_of_infinite, not_finite_iff_infinite.mpr, dite_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ 0 < Nat.card α ↔ Nonempty α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
this : Fintype α
⊢ 0 < Nat.card α ↔ Nonempty α
[PROOFSTEP]
rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
[PROOFSTEP]
haveI := Fintype.ofFinite β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, Fintype.card_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, Fintype.card_le_one_iff_subsingleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ 1 < Nat.card α ↔ Nontrivial α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
this : Fintype α
⊢ 1 < Nat.card α ↔ Nontrivial α
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, Fintype.one_lt_card_iff_nontrivial]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ Nat.card (Option α) = Nat.card α + 1
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (Option α) = Nat.card α + 1
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, Fintype.card_option]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite β
f : α → β
hf : Function.Injective f
⊢ Nat.card α ≤ Nat.card β
[PROOFSTEP]
haveI := Fintype.ofFinite β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite β
f : α → β
hf : Function.Injective f
this : Fintype β
⊢ Nat.card α ≤ Nat.card β
[PROOFSTEP]
haveI := Fintype.ofInjective f hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite β
f : α → β
hf : Function.Injective f
this✝ : Fintype β
this : Fintype α
⊢ Nat.card α ≤ Nat.card β
[PROOFSTEP]
simpa only [Nat.card_eq_fintype_card, ge_iff_le] using Fintype.card_le_of_injective f hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
⊢ Nat.card β ≤ Nat.card α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
this : Fintype α
⊢ Nat.card β ≤ Nat.card α
[PROOFSTEP]
haveI := Fintype.ofSurjective f hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
this✝ : Fintype α
this : Fintype β
⊢ Nat.card β ≤ Nat.card α
[PROOFSTEP]
simpa only [Nat.card_eq_fintype_card, ge_iff_le] using Fintype.card_le_of_surjective f hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ Nat.card α = 0 ↔ IsEmpty α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α = 0 ↔ IsEmpty α
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, Fintype.card_eq_zero_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
⊢ Nat.card α = 0
[PROOFSTEP]
cases finite_or_infinite β
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
⊢ Nat.card α = 0
[PROOFSTEP]
haveI := card_eq_zero_iff.mp h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
this : IsEmpty β
⊢ Nat.card α = 0
[PROOFSTEP]
haveI := Function.isEmpty f
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
this✝ : IsEmpty β
this : IsEmpty α
⊢ Nat.card α = 0
[PROOFSTEP]
exact Nat.card_of_isEmpty
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
⊢ Nat.card α = 0
[PROOFSTEP]
haveI := Infinite.of_surjective f hf
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
this : Infinite α
⊢ Nat.card α = 0
[PROOFSTEP]
exact Nat.card_eq_zero_of_infinite
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
[PROOFSTEP]
haveI := Fintype.ofFinite β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, Fintype.card_sum]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
p : α → Prop
⊢ Nat.card { x // p x } ≤ Nat.card α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
p : α → Prop
this : Fintype α
⊢ Nat.card { x // p x } ≤ Nat.card α
[PROOFSTEP]
simpa only [Nat.card_eq_fintype_card, ge_iff_le] using Fintype.card_subtype_le p
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
⊢ Nat.card { x // p x } < Nat.card α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
this : Fintype α
⊢ Nat.card { x // p x } < Nat.card α
[PROOFSTEP]
simpa only [Nat.card_eq_fintype_card, gt_iff_lt] using Fintype.card_subtype_lt hx
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
⊢ card α = ↑(Nat.card α)
[PROOFSTEP]
unfold PartENat.card
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
⊢ ↑Cardinal.toPartENat (Cardinal.mk α) = ↑(Nat.card α)
[PROOFSTEP]
apply symm
[GOAL]
case a
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
⊢ ↑(Nat.card α) = ↑Cardinal.toPartENat (Cardinal.mk α)
[PROOFSTEP]
rw [Cardinal.natCast_eq_toPartENat_iff]
[GOAL]
case a
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
⊢ ↑(Nat.card α) = Cardinal.mk α
[PROOFSTEP]
exact Finite.cast_card_eq_mk
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
[PROOFSTEP]
cases' _root_.finite_or_infinite (↥(s ∪ t)) with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
h : Finite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
[PROOFSTEP]
rw [finite_coe_iff, finite_union, ← finite_coe_iff, ← finite_coe_iff] at h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
h : Finite ↑s ∧ Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
[PROOFSTEP]
cases h
[GOAL]
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
[PROOFSTEP]
rw [← Cardinal.natCast_le, Nat.cast_add, Finite.cast_card_eq_mk, Finite.cast_card_eq_mk, Finite.cast_card_eq_mk]
[GOAL]
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Cardinal.mk ↑(s ∪ t) ≤ Cardinal.mk ↑s + Cardinal.mk ↑t
[PROOFSTEP]
exact Cardinal.mk_union_le s t
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
h : Infinite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
[PROOFSTEP]
exact Nat.card_eq_zero_of_infinite.trans_le (zero_le _)