[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
x : Option α
⊢ Option.traverse pure x = x
[PROOFSTEP]
cases x
[GOAL]
case none
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
⊢ Option.traverse pure none = none
[PROOFSTEP]
rfl
[GOAL]
case some
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
val✝ : α
⊢ Option.traverse pure (some val✝) = some val✝
[PROOFSTEP]
rfl
[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : Option α
⊢ Option.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) x = Comp.mk (Option.traverse f <$> Option.traverse g x)
[PROOFSTEP]
cases x
[GOAL]
case none
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ Option.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) none =
    Comp.mk (Option.traverse f <$> Option.traverse g none)
[PROOFSTEP]
simp! [functor_norm]
[GOAL]
case some
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Option.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) (some val✝) =
    Comp.mk (Option.traverse f <$> Option.traverse g (some val✝))
[PROOFSTEP]
simp! [functor_norm]
[GOAL]
case none
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ pure none = Comp.mk (pure (pure none))
[PROOFSTEP]
rfl
[GOAL]
case some
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Comp.mk (((fun x => some <$> x) ∘ f) <$> g val✝) = Comp.mk ((Option.traverse f ∘ some) <$> g val✝)
[PROOFSTEP]
rfl
[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u_1
f : α → β
x : Option α
⊢ Option.traverse (pure ∘ f) x = pure (f <$> x)
[PROOFSTEP]
cases x
[GOAL]
case none
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u_1
f : α → β
⊢ Option.traverse (pure ∘ f) none = pure (f <$> none)
[PROOFSTEP]
rfl
[GOAL]
case some
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u_1
f : α → β
val✝ : α
⊢ Option.traverse (pure ∘ f) (some val✝) = pure (f <$> some val✝)
[PROOFSTEP]
rfl
[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : Option α
⊢ (fun {α} => ApplicativeTransformation.app η α) (Option.traverse f x) =
    Option.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
[PROOFSTEP]
cases' x with x
[GOAL]
case none
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
⊢ (fun {α} => ApplicativeTransformation.app η α) (Option.traverse f none) =
    Option.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) none
[PROOFSTEP]
simp! [*, functor_norm, ApplicativeTransformation.preserves_map, ApplicativeTransformation.preserves_seq,
  ApplicativeTransformation.preserves_pure]
[GOAL]
case some
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : α
⊢ (fun {α} => ApplicativeTransformation.app η α) (Option.traverse f (some x)) =
    Option.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (some x)
[PROOFSTEP]
simp! [*, functor_norm, ApplicativeTransformation.preserves_map, ApplicativeTransformation.preserves_seq,
  ApplicativeTransformation.preserves_pure]
[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
xs : List α
⊢ List.traverse pure xs = xs
[PROOFSTEP]
induction xs
[GOAL]
case nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
⊢ List.traverse pure [] = []
[PROOFSTEP]
simp! [*, List.traverse, functor_norm]
[GOAL]
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse pure tail✝ = tail✝
⊢ List.traverse pure (head✝ :: tail✝) = head✝ :: tail✝
[PROOFSTEP]
simp! [*, List.traverse, functor_norm]
[GOAL]
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse pure tail✝ = tail✝
⊢ (Seq.seq (cons head✝) fun x => tail✝) = head✝ :: tail✝
[PROOFSTEP]
rfl
[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : List α
⊢ List.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) x = Comp.mk (List.traverse f <$> List.traverse g x)
[PROOFSTEP]
induction x
[GOAL]
case nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ List.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) [] = Comp.mk (List.traverse f <$> List.traverse g [])
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
head✝ : α
tail✝ : List α
tail_ih✝ :
  List.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) tail✝ = Comp.mk (List.traverse f <$> List.traverse g tail✝)
⊢ List.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) (head✝ :: tail✝) =
    Comp.mk (List.traverse f <$> List.traverse g (head✝ :: tail✝))
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ pure [] = Comp.mk (pure (pure []))
[PROOFSTEP]
rfl
[GOAL]
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
head✝ : α
tail✝ : List α
tail_ih✝ :
  List.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) tail✝ = Comp.mk (List.traverse f <$> List.traverse g tail✝)
⊢ Comp.mk
      (Seq.seq
        (((fun x => x ∘ List.traverse f) ∘ (fun x x_1 => Seq.seq x fun x => x_1) ∘ (fun x => cons <$> x) ∘ f) <$>
          g head✝)
        fun x => List.traverse g tail✝) =
    Comp.mk (Seq.seq (((fun x => List.traverse f ∘ x) ∘ cons) <$> g head✝) fun x => List.traverse g tail✝)
[PROOFSTEP]
rfl
[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u_1
f : α → β
x : List α
⊢ List.traverse (pure ∘ f) x = pure (f <$> x)
[PROOFSTEP]
induction x
[GOAL]
case nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u_1
f : α → β
⊢ List.traverse (pure ∘ f) [] = pure (f <$> [])
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u_1
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse (pure ∘ f) tail✝ = pure (f <$> tail✝)
⊢ List.traverse (pure ∘ f) (head✝ :: tail✝) = pure (f <$> (head✝ :: tail✝))
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u_1
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse (pure ∘ f) tail✝ = pure (f <$> tail✝)
⊢ (Seq.seq (cons (f head✝)) fun x => map f tail✝) = f head✝ :: map f tail✝
[PROOFSTEP]
rfl
[GOAL]
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : List α
⊢ (fun {α} => ApplicativeTransformation.app η α) (List.traverse f x) =
    List.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
[PROOFSTEP]
induction x
[GOAL]
case nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
⊢ (fun {α} => ApplicativeTransformation.app η α) (List.traverse f []) =
    List.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) []
[PROOFSTEP]
simp! [*, functor_norm, ApplicativeTransformation.preserves_map, ApplicativeTransformation.preserves_seq,
  ApplicativeTransformation.preserves_pure]
[GOAL]
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
head✝ : α
tail✝ : List α
tail_ih✝ :
  (fun {α} => ApplicativeTransformation.app η α) (List.traverse f tail✝) =
    List.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) tail✝
⊢ (fun {α} => ApplicativeTransformation.app η α) (List.traverse f (head✝ :: tail✝)) =
    List.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (head✝ :: tail✝)
[PROOFSTEP]
simp! [*, functor_norm, ApplicativeTransformation.preserves_map, ApplicativeTransformation.preserves_seq,
  ApplicativeTransformation.preserves_pure]
[GOAL]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
bs : List α'
⊢ traverse f ([] ++ bs) = Seq.seq ((fun x x_1 => x ++ x_1) <$> traverse f []) fun x => traverse f bs
[PROOFSTEP]
simp [functor_norm]
[GOAL]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ traverse f (a :: as ++ bs) = Seq.seq ((fun x x_1 => x ++ x_1) <$> traverse f (a :: as)) fun x => traverse f bs
[PROOFSTEP]
simp [traverse_append as bs, functor_norm]
[GOAL]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ (Seq.seq
      (Seq.seq (((fun x => x ∘ fun x x_1 => x ++ x_1) ∘ Function.comp ∘ fun x x_1 => x :: x_1) <$> f a) fun x =>
        traverse f as)
      fun x => traverse f bs) =
    Seq.seq (Seq.seq (((fun x => (fun x x_1 => x ++ x_1) ∘ x) ∘ fun x x_1 => x :: x_1) <$> f a) fun x => traverse f as)
      fun x => traverse f bs
[PROOFSTEP]
congr
[GOAL]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f✝ : α' → F β'
inst✝ : LawfulApplicative F
f : α' → Set β'
⊢ [] ∈ traverse f [] ↔ Forall₂ (fun b a => b ∈ f a) [] []
[PROOFSTEP]
simp
[GOAL]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f✝ : α' → F β'
inst✝ : LawfulApplicative F
f : α' → Set β'
a : α'
as : List α'
⊢ [] ∈ traverse f (a :: as) ↔ Forall₂ (fun b a => b ∈ f a) [] (a :: as)
[PROOFSTEP]
simp
[GOAL]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f✝ : α' → F β'
inst✝ : LawfulApplicative F
f : α' → Set β'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f [] ↔ Forall₂ (fun b a => b ∈ f a) (b :: bs) []
[PROOFSTEP]
simp
[GOAL]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f✝ : α' → F β'
inst✝ : LawfulApplicative F
f : α' → Set β'
a : α'
as : List α'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f (a :: as) ↔ Forall₂ (fun b a => b ∈ f a) (b :: bs) (a :: as)
[PROOFSTEP]
simp [mem_traverse as bs]
[GOAL]
σ : Type u
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
x : σ ⊕ α
⊢ Sum.traverse f (g <$> x) = Sum.traverse (f ∘ g) x
[PROOFSTEP]
cases x
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : σ
⊢ Sum.traverse f (g <$> inl val✝) = Sum.traverse (f ∘ g) (inl val✝)
[PROOFSTEP]
simp [Sum.traverse, id_map, functor_norm]
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : α
⊢ Sum.traverse f (g <$> inr val✝) = Sum.traverse (f ∘ g) (inr val✝)
[PROOFSTEP]
simp [Sum.traverse, id_map, functor_norm]
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : σ
⊢ (match g <$> inl val✝ with
    | inl x => pure (inl x)
    | inr x => inr <$> f x) =
    pure (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : α
⊢ (match g <$> inr val✝ with
    | inl x => pure (inl x)
    | inr x => inr <$> f x) =
    inr <$> f (g val✝)
[PROOFSTEP]
rfl
[GOAL]
σ✝ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
σ α : Type u_1
x : σ ⊕ α
⊢ Sum.traverse pure x = x
[PROOFSTEP]
cases x
[GOAL]
case inl
σ✝ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
σ α : Type u_1
val✝ : σ
⊢ Sum.traverse pure (inl val✝) = inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr
σ✝ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
σ α : Type u_1
val✝ : α
⊢ Sum.traverse pure (inr val✝) = inr val✝
[PROOFSTEP]
rfl
[GOAL]
σ : Type u
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 : σ ⊕ α
⊢ Sum.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) x = Comp.mk (Sum.traverse f <$> Sum.traverse g x)
[PROOFSTEP]
cases x
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : σ
⊢ Sum.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) (inl val✝) =
    Comp.mk (Sum.traverse f <$> Sum.traverse g (inl val✝))
[PROOFSTEP]
simp! [Sum.traverse, map_id, functor_norm]
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Sum.traverse (Comp.mk ∘ (fun x x_1 => x <$> x_1) f ∘ g) (inr val✝) =
    Comp.mk (Sum.traverse f <$> Sum.traverse g (inr val✝))
[PROOFSTEP]
simp! [Sum.traverse, map_id, functor_norm]
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : σ
⊢ pure (inl val✝) = Comp.mk (pure (pure (inl val✝)))
[PROOFSTEP]
rfl
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Comp.mk (((fun x => inr <$> x) ∘ f) <$> g val✝) = Comp.mk ((Sum.traverse f ∘ inr) <$> g val✝)
[PROOFSTEP]
rfl
[GOAL]
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
f : α → β
x : σ ⊕ α
⊢ Sum.traverse (pure ∘ f) x = pure (f <$> x)
[PROOFSTEP]
induction x
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
f : α → β
val✝ : σ
⊢ Sum.traverse (pure ∘ f) (inl val✝) = pure (f <$> inl val✝)
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
f : α → β
val✝ : α
⊢ Sum.traverse (pure ∘ f) (inr val✝) = pure (f <$> inr val✝)
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
f : α → β
val✝ : σ
⊢ inl val✝ = f <$> inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
f : α → β
val✝ : α
⊢ inr (f val✝) = f <$> inr val✝
[PROOFSTEP]
rfl
[GOAL]
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
x : σ ⊕ α
⊢ (fun x x_1 => x <$> x_1) f <$> Sum.traverse g x = Sum.traverse ((fun x x_1 => x <$> x_1) f ∘ g) x
[PROOFSTEP]
cases x
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : σ
⊢ (fun x x_1 => x <$> x_1) f <$> Sum.traverse g (inl val✝) = Sum.traverse ((fun x x_1 => x <$> x_1) f ∘ g) (inl val✝)
[PROOFSTEP]
simp [Sum.traverse, id_map, functor_norm]
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : α
⊢ (fun x x_1 => x <$> x_1) f <$> Sum.traverse g (inr val✝) = Sum.traverse ((fun x x_1 => x <$> x_1) f ∘ g) (inr val✝)
[PROOFSTEP]
simp [Sum.traverse, id_map, functor_norm]
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : σ
⊢ pure (f <$> inl val✝) = pure (inl val✝)
[PROOFSTEP]
congr
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : α
⊢ ((fun x => f <$> x) ∘ inr) <$> g val✝ = (inr ∘ f) <$> g val✝
[PROOFSTEP]
congr
[GOAL]
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : σ ⊕ α
⊢ (fun {α} => ApplicativeTransformation.app η α) (Sum.traverse f x) =
    Sum.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
[PROOFSTEP]
cases x
[GOAL]
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
val✝ : σ
⊢ (fun {α} => ApplicativeTransformation.app η α) (Sum.traverse f (inl val✝)) =
    Sum.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (inl val✝)
[PROOFSTEP]
simp! [Sum.traverse, functor_norm, ApplicativeTransformation.preserves_map, ApplicativeTransformation.preserves_seq,
  ApplicativeTransformation.preserves_pure]
[GOAL]
case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
val✝ : α
⊢ (fun {α} => ApplicativeTransformation.app η α) (Sum.traverse f (inr val✝)) =
    Sum.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (inr val✝)
[PROOFSTEP]
simp! [Sum.traverse, functor_norm, ApplicativeTransformation.preserves_map, ApplicativeTransformation.preserves_seq,
  ApplicativeTransformation.preserves_pure]
