awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (hypothesis)
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
⊢ Eq (α := Id (_root_.flip t β β')) (bitraverse (t := _root_.flip t) (pure ∘ f) (pure ∘ f') x)
    (pure (bimap (F := _root_.flip t) f f' x))
have id_bitraverse : ∀ {α β : Type u} (x : t α β), Eq (α := Id (t α β)) (bitraverse (t := t) pure pure x) (pure x)
Tactic: casesm LawfulBitraversable t
Cleared hypotheses: inst_2
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (hypothesis)
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)
⊢ Eq (α := Id (_root_.flip t β β')) (bitraverse (t := _root_.flip t) (pure ∘ f) (pure ∘ f') x)
    (pure (bimap (F := _root_.flip t) f f' x))
have 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)
Tactic: casesm LawfulBitraversable t
Cleared hypotheses: inst_2
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (hypothesis)
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)
⊢ Eq (α := Id (_root_.flip t β β')) (bitraverse (t := _root_.flip t) (pure ∘ f) (pure ∘ f') x)
    (pure (bimap (F := _root_.flip t) f f' x))
have 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))
Tactic: casesm LawfulBitraversable t
Cleared hypotheses: inst_2
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (hypothesis)
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))
⊢ Eq (α := Id (_root_.flip t β β')) (bitraverse (t := _root_.flip t) (pure ∘ f) (pure ∘ f') x)
    (pure (bimap (F := _root_.flip t) f f' x))
have 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 : 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
Cleared hypotheses: inst_2
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (hypothesis)
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 α α'
⊢ 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)
have toLawfulBifunctor : LawfulBifunctor t
Tactic: casesm LawfulBitraversable t
Cleared hypotheses: inst_2
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (hypothesis)
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
⊢ 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)
have id_bitraverse : ∀ {α β : Type u} (x : t α β), Eq (α := Id (t α β)) (bitraverse (t := t) pure pure x) (pure x)
Tactic: casesm LawfulBitraversable t
Cleared hypotheses: inst_2
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (hypothesis)
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)
⊢ 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)
have 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)
Tactic: casesm LawfulBitraversable t
Cleared hypotheses: inst_2
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (hypothesis)
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)
⊢ 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)
have 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))
Tactic: casesm LawfulBitraversable t
Cleared hypotheses: inst_2
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (hypothesis)
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))
⊢ 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)
have binaturality : ∀ {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
Cleared hypotheses: inst_2
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
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
⊢ LawfulTraversable.{u} (t α)
have id_traverse : ∀ {α_1 : Type u} (x : t α α_1), Eq (α := Id (t α α_1)) (traverse pure x) (pure x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
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)
⊢ LawfulTraversable.{u} (t α)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
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)
⊢ LawfulTraversable.{u} (t α)
have traverse_eq_map_id : ∀ {α_1 β : Type u} (f : α_1 → β) (x : t α α_1), Eq (α := Id (t α β)) (traverse (pure ∘ f) x) (pure (f <$> x))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
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))
⊢ LawfulTraversable.{u} (t α)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
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
⊢ Eq (α := G (t α β)) ((fun {α : Type u} ↦ η.app α) (traverse f x)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)
have naturality : η.app (t α β) (tsnd (t := t) f x) = tsnd (t := t) (η.app β ∘ f) x
Tactic: simp [traverse, comp_tsnd, functor_norm]
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
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
⊢ LawfulBitraversable.{u} (bicompl t F G)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
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)
⊢ LawfulBitraversable.{u} (bicompl t F G)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
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)
⊢ LawfulBitraversable.{u} (bicompl t F G)
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
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))
⊢ LawfulBitraversable.{u} (bicompl t F G)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
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 α α'
⊢ 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))
have 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))
Tactic: simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse,
      functor_norm]
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
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 α α'
⊢ 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)
have binaturality : η.app (bicompl t F G β β') (bitraverse (t := t) (traverse f) (traverse f') x) =
  bitraverse (t := t) (traverse (η.app β ∘ f)) (traverse (η.app β' ∘ f')) x
Tactic: simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse,
      functor_norm]
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
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 α α'
⊢ η.app (bicompl t F G β β') (bitraverse (t := t) (traverse f) (traverse f') x) =
    bitraverse (t := t) (traverse (η.app β ∘ f)) (traverse (η.app β' ∘ f')) x
have binaturality : η.app (t (F β) (G β')) (bitraverse (t := t) (traverse f) (traverse f') x) =
  bitraverse (t := t) (traverse (η.app β ∘ f)) (traverse (η.app β' ∘ f')) x
Tactic: dsimp only [bicompl]
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
⊢ LawfulBitraversable.{u} (bicompr F t)
have id_bitraverse : ∀ {α β : Type u} (x : bicompr F t α β),
  Eq (α := Id (bicompr F t α β)) (bitraverse (t := bicompr F t) pure pure x) (pure x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
id_bitraverse :
  ∀ {α β : Type u} (x : bicompr F t α β),
    Eq (α := Id (bicompr F t α β)) (bitraverse (t := bicompr F t) pure pure x) (pure x)
⊢ LawfulBitraversable.{u} (bicompr F t)
have comp_bitraverse : ∀ {F_1 G : Type u → Type u} [inst_4 : Applicative F_1] [inst_5 : Applicative G] [LawfulApplicative F_1]
  [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F_1 γ) (f' : β' → F_1 γ') (g : α → G β) (g' : α' → G β')
  (x : bicompr F t α α'),
  bitraverse (t := bicompr F t) (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
    Functor.Comp.mk (bitraverse (t := bicompr F t) f f' <$> bitraverse (t := bicompr F t) g g' x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
id_bitraverse :
  ∀ {α β : Type u} (x : bicompr F t α β),
    Eq (α := Id (bicompr F t α β)) (bitraverse (t := bicompr F t) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F_1 G : Type u → Type u} [inst_4 : Applicative F_1] [inst_5 : Applicative G] [LawfulApplicative F_1]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F_1 γ) (f' : β' → F_1 γ') (g : α → G β) (g' : α' → G β')
    (x : bicompr F t α α'),
    bitraverse (t := bicompr F t) (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
      Functor.Comp.mk (bitraverse (t := bicompr F t) f f' <$> bitraverse (t := bicompr F t) g g' x)
⊢ LawfulBitraversable.{u} (bicompr F t)
have bitraverse_eq_bimap_id : ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : bicompr F t α α'),
  Eq (α := Id (bicompr F t β β')) (bitraverse (t := bicompr F t) (pure ∘ f) (pure ∘ f') x)
    (pure (bimap (F := bicompr F t) f f' x))
Tactic: constructor