awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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' x))
    (bitraverse (t := Sum) ((fun {α : Type u_1} ↦ η.app α) ∘ f) ((fun {α : Type u_1} ↦ η.app α) ∘ f') x)
have 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))
Tactic: casesm _ ⊕ _
Cleared hypotheses: x
-- 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
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))
⊢ 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)
have 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))
Tactic: casesm _ ⊕ _
Cleared hypotheses: x
-- 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
α α' β β' : Type u_1
f : α → β
f' : α' → β'
x : α
⊢ Eq (α := Id (β ⊕ β')) (bitraverse (t := Sum) (pure ∘ f) (pure ∘ f') (Sum.inl x))
    (pure (bimap (F := Sum) f f' (Sum.inl x)))
have bitraverse_eq_bimap_id : Eq (α := Id (β ⊕ β')) (pure (Sum.inl (f x))) (pure (bimap (F := Sum) f f' (Sum.inl x)))
Tactic: simp [bitraverse, Sum.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 : Type u → Type u
inst_1 : Applicative F
α α' β β' : Type u_1
f : α → β
f' : α' → β'
x : α'
⊢ Eq (α := Id (β ⊕ β')) (bitraverse (t := Sum) (pure ∘ f) (pure ∘ f') (Sum.inr x))
    (pure (bimap (F := Sum) f f' (Sum.inr x)))
have bitraverse_eq_bimap_id : Eq (α := Id (β ⊕ β')) (pure (Sum.inr (f' x))) (pure (bimap (F := Sum) f f' (Sum.inr x)))
Tactic: simp [bitraverse, Sum.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 : Type u → Type u
inst_1 : Applicative F
⊢ LawfulBitraversable Const
have id_bitraverse : ∀ {α β : Type u_1} (x : Const α β), Eq (α := Id (Const α β)) (bitraverse (t := Const) 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 : Applicative F
id_bitraverse :
  ∀ {α β : Type u_1} (x : Const α β), Eq (α := Id (Const α β)) (bitraverse (t := Const) pure pure x) (pure x)
⊢ LawfulBitraversable Const
have 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)
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
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)
⊢ LawfulBitraversable Const
have 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))
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
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))
⊢ LawfulBitraversable Const
have 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)
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
α β : Type u_1
x : Const α β
⊢ Eq (α := Id (Const α β)) (bitraverse (t := Const) pure pure x) (pure x)
have id_bitraverse : Eq (α := Id (Const α β)) (pure x) (pure x)
Tactic: simp [bitraverse, Const.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 : 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 α α'
⊢ 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)
have comp_bitraverse : Comp.mk (f <$> g x) = Comp.mk (f <$> g x)
Tactic: simp [bitraverse, Const.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 : Type u → Type u
inst_1 : Applicative F
α α' β β' : 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))
have bitraverse_eq_bimap_id : Eq (α := Id (Const β β')) (pure (f x)) (pure (bimap (F := Const) f f' x))
Tactic: simp [bitraverse, Const.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 : 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 α α'
⊢ 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)
have binaturality : η.app (Const β β') (f x) = η.app β (f x)
Tactic: simp [bitraverse, Const.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 : Type u → Type u
inst_1 : Applicative F
inst_2 : LawfulBitraversable t
⊢ LawfulBitraversable.{u} (_root_.flip t)
have id_bitraverse : ∀ {α β : Type u} (x : _root_.flip t α β),
  Eq (α := Id (_root_.flip t α β)) (bitraverse (t := _root_.flip 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 : 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)
⊢ LawfulBitraversable.{u} (_root_.flip t)
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 : _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)
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
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)
⊢ LawfulBitraversable.{u} (_root_.flip t)
have 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))
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
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))
⊢ LawfulBitraversable.{u} (_root_.flip t)
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 : _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)
Tactic: constructor
-- 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
x : _root_.flip t α β
⊢ Eq (α := Id (_root_.flip t α β)) (bitraverse (t := _root_.flip t) pure pure x) (pure 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
α β : Type u
x : _root_.flip t α β
toLawfulBifunctor : LawfulBifunctor t
⊢ Eq (α := Id (_root_.flip t α β)) (bitraverse (t := _root_.flip t) pure pure x) (pure 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
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 pure x) (pure 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
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 pure x) (pure 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
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 pure x) (pure 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
α α' β β' γ γ' : Type u
f : β → F_1 γ
f' : β' → F_1 γ'
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)
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
α α' β β' γ γ' : Type u
f : β → F_1 γ
f' : β' → F_1 γ'
g : α → G β
g' : α' → G β'
x : _root_.flip t α α'
toLawfulBifunctor : LawfulBifunctor 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)
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
α α' β β' γ γ' : 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)
⊢ 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)
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
α α' β β' γ γ' : 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 (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)
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
α α' β β' γ γ' : 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))
⊢ 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)
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 (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 α α'
⊢ 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 toLawfulBifunctor : LawfulBifunctor t
Tactic: casesm LawfulBitraversable t
Cleared hypotheses: inst_2