mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case id_traverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {α_1 : Type u} (x : t α α_1), traverse pure x = pure x

pp: case comp_traverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    {α_1 β γ : Type u} (f : β → F γ) (g : α_1 → G β) (x : t α α_1),
    traverse (Comp.mk ∘ map f ∘ g) x = Comp.mk (traverse f <$> traverse g x)

pp: case traverse_eq_map_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {α_1 β : Type u} (f : α_1 → β) (x : t α α_1), traverse (pure ∘ f) x = pure (f <$> x)

pp: case naturality
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    (η : ApplicativeTransformation F G) {α_1 β : Type u} (f : α_1 → F β) (x : t α α_1),
    (fun {α} ↦ η.app α) (traverse f x) = traverse ((fun {α} ↦ η.app α) ∘ f) x

Tactic:
<;>

Goal state after:
case id_traverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {α_1 : Type u} (x : t α α_1), traverse pure x = pure x

case comp_traverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    {α_1 β γ : Type u} (f : β → F γ) (g : α_1 → G β) (x : t α α_1),
    traverse (Comp.mk ∘ map f ∘ g) x = Comp.mk (traverse f <$> traverse g x)

case traverse_eq_map_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {α_1 β : Type u} (f : α_1 → β) (x : t α α_1), traverse (pure ∘ f) x = pure (f <$> x)

case naturality
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    (η : ApplicativeTransformation F G) {α_1 β : Type u} (f : α_1 → F β) (x : t α α_1),
    (fun {α} ↦ η.app α) (traverse f x) = traverse ((fun {α} ↦ η.app α) ∘ f) x
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case id_traverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α α✝ : Type u
x✝ : t α α✝
⊢ traverse pure x✝ = pure x✝

pp: case comp_traverse
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
α : 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✝ : t α α✝
⊢ traverse (Comp.mk ∘ map f✝ ∘ g✝) x✝ = Comp.mk (traverse f✝ <$> traverse g✝ x✝)

pp: case traverse_eq_map_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : t α α✝
⊢ traverse (pure ∘ f✝) x✝ = pure (f✝ <$> x✝)

pp: case naturality
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
α : 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
f✝ : α✝ → F✝ β✝
x✝ : t α α✝
⊢ (fun {α} ↦ η✝.app α) (traverse f✝ x✝) = traverse ((fun {α} ↦ η✝.app α) ∘ f✝) x✝

Tactic:
<;>

Goal state after:
case id_traverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α α✝ : Type u
x✝ : t α α✝
⊢ traverse pure x✝ = pure x✝

case comp_traverse
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
α : 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✝ : t α α✝
⊢ traverse (Comp.mk ∘ map f✝ ∘ g✝) x✝ = Comp.mk (traverse f✝ <$> traverse g✝ x✝)

case traverse_eq_map_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : t α α✝
⊢ traverse (pure ∘ f✝) x✝ = pure (f✝ <$> x✝)

case naturality
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
α : 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
f✝ : α✝ → F✝ β✝
x✝ : t α α✝
⊢ (fun {α} ↦ η✝.app α) (traverse f✝ x✝) = traverse ((fun {α} ↦ η✝.app α) ∘ f✝) x✝
Module: Mathlib.Control.Fix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
⊢ ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f (n + 1).succ x'

Tactic:
| succ n n_ih =>

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case none
α : Type u_1
⊢ Option.traverse pure none = pure none

pp: case some
α : Type u_1
val✝ : α
⊢ Option.traverse pure (some val✝) = pure (some val✝)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
⊢ Option.traverse pure none = pure none

case some
α : Type u_1
val✝ : α
⊢ Option.traverse pure (some val✝) = pure (some val✝)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case none
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ Option.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) none = Comp.mk (Option.traverse f <$> Option.traverse g none)

pp: case some
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Option.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) (some val✝) =
    Comp.mk (Option.traverse f <$> Option.traverse g (some val✝))

Tactic:
<;>

Goal state after:
case none
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ Option.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) none = Comp.mk (Option.traverse f <$> Option.traverse g none)

case some
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Option.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) (some val✝) =
    Comp.mk (Option.traverse f <$> Option.traverse g (some val✝))
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case none
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ pure none = Comp.mk (pure (pure none))

Tactic:
<;>

Goal state after:
case none
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ pure none = Comp.mk (pure (pure none))
Module: Mathlib.Control.Traversable.Instances

Goal state before:

Tactic:
<;>

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case none
α β : Type u_1
f : α → β
⊢ Option.traverse (pure ∘ f) none = pure (f <$> none)

pp: case some
α β : Type u_1
f : α → β
val✝ : α
⊢ Option.traverse (pure ∘ f) (some val✝) = pure (f <$> some val✝)

Tactic:
<;>

Goal state after:
case none
α β : Type u_1
f : α → β
⊢ Option.traverse (pure ∘ f) none = pure (f <$> none)

case some
α β : Type u_1
f : α → β
val✝ : α
⊢ Option.traverse (pure ∘ f) (some val✝) = pure (f <$> some val✝)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case none
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
inst✝ : LawfulApplicative F
α : Type u_1
β : Type u
f : α → F β
⊢ (fun {α} ↦ η.app α) (Option.traverse f none) = Option.traverse ((fun {α} ↦ η.app α) ∘ f) none

pp: case some
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
inst✝ : LawfulApplicative F
α : Type u_1
β : Type u
f : α → F β
x : α
⊢ (fun {α} ↦ η.app α) (Option.traverse f (some x)) = Option.traverse ((fun {α} ↦ η.app α) ∘ f) (some x)

Tactic:
<;>

Goal state after:
case none
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
inst✝ : LawfulApplicative F
α : Type u_1
β : Type u
f : α → F β
⊢ (fun {α} ↦ η.app α) (Option.traverse f none) = Option.traverse ((fun {α} ↦ η.app α) ∘ f) none

case some
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
inst✝ : LawfulApplicative F
α : Type u_1
β : Type u
f : α → F β
x : α
⊢ (fun {α} ↦ η.app α) (Option.traverse f (some x)) = Option.traverse ((fun {α} ↦ η.app α) ∘ f) (some x)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case nil
α : Type u_1
⊢ List.traverse pure [] = pure []

pp: case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse pure tail✝ = pure tail✝
⊢ List.traverse pure (head✝ :: tail✝) = pure (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
⊢ List.traverse pure [] = pure []

case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse pure tail✝ = pure tail✝
⊢ List.traverse pure (head✝ :: tail✝) = pure (head✝ :: tail✝)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case nil
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) [] = Comp.mk (List.traverse f <$> List.traverse g [])

pp: case cons
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) tail✝ = Comp.mk (List.traverse f <$> List.traverse g tail✝)
⊢ List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) (head✝ :: tail✝) =
    Comp.mk (List.traverse f <$> List.traverse g (head✝ :: tail✝))

Tactic:
<;>

Goal state after:
case nil
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) [] = Comp.mk (List.traverse f <$> List.traverse g [])

case cons
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) tail✝ = Comp.mk (List.traverse f <$> List.traverse g tail✝)
⊢ List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) (head✝ :: tail✝) =
    Comp.mk (List.traverse f <$> List.traverse g (head✝ :: tail✝))
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case nil
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ pure [] = Comp.mk (pure (pure []))

pp: case cons
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) tail✝ = Comp.mk (List.traverse f <$> List.traverse g tail✝)
⊢ Comp.mk ((fun a ↦ (fun x2 ↦ cons <$> f a <*> x2) ∘ List.traverse f) <$> g head✝ <*> List.traverse g tail✝) =
    Comp.mk ((fun a ↦ List.traverse f ∘ cons a) <$> g head✝ <*> List.traverse g tail✝)

Tactic:
<;>

Goal state after:
case nil
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ pure [] = Comp.mk (pure (pure []))

case cons
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) tail✝ = Comp.mk (List.traverse f <$> List.traverse g tail✝)
⊢ Comp.mk ((fun a ↦ (fun x2 ↦ cons <$> f a <*> x2) ∘ List.traverse f) <$> g head✝ <*> List.traverse g tail✝) =
    Comp.mk ((fun a ↦ List.traverse f ∘ cons a) <$> g head✝ <*> List.traverse g tail✝)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case nil
α β : Type u_1
f : α → β
⊢ List.traverse (pure ∘ f) [] = pure (f <$> [])

pp: case cons
α β : 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✝))

Tactic:
<;>

Goal state after:
case nil
α β : Type u_1
f : α → β
⊢ List.traverse (pure ∘ f) [] = pure (f <$> [])

case cons
α β : 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✝))
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
⊢ (fun {α} ↦ η.app α) (List.traverse f []) = List.traverse ((fun {α} ↦ η.app α) ∘ f) []

pp: case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
head✝ : α
tail✝ : List α
tail_ih✝ : (fun {α} ↦ η.app α) (List.traverse f tail✝) = List.traverse ((fun {α} ↦ η.app α) ∘ f) tail✝
⊢ (fun {α} ↦ η.app α) (List.traverse f (head✝ :: tail✝)) = List.traverse ((fun {α} ↦ η.app α) ∘ f) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
⊢ (fun {α} ↦ η.app α) (List.traverse f []) = List.traverse ((fun {α} ↦ η.app α) ∘ f) []

case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
head✝ : α
tail✝ : List α
tail_ih✝ : (fun {α} ↦ η.app α) (List.traverse f tail✝) = List.traverse ((fun {α} ↦ η.app α) ∘ f) tail✝
⊢ (fun {α} ↦ η.app α) (List.traverse f (head✝ :: tail✝)) = List.traverse ((fun {α} ↦ η.app α) ∘ f) (head✝ :: tail✝)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ : Type u
G : Type u → Type u
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : σ
⊢ Sum.traverse f (g <$> inl val✝) = Sum.traverse (f ∘ g) (inl val✝)

pp: case inr
σ : Type u
G : Type u → Type u
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : α
⊢ Sum.traverse f (g <$> inr val✝) = Sum.traverse (f ∘ g) (inr val✝)

Tactic:
<;>

Goal state after:
case inl
σ : Type u
G : Type u → Type u
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : σ
⊢ Sum.traverse f (g <$> inl val✝) = Sum.traverse (f ∘ g) (inl val✝)

case inr
σ : Type u
G : Type u → Type u
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : α
⊢ Sum.traverse f (g <$> inr val✝) = Sum.traverse (f ∘ g) (inr val✝)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ : Type u
G : Type u → Type u
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✝)

pp: case inr
σ : Type u
G : Type u → Type u
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✝)

Tactic:
<;>

Goal state after:
case inl
σ : Type u
G : Type u → Type u
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✝)

case inr
σ : Type u
G : Type u → Type u
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✝)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ α : Type u_1
val✝ : σ
⊢ Sum.traverse pure (inl val✝) = inl val✝

pp: case inr
σ α : Type u_1
val✝ : α
⊢ Sum.traverse pure (inr val✝) = inr val✝

Tactic:
<;>

Goal state after:
case inl
σ α : Type u_1
val✝ : σ
⊢ Sum.traverse pure (inl val✝) = inl val✝

case inr
σ α : Type u_1
val✝ : α
⊢ Sum.traverse pure (inr val✝) = inr val✝
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ : Type u
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : σ
⊢ Sum.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) (inl val✝) = Comp.mk (Sum.traverse f <$> Sum.traverse g (inl val✝))

pp: case inr
σ : Type u
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Sum.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) (inr val✝) = Comp.mk (Sum.traverse f <$> Sum.traverse g (inr val✝))

Tactic:
<;>

Goal state after:
case inl
σ : Type u
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : σ
⊢ Sum.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) (inl val✝) = Comp.mk (Sum.traverse f <$> Sum.traverse g (inl val✝))

case inr
σ : Type u
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Sum.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) (inr val✝) = Comp.mk (Sum.traverse f <$> Sum.traverse g (inr val✝))
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ : Type u
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : σ
⊢ pure (inl val✝) = Comp.mk (pure (pure (inl val✝)))

Tactic:
<;>

Goal state after:
case inl
σ : Type u
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : σ
⊢ pure (inl val✝) = Comp.mk (pure (pure (inl val✝)))
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ α β : Type u
f : α → β
val✝ : σ
⊢ Sum.traverse (pure ∘ f) (inl val✝) = pure (f <$> inl val✝)

pp: case inr
σ α β : Type u
f : α → β
val✝ : α
⊢ Sum.traverse (pure ∘ f) (inr val✝) = pure (f <$> inr val✝)

Tactic:
<;>

Goal state after:
case inl
σ α β : Type u
f : α → β
val✝ : σ
⊢ Sum.traverse (pure ∘ f) (inl val✝) = pure (f <$> inl val✝)

case inr
σ α β : Type u
f : α → β
val✝ : α
⊢ Sum.traverse (pure ∘ f) (inr val✝) = pure (f <$> inr val✝)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ α β : Type u
f : α → β
val✝ : σ
⊢ pure (inl val✝) = pure (f <$> inl val✝)

pp: case inr
σ α β : Type u
f : α → β
val✝ : α
⊢ pure (inr (f val✝)) = pure (f <$> inr val✝)

Tactic:
<;>

Goal state after:
case inl
σ α β : Type u
f : α → β
val✝ : σ
⊢ pure (inl val✝) = pure (f <$> inl val✝)

case inr
σ α β : Type u
f : α → β
val✝ : α
⊢ pure (inr (f val✝)) = pure (f <$> inr val✝)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : σ
⊢ (fun x ↦ f <$> x) <$> Sum.traverse g (inl val✝) = Sum.traverse (fun x ↦ f <$> g x) (inl val✝)

pp: case inr
σ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : α
⊢ (fun x ↦ f <$> x) <$> Sum.traverse g (inr val✝) = Sum.traverse (fun x ↦ f <$> g x) (inr val✝)

Tactic:
<;>

Goal state after:
case inl
σ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : σ
⊢ (fun x ↦ f <$> x) <$> Sum.traverse g (inl val✝) = Sum.traverse (fun x ↦ f <$> g x) (inl val✝)

case inr
σ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : α
⊢ (fun x ↦ f <$> x) <$> Sum.traverse g (inr val✝) = Sum.traverse (fun x ↦ f <$> g x) (inr val✝)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : σ
⊢ pure (f <$> inl val✝) = pure (inl val✝)

pp: case inr
σ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : α
⊢ (fun a ↦ f <$> inr a) <$> g val✝ = (fun a ↦ inr (f a)) <$> g val✝

Tactic:
<;>

Goal state after:
case inl
σ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : σ
⊢ pure (f <$> inl val✝) = pure (inl val✝)

case inr
σ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : α
⊢ (fun a ↦ f <$> inr a) <$> g val✝ = (fun a ↦ inr (f a)) <$> g val✝
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
val✝ : σ
⊢ (fun {α} ↦ η.app α) (Sum.traverse f (inl val✝)) = Sum.traverse ((fun {α} ↦ η.app α) ∘ f) (inl val✝)

pp: case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
val✝ : α
⊢ (fun {α} ↦ η.app α) (Sum.traverse f (inr val✝)) = Sum.traverse ((fun {α} ↦ η.app α) ∘ f) (inr val✝)

Tactic:
<;>

Goal state after:
case inl
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
val✝ : σ
⊢ (fun {α} ↦ η.app α) (Sum.traverse f (inl val✝)) = Sum.traverse ((fun {α} ↦ η.app α) ∘ f) (inl val✝)

case inr
σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
val✝ : α
⊢ (fun {α} ↦ η.app α) (Sum.traverse f (inr val✝)) = Sum.traverse ((fun {α} ↦ η.app α) ∘ f) (inr val✝)