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))
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)
induction' x using Vector.inductionOn with n x xs ih
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))

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))
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))
simp! [cast, *, functor_norm]
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))
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))

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))
. rfl
no goals
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))
. rw [Vector.traverse_def, ih]
  simp [functor_norm, (. ∘ .)]
no goals
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))
rfl
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))
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))
rw [Vector.traverse_def, ih]
no goals
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))
simp [functor_norm, (. ∘ .)]