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) })
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)
rintro ⟨x, rfl⟩
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) }
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) })
simp!
no goals
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) }
induction x <;> simp! [*, functor_norm] <;> rfl