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
α α' β β' : Type u_1
f : α → β
f' : α' → β'
x : α ⊕ α'
bitraverse_eq_bimap_id :
  ∀ (x : α),
    Eq (α := Id (β ⊕ β')) (bitraverse (t := Sum) (pure ∘ f) (pure ∘ f') (Sum.inl x))
      (pure (bimap (F := Sum) f f' (Sum.inl x)))
bitraverse_eq_bimap_id₁ :
  ∀ (x : α'),
    Eq (α := Id (β ⊕ β')) (bitraverse (t := Sum) (pure ∘ f) (pure ∘ f') (Sum.inr x))
      (pure (bimap (F := Sum) f f' (Sum.inr x)))
⊢ Eq (α := Id (β ⊕ β')) (bitraverse (t := Sum) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := Sum) f f' x))

Tactic:
casesm _ ⊕ _
-- 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_1 → Type u_1
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u_1
f : α → F_1 β
f' : α' → F_1 β'
x : α ⊕ α'
binaturality :
  ∀ (x : α),
    Eq (α := G (β ⊕ β')) ((fun {α : Type u_1} ↦ η.app α) (bitraverse (t := Sum) f f' (Sum.inl x)))
      (bitraverse (t := Sum) ((fun {α : Type u_1} ↦ η.app α) ∘ f) ((fun {α : Type u_1} ↦ η.app α) ∘ f') (Sum.inl x))
binaturality₁ :
  ∀ (x : α'),
    Eq (α := G (β ⊕ β')) ((fun {α : Type u_1} ↦ η.app α) (bitraverse (t := Sum) f f' (Sum.inr x)))
      (bitraverse (t := Sum) ((fun {α : Type u_1} ↦ η.app α) ∘ f) ((fun {α : Type u_1} ↦ η.app α) ∘ f') (Sum.inr x))
⊢ Eq (α := G (β ⊕ β')) ((fun {α : Type u_1} ↦ η.app α) (bitraverse (t := Sum) f f' x))
    (bitraverse (t := Sum) ((fun {α : Type u_1} ↦ η.app α) ∘ f) ((fun {α : Type u_1} ↦ η.app α) ∘ f') x)

Tactic:
casesm _ ⊕ _
-- 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_1
x : α
⊢ Eq (α := Id (α ⊕ β)) (bitraverse (t := Sum) pure pure (Sum.inl x)) (pure (Sum.inl x))

Tactic:
simp [bitraverse, Sum.bitraverse, functor_norm]

Premises used: Sum.bitraverse, Bitraversable.bitraverse
-- 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_1
x : β
⊢ Eq (α := Id (α ⊕ β)) (bitraverse (t := Sum) pure pure (Sum.inr x)) (pure (Sum.inr x))

Tactic:
simp [bitraverse, Sum.bitraverse, functor_norm]

Premises used: Sum.bitraverse, Bitraversable.bitraverse
-- 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_1 → Type u_1
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
α α' β β' γ γ' : Type u_1
f : β → F_1 γ
f' : β' → F_1 γ'
g : α → G β
g' : α' → G β'
x : α
⊢ bitraverse (t := Sum) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') (Sum.inl x) =
    Comp.mk (bitraverse (t := Sum) f f' <$> bitraverse (t := Sum) g g' (Sum.inl x))

Tactic:
simp [bitraverse, Sum.bitraverse, functor_norm]

Premises used: Sum.bitraverse, Bitraversable.bitraverse
-- 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_1 → Type u_1
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
α α' β β' γ γ' : Type u_1
f : β → F_1 γ
f' : β' → F_1 γ'
g : α → G β
g' : α' → G β'
x : α'
⊢ bitraverse (t := Sum) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') (Sum.inr x) =
    Comp.mk (bitraverse (t := Sum) f f' <$> bitraverse (t := Sum) g g' (Sum.inr x))

Tactic:
simp [bitraverse, Sum.bitraverse, functor_norm]

Premises used: Sum.bitraverse, Bitraversable.bitraverse
-- 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_1
f : α → β
f' : α' → β'
x : α
bitraverse_eq_bimap_id : Eq (α := Id (β ⊕ β')) (pure (Sum.inl (f x))) (pure (bimap (F := Sum) f f' (Sum.inl x)))
⊢ Eq (α := Id (β ⊕ β')) (bitraverse (t := Sum) (pure ∘ f) (pure ∘ f') (Sum.inl x))
    (pure (bimap (F := Sum) f f' (Sum.inl x)))

Tactic:
simp [bitraverse, Sum.bitraverse, functor_norm]

Premises used: Sum.bitraverse, Bitraversable.bitraverse
-- 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_1
f : α → β
f' : α' → β'
x : α'
bitraverse_eq_bimap_id : Eq (α := Id (β ⊕ β')) (pure (Sum.inr (f' x))) (pure (bimap (F := Sum) f f' (Sum.inr x)))
⊢ Eq (α := Id (β ⊕ β')) (bitraverse (t := Sum) (pure ∘ f) (pure ∘ f') (Sum.inr x))
    (pure (bimap (F := Sum) f f' (Sum.inr x)))

Tactic:
simp [bitraverse, Sum.bitraverse, functor_norm]

Premises used: Sum.bitraverse, Bitraversable.bitraverse
-- 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_1 → Type u_1
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u_1
f : α → F_1 β
f' : α' → F_1 β'
x : α
⊢ Eq (α := G (β ⊕ β')) ((fun {α : Type u_1} ↦ η.app α) (bitraverse (t := Sum) f f' (Sum.inl x)))
    (bitraverse (t := Sum) ((fun {α : Type u_1} ↦ η.app α) ∘ f) ((fun {α : Type u_1} ↦ η.app α) ∘ f') (Sum.inl x))

Tactic:
simp [bitraverse, Sum.bitraverse, functor_norm]

Premises used: Sum.bitraverse, Bitraversable.bitraverse
-- 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_1 → Type u_1
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u_1
f : α → F_1 β
f' : α' → F_1 β'
x : α'
⊢ Eq (α := G (β ⊕ β')) ((fun {α : Type u_1} ↦ η.app α) (bitraverse (t := Sum) f f' (Sum.inr x)))
    (bitraverse (t := Sum) ((fun {α : Type u_1} ↦ η.app α) ∘ f) ((fun {α : Type u_1} ↦ η.app α) ∘ f') (Sum.inr x))

Tactic:
simp [bitraverse, Sum.bitraverse, functor_norm]

Premises used: Sum.bitraverse, Bitraversable.bitraverse
-- 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_1
f : α → β
f' : α' → β'
x : α
⊢ Eq (α := Id (β ⊕ β')) (pure (Sum.inl (f x))) (pure (bimap (F := Sum) f f' (Sum.inl x)))

Tactic:
rfl
-- 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_1
f : α → β
f' : α' → β'
x : α'
⊢ Eq (α := Id (β ⊕ β')) (pure (Sum.inr (f' x))) (pure (bimap (F := Sum) f f' (Sum.inr x)))

Tactic:
rfl
-- 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
id_bitraverse :
  ∀ {α β : Type u_1} (x : Const α β), Eq (α := Id (Const α β)) (bitraverse (t := Const) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u_1} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : Const α α'),
    bitraverse (t := Const) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
      Comp.mk (bitraverse (t := Const) f f' <$> bitraverse (t := Const) g g' x)
bitraverse_eq_bimap_id :
  ∀ {α α' β β' : Type u_1} (f : α → β) (f' : α' → β') (x : Const α α'),
    Eq (α := Id (Const β β')) (bitraverse (t := Const) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := Const) f f' x))
binaturality :
  ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u_1} (f : α → F β) (f' : α' → F β')
    (x : Const α α'),
    Eq (α := G (Const β β')) ((fun {α : Type u_1} ↦ η.app α) (bitraverse (t := Const) f f' x))
      (bitraverse (t := Const) ((fun {α : Type u_1} ↦ η.app α) ∘ f) ((fun {α : Type u_1} ↦ η.app α) ∘ f') x)
⊢ LawfulBitraversable Const

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
α β : Type u_1
x : Const α β
id_bitraverse : Eq (α := Id (Const α β)) (pure x) (pure x)
⊢ Eq (α := Id (Const α β)) (bitraverse (t := Const) pure pure x) (pure x)

Tactic:
simp [bitraverse, Const.bitraverse, functor_norm]

Premises used: Const.bitraverse, Bitraversable.bitraverse
-- 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_1 → Type u_1
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
α α' β β' γ γ' : Type u_1
f : β → F_1 γ
f' : β' → F_1 γ'
g : α → G β
g' : α' → G β'
x : Const α α'
comp_bitraverse : Comp.mk (f <$> g x) = Comp.mk (f <$> g x)
⊢ bitraverse (t := Const) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
    Comp.mk (bitraverse (t := Const) f f' <$> bitraverse (t := Const) g g' x)

Tactic:
simp [bitraverse, Const.bitraverse, functor_norm]

Premises used: Const.bitraverse, Bitraversable.bitraverse
-- 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_1
f : α → β
f' : α' → β'
x : Const α α'
bitraverse_eq_bimap_id : Eq (α := Id (Const β β')) (pure (f x)) (pure (bimap (F := Const) f f' x))
⊢ Eq (α := Id (Const β β')) (bitraverse (t := Const) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := Const) f f' x))

Tactic:
simp [bitraverse, Const.bitraverse, functor_norm]

Premises used: Const.bitraverse, Bitraversable.bitraverse
-- 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_1 → Type u_1
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u_1
f : α → F_1 β
f' : α' → F_1 β'
x : Const α α'
binaturality : η.app (Const β β') (f x) = η.app β (f x)
⊢ Eq (α := G (Const β β')) ((fun {α : Type u_1} ↦ η.app α) (bitraverse (t := Const) f f' x))
    (bitraverse (t := Const) ((fun {α : Type u_1} ↦ η.app α) ∘ f) ((fun {α : Type u_1} ↦ η.app α) ∘ f') x)

Tactic:
simp [bitraverse, Const.bitraverse, functor_norm]

Premises used: Const.bitraverse, Bitraversable.bitraverse
-- 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_1
x : Const α β
⊢ Eq (α := Id (Const α β)) (pure x) (pure x)

Tactic:
rfl
-- 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_1 → Type u_1
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
α α' β β' γ γ' : Type u_1
f : β → F_1 γ
f' : β' → F_1 γ'
g : α → G β
g' : α' → G β'
x : Const α α'
⊢ Comp.mk (f <$> g x) = Comp.mk (f <$> g x)

Tactic:
rfl
-- 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_1
f : α → β
f' : α' → β'
x : Const α α'
⊢ Eq (α := Id (Const β β')) (pure (f x)) (pure (bimap (F := Const) f f' x))

Tactic:
rfl
-- 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_1 → Type u_1
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u_1
f : α → F_1 β
f' : α' → F_1 β'
x : Const α α'
⊢ η.app (Const β β') (f x) = η.app β (f x)

Tactic:
rfl
-- 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
id_bitraverse :
  ∀ {α β : Type u} (x : _root_.flip t α β),
    Eq (α := Id (_root_.flip t α β)) (bitraverse (t := _root_.flip 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 : _root_.flip t α α'),
    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)
bitraverse_eq_bimap_id :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : _root_.flip t α α'),
    Eq (α := Id (_root_.flip t β β')) (bitraverse (t := _root_.flip t) (pure ∘ f) (pure ∘ f') x)
      (pure (bimap (F := _root_.flip t) f f' x))
binaturality :
  ∀ {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 : _root_.flip t α α'),
    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)
⊢ LawfulBitraversable.{u} (_root_.flip 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
α β : Type u
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
α β : Type u
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
α β : 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)
⊢ ∀ {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
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
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
α α' β β' γ γ' : Type u
f : β → F_1 γ
f' : β' → F_1 γ'
g : α → G β
g' : α' → G β'
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
α α' β β' γ γ' : Type u
f : β → F_1 γ
f' : β' → F_1 γ'
g : α → G β
g' : α' → G β'
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
α α' β β' γ γ' : 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)
⊢ ∀ {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
α α' β β' γ γ' : 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_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
α α' β β' γ γ' : 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_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
inst_2 : LawfulBitraversable t
α α' β β' : Type u
f : α → β
f' : α' → β'
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
α α' β β' : Type u
f : α → β
f' : α' → β'
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