[GOAL]
n : ℕ
α : Type u_1
v : List α
hv : List.length v = n
w : List α
hw : List.length w = n
h : ∀ (m : Fin n), get { val := v, property := hv } m = get { val := w, property := hw } m
⊢ List.length ↑{ val := v, property := hv } = List.length ↑{ val := w, property := hw }
[PROOFSTEP]
rw [hv, hw]
[GOAL]
n : ℕ
α : Type u_1
a : α
v : Vector α (Nat.succ n)
v' : Vector α n
h : head v = a ∧ tail v = v'
⊢ head v ::ᵥ tail v = a ::ᵥ v'
[PROOFSTEP]
rw [h.1, h.2]
[GOAL]
n : ℕ
α : Type u_1
a : α
v : Vector α (Nat.succ n)
v' : Vector α n
⊢ v ≠ a ::ᵥ v' ↔ head v ≠ a ∨ tail v ≠ v'
[PROOFSTEP]
rw [Ne.def, eq_cons_iff a v v', not_and_or]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (n + 1) → α
⊢ toList (ofFn f) = List.ofFn f
[PROOFSTEP]
rw [ofFn, List.ofFn_succ, toList_cons, toList_ofFn]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
v : Vector α n
f : α → β
⊢ toList (map f v) = List.map f (toList v)
[PROOFSTEP]
cases v
[GOAL]
case mk
n : ℕ
α : Type u_1
β : Type u_2
f : α → β
val✝ : List α
property✝ : List.length val✝ = n
⊢ toList (map f { val := val✝, property := property✝ }) = List.map f (toList { val := val✝, property := property✝ })
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
v : Vector α (n + 1)
f : α → β
⊢ head (map f v) = f (head v)
[PROOFSTEP]
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
[GOAL]
case intro.intro
n : ℕ
α : Type u_1
β : Type u_2
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ head (map f v) = f (head v)
[PROOFSTEP]
rw [h, map_cons, head_cons, head_cons]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
v : Vector α (n + 1)
f : α → β
⊢ tail (map f v) = map f (tail v)
[PROOFSTEP]
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
[GOAL]
case intro.intro
n : ℕ
α : Type u_1
β : Type u_2
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ tail (map f v) = map f (tail v)
[PROOFSTEP]
rw [h, map_cons, tail_cons, tail_cons]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α n
i : Fin n
⊢ ↑i < List.length (toList v)
[PROOFSTEP]
rw [toList_length]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α n
i : Fin n
⊢ ↑i < n
[PROOFSTEP]
exact i.2
[GOAL]
n : ℕ
α : Type u_1
a : α
i : Fin n
⊢ get (replicate n a) i = a
[PROOFSTEP]
apply List.get_replicate
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
v : Vector α n
f : α → β
i : Fin n
⊢ get (map f v) i = f (get v i)
[PROOFSTEP]
cases v
[GOAL]
case mk
n : ℕ
α : Type u_1
β : Type u_2
f : α → β
i : Fin n
val✝ : List α
property✝ : List.length val✝ = n
⊢ get (map f { val := val✝, property := property✝ }) i = f (get { val := val✝, property := property✝ } i)
[PROOFSTEP]
simp [Vector.map, get_eq_get]
[GOAL]
case mk
n : ℕ
α : Type u_1
β : Type u_2
f : α → β
i : Fin n
val✝ : List α
property✝ : List.length val✝ = n
⊢ f (List.get val✝ { val := ↑i, isLt := (_ : ↑i < List.length val✝) }) =
    f (List.get val✝ (↑(Fin.castIso (_ : n = List.length (toList { val := val✝, property := property✝ }))) i))
[PROOFSTEP]
rfl
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ get (ofFn f) i = f i
[PROOFSTEP]
conv_rhs => erw [← List.get_ofFn f ⟨i, by simp⟩]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
| f i
[PROOFSTEP]
erw [← List.get_ofFn f ⟨i, by simp⟩]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
| f i
[PROOFSTEP]
erw [← List.get_ofFn f ⟨i, by simp⟩]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
| f i
[PROOFSTEP]
erw [← List.get_ofFn f ⟨i, by simp⟩]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ ↑i < List.length (List.ofFn f)
[PROOFSTEP]
simp
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ get (ofFn f) i = List.get (List.ofFn f) { val := ↑i, isLt := (_ : ↑i < List.length (List.ofFn f)) }
[PROOFSTEP]
simp only [get_eq_get]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ List.get (toList (ofFn f)) (↑(Fin.castIso (_ : n = List.length (toList (ofFn f)))) i) =
    List.get (List.ofFn f) { val := ↑i, isLt := (_ : ↑i < List.length (List.ofFn f)) }
[PROOFSTEP]
congr
[GOAL]
case h.e_2.h
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ toList (ofFn f) = List.ofFn f
[PROOFSTEP]
simp [Fin.heq_ext_iff]
[GOAL]
case h.e_3
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ HEq (↑(Fin.castIso (_ : n = List.length (toList (ofFn f)))) i)
    { val := ↑i, isLt := (_ : ↑i < List.length (List.ofFn f)) }
[PROOFSTEP]
simp [Fin.heq_ext_iff]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α n
⊢ ofFn (get v) = v
[PROOFSTEP]
rcases v with ⟨l, rfl⟩
[GOAL]
case mk
α : Type u_1
l : List α
⊢ ofFn (get { val := l, property := (_ : List.length l = List.length l) }) =
    { val := l, property := (_ : List.length l = List.length l) }
[PROOFSTEP]
apply toList_injective
[GOAL]
case mk.a
α : Type u_1
l : List α
⊢ toList (ofFn (get { val := l, property := (_ : List.length l = List.length l) })) =
    toList { val := l, property := (_ : List.length l = List.length l) }
[PROOFSTEP]
dsimp
[GOAL]
case mk.a
α : Type u_1
l : List α
⊢ toList (ofFn (get { val := l, property := (_ : List.length l = List.length l) })) = l
[PROOFSTEP]
simpa only [toList_ofFn] using List.ofFn_get _
[GOAL]
n : ℕ
α : Type u_1
x : Vector α n
i : Fin (n - 1)
⊢ get (tail x) i = get x { val := ↑i + 1, isLt := (_ : ↑i + 1 < n) }
[PROOFSTEP]
cases' i with i ih
[GOAL]
case mk
n : ℕ
α : Type u_1
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ get (tail x) { val := i, isLt := ih } =
    get x { val := ↑{ val := i, isLt := ih } + 1, isLt := (_ : ↑{ val := i, isLt := ih } + 1 < n) }
[PROOFSTEP]
dsimp
[GOAL]
case mk
n : ℕ
α : Type u_1
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ get (tail x) { val := i, isLt := ih } = get x { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
rcases x with ⟨_ | _, h⟩
[GOAL]
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
h : List.length [] = n
⊢ get (tail { val := [], property := h }) { val := i, isLt := ih } =
    get { val := [], property := h } { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
try rfl
[GOAL]
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
h : List.length [] = n
⊢ get (tail { val := [], property := h }) { val := i, isLt := ih } =
    get { val := [], property := h } { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.cons
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
head✝ : α
tail✝ : List α
h : List.length (head✝ :: tail✝) = n
⊢ get (tail { val := head✝ :: tail✝, property := h }) { val := i, isLt := ih } =
    get { val := head✝ :: tail✝, property := h } { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
try rfl
[GOAL]
case mk.mk.cons
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
head✝ : α
tail✝ : List α
h : List.length (head✝ :: tail✝) = n
⊢ get (tail { val := head✝ :: tail✝, property := h }) { val := i, isLt := ih } =
    get { val := head✝ :: tail✝, property := h } { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
h : List.length [] = n
⊢ get (tail { val := [], property := h }) { val := i, isLt := ih } =
    get { val := [], property := h } { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
rw [List.length] at h 
[GOAL]
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
h✝ : List.length [] = n
h : 0 = n
⊢ get (tail { val := [], property := h✝ }) { val := i, isLt := ih } =
    get { val := [], property := h✝ } { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
rw [← h] at ih 
[GOAL]
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih✝ : i < n - 1
ih : i < 0 - 1
h✝ : List.length [] = n
h : 0 = n
⊢ get (tail { val := [], property := h✝ }) { val := i, isLt := ih✝ } =
    get { val := [], property := h✝ } { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
α : Type u_1
a : α
l : List α
e : List.length (a :: l) = Nat.succ n
i : ℕ
h : i < n
⊢ get (tail { val := a :: l, property := e }) { val := i, isLt := h } =
    get { val := a :: l, property := e } (Fin.succ { val := i, isLt := h })
[PROOFSTEP]
simp [get_eq_get]
[GOAL]
n : ℕ
α : Type u_1
a : α
l : List α
e : List.length (a :: l) = Nat.succ n
i : ℕ
h : i < n
⊢ List.get (toList (tail { val := a :: l, property := e }))
      { val := i, isLt := (_ : i < List.length (toList (tail { val := a :: l, property := e }))) } =
    List.get l { val := i, isLt := (_ : i < List.length l) }
[PROOFSTEP]
rfl
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
⊢ ofFn (get (tail (ofFn f))) = ofFn fun i => f (Fin.succ i)
[PROOFSTEP]
congr
[GOAL]
case e_a
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
⊢ get (tail (ofFn f)) = fun i => f (Fin.succ i)
[PROOFSTEP]
funext i
[GOAL]
case e_a.h
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
i : Fin (Nat.succ n - 1)
⊢ get (tail (ofFn f)) i = f (Fin.succ i)
[PROOFSTEP]
rw [get_tail, get_ofFn]
[GOAL]
case e_a.h
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
i : Fin (Nat.succ n - 1)
⊢ f { val := ↑i + 1, isLt := (_ : ↑i + 1 < Nat.succ n) } = f (Fin.succ i)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : Type u_1
v : Vector α 1
⊢ toList v = [head v]
[PROOFSTEP]
rw [← v.cons_head_tail]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α 1
⊢ toList (head v ::ᵥ tail v) = [head (head v ::ᵥ tail v)]
[PROOFSTEP]
simp only [toList_cons, toList_nil, head_cons, eq_self_iff_true, and_self_iff, singleton_tail]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ ¬List.isEmpty (toList v) = true
[PROOFSTEP]
simp only [empty_toList_eq_ff, Bool.coe_sort_false, not_false_iff]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
v : Vector α n
⊢ toList (map id v) = toList v
[PROOFSTEP]
simp only [List.map_id, Vector.toList_map]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α n
⊢ List.Nodup (toList v) ↔ Function.Injective (get v)
[PROOFSTEP]
cases' v with l hl
[GOAL]
case mk
n : ℕ
α : Type u_1
l : List α
hl : List.length l = n
⊢ List.Nodup (toList { val := l, property := hl }) ↔ Function.Injective (get { val := l, property := hl })
[PROOFSTEP]
subst hl
[GOAL]
case mk
α : Type u_1
l : List α
⊢ List.Nodup (toList { val := l, property := (_ : List.length l = List.length l) }) ↔
    Function.Injective (get { val := l, property := (_ : List.length l = List.length l) })
[PROOFSTEP]
exact List.nodup_iff_injective_get
[GOAL]
n : ℕ
α : Type u_1
v : Vector α n
⊢ List.length (List.reverse (toList v)) = n
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : Type u_1
v : Vector α n
⊢ reverse (reverse v) = v
[PROOFSTEP]
cases v
[GOAL]
case mk
n : ℕ
α : Type u_1
val✝ : List α
property✝ : List.length val✝ = n
⊢ reverse (reverse { val := val✝, property := property✝ }) = { val := val✝, property := property✝ }
[PROOFSTEP]
simp [Vector.reverse]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
⊢ head (ofFn f) = f 0
[PROOFSTEP]
rw [← get_zero, get_ofFn]
[GOAL]
n : ℕ
α : Type u_1
a : α
v : Vector α n
⊢ get (a ::ᵥ v) 0 = a
[PROOFSTEP]
simp [get_zero]
[GOAL]
n : ℕ
α : Type u_1
a : α
v : Vector α n
i : Fin n
⊢ get (a ::ᵥ v) (Fin.succ i) = get v i
[PROOFSTEP]
rw [← get_tail_succ, tail_cons]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ head (reverse v) = last v
[PROOFSTEP]
rw [← get_zero, last_def, get_eq_get, get_eq_get]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.get (toList (reverse v)) (↑(Fin.castIso (_ : Nat.succ n = List.length (toList (reverse v)))) 0) =
    List.get (toList v) (↑(Fin.castIso (_ : n + 1 = List.length (toList v))) (Fin.last n))
[PROOFSTEP]
simp_rw [toList_reverse]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.get (List.reverse (toList v)) (↑(Fin.castIso (_ : Nat.succ n = List.length (toList (reverse v)))) 0) =
    List.get (toList v) (↑(Fin.castIso (_ : n + 1 = List.length (toList v))) (Fin.last n))
[PROOFSTEP]
rw [← Option.some_inj, ← List.get?_eq_get, ← List.get?_eq_get, List.get?_reverse]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.get? (toList v)
      (List.length (toList v) - 1 - ↑(↑(Fin.castIso (_ : Nat.succ n = List.length (toList (reverse v)))) 0)) =
    List.get? (toList v) ↑(↑(Fin.castIso (_ : n + 1 = List.length (toList v))) (Fin.last n))
[PROOFSTEP]
congr
[GOAL]
case e_a
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.length (toList v) - 1 - ↑(↑(Fin.castIso (_ : Nat.succ n = List.length (toList (reverse v)))) 0) =
    ↑(↑(Fin.castIso (_ : n + 1 = List.length (toList v))) (Fin.last n))
[PROOFSTEP]
simp
[GOAL]
case h
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ ↑(↑(Fin.castIso (_ : Nat.succ n = List.length (toList (reverse v)))) 0) < List.length (toList v)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α n
⊢ List.length (List.scanl f b (toList v)) = n + 1
[PROOFSTEP]
rw [List.length_scanl, toList_length]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α n
x : α
⊢ scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v
[PROOFSTEP]
simp only [scanl, toList_cons, List.scanl]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α n
x : α
⊢ { val := b :: List.scanl f (f b x) ↑v,
      property := (_ : (fun l => List.length l = Nat.succ n + 1) (b :: List.scanl f (f b x) ↑v)) } =
    b ::ᵥ
      { val := List.scanl f (f b x) (toList v),
        property := (_ : List.length (List.scanl f (f b x) (toList v)) = n + 1) }
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α n
x : α
⊢ { val := b :: List.scanl f (f b x) ↑v,
      property := (_ : List.length (List.scanl f b (toList (x ::ᵥ v))) = Nat.succ n + 1) } =
    b ::ᵥ
      { val := List.scanl f (f b x) (toList v),
        property := (_ : List.length (List.scanl f (f b x) (toList v)) = n + 1) }
[PROOFSTEP]
simp only [cons]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α n
x : α
⊢ { val := b :: List.scanl f (f b x) ↑v,
      property := (_ : List.length (List.scanl f b (toList (x ::ᵥ v))) = Nat.succ n + 1) } =
    { val := b :: List.scanl f (f b x) (toList v),
      property := (_ : Nat.succ (List.length (List.scanl f (f b x) (toList v))) = Nat.succ (n + 1)) }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v✝ : Vector α n
v : Vector α 1
⊢ scanl f b v = b ::ᵥ f b (head v) ::ᵥ nil
[PROOFSTEP]
rw [← cons_head_tail v]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v✝ : Vector α n
v : Vector α 1
⊢ scanl f b (head v ::ᵥ tail v) = b ::ᵥ f b (head (head v ::ᵥ tail v)) ::ᵥ nil
[PROOFSTEP]
simp only [scanl_cons, scanl_nil, head_cons, singleton_tail]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α n
⊢ head (scanl f b v) = b
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α Nat.zero
⊢ head (scanl f b v) = b
[PROOFSTEP]
have : v = nil := by simp only [Nat.zero_eq, eq_iff_true_of_subsingleton]
[GOAL]
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α Nat.zero
⊢ v = nil
[PROOFSTEP]
simp only [Nat.zero_eq, eq_iff_true_of_subsingleton]
[GOAL]
case zero
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α Nat.zero
this : v = nil
⊢ head (scanl f b v) = b
[PROOFSTEP]
simp only [this, scanl_nil, head_cons]
[GOAL]
case succ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (Nat.succ n✝)
⊢ head (scanl f b v) = b
[PROOFSTEP]
rw [← cons_head_tail v]
[GOAL]
case succ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (Nat.succ n✝)
⊢ head (scanl f b (head v ::ᵥ tail v)) = b
[PROOFSTEP]
simp only [← get_zero, get_eq_get, toList_scanl, toList_cons, List.scanl, Fin.val_zero, List.get]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α n
i : Fin n
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α Nat.zero
i : Fin Nat.zero
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
[PROOFSTEP]
exact i.elim0
[GOAL]
case succ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
n : ℕ
v : Vector α (Nat.succ n)
i : Fin (Nat.succ n)
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
[PROOFSTEP]
induction' n with n hn generalizing b
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n : ℕ
v✝ : Vector α (Nat.succ n)
i✝ : Fin (Nat.succ n)
b : β
v : Vector α (Nat.succ Nat.zero)
i : Fin (Nat.succ Nat.zero)
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
[PROOFSTEP]
have i0 : i = 0 := Fin.eq_zero _
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n : ℕ
v✝ : Vector α (Nat.succ n)
i✝ : Fin (Nat.succ n)
b : β
v : Vector α (Nat.succ Nat.zero)
i : Fin (Nat.succ Nat.zero)
i0 : i = 0
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
[PROOFSTEP]
simp [scanl_singleton, i0, get_zero]
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n : ℕ
v✝ : Vector α (Nat.succ n)
i✝ : Fin (Nat.succ n)
b : β
v : Vector α (Nat.succ Nat.zero)
i : Fin (Nat.succ Nat.zero)
i0 : i = 0
⊢ get (b ::ᵥ f b (head v) ::ᵥ nil) 1 = f b (head v)
[PROOFSTEP]
simp [get_eq_get]
[GOAL]
case succ.succ
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
[PROOFSTEP]
rw [← cons_head_tail v, scanl_cons, get_cons_succ]
[GOAL]
case succ.succ
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ get (scanl f (f b (head v)) (tail v)) i =
    f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (Fin.castSucc i)) (get (head v ::ᵥ tail v) i)
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case succ.succ.refine'_1
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ get (scanl f (f b (head v)) (tail v)) 0 =
    f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (Fin.castSucc 0)) (get (head v ::ᵥ tail v) 0)
[PROOFSTEP]
simp only [get_zero, scanl_head, Fin.castSucc_zero, head_cons]
[GOAL]
case succ.succ.refine'_2
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ ∀ (i : Fin (n + 1)),
    get (scanl f (f b (head v)) (tail v)) (Fin.succ i) =
      f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (Fin.castSucc (Fin.succ i))) (get (head v ::ᵥ tail v) (Fin.succ i))
[PROOFSTEP]
intro i'
[GOAL]
case succ.succ.refine'_2
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
i' : Fin (n + 1)
⊢ get (scanl f (f b (head v)) (tail v)) (Fin.succ i') =
    f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (Fin.castSucc (Fin.succ i'))) (get (head v ::ᵥ tail v) (Fin.succ i'))
[PROOFSTEP]
simp only [hn, Fin.castSucc_fin_succ, get_cons_succ]
[GOAL]
n✝ : ℕ
α✝ : Type u_1
m : Type u_2 → Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_2
n : ℕ
f : Fin (n + 1) → α
⊢ (mOfFn fun i => pure (f i)) = pure (ofFn f)
[PROOFSTEP]
rw [mOfFn, @mOfFn_pure m _ _ _ n _, ofFn]
[GOAL]
n✝ : ℕ
α✝ : Type u_1
m : Type u_2 → Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_2
n : ℕ
f : Fin (n + 1) → α
⊢ (do
      let a ← pure (f 0)
      let v ← pure (ofFn fun i => f (Fin.succ i))
      pure (a ::ᵥ v)) =
    pure (f 0 ::ᵥ ofFn fun i => f (Fin.succ i))
[PROOFSTEP]
simp
[GOAL]
n✝ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n : ℕ
v : Vector α n
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
⊢ C v
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
n✝ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n : ℕ
v✝ : Vector α n
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
v : Vector α Nat.zero
⊢ C v
[PROOFSTEP]
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
[GOAL]
case zero.mk.nil.refl
n✝ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n : ℕ
v : Vector α n
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
⊢ C { val := [], property := (_ : List.length [] = List.length []) }
[PROOFSTEP]
exact h_nil
[GOAL]
case succ
n✝¹ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n✝ : ℕ
v✝ : Vector α n✝
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
v : Vector α (Nat.succ n)
⊢ C v
[PROOFSTEP]
rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
[GOAL]
case succ.mk.nil
n✝¹ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n✝ : ℕ
v : Vector α n✝
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
v_property : List.length [] = Nat.succ n
⊢ C { val := [], property := v_property }
case succ.mk.cons
n✝¹ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n✝ : ℕ
v✝ : Vector α n✝
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
⊢ C { val := a :: v, property := v_property }
[PROOFSTEP]
cases v_property
[GOAL]
case succ.mk.cons
n✝¹ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n✝ : ℕ
v✝ : Vector α n✝
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
⊢ C { val := a :: v, property := v_property }
[PROOFSTEP]
apply @h_cons n _ ⟨v, (add_left_inj 1).mp v_property⟩
[GOAL]
case succ.mk.cons
n✝¹ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n✝ : ℕ
v✝ : Vector α n✝
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
⊢ C { val := v, property := (_ : List.length v = n) }
[PROOFSTEP]
apply ih
[GOAL]
n : ℕ
α : Type u_1
v : Vector α n
⊢ True
[PROOFSTEP]
induction v using Vector.inductionOn
[GOAL]
case h_nil
n : ℕ
α : Type u_1
⊢ True
[PROOFSTEP]
trivial
[GOAL]
case h_cons
n : ℕ
α : Type u_1
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ : True
⊢ True
[PROOFSTEP]
trivial
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v : Vector α n
w : Vector β n
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
⊢ C v w
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n
w✝ : Vector β n
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
v : Vector α Nat.zero
w : Vector β Nat.zero
⊢ C v w
[PROOFSTEP]
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
[GOAL]
case zero.mk.nil.refl
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v : Vector α n
w✝ : Vector β n
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
w : Vector β Nat.zero
⊢ C { val := [], property := (_ : List.length [] = List.length []) } w
[PROOFSTEP]
rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
[GOAL]
case zero.mk.nil.refl.mk.nil.refl
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v : Vector α n
w : Vector β n
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
⊢ C { val := [], property := (_ : List.length [] = List.length []) }
    { val := [], property := (_ : List.length [] = List.length []) }
[PROOFSTEP]
exact nil
[GOAL]
case succ
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n✝
w✝ : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
v : Vector α (Nat.succ n)
w : Vector β (Nat.succ n)
⊢ C v w
[PROOFSTEP]
rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
[GOAL]
case succ.mk.nil
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v : Vector α n✝
w✝ : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
w : Vector β (Nat.succ n)
v_property : List.length [] = Nat.succ n
⊢ C { val := [], property := v_property } w
case succ.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n✝
w✝ : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
w : Vector β (Nat.succ n)
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
⊢ C { val := a :: v, property := v_property } w
[PROOFSTEP]
cases v_property
[GOAL]
case succ.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n✝
w✝ : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
w : Vector β (Nat.succ n)
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
⊢ C { val := a :: v, property := v_property } w
[PROOFSTEP]
rcases w with ⟨_ | ⟨b, w⟩, w_property⟩
[GOAL]
case succ.mk.cons.mk.nil
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n✝
w : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
w_property : List.length [] = Nat.succ n
⊢ C { val := a :: v, property := v_property } { val := [], property := w_property }
case succ.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n✝
w✝ : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
b : β
w : List β
w_property : List.length (b :: w) = Nat.succ n
⊢ C { val := a :: v, property := v_property } { val := b :: w, property := w_property }
[PROOFSTEP]
cases w_property
[GOAL]
case succ.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n✝
w✝ : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
b : β
w : List β
w_property : List.length (b :: w) = Nat.succ n
⊢ C { val := a :: v, property := v_property } { val := b :: w, property := w_property }
[PROOFSTEP]
apply @cons n _ _ ⟨v, (add_left_inj 1).mp v_property⟩ ⟨w, (add_left_inj 1).mp w_property⟩
[GOAL]
case succ.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n✝
w✝ : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
b : β
w : List β
w_property : List.length (b :: w) = Nat.succ n
⊢ C { val := v, property := (_ : List.length v = n) } { val := w, property := (_ : List.length w = n) }
[PROOFSTEP]
apply ih
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u : Vector α n
v : Vector β n
w : Vector γ n
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
⊢ C u v w
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n
v✝ : Vector β n
w✝ : Vector γ n
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
u : Vector α Nat.zero
v : Vector β Nat.zero
w : Vector γ Nat.zero
⊢ C u v w
[PROOFSTEP]
rcases u with ⟨_ | ⟨-, -⟩, - | -⟩
[GOAL]
case zero.mk.nil.refl
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u : Vector α n
v✝ : Vector β n
w✝ : Vector γ n
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
v : Vector β Nat.zero
w : Vector γ Nat.zero
⊢ C { val := [], property := (_ : List.length [] = List.length []) } v w
[PROOFSTEP]
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
[GOAL]
case zero.mk.nil.refl.mk.nil.refl
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u : Vector α n
v : Vector β n
w✝ : Vector γ n
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
w : Vector γ Nat.zero
⊢ C { val := [], property := (_ : List.length [] = List.length []) }
    { val := [], property := (_ : List.length [] = List.length []) } w
[PROOFSTEP]
rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
[GOAL]
case zero.mk.nil.refl.mk.nil.refl.mk.nil.refl
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u : Vector α n
v : Vector β n
w : Vector γ n
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
⊢ C { val := [], property := (_ : List.length [] = List.length []) }
    { val := [], property := (_ : List.length [] = List.length []) }
    { val := [], property := (_ : List.length [] = List.length []) }
[PROOFSTEP]
exact nil
[GOAL]
case succ
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
u : Vector α (Nat.succ n)
v : Vector β (Nat.succ n)
w : Vector γ (Nat.succ n)
⊢ C u v w
[PROOFSTEP]
rcases u with ⟨_ | ⟨a, u⟩, u_property⟩
[GOAL]
case succ.mk.nil
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
v : Vector β (Nat.succ n)
w : Vector γ (Nat.succ n)
u_property : List.length [] = Nat.succ n
⊢ C { val := [], property := u_property } v w
case succ.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
v : Vector β (Nat.succ n)
w : Vector γ (Nat.succ n)
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
⊢ C { val := a :: u, property := u_property } v w
[PROOFSTEP]
cases u_property
[GOAL]
case succ.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
v : Vector β (Nat.succ n)
w : Vector γ (Nat.succ n)
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
⊢ C { val := a :: u, property := u_property } v w
[PROOFSTEP]
rcases v with ⟨_ | ⟨b, v⟩, v_property⟩
[GOAL]
case succ.mk.cons.mk.nil
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
w : Vector γ (Nat.succ n)
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
v_property : List.length [] = Nat.succ n
⊢ C { val := a :: u, property := u_property } { val := [], property := v_property } w
case succ.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
w : Vector γ (Nat.succ n)
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
b : β
v : List β
v_property : List.length (b :: v) = Nat.succ n
⊢ C { val := a :: u, property := u_property } { val := b :: v, property := v_property } w
[PROOFSTEP]
cases v_property
[GOAL]
case succ.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
w : Vector γ (Nat.succ n)
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
b : β
v : List β
v_property : List.length (b :: v) = Nat.succ n
⊢ C { val := a :: u, property := u_property } { val := b :: v, property := v_property } w
[PROOFSTEP]
rcases w with ⟨_ | ⟨c, w⟩, w_property⟩
[GOAL]
case succ.mk.cons.mk.cons.mk.nil
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
b : β
v : List β
v_property : List.length (b :: v) = Nat.succ n
w_property : List.length [] = Nat.succ n
⊢ C { val := a :: u, property := u_property } { val := b :: v, property := v_property }
    { val := [], property := w_property }
case succ.mk.cons.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
b : β
v : List β
v_property : List.length (b :: v) = Nat.succ n
c : γ
w : List γ
w_property : List.length (c :: w) = Nat.succ n
⊢ C { val := a :: u, property := u_property } { val := b :: v, property := v_property }
    { val := c :: w, property := w_property }
[PROOFSTEP]
cases w_property
[GOAL]
case succ.mk.cons.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
b : β
v : List β
v_property : List.length (b :: v) = Nat.succ n
c : γ
w : List γ
w_property : List.length (c :: w) = Nat.succ n
⊢ C { val := a :: u, property := u_property } { val := b :: v, property := v_property }
    { val := c :: w, property := w_property }
[PROOFSTEP]
apply
  @cons n _ _ _ ⟨u, (add_left_inj 1).mp u_property⟩ ⟨v, (add_left_inj 1).mp v_property⟩
    ⟨w, (add_left_inj 1).mp w_property⟩
[GOAL]
case succ.mk.cons.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
b : β
v : List β
v_property : List.length (b :: v) = Nat.succ n
c : γ
w : List γ
w_property : List.length (c :: w) = Nat.succ n
⊢ C { val := u, property := (_ : List.length u = n) } { val := v, property := (_ : List.length v = n) }
    { val := w, property := (_ : List.length w = n) }
[PROOFSTEP]
apply ih
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
xs : List α
property✝ : List.length xs = n
⊢ Array α = Array α
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a : α
i : Fin (n + 1)
v : Vector α n
⊢ List.length (List.insertNth (↑i) a ↑v) = n + 1
[PROOFSTEP]
rw [List.length_insertNth, v.2]
[GOAL]
case a
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a : α
i : Fin (n + 1)
v : Vector α n
⊢ ↑i ≤ List.length ↑v
[PROOFSTEP]
rw [v.2, ← Nat.succ_le_succ_iff]
[GOAL]
case a
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a : α
i : Fin (n + 1)
v : Vector α n
⊢ Nat.succ ↑i ≤ Nat.succ n
[PROOFSTEP]
exact i.2
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ removeNth (Fin.succAbove { val := j, isLt := hj } { val := i, isLt := hi }) (insertNth a { val := j, isLt := hj } v) =
    insertNth a (Fin.predAbove { val := i, isLt := hi } { val := j, isLt := hj }) (removeNth { val := i, isLt := hi } v)
[PROOFSTEP]
dsimp [insertNth, removeNth, Fin.succAbove, Fin.predAbove]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ {
      val :=
        List.removeNth (List.insertNth j a ↑v)
          ↑(if i < j then { val := i, isLt := (_ : i < Nat.succ (n + 1)) }
            else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (n + 1)) }),
      property :=
        (_ :
          List.length
              (List.removeNth (List.insertNth j a ↑v)
                ↑(if i < j then { val := i, isLt := (_ : i < Nat.succ (n + 1)) }
                  else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (n + 1)) })) =
            n + 1 + 1 - 1) } =
    {
      val :=
        List.insertNth
          (↑(if h : { val := i, isLt := (_ : i < Nat.succ (n + 1)) } < { val := j, isLt := hj } then
              Fin.pred { val := j, isLt := hj } (_ : { val := j, isLt := hj } ≠ 0)
            else { val := j, isLt := (_ : ↑{ val := j, isLt := hj } < n + 1) }))
          a
          ↑(match v with
            | { val := l, property := p } =>
              { val := List.removeNth l i,
                property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) }),
      property :=
        (_ :
          List.length
              (List.insertNth
                (↑(if h : { val := i, isLt := (_ : i < Nat.succ (n + 1)) } < { val := j, isLt := hj } then
                    Fin.pred { val := j, isLt := hj } (_ : { val := j, isLt := hj } ≠ 0)
                  else { val := j, isLt := (_ : ↑{ val := j, isLt := hj } < n + 1) }))
                a
                ↑(match v with
                  | { val := l, property := p } =>
                    { val := List.removeNth l i,
                      property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })) =
            n + 1) }
[PROOFSTEP]
rw [Subtype.mk_eq_mk]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ List.removeNth (List.insertNth j a ↑v)
      ↑(if i < j then { val := i, isLt := (_ : i < Nat.succ (n + 1)) }
        else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (n + 1)) }) =
    List.insertNth
      (↑(if h : { val := i, isLt := (_ : i < Nat.succ (n + 1)) } < { val := j, isLt := hj } then
          Fin.pred { val := j, isLt := hj } (_ : { val := j, isLt := hj } ≠ 0)
        else { val := j, isLt := (_ : ↑{ val := j, isLt := hj } < n + 1) }))
      a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
simp only [Fin.lt_iff_val_lt_val]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ List.removeNth (List.insertNth j a ↑v)
      ↑(if i < j then { val := i, isLt := (_ : i < Nat.succ (n + 1)) }
        else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (n + 1)) }) =
    List.insertNth
      (↑(if h : i < j then Fin.pred { val := j, isLt := hj } (_ : { val := j, isLt := hj } ≠ 0)
        else { val := j, isLt := (_ : ↑{ val := j, isLt := hj } < n + 1) }))
      a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
split_ifs with hij
[GOAL]
case pos
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : i < j
⊢ List.removeNth (List.insertNth j a ↑v) ↑{ val := i, isLt := (_ : i < Nat.succ (n + 1)) } =
    List.insertNth (↑(Fin.pred { val := j, isLt := hj } (_ : { val := j, isLt := hj } ≠ 0))) a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
rcases Nat.exists_eq_succ_of_ne_zero (Nat.pos_iff_ne_zero.1 (lt_of_le_of_lt (Nat.zero_le _) hij)) with ⟨j, rfl⟩
[GOAL]
case pos.intro
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : Nat.succ j < n + 2
hij : i < Nat.succ j
⊢ List.removeNth (List.insertNth (Nat.succ j) a ↑v) ↑{ val := i, isLt := (_ : i < Nat.succ (n + 1)) } =
    List.insertNth (↑(Fin.pred { val := Nat.succ j, isLt := hj } (_ : { val := Nat.succ j, isLt := hj } ≠ 0))) a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
rw [← List.insertNth_removeNth_of_ge]
[GOAL]
case pos.intro
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : Nat.succ j < n + 2
hij : i < Nat.succ j
⊢ List.insertNth j a (List.removeNth ↑v ↑{ val := i, isLt := (_ : i < Nat.succ (n + 1)) }) =
    List.insertNth (↑(Fin.pred { val := Nat.succ j, isLt := hj } (_ : { val := Nat.succ j, isLt := hj } ≠ 0))) a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
simp
[GOAL]
case pos.intro
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : Nat.succ j < n + 2
hij : i < Nat.succ j
⊢ List.insertNth j a (List.removeNth (↑v) i) =
    List.insertNth j a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
rfl
[GOAL]
case pos.intro.a
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : Nat.succ j < n + 2
hij : i < Nat.succ j
⊢ ↑{ val := i, isLt := (_ : i < Nat.succ (n + 1)) } < List.length ↑v
[PROOFSTEP]
simpa
[GOAL]
case pos.intro.a
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : Nat.succ j < n + 2
hij : i < Nat.succ j
⊢ ↑{ val := i, isLt := (_ : i < Nat.succ (n + 1)) } ≤ j
[PROOFSTEP]
simpa [Nat.lt_succ_iff] using hij
[GOAL]
case neg
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ List.removeNth (List.insertNth j a ↑v) ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (n + 1)) } =
    List.insertNth (↑{ val := j, isLt := (_ : ↑{ val := j, isLt := hj } < n + 1) }) a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
dsimp
[GOAL]
case neg
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ List.removeNth (List.insertNth j a ↑v) (i + 1) =
    List.insertNth j a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
rw [← List.insertNth_removeNth_of_le i j _ _ _]
[GOAL]
case neg
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ List.insertNth j a (List.removeNth (↑v) i) =
    List.insertNth j a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ i < List.length ↑v
[PROOFSTEP]
simpa
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ j ≤ i
[PROOFSTEP]
simpa [not_lt] using hij
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ insertNth b (Fin.succ j) (insertNth a i { val := l, property := hl }) =
    insertNth a (Fin.castSucc i) (insertNth b j { val := l, property := hl })
[PROOFSTEP]
refine' Subtype.eq _
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑(insertNth b (Fin.succ j) (insertNth a i { val := l, property := hl })) =
    ↑(insertNth a (Fin.castSucc i) (insertNth b j { val := l, property := hl }))
[PROOFSTEP]
simp only [insertNth_val, Fin.val_succ, Fin.castSucc, Fin.coe_castAdd]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ List.insertNth (↑j + 1) b (List.insertNth (↑i) a l) = List.insertNth (↑i) a (List.insertNth (↑j) b l)
[PROOFSTEP]
apply List.insertNth_comm
[GOAL]
case x
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑i ≤ ↑j
[PROOFSTEP]
assumption
[GOAL]
case x
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑j ≤ List.length l
[PROOFSTEP]
rw [hl]
[GOAL]
case x
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑j ≤ n
[PROOFSTEP]
exact Nat.le_of_succ_le_succ j.2
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i : Fin n
a : α
⊢ List.length (List.set (↑v) (↑i) a) = n
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i : Fin n
a : α
⊢ get (set v i a) i = a
[PROOFSTEP]
cases v
[GOAL]
case mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
i : Fin n
a : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ get (set { val := val✝, property := property✝ } i a) i = a
[PROOFSTEP]
cases i
[GOAL]
case mk.mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ get (set { val := val✝¹, property := property✝ } { val := val✝, isLt := isLt✝ } a) { val := val✝, isLt := isLt✝ } = a
[PROOFSTEP]
simp [Vector.set, get_eq_get]
[GOAL]
case mk.mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ List.get (List.set val✝¹ val✝ a)
      (↑(Fin.castIso
            (_ :
              n =
                List.length
                  (toList
                    { val := List.set val✝¹ val✝ a,
                      property :=
                        (_ :
                          List.length
                              (List.set (↑{ val := val✝¹, property := property✝ }) (↑{ val := val✝, isLt := isLt✝ })
                                a) =
                            n) })))
        { val := val✝, isLt := isLt✝ }) =
    a
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ List.get (List.set val✝¹ val✝ a)
      (↑(Fin.castIso (_ : n = List.length (List.set val✝¹ val✝ a))) { val := val✝, isLt := isLt✝ }) =
    a
[PROOFSTEP]
exact List.get_set_eq _ _ _ _
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i j : Fin n
h : i ≠ j
a : α
⊢ get (set v i a) j = get v j
[PROOFSTEP]
cases v
[GOAL]
case mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
i j : Fin n
h : i ≠ j
a : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ get (set { val := val✝, property := property✝ } i a) j = get { val := val✝, property := property✝ } j
[PROOFSTEP]
cases i
[GOAL]
case mk.mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
j : Fin n
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝, isLt := isLt✝ } ≠ j
⊢ get (set { val := val✝¹, property := property✝ } { val := val✝, isLt := isLt✝ } a) j =
    get { val := val✝¹, property := property✝ } j
[PROOFSTEP]
cases j
[GOAL]
case mk.mk.mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ get (set { val := val✝², property := property✝ } { val := val✝¹, isLt := isLt✝¹ } a) { val := val✝, isLt := isLt✝ } =
    get { val := val✝², property := property✝ } { val := val✝, isLt := isLt✝ }
[PROOFSTEP]
simp [Vector.set, Vector.get_eq_get, List.get_set_of_ne (Fin.vne_of_ne h)]
[GOAL]
case mk.mk.mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ List.get (List.set val✝² val✝¹ a)
      (↑(Fin.castIso
            (_ :
              n =
                List.length
                  (toList
                    { val := List.set val✝² val✝¹ a,
                      property :=
                        (_ :
                          List.length
                              (List.set (↑{ val := val✝², property := property✝ }) (↑{ val := val✝¹, isLt := isLt✝¹ })
                                a) =
                            n) })))
        { val := val✝, isLt := isLt✝ }) =
    List.get val✝²
      (↑(Fin.castIso (_ : n = List.length (toList { val := val✝², property := property✝ })))
        { val := val✝, isLt := isLt✝ })
[PROOFSTEP]
rw [List.get_set_of_ne]
[GOAL]
case mk.mk.mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ List.get val✝²
      {
        val :=
          ↑(↑(Fin.castIso
                  (_ :
                    n =
                      List.length
                        (toList
                          { val := List.set val✝² val✝¹ a,
                            property :=
                              (_ :
                                List.length
                                    (List.set (↑{ val := val✝², property := property✝ })
                                      (↑{ val := val✝¹, isLt := isLt✝¹ }) a) =
                                  n) })))
              { val := val✝, isLt := isLt✝ }),
        isLt :=
          (_ :
            ↑(↑(Fin.castIso
                      (_ :
                        n =
                          List.length
                            (toList
                              { val := List.set val✝² val✝¹ a,
                                property :=
                                  (_ :
                                    List.length
                                        (List.set (↑{ val := val✝², property := property✝ })
                                          (↑{ val := val✝¹, isLt := isLt✝¹ }) a) =
                                      n) })))
                  { val := val✝, isLt := isLt✝ }) <
              List.length val✝²) } =
    List.get val✝²
      (↑(Fin.castIso (_ : n = List.length (toList { val := val✝², property := property✝ })))
        { val := val✝, isLt := isLt✝ })
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.mk.h
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ val✝¹ ≠
    ↑(↑(Fin.castIso
            (_ :
              n =
                List.length
                  (toList
                    { val := List.set val✝² val✝¹ a,
                      property :=
                        (_ :
                          List.length
                              (List.set (↑{ val := val✝², property := property✝ }) (↑{ val := val✝¹, isLt := isLt✝¹ })
                                a) =
                            n) })))
        { val := val✝, isLt := isLt✝ })
[PROOFSTEP]
simpa using h
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i j : Fin n
a : α
⊢ get (set v i a) j = if i = j then a else get v j
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i j : Fin n
a : α
h✝ : i = j
⊢ get (set v i a) j = a
[PROOFSTEP]
try simp [*]
[GOAL]
case pos
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i j : Fin n
a : α
h✝ : i = j
⊢ get (set v i a) j = a
[PROOFSTEP]
simp [*]
[GOAL]
case neg
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ get (set v i a) j = get v j
[PROOFSTEP]
try simp [*]
[GOAL]
case neg
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ get (set v i a) j = get v j
[PROOFSTEP]
simp [*]
[GOAL]
case neg
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ get (set v i a) j = get v j
[PROOFSTEP]
rwa [get_set_of_ne]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ List.prod (toList (set v i a)) = List.prod (toList (take (↑i) v)) * a * List.prod (toList (drop (↑i + 1) v))
[PROOFSTEP]
refine' (List.prod_set v.toList i a).trans _
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ (List.prod (List.take (↑i) (toList v)) * if ↑i < List.length (toList v) then a else 1) *
      List.prod (List.drop (↑i + 1) (toList v)) =
    List.prod (toList (take (↑i) v)) * a * List.prod (toList (drop (↑i + 1) v))
[PROOFSTEP]
simp_all
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ List.prod (toList (set v i a)) = List.prod (toList v) * (get v i)⁻¹ * a
[PROOFSTEP]
refine' (List.prod_set' v.toList i a).trans _
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ (List.prod (toList v) * if hn : ↑i < List.length (toList v) then (List.nthLe (toList v) (↑i) hn)⁻¹ * a else 1) =
    List.prod (toList v) * (get v i)⁻¹ * a
[PROOFSTEP]
simp [get_eq_get, mul_assoc]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ List.nthLe (toList v) ↑i (_ : ↑i < List.length (toList v)) =
    List.get (toList v) (↑(Fin.castIso (_ : n = List.length (toList v))) i)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
f : α → F β
v : List α
Hv : List.length v = n
⊢ F (Vector β (List.length v)) = F (Vector β n)
[PROOFSTEP]
rw [Hv]
[GOAL]
n : ℕ
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
f : α → F β
x : α
⊢ ∀ (xs : Vector α n), Vector.traverse f (x ::ᵥ xs) = Seq.seq (cons <$> f x) fun x => Vector.traverse f xs
[PROOFSTEP]
rintro ⟨xs, rfl⟩
[GOAL]
case mk
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
f : α → F β
x : α
xs : List α
⊢ Vector.traverse f (x ::ᵥ { val := xs, property := (_ : List.length xs = List.length xs) }) =
    Seq.seq (cons <$> f x) fun x => Vector.traverse f { val := xs, property := (_ : List.length xs = List.length xs) }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
⊢ ∀ (x : Vector α n), Vector.traverse pure x = x
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case mk
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
x : List α
⊢ Vector.traverse pure { val := x, property := (_ : List.length x = List.length x) } =
    { val := x, property := (_ : List.length x = List.length x) }
[PROOFSTEP]
dsimp [Vector.traverse, cast]
[GOAL]
case mk
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
x : List α
⊢ Vector.traverseAux pure x = { val := x, property := (_ : List.length x = List.length x) }
[PROOFSTEP]
induction' x with x xs IH
[GOAL]
case mk.nil
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
⊢ Vector.traverseAux pure [] = { val := [], property := (_ : List.length [] = List.length []) }
[PROOFSTEP]
rfl
[GOAL]
case mk.cons
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
x : α
xs : List α
IH : Vector.traverseAux pure xs = { val := xs, property := (_ : List.length xs = List.length xs) }
⊢ Vector.traverseAux pure (x :: xs) =
    { val := x :: xs, property := (_ : List.length (x :: xs) = List.length (x :: xs)) }
[PROOFSTEP]
simp! [IH]
[GOAL]
case mk.cons
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
x : α
xs : List α
IH : Vector.traverseAux pure xs = { val := xs, property := (_ : List.length xs = List.length xs) }
⊢ (Seq.seq (cons x) fun x => { val := xs, property := (_ : List.length xs = List.length xs) }) =
    { val := x :: xs, property := (_ : List.length (x :: xs) = List.length (x :: xs)) }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : Vector α n
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) x = Comp.mk (Vector.traverse f <$> Vector.traverse g x)
[PROOFSTEP]
induction' x using Vector.inductionOn with n x xs ih
[GOAL]
case h_nil
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) nil = Comp.mk (Vector.traverse f <$> Vector.traverse g nil)
case h_cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
n : ℕ
x : α
xs : Vector α n
ih : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) xs = Comp.mk (Vector.traverse f <$> Vector.traverse g xs)
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) (x ::ᵥ xs) =
    Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ xs))
[PROOFSTEP]
simp! [cast, *, functor_norm]
[GOAL]
case h_nil
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
⊢ pure nil = Comp.mk (pure (pure nil))
[PROOFSTEP]
rfl
[GOAL]
case h_cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
n : ℕ
x : α
xs : Vector α n
ih : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) xs = Comp.mk (Vector.traverse f <$> Vector.traverse g xs)
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) (x ::ᵥ xs) =
    Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ xs))
[PROOFSTEP]
rw [Vector.traverse_def, ih]
[GOAL]
case h_cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
n : ℕ
x : α
xs : Vector α n
ih : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) xs = Comp.mk (Vector.traverse f <$> Vector.traverse g xs)
⊢ (Seq.seq (cons <$> (Comp.mk ∘ Functor.map f ∘ g) x) fun x => Comp.mk (Vector.traverse f <$> Vector.traverse g xs)) =
    Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ xs))
[PROOFSTEP]
simp [functor_norm, (· ∘ ·)]
[GOAL]
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
α β : Type u_1
f : α → β
⊢ ∀ (x : Vector α n), Vector.traverse (pure ∘ f) x = pure (map f x)
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case mk
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
α β : Type u_1
f : α → β
x : List α
⊢ Vector.traverse (pure ∘ f) { val := x, property := (_ : List.length x = List.length x) } =
    pure (map f { val := x, property := (_ : List.length x = List.length x) })
[PROOFSTEP]
simp!
[GOAL]
case mk
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
α β : Type u_1
f : α → β
x : List α
⊢ Vector.traverseAux (pure ∘ f) x =
    { val := List.map f x, property := (_ : List.length (List.map f x) = List.length x) }
[PROOFSTEP]
induction x
[GOAL]
case mk.nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
α β : Type u_1
f : α → β
⊢ Vector.traverseAux (pure ∘ f) [] =
    { val := List.map f [], property := (_ : List.length (List.map f []) = List.length []) }
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case mk.cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
α β : Type u_1
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ :
  Vector.traverseAux (pure ∘ f) tail✝ =
    { val := List.map f tail✝, property := (_ : List.length (List.map f tail✝) = List.length tail✝) }
⊢ Vector.traverseAux (pure ∘ f) (head✝ :: tail✝) =
    { val := List.map f (head✝ :: tail✝),
      property := (_ : List.length (List.map f (head✝ :: tail✝)) = List.length (head✝ :: tail✝)) }
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case mk.nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
α β : Type u_1
f : α → β
⊢ nil = { val := [], property := (_ : (fun l => List.length l = List.length []) []) }
[PROOFSTEP]
rfl
[GOAL]
case mk.cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
α β : Type u_1
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ :
  Vector.traverseAux (pure ∘ f) tail✝ =
    { val := List.map f tail✝, property := (_ : List.length (List.map f tail✝) = List.length tail✝) }
⊢ (Seq.seq (cons (f head✝)) fun x =>
      { val := List.map f tail✝, property := (_ : List.length (List.map f tail✝) = List.length tail✝) }) =
    { val := f head✝ :: List.map f tail✝,
      property := (_ : (fun l => List.length l = List.length (head✝ :: tail✝)) (f head✝ :: List.map f tail✝)) }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
x : Vector α n
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f x) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
[PROOFSTEP]
induction' x using Vector.inductionOn with n x xs ih
[GOAL]
case h_nil
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f nil) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) nil
[PROOFSTEP]
simp! [functor_norm, cast, η.preserves_pure]
[GOAL]
case h_cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih :
  (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) xs
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f (x ::ᵥ xs)) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (x ::ᵥ xs)
[PROOFSTEP]
rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]
[GOAL]
case h_cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih :
  (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) xs
⊢ (Seq.seq (cons <$> (fun {α} => ApplicativeTransformation.app η α) (f x)) fun x =>
      (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs)) =
    Seq.seq (cons <$> ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x) fun x =>
      (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ ∀ {α : Type u} (x : flip Vector n α), id <$> x = x
[PROOFSTEP]
intro _ x
[GOAL]
n : ℕ
α✝ : Type u
x : flip Vector n α✝
⊢ id <$> x = x
[PROOFSTEP]
cases x
[GOAL]
case mk
n : ℕ
α✝ : Type u
val✝ : List α✝
property✝ : List.length val✝ = n
⊢ id <$> { val := val✝, property := property✝ } = { val := val✝, property := property✝ }
[PROOFSTEP]
simp! [(· <$> ·)]
[GOAL]
n : ℕ
⊢ ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : flip Vector n α), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intro _ _ _ _ _ x
[GOAL]
n : ℕ
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x : flip Vector n α✝
⊢ (h✝ ∘ g✝) <$> x = h✝ <$> g✝ <$> x
[PROOFSTEP]
cases x
[GOAL]
case mk
n : ℕ
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
val✝ : List α✝
property✝ : List.length val✝ = n
⊢ (h✝ ∘ g✝) <$> { val := val✝, property := property✝ } = h✝ <$> g✝ <$> { val := val✝, property := property✝ }
[PROOFSTEP]
simp! [(· <$> ·)]
[GOAL]
α : Type ?u.94018
m n : ℕ
xs : Vector α n
ys : Vector α m
x : α
⊢ 0 < Nat.succ n + m
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
m n : ℕ
xs : Vector α n
ys : Vector α m
⊢ append xs nil = xs
[PROOFSTEP]
cases xs
[GOAL]
case mk
α : Type u_1
m n : ℕ
ys : Vector α m
val✝ : List α
property✝ : List.length val✝ = n
⊢ append { val := val✝, property := property✝ } nil = { val := val✝, property := property✝ }
[PROOFSTEP]
simp [append]
[GOAL]
α : Type u_2
β : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
γ : Type u_1
v₁ : Vector α n
v₂ : Vector β n
f : α → β → γ
i : Fin n
⊢ get (map₂ f v₁ v₂) i = f (get v₁ i) (get v₂ i)
[PROOFSTEP]
clear * - v₁ v₂
[GOAL]
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
v₁ : Vector α n
v₂ : Vector β n
f : α → β → γ
i : Fin n
⊢ get (map₂ f v₁ v₂) i = f (get v₁ i) (get v₂ i)
[PROOFSTEP]
induction v₁, v₂ using inductionOn₂
[GOAL]
case nil
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
i : Fin 0
⊢ get (map₂ f nil nil) i = f (get nil i) (get nil i)
case cons
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : ∀ (i : Fin n✝), get (map₂ f x✝ y✝) i = f (get x✝ i) (get y✝ i)
i : Fin (Nat.succ n✝)
⊢ get (map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝)) i = f (get (a✝¹ ::ᵥ x✝) i) (get (b✝ ::ᵥ y✝) i)
[PROOFSTEP]
case nil => exact Fin.elim0 i
[GOAL]
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
i : Fin 0
⊢ get (map₂ f nil nil) i = f (get nil i) (get nil i)
[PROOFSTEP]
case nil => exact Fin.elim0 i
[GOAL]
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
i : Fin 0
⊢ get (map₂ f nil nil) i = f (get nil i) (get nil i)
[PROOFSTEP]
exact Fin.elim0 i
[GOAL]
case cons
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : ∀ (i : Fin n✝), get (map₂ f x✝ y✝) i = f (get x✝ i) (get y✝ i)
i : Fin (Nat.succ n✝)
⊢ get (map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝)) i = f (get (a✝¹ ::ᵥ x✝) i) (get (b✝ ::ᵥ y✝) i)
[PROOFSTEP]
case cons x xs y ys ih =>
  rw [map₂_cons]
  cases i using Fin.cases
  · simp only [get_zero, head_cons]
  · simp only [get_cons_succ, ih]
[GOAL]
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
n✝ : ℕ
x : α
xs : β
y : Vector α n✝
ys : Vector β n✝
ih : ∀ (i : Fin n✝), get (map₂ f y ys) i = f (get y i) (get ys i)
i : Fin (Nat.succ n✝)
⊢ get (map₂ f (x ::ᵥ y) (xs ::ᵥ ys)) i = f (get (x ::ᵥ y) i) (get (xs ::ᵥ ys) i)
[PROOFSTEP]
case cons x xs y ys ih =>
  rw [map₂_cons]
  cases i using Fin.cases
  · simp only [get_zero, head_cons]
  · simp only [get_cons_succ, ih]
[GOAL]
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
n✝ : ℕ
x : α
xs : β
y : Vector α n✝
ys : Vector β n✝
ih : ∀ (i : Fin n✝), get (map₂ f y ys) i = f (get y i) (get ys i)
i : Fin (Nat.succ n✝)
⊢ get (map₂ f (x ::ᵥ y) (xs ::ᵥ ys)) i = f (get (x ::ᵥ y) i) (get (xs ::ᵥ ys) i)
[PROOFSTEP]
rw [map₂_cons]
[GOAL]
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
n✝ : ℕ
x : α
xs : β
y : Vector α n✝
ys : Vector β n✝
ih : ∀ (i : Fin n✝), get (map₂ f y ys) i = f (get y i) (get ys i)
i : Fin (Nat.succ n✝)
⊢ get (f x xs ::ᵥ map₂ f y ys) i = f (get (x ::ᵥ y) i) (get (xs ::ᵥ ys) i)
[PROOFSTEP]
cases i using Fin.cases
[GOAL]
case zero
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
n✝ : ℕ
x : α
xs : β
y : Vector α n✝
ys : Vector β n✝
ih : ∀ (i : Fin n✝), get (map₂ f y ys) i = f (get y i) (get ys i)
⊢ get (f x xs ::ᵥ map₂ f y ys) 0 = f (get (x ::ᵥ y) 0) (get (xs ::ᵥ ys) 0)
[PROOFSTEP]
simp only [get_zero, head_cons]
[GOAL]
case succ
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
n✝ : ℕ
x : α
xs : β
y : Vector α n✝
ys : Vector β n✝
ih : ∀ (i : Fin n✝), get (map₂ f y ys) i = f (get y i) (get ys i)
i✝ : Fin n✝
⊢ get (f x xs ::ᵥ map₂ f y ys) (Fin.succ i✝) = f (get (x ::ᵥ y) (Fin.succ i✝)) (get (xs ::ᵥ ys) (Fin.succ i✝))
[PROOFSTEP]
simp only [get_cons_succ, ih]
