case h_nil
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f nil) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) 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
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih :
  (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) xs
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f (x ::ᵥ xs)) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (x ::ᵥ xs)
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
x : Vector α n
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f x) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
induction' x using Vector.inductionOn with n x xs ih
case h_cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih :
  (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) xs
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f (x ::ᵥ xs)) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (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
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f nil) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) 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
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih :
  (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) xs
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f (x ::ᵥ xs)) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (x ::ᵥ xs)
. simp! [functor_norm, cast, η.preserves_pure]
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
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih :
  (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) xs
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f (x ::ᵥ xs)) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (x ::ᵥ xs)
. rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]
  rfl
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
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f nil) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) nil
simp! [functor_norm, cast, η.preserves_pure]
case h_cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih :
  (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) xs
⊢ (Seq.seq (cons <$> (fun {α} => ApplicativeTransformation.app η α) (f x)) fun x =>
      (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs)) =
    Seq.seq (cons <$> ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x) fun x =>
      (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f 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
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih :
  (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) xs
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f (x ::ᵥ xs)) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (x ::ᵥ xs)
rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]
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
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih :
  (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) xs
⊢ (Seq.seq (cons <$> (fun {α} => ApplicativeTransformation.app η α) (f x)) fun x =>
      (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs)) =
    Seq.seq (cons <$> ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x) fun x =>
      (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs)
rfl