-- Mathlib/Data/Vector/Basic.lean
theorem naturality {α β : Type u} (f : α → F β) (x : Vector α n) :
    η (x.traverse f) = x.traverse (@η _ ∘ f)

Proof state:
case cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih : (fun {α} => η.app α) (Vector.traverse f xs) = Vector.traverse ((fun {α} => η.app α) ∘ f) xs
⊢ (fun {α} => η.app α) (Vector.traverse f (x ::ᵥ xs)) = Vector.traverse ((fun {α} => η.app α) ∘ f) (x ::ᵥ xs)

Tactic:
rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]

Result:
case cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih : (fun {α} => η.app α) (Vector.traverse f xs) = Vector.traverse ((fun {α} => η.app α) ∘ f) xs
⊢ cons <$> (fun {α} => η.app α) (f x) <*> (fun {α} => η.app α) (Vector.traverse f xs) =
    cons <$> ((fun {α} => η.app α) ∘ f) x <*> (fun {α} => η.app α) (Vector.traverse f xs)

Proof state:
case nil
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
⊢ (fun {α} => η.app α) (Vector.traverse f nil) = Vector.traverse ((fun {α} => η.app α) ∘ f) nil

Tactic:
simp! [functor_norm, cast, η.preserves_pure]

Result:
no goals

Proof state:
case cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih : (fun {α} => η.app α) (Vector.traverse f xs) = Vector.traverse ((fun {α} => η.app α) ∘ f) xs
⊢ cons <$> (fun {α} => η.app α) (f x) <*> (fun {α} => η.app α) (Vector.traverse f xs) =
    cons <$> ((fun {α} => η.app α) ∘ f) x <*> (fun {α} => η.app α) (Vector.traverse f xs)

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
x : Vector α n
⊢ (fun {α} => η.app α) (Vector.traverse f x) = Vector.traverse ((fun {α} => η.app α) ∘ f) x

Tactic:
induction' x with n x xs ih

Result:
case nil
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
⊢ (fun {α} => η.app α) (Vector.traverse f nil) = Vector.traverse ((fun {α} => η.app α) ∘ f) nil

case cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih : (fun {α} => η.app α) (Vector.traverse f xs) = Vector.traverse ((fun {α} => η.app α) ∘ f) xs
⊢ (fun {α} => η.app α) (Vector.traverse f (x ::ᵥ xs)) = Vector.traverse ((fun {α} => η.app α) ∘ f) (x ::ᵥ xs)