awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
F : Functor t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
this : F = Equiv.functor eqv
subst :
  ∀ (h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f)
    (h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f), LawfulFunctor t'
⊢ LawfulFunctor t'

Tactic:
subst this
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ LawfulFunctor t'

Tactic:
Equiv.lawfulFunctor eqv

Premises used: Equiv.lawfulFunctor
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ LawfulFunctor t'

Tactic:
exact Equiv.lawfulFunctor eqv

Premises used: Equiv.lawfulFunctor
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
m : Type u → Type u
inst_1 : Applicative m
α β : Type u
f : α → m β
x : t' α
⊢ Equiv.traverse eqv f x =
    Functor.map (α := t β) (⇑(eqv β) : (a : t β) → t' β) (traverse f (((eqv α).symm : (a : t' α) → t α) x))

Tactic:
rfl

Premises used: Equiv.traverse, rfl
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
α : Type u
x : t' α
rw :
  Eq (α := Id (t' α))
    (map (α := t α) (⇑(eqv α) : (a : t α) → t' α) (traverse pure (((eqv α).symm : (a : t' α) → t α) x))) (pure x)
rw₁ :
  Eq (α := Id (t' α))
    (map (α := t α) ((⇑(eqv α) : (a : t α) → t' α) : (a : t α) → t' α)
      (pure (((eqv α).symm : (a : t' α) → t α) x) : Id (t α)))
    (pure x)
rw₂ :
  Eq (α := Id (t' α)) (pure ((eqv α : (a : t α) → t' α) (((eqv α).symm : (a : t' α) → t α) x : t α)) : Id (t' α))
    (pure x : Id (t' α))
rw₃ rw₄ : Eq (α := Id (t' α)) (pure x) (pure x)
⊢ Eq (α := Id (t' α)) (Equiv.traverse eqv pure x) (pure x)

Tactic:
rw [Equiv.traverse, id_traverse, map_pure, apply_symm_apply]

Premises used: Equiv.apply_symm_apply, LawfulTraversable.id_traverse, Equiv.traverse, LawfulApplicative.map_pure
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
α β : Type u
f : α → β
x : t' α
simp :
  Eq (α := Id (t' β)) (map (α := t β) (⇑(eqv β) : (a : t β) → t' β) (pure (f <$> ((eqv α).symm : (a : t' α) → t α) x)))
    (pure (Equiv.map eqv f x))
⊢ Eq (α := Id (t' β)) (Equiv.traverse eqv (pure ∘ f) x) (pure (Equiv.map eqv f x))

Tactic:
simp only [Equiv.traverse, traverse_eq_map_id]

Premises used: Equiv.traverse, LawfulTraversable.traverse_eq_map_id
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
α β : Type u
f : α → β
x : t' α
⊢ Eq (α := Id (t' β)) (map (α := t β) (⇑(eqv β) : (a : t β) → t' β) (pure (f <$> ((eqv α).symm : (a : t' α) → t α) x)))
    (pure (Equiv.map eqv f x))

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : Applicative G
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
rw :
  Comp.mk
      ((fun (x : F (t γ)) ↦ (⇑(eqv γ) : (a : t γ) → t' γ) <$> x) <$>
        traverse f <$> traverse g (((eqv α).symm : (a : t' α) → t α) x)) =
    Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)
⊢ Equiv.traverse eqv (Comp.mk ∘ map f ∘ g) x = Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)

Tactic:
rw [traverse_def, comp_traverse, Comp.map_mk]

Premises used: LawfulTraversable.comp_traverse, Equiv.traverse_def, Functor.Comp.map_mk
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : Applicative G
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Comp.mk
      ((fun (x : F (t γ)) ↦ (⇑(eqv γ) : (a : t γ) → t' γ) <$> x) <$>
        traverse f <$> traverse g (((eqv α).symm : (a : t' α) → t α) x)) =
    Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)

Tactic:
simp only [map_map, traverse_def, symm_apply_apply]

Premises used: Equiv.traverse_def, Equiv.symm_apply_apply, Functor.map_map
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : Applicative G
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
x : t' α
⊢ Eq (α := G (t' β)) ((fun {α : Type u} ↦ η.app α) (Equiv.traverse eqv f x))
    (Equiv.traverse eqv ((fun {α : Type u} ↦ η.app α) ∘ f) x)

Tactic:
simp only [Equiv.traverse, functor_norm]

Premises used: Equiv.traverse
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
⊢ LawfulTraversable t'

Tactic:
let _inst := Equiv.traversable eqv
  { toLawfulFunctor := Equiv.lawfulFunctor eqv
    id_traverse := Equiv.id_traverse eqv
    comp_traverse := Equiv.comp_traverse eqv
    traverse_eq_map_id := Equiv.traverse_eq_map_id eqv
    naturality := Equiv.naturality eqv }

Premises used: Equiv.traverse_eq_map_id, LawfulTraversable.mk, Equiv.id_traverse, Equiv.lawfulFunctor, Equiv.comp_traverse, Equiv.naturality, Equiv.traversable
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_3 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α : Type u
x : t' α
rw : Eq (α := Id (t' α)) (Equiv.traverse eqv pure x) (pure x)
rw₁ rw₂ : Eq (α := Id (t' α)) (pure x) (pure x)
⊢ Eq (α := Id (t' α)) (traverse pure x) (pure x)

Tactic:
rw [h₂, Equiv.id_traverse]

Premises used: Equiv.id_traverse
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_7 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F G : Type u → Type u
inst_3 : Applicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative F
inst_6 : LawfulApplicative G
α β γ : Type u
x : β → F γ
x_1 : α → G β
x_2 : t' α
rw : Comp.mk (Equiv.traverse eqv x <$> Equiv.traverse eqv x_1 x_2) = Comp.mk (Equiv.traverse eqv x <$> traverse x_1 x_2)
⊢ traverse (Comp.mk ∘ map x ∘ x_1) x_2 = Comp.mk (traverse x <$> traverse x_1 x_2)

Tactic:
rw [h₂, Equiv.comp_traverse, h₂]

Premises used: Equiv.comp_traverse
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_7 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F G : Type u → Type u
inst_3 : Applicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative F
inst_6 : LawfulApplicative G
α β γ : Type u
x : β → F γ
x_1 : α → G β
x_2 : t' α
e_x : Equiv.traverse eqv x_1 x_2 = traverse x_1 x_2
⊢ Comp.mk (Equiv.traverse eqv x <$> Equiv.traverse eqv x_1 x_2) = Comp.mk (Equiv.traverse eqv x <$> traverse x_1 x_2)

Tactic:
congr
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_7 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F G : Type u → Type u
inst_3 : Applicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative F
inst_6 : LawfulApplicative G
α β γ : Type u
x : β → F γ
x_1 : α → G β
x_2 : t' α
e_x e_x₁ : Equiv.traverse eqv x_1 x_2 = Equiv.traverse eqv x_1 x_2
⊢ Equiv.traverse eqv x_1 x_2 = traverse x_1 x_2

Tactic:
rw [h₂]
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_3 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α β : Type u
x : α → β
x_1 : t' α
rw : Eq (α := Id (t' β)) (Equiv.traverse eqv (pure ∘ x) x_1) (pure (x <$> x_1))
rw₁ : Eq (α := Id (t' β)) (pure (Equiv.map eqv x x_1)) (pure (x <$> x_1))
rw₂ rw₃ : Eq (α := Id (t' β)) (pure (Equiv.map eqv x x_1)) (pure (Equiv.map eqv x x_1))
⊢ Eq (α := Id (t' β)) (traverse (pure ∘ x) x_1) (pure (x <$> x_1))

Tactic:
rw [h₂, Equiv.traverse_eq_map_id, h₀]

Premises used: Equiv.traverse_eq_map_id
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_7 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F G : Type u → Type u
inst_3 : Applicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative F
inst_6 : LawfulApplicative G
x : ApplicativeTransformation F G
x_1 x_2 : Type u
x_3 : x_1 → F x_2
x_4 : t' x_1
rw :
  Eq (α := G (t' x_2)) ((fun {α : Type u} ↦ x.app α) (Equiv.traverse eqv x_3 x_4))
    (traverse ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
rw₁ :
  Eq (α := G (t' x_2)) (Equiv.traverse eqv ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
    (traverse ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
rw₂ rw₃ :
  Eq (α := G (t' x_2)) (Equiv.traverse eqv ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
    (Equiv.traverse eqv ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
⊢ Eq (α := G (t' x_2)) ((fun {α : Type u} ↦ x.app α) (traverse x_3 x_4))
    (traverse ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)

Tactic:
rw [h₂, Equiv.naturality, h₂]

Premises used: Equiv.naturality
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α : Type u_1
x : Option α
none : Eq.{u_1 + 1} (α := Id (Option α)) (Option.traverse pure Option.none) (pure Option.none)
some : ∀ (val : α), Eq (α := Id (Option α)) (Option.traverse pure (Option.some val)) (pure (Option.some val))
⊢ Eq (α := Id (Option α)) (Option.traverse pure x) (pure x)

Tactic:
cases x
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Id (Option α)) (Option.traverse pure none) (pure none)

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α : Type u_1
val : α
⊢ Eq (α := Id (Option α)) (Option.traverse pure (some val)) (pure (some val))

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

Tactic:
cases x
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
none : Eq.{u + 1} (α := Comp G F (Option γ)) (pure Option.none) (Comp.mk (pure (pure Option.none)))
⊢ Option.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) Option.none =
    Comp.mk (Option.traverse f <$> Option.traverse g Option.none)

Tactic:
simp [Option.traverse, Option.mapM, functor_norm]

Premises used: Option.mapM, Option.traverse
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ Eq.{u + 1} (α := Comp G F (Option γ)) (pure none) (Comp.mk (pure (pure none)))

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

Tactic:
simp [Option.traverse, Option.mapM, functor_norm]

Premises used: Option.mapM, Option.traverse
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α β : Type u_1
f : α → β
x : Option α
none : Eq (α := Id (Option β)) (Option.traverse (pure ∘ f) Option.none) (pure (f <$> Option.none))
some :
  ∀ (val : α), Eq (α := Id (Option β)) (Option.traverse (pure ∘ f) (Option.some val)) (pure (f <$> Option.some val))
⊢ Eq (α := Id (Option β)) (Option.traverse (pure ∘ f) x) (pure (f <$> x))

Tactic:
cases x
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α β : Type u_1
f : α → β
⊢ Eq (α := Id (Option β)) (Option.traverse (pure ∘ f) none) (pure (f <$> none))

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α β : Type u_1
f : α → β
val : α
⊢ Eq (α := Id (Option β)) (Option.traverse (pure ∘ f) (some val)) (pure (f <$> some val))

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
η : ApplicativeTransformation F G
inst_3 : LawfulApplicative F
α : Type u_1
β : Type u
f : α → F β
x : Option α
none :
  Eq (α := G (Option β)) ((fun {α : Type u} ↦ η.app α) (Option.traverse f Option.none))
    (Option.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) Option.none)
some :
  ∀ (x : α),
    Eq (α := G (Option β)) ((fun {α : Type u} ↦ η.app α) (Option.traverse f (Option.some x)))
      (Option.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (Option.some x))
⊢ Eq (α := G (Option β)) ((fun {α : Type u} ↦ η.app α) (Option.traverse f x))
    (Option.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)

Tactic:
rcases x with - | x
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
η : ApplicativeTransformation F G
inst_3 : LawfulApplicative F
α : Type u_1
β : Type u
f : α → F β
⊢ Eq (α := G (Option β)) ((fun {α : Type u} ↦ η.app α) (Option.traverse f none))
    (Option.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) none)

Tactic:
simp! [*, functor_norm, Option.traverse]

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

Tactic:
simp! [*, functor_norm, Option.traverse]

Premises used: Option.traverse
-- Module: Mathlib.Control.Traversable.Instances
Goal:
⊢ LawfulTraversable Option

Tactic:
{ show LawfulMonad Option from inferInstance with
    id_traverse := Option.id_traverse
    comp_traverse := Option.comp_traverse
    traverse_eq_map_id := Option.traverse_eq_map_id
    naturality := fun η _ _ f x => Option.naturality η f x }

Premises used: LawfulTraversable.mk, Option.naturality, inferInstance, Option.id_traverse, Option.traverse_eq_map_id, Option.comp_traverse
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α : Type u_1
xs : List α
nil : Eq.{u_1 + 1} (α := Id (List α)) (List.traverse pure []) (pure [])
cons :
  ∀ (head : α) (tail : List α),
    Eq (α := Id (List α)) (List.traverse pure tail) (pure tail) →
      Eq (α := Id (List α)) (List.traverse pure (head :: tail)) (pure (head :: tail))
⊢ Eq (α := Id (List α)) (List.traverse pure xs) (pure xs)

Tactic:
induction xs
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Id (List α)) (List.traverse pure []) (pure [])

Tactic:
simp! [*, List.traverse, functor_norm]

Premises used: List.traverse
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α : Type u_1
head : α
tail : List α
tail_ih : Eq (α := Id (List α)) (List.traverse pure tail) (pure tail)
⊢ Eq (α := Id (List α)) (List.traverse pure (head :: tail)) (pure (head :: tail))

Tactic:
simp! [*, List.traverse, functor_norm]

Premises used: List.traverse
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : List α
nil : List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) [] = Comp.mk (List.traverse f <$> List.traverse g [])
cons :
  ∀ (head : α) (tail : List α),
    List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) tail = Comp.mk (List.traverse f <$> List.traverse g tail) →
      List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (head :: tail) =
        Comp.mk (List.traverse f <$> List.traverse g (head :: tail))
⊢ List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) x = Comp.mk (List.traverse f <$> List.traverse g x)

Tactic:
induction x
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
nil : Eq.{u + 1} (α := Comp G F (List γ)) (pure []) (Comp.mk (pure (pure [])))
⊢ List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) [] = Comp.mk (List.traverse f <$> List.traverse g [])

Tactic:
simp! [*, functor_norm]
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
head : α
tail : List α
tail_ih :
  List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) tail = Comp.mk (List.traverse f <$> List.traverse g tail)
cons :
  Eq (α := Comp G F (List γ))
    (Comp.mk
      ((fun (a : β) ↦ (fun (x2 : F (List γ)) ↦ List.cons <$> f a <*> x2) ∘ List.traverse f) <$> g head <*>
        List.traverse g tail))
    (Comp.mk ((fun (a : β) ↦ List.traverse f ∘ List.cons a) <$> g head <*> List.traverse g tail))
⊢ List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (head :: tail) =
    Comp.mk (List.traverse f <$> List.traverse g (head :: tail))

Tactic:
simp! [*, functor_norm]
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ Eq.{u + 1} (α := Comp G F (List γ)) (pure []) (Comp.mk (pure (pure [])))

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Instances
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
head : α
tail : List α
tail_ih :
  List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) tail = Comp.mk (List.traverse f <$> List.traverse g tail)
⊢ Eq (α := Comp G F (List γ))
    (Comp.mk
      ((fun (a : β) ↦ (fun (x2 : F (List γ)) ↦ 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:
rfl
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α β : Type u_1
f : α → β
x : List α
nil : Eq (α := Id (List β)) (List.traverse (pure ∘ f) []) (pure (f <$> []))
cons :
  ∀ (head : α) (tail : List α),
    Eq (α := Id (List β)) (List.traverse (pure ∘ f) tail) (pure (f <$> tail)) →
      Eq (α := Id (List β)) (List.traverse (pure ∘ f) (head :: tail)) (pure (f <$> (head :: tail)))
⊢ Eq (α := Id (List β)) (List.traverse (pure ∘ f) x) (pure (f <$> x))

Tactic:
induction x
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α β : Type u_1
f : α → β
⊢ Eq (α := Id (List β)) (List.traverse (pure ∘ f) []) (pure (f <$> []))

Tactic:
simp! [*, functor_norm]
-- Module: Mathlib.Control.Traversable.Instances
Goal:
α β : Type u_1
f : α → β
head : α
tail : List α
tail_ih : Eq (α := Id (List β)) (List.traverse (pure ∘ f) tail) (pure (f <$> tail))
⊢ Eq (α := Id (List β)) (List.traverse (pure ∘ f) (head :: tail)) (pure (f <$> (head :: tail)))

Tactic:
simp! [*, functor_norm]
-- 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
α : Type u_1
β : Type u
f : α → F β
x : List α
nil :
  Eq (α := G (List β)) ((fun {α : Type u} ↦ η.app α) (List.traverse f []))
    (List.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) [])
cons :
  ∀ (head : α) (tail : List α),
    Eq (α := G (List β)) ((fun {α : Type u} ↦ η.app α) (List.traverse f tail))
        (List.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) tail) →
      Eq (α := G (List β)) ((fun {α : Type u} ↦ η.app α) (List.traverse f (head :: tail)))
        (List.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (head :: tail))
⊢ Eq (α := G (List β)) ((fun {α : Type u} ↦ η.app α) (List.traverse f x))
    (List.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)

Tactic:
induction x
-- 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
α : Type u_1
β : Type u
f : α → F β
⊢ Eq (α := G (List β)) ((fun {α : Type u} ↦ η.app α) (List.traverse f []))
    (List.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) [])

Tactic:
simp! [*, functor_norm]
-- 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
α : Type u_1
β : Type u
f : α → F β
head : α
tail : List α
tail_ih :
  Eq (α := G (List β)) ((fun {α : Type u} ↦ η.app α) (List.traverse f tail))
    (List.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) tail)
⊢ Eq (α := G (List β)) ((fun {α : Type u} ↦ η.app α) (List.traverse f (head :: tail)))
    (List.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (head :: tail))

Tactic:
simp! [*, functor_norm]