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) }
n : ℕ
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
⊢ ∀ (x : Vector α n), Vector.traverse pure x = x
rintro ⟨x, rfl⟩
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) }
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) }
dsimp [Vector.traverse, cast]
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 []) }

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)) }
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) }
induction' x with x xs IH
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)) }
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)) }
simp! [IH]
no goals
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)) }
rfl
no goals
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 []) }
rfl