[GOAL]
α : Type u
β : Type v
φ : Type w
n : ℕ
h : List.length [] = succ n
⊢ α
[PROOFSTEP]
contradiction
[GOAL]
α : Type u
β : Type v
φ : Type w
n : ℕ
h : List.length [] = succ n
⊢ cons (head { val := [], property := h }) (tail { val := [], property := h }) = { val := [], property := h }
[PROOFSTEP]
contradiction
[GOAL]
α : Type u
β : Type v
φ : Type w
n : ℕ
l : List α
h : List.length l = n
i : Fin n
⊢ ↑i < List.length l
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : Type v
φ : Type w
n : ℕ
l : List α
h : List.length l = n
i : Fin n
⊢ ↑i < n
[PROOFSTEP]
exact i.2
[GOAL]
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
l₁ : List α
h₁ : List.length l₁ = n
l₂ : List α
h₂ : List.length l₂ = m
⊢ List.length (l₁ ++ l₂) = n + m
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type v
φ : Type w
n : ℕ
f : α → β
l : List α
h : List.length l = n
⊢ List.length (List.map f l) = n
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type v
φ : Type w
n : ℕ
f : α → β → φ
x : List α
property✝¹ : List.length x = n
y : List β
property✝ : List.length y = n
⊢ List.length (List.zipWith f x y) = n
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type v
φ : Type w
n i : ℕ
l : List α
p : List.length l = n
⊢ List.length (List.drop i l) = n - i
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type v
φ : Type w
n i : ℕ
l : List α
p : List.length l = n
⊢ List.length (List.take i l) = min i n
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type v
φ : Type w
n : ℕ
i : Fin n
l : List α
p : List.length l = n
⊢ List.length (List.removeNth l ↑i) = n - 1
[PROOFSTEP]
rw [l.length_removeNth]
[GOAL]
α : Type u
β : Type v
φ : Type w
n : ℕ
i : Fin n
l : List α
p : List.length l = n
⊢ List.length l - 1 = n - 1
[PROOFSTEP]
rw [p]
[GOAL]
α : Type u
β : Type v
φ : Type w
n : ℕ
i : Fin n
l : List α
p : List.length l = n
⊢ ↑i < List.length l
[PROOFSTEP]
rw [p]
[GOAL]
α : Type u
β : Type v
φ : Type w
n : ℕ
i : Fin n
l : List α
p : List.length l = n
⊢ ↑i < n
[PROOFSTEP]
exact i.2
[GOAL]
α : Type u
β : Type v
φ : Type w
n : ℕ
σ : Type
f : α → σ → σ × β
x : List α
px : List.length x = n
c : σ
res : σ × List β := List.mapAccumr f x c
⊢ List.length res.snd = n
[PROOFSTEP]
simp [*]
[GOAL]
α✝ : Type u
β✝ : Type v
φ✝ : Type w
n : ℕ
σ✝ α β σ φ : Type
f : α → β → σ → σ × φ
x : List α
px : List.length x = n
y : List β
py : List.length y = n
c : σ
res : σ × List φ := List.mapAccumr₂ f x y c
⊢ List.length res.snd = n
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type v
φ : Type w
n : ℕ
v : Vector α n
i : ℕ
fill : α
⊢ n - i + min n i = n
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
φ : Type w
n : ℕ
v : Vector α n
i : ℕ
fill : α
⊢ min n i + min (n - i) n = n
[PROOFSTEP]
by_cases h : i ≤ n
[GOAL]
case pos
α : Type u
β : Type v
φ : Type w
n : ℕ
v : Vector α n
i : ℕ
fill : α
h : i ≤ n
⊢ min n i + min (n - i) n = n
[PROOFSTEP]
have h₁ := Nat.sub_le n i
[GOAL]
case pos
α : Type u
β : Type v
φ : Type w
n : ℕ
v : Vector α n
i : ℕ
fill : α
h : i ≤ n
h₁ : n - i ≤ n
⊢ min n i + min (n - i) n = n
[PROOFSTEP]
rw [min_eq_right h]
[GOAL]
case pos
α : Type u
β : Type v
φ : Type w
n : ℕ
v : Vector α n
i : ℕ
fill : α
h : i ≤ n
h₁ : n - i ≤ n
⊢ i + min (n - i) n = n
[PROOFSTEP]
rw [min_eq_left h₁, ← add_tsub_assoc_of_le h, Nat.add_comm, add_tsub_cancel_right]
[GOAL]
case neg
α : Type u
β : Type v
φ : Type w
n : ℕ
v : Vector α n
i : ℕ
fill : α
h : ¬i ≤ n
⊢ min n i + min (n - i) n = n
[PROOFSTEP]
have h₁ := le_of_not_ge h
[GOAL]
case neg
α : Type u
β : Type v
φ : Type w
n : ℕ
v : Vector α n
i : ℕ
fill : α
h : ¬i ≤ n
h₁ : n ≤ i
⊢ min n i + min (n - i) n = n
[PROOFSTEP]
rw [min_eq_left h₁, tsub_eq_zero_iff_le.mpr h₁, zero_min, Nat.add_zero]
[GOAL]
α : Type u
β : Type v
φ : Type w
n : ℕ
a : α
v : Vector α n
⊢ toList (cons a v) = a :: toList v
[PROOFSTEP]
cases v
[GOAL]
case mk
α : Type u
β : Type v
φ : Type w
n : ℕ
a : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ toList (cons a { val := val✝, property := property✝ }) = a :: toList { val := val✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
v : Vector α n
w : Vector α m
⊢ toList (append v w) = toList v ++ toList w
[PROOFSTEP]
cases v
[GOAL]
case mk
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
w : Vector α m
val✝ : List α
property✝ : List.length val✝ = n
⊢ toList (append { val := val✝, property := property✝ } w) = toList { val := val✝, property := property✝ } ++ toList w
[PROOFSTEP]
cases w
[GOAL]
case mk.mk
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
val✝¹ : List α
property✝¹ : List.length val✝¹ = n
val✝ : List α
property✝ : List.length val✝ = m
⊢ toList (append { val := val✝¹, property := property✝¹ } { val := val✝, property := property✝ }) =
    toList { val := val✝¹, property := property✝¹ } ++ toList { val := val✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
v : Vector α m
⊢ toList (drop n v) = List.drop n (toList v)
[PROOFSTEP]
cases v
[GOAL]
case mk
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
val✝ : List α
property✝ : List.length val✝ = m
⊢ toList (drop n { val := val✝, property := property✝ }) = List.drop n (toList { val := val✝, property := property✝ })
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
v : Vector α m
⊢ toList (take n v) = List.take n (toList v)
[PROOFSTEP]
cases v
[GOAL]
case mk
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
val✝ : List α
property✝ : List.length val✝ = m
⊢ toList (take n { val := val✝, property := property✝ }) = List.take n (toList { val := val✝, property := property✝ })
[PROOFSTEP]
rfl
