awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
inst_3 : LawfulApplicative F
η : ApplicativeTransformation F G
⊢ LawfulTraversable List

Tactic:
{ show LawfulMonad List from inferInstance with
    id_traverse := List.id_traverse
    comp_traverse := List.comp_traverse
    traverse_eq_map_id := List.traverse_eq_map_id
    naturality := List.naturality }

Premises used: LawfulTraversable.mk, inferInstance, List.comp_traverse, List.naturality, List.id_traverse, List.traverse_eq_map_id
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F : Type u → Type u
inst : Applicative F
α' β' : Type u
f : α' → F β'
⊢ traverse f [] = pure []

Tactic:
rfl

Premises used: List.traverse, rfl
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F : Type u → Type u
inst : Applicative F
α' β' : Type u
f : α' → F β'
a : α'
l : List α'
⊢ traverse f (a :: l) = (fun (x1 : β') (x2 : List β') ↦ x1 :: x2) <$> f a <*> traverse f l

Tactic:
rfl

Premises used: List.traverse, rfl
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F : Type u → Type u
inst : Applicative F
α' β' : Type u
f : α' → F β'
inst_1 : LawfulApplicative F
bs : List α'
⊢ traverse f ([] ++ bs) = (fun (x1 x2 : List β') ↦ x1 ++ x2) <$> traverse f [] <*> traverse f bs

Tactic:
simp [functor_norm]
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F : Type u → Type u
inst : Applicative F
α' β' : Type u
f : α' → F β'
inst_1 : LawfulApplicative F
a : α'
as bs : List α'
simp :
  Eq (α := F (List β'))
    ((fun (a : β') ↦
            Function.comp (β := List β' → List β') (Function.comp fun (x2 : List β') ↦ a :: x2) fun (x1 x2 : List β') ↦
              x1 ++ x2) <$>
          f a <*>
        traverse f as <*>
      traverse f bs)
    ((fun (a : β') ↦ (fun (x1 x2 : List β') ↦ x1 ++ x2) ∘ fun (x2 : List β') ↦ a :: x2) <$> f a <*> traverse f as <*>
      traverse f bs)
⊢ traverse f (a :: as ++ bs) = (fun (x1 x2 : List β') ↦ x1 ++ x2) <$> traverse f (a :: as) <*> traverse f bs

Tactic:
simp [traverse_append as bs, functor_norm]
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F : Type u → Type u
inst : Applicative F
α' β' : Type u
f : α' → F β'
inst_1 : LawfulApplicative F
a : α'
as bs : List α'
⊢ Eq (α := F (List β'))
    ((fun (a : β') ↦
            Function.comp (β := List β' → List β') (Function.comp fun (x2 : List β') ↦ a :: x2) fun (x1 x2 : List β') ↦
              x1 ++ x2) <$>
          f a <*>
        traverse f as <*>
      traverse f bs)
    ((fun (a : β') ↦ (fun (x1 x2 : List β') ↦ x1 ++ x2) ∘ fun (x2 : List β') ↦ a :: x2) <$> f a <*> traverse f as <*>
      traverse f bs)

Tactic:
congr
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α' β' : Type u
f : α' → Set β'
⊢ [] ∈ traverse f [] ↔ Forall₂ (fun (b : β') (a : α') ↦ b ∈ f a) [] []

Tactic:
simp
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α' β' : Type u
f : α' → Set β'
a : α'
as : List α'
⊢ [] ∈ traverse f (a :: as) ↔ Forall₂ (fun (b : β') (a : α') ↦ b ∈ f a) [] (a :: as)

Tactic:
simp
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α' β' : Type u
f : α' → Set β'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f [] ↔ Forall₂ (fun (b : β') (a : α') ↦ b ∈ f a) (b :: bs) []

Tactic:
simp
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α' β' : Type u
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)

Tactic:
simp [mem_traverse as bs]
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
x : σ ⊕ α
inl : ∀ (val : σ), Sum.traverse f (g <$> Sum.inl val) = Sum.traverse (f ∘ g) (Sum.inl val)
inr : ∀ (val : α), Eq (α := G (σ ⊕ γ)) (Sum.traverse f (g <$> Sum.inr val)) (Sum.traverse (f ∘ g) (Sum.inr val))
⊢ Sum.traverse f (g <$> x) = Sum.traverse (f ∘ g) x

Tactic:
cases x
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val : σ
inl :
  Eq (α := G (σ ⊕ γ))
    (match (motive := σ ⊕ β → G (σ ⊕ γ)) g <$> Sum.inl val with
      | Sum.inl x => pure (Sum.inl x)
      | inr x => inr <$> f x :
      G (σ ⊕ γ))
    (pure (Sum.inl val) : G (σ ⊕ γ))
⊢ Sum.traverse f (g <$> Sum.inl val) = Sum.traverse (f ∘ g) (Sum.inl val)

Tactic:
simp [Sum.traverse, functor_norm]

Premises used: Sum.traverse
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val : α
inr :
  Eq (α := G (σ ⊕ γ))
    (match (motive := σ ⊕ β → G (σ ⊕ γ)) g <$> Sum.inr val with
      | inl x => pure (inl x)
      | Sum.inr x => Sum.inr <$> f x :
      G (σ ⊕ γ))
    (Sum.inr <$> f (g val) : G (σ ⊕ γ))
⊢ Eq (α := G (σ ⊕ γ)) (Sum.traverse f (g <$> Sum.inr val)) (Sum.traverse (f ∘ g) (Sum.inr val))

Tactic:
simp [Sum.traverse, functor_norm]

Premises used: Sum.traverse
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val : σ
⊢ Eq (α := G (σ ⊕ γ))
    (match (motive := σ ⊕ β → G (σ ⊕ γ)) g <$> inl val with
      | inl x => pure (inl x)
      | inr x => inr <$> f x :
      G (σ ⊕ γ))
    (pure (inl val) : G (σ ⊕ γ))

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val : α
⊢ Eq (α := G (σ ⊕ γ))
    (match (motive := σ ⊕ β → G (σ ⊕ γ)) g <$> inr val with
      | inl x => pure (inl x)
      | inr x => inr <$> f x :
      G (σ ⊕ γ))
    (inr <$> f (g val) : G (σ ⊕ γ))

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ α : Type u_1
x : σ ⊕ α
inl : ∀ (val : σ), Eq (α := Id (σ ⊕ α)) (Sum.traverse pure (Sum.inl val) : Id (σ ⊕ α)) (Sum.inl val : σ ⊕ α)
inr : ∀ (val : α), Eq (α := Id (σ ⊕ α)) (Sum.traverse pure (Sum.inr val)) (Sum.inr val)
⊢ Sum.traverse pure x = x

Tactic:
cases x
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ α : Type u_1
val : σ
⊢ Eq (α := Id (σ ⊕ α)) (Sum.traverse pure (inl val) : Id (σ ⊕ α)) (inl val : σ ⊕ α)

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ α : Type u_1
val : α
⊢ Eq (α := Id (σ ⊕ α)) (Sum.traverse pure (inr val)) (inr val)

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : σ ⊕ α
inl :
  ∀ (val : σ),
    Sum.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (Sum.inl val) =
      Comp.mk (Sum.traverse f <$> Sum.traverse g (Sum.inl val))
inr :
  ∀ (val : α),
    Eq (α := Comp G F (σ ⊕ γ)) (Sum.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (Sum.inr val))
      (Comp.mk (Sum.traverse f <$> Sum.traverse g (Sum.inr val)))
⊢ Sum.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) x = Comp.mk (Sum.traverse f <$> Sum.traverse g x)

Tactic:
cases x
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val : σ
inl : Eq (α := Comp G F (σ ⊕ γ)) (pure (Sum.inl val)) (Comp.mk (pure (pure (Sum.inl val))))
⊢ Sum.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (Sum.inl val) =
    Comp.mk (Sum.traverse f <$> Sum.traverse g (Sum.inl val))

Tactic:
simp! [Sum.traverse, map_id, functor_norm]

Premises used: Sum.traverse, Functor.map_id
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val : σ
⊢ Eq (α := Comp G F (σ ⊕ γ)) (pure (inl val)) (Comp.mk (pure (pure (inl val))))

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val : α
⊢ Eq (α := Comp G F (σ ⊕ γ)) (Sum.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (inr val))
    (Comp.mk (Sum.traverse f <$> Sum.traverse g (inr val)))

Tactic:
simp! [Sum.traverse, map_id, functor_norm]

Premises used: Sum.traverse, Functor.map_id
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ α β : Type u
f : α → β
x : σ ⊕ α
inl : ∀ (val : σ), Eq (α := Id (σ ⊕ β)) (Sum.traverse (pure ∘ f) (Sum.inl val)) (pure (f <$> Sum.inl val))
inr : ∀ (val : α), Eq (α := Id (σ ⊕ β)) (Sum.traverse (pure ∘ f) (Sum.inr val)) (pure (f <$> Sum.inr val))
⊢ Eq (α := Id (σ ⊕ β)) (Sum.traverse (pure ∘ f) x) (pure (f <$> x))

Tactic:
induction x
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ α β : Type u
f : α → β
val : α
inr : Eq (α := Id (σ ⊕ β)) (pure (Sum.inr (f val))) (pure (f <$> Sum.inr val))
⊢ Eq (α := Id (σ ⊕ β)) (Sum.traverse (pure ∘ f) (Sum.inr val)) (pure (f <$> Sum.inr val))

Tactic:
simp! [*, functor_norm]
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ α β : Type u
f : α → β
val : σ
⊢ Eq (α := Id (σ ⊕ β)) (pure (inl val)) (pure (f <$> inl val))

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ α β : Type u
f : α → β
val : α
⊢ Eq (α := Id (σ ⊕ β)) (pure (inr (f val))) (pure (f <$> inr val))

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
inst_1 : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
x : σ ⊕ α
inl :
  ∀ (val : σ),
    Eq (α := G (σ ⊕ γ)) ((fun (x : σ ⊕ β) ↦ f <$> x) <$> Sum.traverse g (Sum.inl val))
      (Sum.traverse (fun (x : α) ↦ f <$> g x) (Sum.inl val))
inr :
  ∀ (val : α),
    Eq (α := G (σ ⊕ γ)) ((fun (x : σ ⊕ β) ↦ f <$> x) <$> Sum.traverse g (Sum.inr val))
      (Sum.traverse (fun (x : α) ↦ f <$> g x) (Sum.inr val))
⊢ Eq (α := G (σ ⊕ γ)) ((fun (x : σ ⊕ β) ↦ f <$> x) <$> Sum.traverse g x) (Sum.traverse (fun (x : α) ↦ f <$> g x) x)

Tactic:
cases x
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
inst_1 : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val : σ
inl : Eq (α := G (σ ⊕ γ)) (pure (f <$> Sum.inl val)) (pure (Sum.inl val))
⊢ Eq (α := G (σ ⊕ γ)) ((fun (x : σ ⊕ β) ↦ f <$> x) <$> Sum.traverse g (Sum.inl val))
    (Sum.traverse (fun (x : α) ↦ f <$> g x) (Sum.inl val))

Tactic:
simp [Sum.traverse, functor_norm]

Premises used: Sum.traverse
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
inst_1 : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val : α
inr : Eq (α := G (σ ⊕ γ)) ((fun (a : β) ↦ f <$> Sum.inr a) <$> g val) ((fun (a : β) ↦ Sum.inr (f a)) <$> g val)
⊢ Eq (α := G (σ ⊕ γ)) ((fun (x : σ ⊕ β) ↦ f <$> x) <$> Sum.traverse g (Sum.inr val))
    (Sum.traverse (fun (x : α) ↦ f <$> g x) (Sum.inr val))

Tactic:
simp [Sum.traverse, functor_norm]

Premises used: Sum.traverse
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
inst_1 : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val : σ
⊢ Eq (α := G (σ ⊕ γ)) (pure (f <$> inl val)) (pure (inl val))

Tactic:
congr
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
inst_1 : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val : α
⊢ Eq (α := G (σ ⊕ γ)) ((fun (a : β) ↦ f <$> inr a) <$> g val) ((fun (a : β) ↦ inr (f a)) <$> g val)

Tactic:
congr
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
inst_3 : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : σ ⊕ α
inl :
  ∀ (val : σ),
    Eq (α := G (σ ⊕ β)) ((fun {α : Type u} ↦ η.app α) (Sum.traverse f (Sum.inl val)))
      (Sum.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (Sum.inl val))
inr :
  ∀ (val : α),
    Eq (α := G (σ ⊕ β)) ((fun {α : Type u} ↦ η.app α) (Sum.traverse f (Sum.inr val)))
      (Sum.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (Sum.inr val))
⊢ Eq (α := G (σ ⊕ β)) ((fun {α : Type u} ↦ η.app α) (Sum.traverse f x))
    (Sum.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)

Tactic:
cases x
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
inst_3 : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
val : σ
⊢ Eq (α := G (σ ⊕ β)) ((fun {α : Type u} ↦ η.app α) (Sum.traverse f (inl val)))
    (Sum.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (inl val))

Tactic:
simp! [Sum.traverse, functor_norm]

Premises used: Sum.traverse
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
inst_3 : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
val : α
⊢ Eq (α := G (σ ⊕ β)) ((fun {α : Type u} ↦ η.app α) (Sum.traverse f (inr val)))
    (Sum.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (inr val))

Tactic:
simp! [Sum.traverse, functor_norm]

Premises used: Sum.traverse
-- Module: Mathlib.Control.Traversable.Instances
Goal:
σ : Type u
⊢ LawfulTraversable.{u} (Sum σ)

Tactic:
{ show LawfulMonad (Sum σ) from inferInstance with
    id_traverse := Sum.id_traverse
    comp_traverse := Sum.comp_traverse
    traverse_eq_map_id := Sum.traverse_eq_map_id
    naturality := Sum.naturality }

Premises used: LawfulTraversable.mk, inferInstance, Sum.comp_traverse, Sum.naturality, Sum.traverse_eq_map_id, Sum.id_traverse
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α β γ : Type u
g : α → F β
f_1 : β → γ
α_1 β_1 : Type u
f : Id (α_1 → β_1)
x : Id α_1
simp : Eq (α := F β_1) (pure (f <*> x)) (pure (f x))
⊢ Eq (α := F β_1) (pure (f <*> x)) (pure f <*> pure x)

Tactic:
simp only [map_pure, seq_pure]

Premises used: LawfulApplicative.seq_pure, LawfulApplicative.map_pure
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α β γ : Type u
g : α → F β
f_1 : β → γ
α_1 β_1 : Type u
f : Id (α_1 → β_1)
x : Id α_1
⊢ Eq (α := F β_1) (pure (f <*> x)) (pure (f x))

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
F : Type u → Type u
inst : Applicative F
inst_1 : LawfulApplicative F
α : Type u
x : id α
⊢ Eq (α := F α) ((fun {α : Type u} ↦ ApplicativeTransformation.app (PureTransformation F) α) x) (pure x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
β γ : Type u
f : β → γ
⊢ Eq (α := t β → t γ) (map f) (Id.run ∘ traverse (pure ∘ f))

Tactic:
funext fun y => (traverse_eq_map_id f y).symm

Premises used: funext, LawfulTraversable.traverse_eq_map_id, Eq.symm
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
rw : (Id.run ∘ traverse (pure ∘ f)) <$> traverse g x = traverse (map f ∘ g) x
⊢ map f <$> traverse g x = traverse (map f ∘ g) x

Tactic:
rw [map_eq_traverse_id f]

Premises used: Traversable.map_eq_traverse_id
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ (Id.run ∘ traverse (pure ∘ f)) <$> traverse g x = traverse (map f ∘ g) x

Tactic:
(comp_traverse (pure ∘ f) g x).symm.trans ?_

Premises used: Pure.pure, LawfulTraversable.comp_traverse, Function.comp, Id, Functor.Comp.mk, Functor.Comp, Eq.symm, Eq.trans
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
refine : traverse (Comp.mk ∘ map (pure ∘ f) ∘ g) x = traverse (map f ∘ g) x
⊢ (Id.run ∘ traverse (pure ∘ f)) <$> traverse g x = traverse (map f ∘ g) x

Tactic:
refine (comp_traverse (pure ∘ f) g x).symm.trans ?_

Premises used: Pure.pure, LawfulTraversable.comp_traverse, Function.comp, Eq.symm, Eq.trans
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
h : Comp.instApplicativeComp = inst_2
⊢ traverse (Comp.mk ∘ map (pure ∘ f) ∘ g) x = traverse (map f ∘ g) x

Tactic:
congr 1
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ Comp.instApplicativeComp = inst_2

Tactic:
apply Comp.applicative_comp_id

Premises used: Functor.Comp.applicative_comp_id
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
rw : traverse f ((Id.run ∘ traverse (pure ∘ g)) x) = traverse (f ∘ g) x
⊢ traverse f (g <$> x) = traverse (f ∘ g) x

Tactic:
rw [@map_eq_traverse_id t _ _ _ _ g]

Premises used: Traversable.map_eq_traverse_id
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ traverse f ((Id.run ∘ traverse (pure ∘ g)) x) = traverse (f ∘ g) x

Tactic:
(comp_traverse (G := Id) f (pure ∘ g) x).symm.trans ?_

Premises used: Pure.pure, LawfulTraversable.comp_traverse, Function.comp, Id, Functor.Comp.mk, Functor.Comp, Eq.symm, Eq.trans
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
refine : traverse (Comp.mk ∘ map f ∘ pure ∘ g) x = traverse (f ∘ g) x
⊢ traverse f ((Id.run ∘ traverse (pure ∘ g)) x) = traverse (f ∘ g) x

Tactic:
refine (comp_traverse (G := Id) f (pure ∘ g) x).symm.trans ?_

Premises used: Pure.pure, LawfulTraversable.comp_traverse, Function.comp, Eq.symm, Eq.trans
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
h : Comp.instApplicativeComp = inst_2
⊢ traverse (Comp.mk ∘ map f ∘ pure ∘ g) x = traverse (f ∘ g) x

Tactic:
congr 1
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ Comp.instApplicativeComp = inst_2

Tactic:
apply Comp.applicative_id_comp

Premises used: Functor.Comp.applicative_id_comp
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α : Type u
x : t α
⊢ Eq (α := F (t α)) (traverse pure x) (pure (traverse pure x))

Tactic:
have : traverse pure x = pure (traverse (m := Id) pure x) :=
      (naturality (PureTransformation F) pure x).symm
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α : Type u
x : t α
this : Eq (α := F (t α)) (traverse pure x) (pure (traverse pure x))
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : Eq (α := F (t α)) (traverse pure x) (pure (pure x))), Eq (α := F (t α)) (traverse pure x) (pure x)
⊢ Eq (α := F (t α)) (traverse pure x) (pure x)

Tactic:
rwa [id_traverse] at this

Premises used: LawfulTraversable.id_traverse
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
α : Type u
x : t α
⊢ Eq (α := Id (t α)) (sequence (pure <$> x)) (pure x)

Tactic:
simp [sequence, traverse_map, id_traverse]

Premises used: LawfulTraversable.id_traverse, Traversable.traverse_map, sequence
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α : Type u
x : t (F (G α))
simp : traverse Comp.mk x = Comp.mk (traverse id <$> traverse id x)
⊢ sequence (Comp.mk <$> x) = Comp.mk (sequence <$> sequence x)

Tactic:
simp only [sequence, traverse_map, id_comp]

Premises used: Traversable.traverse_map, sequence, Function.id_comp
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α : Type u
x : t (F (G α))
rw : traverse Comp.mk x = traverse (Comp.mk ∘ map id ∘ id) x
⊢ traverse Comp.mk x = Comp.mk (traverse id <$> traverse id x)

Tactic:
rw [← comp_traverse]

Premises used: LawfulTraversable.comp_traverse
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ traverse Comp.mk x = traverse (Comp.mk ∘ map id ∘ id) x

Tactic:
simp [map_id]

Premises used: Functor.map_id
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α : Type u
η : ApplicativeTransformation F G
x : t (F α)
⊢ Eq (α := G (t α)) ((fun {α : Type u} ↦ η.app α) (sequence x)) (sequence ((fun {α : Type u} ↦ η.app α) <$> x))

Tactic:
simp [sequence, naturality, traverse_map]

Premises used: Traversable.traverse_map, LawfulTraversable.naturality, sequence
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
α : Type u
h : ∀ (x : t α), Id.run (traverse pure x) = Id.run (pure x)
⊢ Eq.{u + 1} (α := t α → Id (t α)) (traverse pure) pure

Tactic:
ext
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
α : Type u
x : t α
⊢ Id.run (traverse pure x) = Id.run (pure x)

Tactic:
id_traverse _

Premises used: LawfulTraversable.id_traverse, Id
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
α : Type u
x : t α
⊢ Id.run (traverse pure x) = Id.run (pure x)

Tactic:
exact id_traverse _

Premises used: LawfulTraversable.id_traverse
-- Module: Mathlib.Control.Traversable.Lemmas
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
h₁ : ∀ (x : t α), traverse (Comp.mk ∘ map h ∘ g) x = (Comp.mk ∘ map (traverse h) ∘ traverse g) x
⊢ Eq (α := t α → Comp F G (t γ)) (traverse (Comp.mk ∘ map h ∘ g)) (Comp.mk ∘ map (traverse h) ∘ traverse g)

Tactic:
ext