case h
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ σ : Type u
f : α → β
x✝ : F α
⊢ (fun x x_1 => Seq.seq x fun x => x_1) (pure f) x✝ = (fun x x_1 => x <$> x_1) f x✝
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ σ : Type u
f : α → β
⊢ (fun x x_1 => Seq.seq x fun x => x_1) (pure f) = (fun x x_1 => x <$> x_1) f
ext
no goals
case h
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ σ : Type u
f : α → β
x✝ : F α
⊢ (fun x x_1 => Seq.seq x fun x => x_1) (pure f) x✝ = (fun x x_1 => x <$> x_1) f x✝
simp [functor_norm]