-- Mathlib/Data/Vector/Basic.lean
theorem comp_traverse (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)

Proof state:
case cons
n✝ : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
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)
⊢ cons <$> (Comp.mk ∘ Functor.map f ∘ g) x <*> Comp.mk (Vector.traverse f <$> Vector.traverse g xs) =
    Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ xs))

Tactic:
simp [functor_norm, Function.comp_def]

Result:
no goals

Proof state:
case cons
n✝ : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
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))

Tactic:
rw [Vector.traverse_def, ih]

Result:
case cons
n✝ : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
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)
⊢ cons <$> (Comp.mk ∘ Functor.map f ∘ g) x <*> Comp.mk (Vector.traverse f <$> Vector.traverse g xs) =
    Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ xs))

Proof state:
n : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
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)

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
α β γ : 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 cons
n✝ : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
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))

Proof state:
case nil
n : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
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)

Tactic:
simp! [cast, *, functor_norm]

Result:
case nil
n : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
⊢ pure nil = Comp.mk (pure (pure nil))

Proof state:
case nil
n : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
⊢ pure nil = Comp.mk (pure (pure nil))

Tactic:
rfl

Result:
no goals