awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
α α' β β' : Type u
f : α → β
f' : α' → β'
x : _root_.flip t α α'
toLawfulBifunctor : LawfulBifunctor t
id_bitraverse : ∀ {α β : Type u} (x : t α β), Eq (α := Id (t α β)) (bitraverse (t := t) pure pure x) (pure x)
⊢ ∀ {F G : Type u → Type u} [inst_3 : Applicative F] [inst_4 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : t α α'),
    bitraverse (t := t) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
      Comp.mk (bitraverse (t := t) f f' <$> bitraverse (t := t) g g' x)

Tactic:
casesm LawfulBitraversable t

Premises used: LawfulBitraversable
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
α α' β β' : Type u
f : α → β
f' : α' → β'
x : _root_.flip t α α'
toLawfulBifunctor : LawfulBifunctor t
id_bitraverse : ∀ {α β : Type u} (x : t α β), Eq (α := Id (t α β)) (bitraverse (t := t) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F G : Type u → Type u} [inst_3 : Applicative F] [inst_4 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : t α α'),
    bitraverse (t := t) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
      Comp.mk (bitraverse (t := t) f f' <$> bitraverse (t := t) g g' x)
⊢ ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    Eq (α := Id (t β β')) (bitraverse (t := t) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := t) f f' x))

Tactic:
casesm LawfulBitraversable t

Premises used: LawfulBitraversable
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
α α' β β' : Type u
f : α → β
f' : α' → β'
x : _root_.flip t α α'
toLawfulBifunctor : LawfulBifunctor t
id_bitraverse : ∀ {α β : Type u} (x : t α β), Eq (α := Id (t α β)) (bitraverse (t := t) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F G : Type u → Type u} [inst_3 : Applicative F] [inst_4 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : t α α'),
    bitraverse (t := t) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
      Comp.mk (bitraverse (t := t) f f' <$> bitraverse (t := t) g g' x)
bitraverse_eq_bimap_id :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    Eq (α := Id (t β β')) (bitraverse (t := t) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := t) f f' x))
⊢ ∀ {F G : Type u → Type u} [inst_3 : Applicative F] [inst_4 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β')
    (x : t α α'),
    Eq (α := G (t β β')) ((fun {α : Type u} ↦ η.app α) (bitraverse (t := t) f f' x))
      (bitraverse (t := t) ((fun {α : Type u} ↦ η.app α) ∘ f) ((fun {α : Type u} ↦ η.app α) ∘ f') x)

Tactic:
casesm LawfulBitraversable t

Premises used: LawfulBitraversable
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
F_1 G : Type u → Type u
inst_3 : Applicative F_1
inst_4 : Applicative G
inst_5 : LawfulApplicative F_1
inst_6 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u
f : α → F_1 β
f' : α' → F_1 β'
x : _root_.flip t α α'
⊢ LawfulBifunctor t

Tactic:
casesm LawfulBitraversable t

Premises used: LawfulBitraversable
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
F_1 G : Type u → Type u
inst_3 : Applicative F_1
inst_4 : Applicative G
inst_5 : LawfulApplicative F_1
inst_6 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u
f : α → F_1 β
f' : α' → F_1 β'
x : _root_.flip t α α'
toLawfulBifunctor : LawfulBifunctor t
⊢ ∀ {α β : Type u} (x : t α β), Eq (α := Id (t α β)) (bitraverse (t := t) pure pure x) (pure x)

Tactic:
casesm LawfulBitraversable t

Premises used: LawfulBitraversable
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
F_1 G : Type u → Type u
inst_3 : Applicative F_1
inst_4 : Applicative G
inst_5 : LawfulApplicative F_1
inst_6 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u
f : α → F_1 β
f' : α' → F_1 β'
x : _root_.flip t α α'
toLawfulBifunctor : LawfulBifunctor t
id_bitraverse : ∀ {α β : Type u} (x : t α β), Eq (α := Id (t α β)) (bitraverse (t := t) pure pure x) (pure x)
⊢ ∀ {F G : Type u → Type u} [inst_7 : Applicative F] [inst_8 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : t α α'),
    bitraverse (t := t) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
      Comp.mk (bitraverse (t := t) f f' <$> bitraverse (t := t) g g' x)

Tactic:
casesm LawfulBitraversable t

Premises used: LawfulBitraversable
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
F_1 G : Type u → Type u
inst_3 : Applicative F_1
inst_4 : Applicative G
inst_5 : LawfulApplicative F_1
inst_6 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u
f : α → F_1 β
f' : α' → F_1 β'
x : _root_.flip t α α'
toLawfulBifunctor : LawfulBifunctor t
id_bitraverse : ∀ {α β : Type u} (x : t α β), Eq (α := Id (t α β)) (bitraverse (t := t) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F G : Type u → Type u} [inst_7 : Applicative F] [inst_8 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : t α α'),
    bitraverse (t := t) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
      Comp.mk (bitraverse (t := t) f f' <$> bitraverse (t := t) g g' x)
⊢ ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    Eq (α := Id (t β β')) (bitraverse (t := t) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := t) f f' x))

Tactic:
casesm LawfulBitraversable t

Premises used: LawfulBitraversable
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
F_1 G : Type u → Type u
inst_3 : Applicative F_1
inst_4 : Applicative G
inst_5 : LawfulApplicative F_1
inst_6 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u
f : α → F_1 β
f' : α' → F_1 β'
x : _root_.flip t α α'
toLawfulBifunctor : LawfulBifunctor t
id_bitraverse : ∀ {α β : Type u} (x : t α β), Eq (α := Id (t α β)) (bitraverse (t := t) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F G : Type u → Type u} [inst_7 : Applicative F] [inst_8 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : t α α'),
    bitraverse (t := t) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
      Comp.mk (bitraverse (t := t) f f' <$> bitraverse (t := t) g g' x)
bitraverse_eq_bimap_id :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    Eq (α := Id (t β β')) (bitraverse (t := t) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := t) f f' x))
⊢ ∀ {F G : Type u → Type u} [inst_7 : Applicative F] [inst_8 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β')
    (x : t α α'),
    Eq (α := G (t β β')) ((fun {α : Type u} ↦ η.app α) (bitraverse (t := t) f f' x))
      (bitraverse (t := t) ((fun {α : Type u} ↦ η.app α) ∘ f) ((fun {α : Type u} ↦ η.app α) ∘ f') x)

Tactic:
casesm LawfulBitraversable t

Premises used: LawfulBitraversable
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
α β : Type u
x : _root_.flip t α β
toLawfulBifunctor : LawfulBifunctor t
id_bitraverse : ∀ {α β : Type u} (x : t α β), Eq (α := Id (t α β)) (bitraverse (t := t) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F G : Type u → Type u} [inst_2 : Applicative F] [inst_3 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : t α α'),
    bitraverse (t := t) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
      Comp.mk (bitraverse (t := t) f f' <$> bitraverse (t := t) g g' x)
bitraverse_eq_bimap_id :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    Eq (α := Id (t β β')) (bitraverse (t := t) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := t) f f' x))
binaturality :
  ∀ {F G : Type u → Type u} [inst_2 : Applicative F] [inst_3 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β')
    (x : t α α'),
    Eq (α := G (t β β')) ((fun {α : Type u} ↦ η.app α) (bitraverse (t := t) f f' x))
      (bitraverse (t := t) ((fun {α : Type u} ↦ η.app α) ∘ f) ((fun {α : Type u} ↦ η.app α) ∘ f') x)
⊢ Eq (α := Id (_root_.flip t α β)) (bitraverse (t := _root_.flip t) pure pure x) (pure x)

Tactic:
apply_assumption only [*]
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
F_1 G : Type u → Type u
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
α α' β β' γ γ' : Type u
f : β → F_1 γ
f' : β' → F_1 γ'
g : α → G β
g' : α' → G β'
x : _root_.flip t α α'
toLawfulBifunctor : LawfulBifunctor t
id_bitraverse : ∀ {α β : Type u} (x : t α β), Eq (α := Id (t α β)) (bitraverse (t := t) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F G : Type u → Type u} [inst_6 : Applicative F] [inst_7 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : t α α'),
    bitraverse (t := t) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
      Comp.mk (bitraverse (t := t) f f' <$> bitraverse (t := t) g g' x)
bitraverse_eq_bimap_id :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    Eq (α := Id (t β β')) (bitraverse (t := t) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := t) f f' x))
binaturality :
  ∀ {F G : Type u → Type u} [inst_6 : Applicative F] [inst_7 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β')
    (x : t α α'),
    Eq (α := G (t β β')) ((fun {α : Type u} ↦ η.app α) (bitraverse (t := t) f f' x))
      (bitraverse (t := t) ((fun {α : Type u} ↦ η.app α) ∘ f) ((fun {α : Type u} ↦ η.app α) ∘ f') x)
⊢ bitraverse (t := _root_.flip t) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
    Comp.mk (bitraverse (t := _root_.flip t) f f' <$> bitraverse (t := _root_.flip t) g g' x)

Tactic:
apply_assumption only [*]
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
α α' β β' : Type u
f : α → β
f' : α' → β'
x : _root_.flip t α α'
toLawfulBifunctor : LawfulBifunctor t
id_bitraverse : ∀ {α β : Type u} (x : t α β), Eq (α := Id (t α β)) (bitraverse (t := t) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F G : Type u → Type u} [inst_2 : Applicative F] [inst_3 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : t α α'),
    bitraverse (t := t) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
      Comp.mk (bitraverse (t := t) f f' <$> bitraverse (t := t) g g' x)
bitraverse_eq_bimap_id :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    Eq (α := Id (t β β')) (bitraverse (t := t) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := t) f f' x))
binaturality :
  ∀ {F G : Type u → Type u} [inst_2 : Applicative F] [inst_3 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β')
    (x : t α α'),
    Eq (α := G (t β β')) ((fun {α : Type u} ↦ η.app α) (bitraverse (t := t) f f' x))
      (bitraverse (t := t) ((fun {α : Type u} ↦ η.app α) ∘ f) ((fun {α : Type u} ↦ η.app α) ∘ f') x)
⊢ Eq (α := Id (_root_.flip t β β')) (bitraverse (t := _root_.flip t) (pure ∘ f) (pure ∘ f') x)
    (pure (bimap (F := _root_.flip t) f f' x))

Tactic:
apply_assumption only [*]
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
F_1 G : Type u → Type u
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u
f : α → F_1 β
f' : α' → F_1 β'
x : _root_.flip t α α'
toLawfulBifunctor : LawfulBifunctor t
id_bitraverse : ∀ {α β : Type u} (x : t α β), Eq (α := Id (t α β)) (bitraverse (t := t) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F G : Type u → Type u} [inst_6 : Applicative F] [inst_7 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : t α α'),
    bitraverse (t := t) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
      Comp.mk (bitraverse (t := t) f f' <$> bitraverse (t := t) g g' x)
bitraverse_eq_bimap_id :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    Eq (α := Id (t β β')) (bitraverse (t := t) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := t) f f' x))
binaturality :
  ∀ {F G : Type u → Type u} [inst_6 : Applicative F] [inst_7 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β')
    (x : t α α'),
    Eq (α := G (t β β')) ((fun {α : Type u} ↦ η.app α) (bitraverse (t := t) f f' x))
      (bitraverse (t := t) ((fun {α : Type u} ↦ η.app α) ∘ f) ((fun {α : Type u} ↦ η.app α) ∘ f') x)
⊢ Eq (α := G (_root_.flip t β β')) ((fun {α : Type u} ↦ η.app α) (bitraverse (t := _root_.flip t) f f' x))
    (bitraverse (t := _root_.flip t) ((fun {α : Type u} ↦ η.app α) ∘ f) ((fun {α : Type u} ↦ η.app α) ∘ f') x)

Tactic:
apply_assumption only [*]
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
α : Type u
id_traverse : ∀ {α_1 : Type u} (x : t α α_1), Eq (α := Id (t α α_1)) (traverse pure x) (pure x)
comp_traverse :
  ∀ {F G : Type u → Type u} [inst_3 : Applicative F] [inst_4 : 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)
traverse_eq_map_id :
  ∀ {α_1 β : Type u} (f : α_1 → β) (x : t α α_1), Eq (α := Id (t α β)) (traverse (pure ∘ f) x) (pure (f <$> x))
naturality :
  ∀ {F G : Type u → Type u} [inst_3 : Applicative F] [inst_4 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] (η : ApplicativeTransformation F G) {α_1 β : Type u} (f : α_1 → F β) (x : t α α_1),
    Eq (α := G (t α β)) ((fun {α : Type u} ↦ η.app α) (traverse f x)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)
⊢ LawfulTraversable.{u} (t α)

Tactic:
constructor
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
α α_1 : Type u
x : t α α_1
⊢ Eq (α := Id (t α α_1)) (traverse pure x) (pure x)

Tactic:
simp [traverse, comp_tsnd, functor_norm]

Premises used: Bitraversable.comp_tsnd, Traversable.traverse
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
α : Type u
F_1 G : Type u → Type u
inst_3 : Applicative F_1
inst_4 : Applicative G
inst_5 : LawfulApplicative F_1
inst_6 : LawfulApplicative G
α_1 β γ : Type u
f : β → F_1 γ
g : α_1 → G β
x : t α α_1
⊢ traverse (Comp.mk ∘ map f ∘ g) x = Comp.mk (traverse f <$> traverse g x)

Tactic:
simp [traverse, comp_tsnd, functor_norm]

Premises used: Bitraversable.comp_tsnd, Traversable.traverse
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
α : Type u
F_1 G : Type u → Type u
inst_3 : Applicative F_1
inst_4 : Applicative G
inst_5 : LawfulApplicative F_1
inst_6 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α_1 β : Type u
f : α_1 → F_1 β
x : t α α_1
naturality : η.app (t α β) (tsnd (t := t) f x) = tsnd (t := t) (η.app β ∘ f) x
⊢ Eq (α := G (t α β)) ((fun {α : Type u} ↦ η.app α) (traverse f x)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)

Tactic:
simp [traverse, comp_tsnd, functor_norm]

Premises used: Bitraversable.comp_tsnd, Traversable.traverse
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
α α_1 β : Type u
f : α_1 → β
x : t α α_1
⊢ Eq (α := Id (t α β)) (tsnd (t := t) (pure ∘ f) x) (pure (f <$> x))

Tactic:
simp [tsnd_eq_snd_id, (· <$> ·)]

Premises used: Bitraversable.tsnd_eq_snd_id, Functor.map
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
α : Type u
F_1 G : Type u → Type u
inst_3 : Applicative F_1
inst_4 : Applicative G
inst_5 : LawfulApplicative F_1
inst_6 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α_1 β : Type u
f : α_1 → F_1 β
x : t α α_1
⊢ η.app (t α β) (tsnd (t := t) f x) = tsnd (t := t) (η.app β ∘ f) x

Tactic:
simp [tsnd, binaturality, Function.comp_def, functor_norm]

Premises used: Bitraversable.tsnd, LawfulBitraversable.binaturality, Function.comp_def
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Traversable F
inst_2 : Traversable G
inst_3 : LawfulTraversable F
inst_4 : LawfulTraversable G
inst_5 : LawfulBitraversable t
id_bitraverse :
  ∀ {α β : Type u} (x : bicompl t F G α β),
    Eq (α := Id (bicompl t F G α β)) (bitraverse (t := bicompl t F G) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F_1 G_1 : Type u → Type u} [inst_6 : Applicative F_1] [inst_7 : Applicative G_1] [LawfulApplicative F_1]
    [LawfulApplicative G_1] {α α' β β' γ γ' : Type u} (f : β → F_1 γ) (f' : β' → F_1 γ') (g : α → G_1 β)
    (g' : α' → G_1 β') (x : bicompl t F G α α'),
    bitraverse (t := bicompl t F G) (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
      Functor.Comp.mk (bitraverse (t := bicompl t F G) f f' <$> bitraverse (t := bicompl t F G) g g' x)
bitraverse_eq_bimap_id :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : bicompl t F G α α'),
    Eq (α := Id (bicompl t F G β β')) (bitraverse (t := bicompl t F G) (pure ∘ f) (pure ∘ f') x)
      (pure (bimap (F := bicompl t F G) f f' x))
binaturality :
  ∀ {F_1 G_1 : Type u → Type u} [inst_6 : Applicative F_1] [inst_7 : Applicative G_1] [LawfulApplicative F_1]
    [LawfulApplicative G_1] (η : ApplicativeTransformation F_1 G_1) {α α' β β' : Type u} (f : α → F_1 β)
    (f' : α' → F_1 β') (x : bicompl t F G α α'),
    Eq (α := G_1 (bicompl t F G β β')) ((fun {α : Type u} ↦ η.app α) (bitraverse (t := bicompl t F G) f f' x))
      (bitraverse (t := bicompl t F G) ((fun {α : Type u} ↦ η.app α) ∘ f) ((fun {α : Type u} ↦ η.app α) ∘ f') x)
⊢ LawfulBitraversable.{u} (bicompl t F G)

Tactic:
constructor
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Traversable F
inst_2 : Traversable G
inst_3 : LawfulTraversable F
inst_4 : LawfulTraversable G
inst_5 : LawfulBitraversable t
α β : Type u
x : bicompl t F G α β
⊢ Eq (α := Id (bicompl t F G α β)) (bitraverse (t := bicompl t F G) pure pure x) (pure x)

Tactic:
simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse,
      functor_norm]

Premises used: LawfulBitraversable.comp_bitraverse, Bicompl.bitraverse, LawfulBitraversable.bitraverse_id_id, Bifunctor.bimap, Traversable.traverse_id, Bitraversable.bitraverse
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Traversable F
inst_2 : Traversable G
inst_3 : LawfulTraversable F
inst_4 : LawfulTraversable G
inst_5 : LawfulBitraversable t
F_1 G_1 : Type u → Type u
inst_6 : Applicative F_1
inst_7 : Applicative G_1
inst_8 : LawfulApplicative F_1
inst_9 : LawfulApplicative G_1
α α' β β' γ γ' : Type u
f : β → F_1 γ
f' : β' → F_1 γ'
g : α → G_1 β
g' : α' → G_1 β'
x : bicompl t F G α α'
⊢ bitraverse (t := bicompl t F G) (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
    Functor.Comp.mk (bitraverse (t := bicompl t F G) f f' <$> bitraverse (t := bicompl t F G) g g' x)

Tactic:
simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse,
      functor_norm]

Premises used: LawfulBitraversable.comp_bitraverse, Bicompl.bitraverse, LawfulBitraversable.bitraverse_id_id, Bifunctor.bimap, Traversable.traverse_id, Bitraversable.bitraverse
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Traversable F
inst_2 : Traversable G
inst_3 : LawfulTraversable F
inst_4 : LawfulTraversable G
inst_5 : LawfulBitraversable t
α α' β β' : Type u
f : α → β
f' : α' → β'
x : bicompl t F G α α'
bitraverse_eq_bimap_id :
  Eq (α := Id (bicompl t F G β β')) (bitraverse (t := t) (traverse (pure ∘ f)) (traverse (pure ∘ f')) x)
    (pure (bimap (F := t) (Functor.map f) (Functor.map f') x))
⊢ Eq (α := Id (bicompl t F G β β')) (bitraverse (t := bicompl t F G) (pure ∘ f) (pure ∘ f') x)
    (pure (bimap (F := bicompl t F G) f f' x))

Tactic:
simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse,
      functor_norm]

Premises used: LawfulBitraversable.comp_bitraverse, Bicompl.bitraverse, LawfulBitraversable.bitraverse_id_id, Bifunctor.bimap, Traversable.traverse_id, Bitraversable.bitraverse
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Traversable F
inst_2 : Traversable G
inst_3 : LawfulTraversable F
inst_4 : LawfulTraversable G
inst_5 : LawfulBitraversable t
F_1 G_1 : Type u → Type u
inst_6 : Applicative F_1
inst_7 : Applicative G_1
inst_8 : LawfulApplicative F_1
inst_9 : LawfulApplicative G_1
η : ApplicativeTransformation F_1 G_1
α α' β β' : Type u
f : α → F_1 β
f' : α' → F_1 β'
x : bicompl t F G α α'
binaturality :
  η.app (bicompl t F G β β') (bitraverse (t := t) (traverse f) (traverse f') x) =
    bitraverse (t := t) (traverse (η.app β ∘ f)) (traverse (η.app β' ∘ f')) x
⊢ Eq (α := G_1 (bicompl t F G β β')) ((fun {α : Type u} ↦ η.app α) (bitraverse (t := bicompl t F G) f f' x))
    (bitraverse (t := bicompl t F G) ((fun {α : Type u} ↦ η.app α) ∘ f) ((fun {α : Type u} ↦ η.app α) ∘ f') x)

Tactic:
simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse,
      functor_norm]

Premises used: LawfulBitraversable.comp_bitraverse, Bicompl.bitraverse, LawfulBitraversable.bitraverse_id_id, Bifunctor.bimap, Traversable.traverse_id, Bitraversable.bitraverse