Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (_root_.flip t)

Tactic:
constructor <;> intros <;> casesm LawfulBitraversable t

Goal state after:
case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type u
x✝ : _root_.flip t α✝ β✝
toLawfulBifunctor✝ : LawfulBifunctor t
id_bitraverse✝ : ∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x
comp_bitraverse✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') (x : t α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
bitraverse_eq_bimap_id✝ :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
binaturality✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β') (x : t α α'),
    (fun {α} ↦ η.app α) (bitraverse f f' x) = bitraverse ((fun {α} ↦ η.app α) ∘ f) ((fun {α} ↦ η.app α) ∘ f') x
⊢ bitraverse pure pure x✝ = pure x✝

case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : _root_.flip t α✝ α'✝
toLawfulBifunctor✝ : LawfulBifunctor t
id_bitraverse✝ : ∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x
comp_bitraverse✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') (x : t α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
bitraverse_eq_bimap_id✝ :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
binaturality✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β') (x : t α α'),
    (fun {α} ↦ η.app α) (bitraverse f f' x) = bitraverse ((fun {α} ↦ η.app α) ∘ f) ((fun {α} ↦ η.app α) ∘ f') x
⊢ bitraverse (Comp.mk ∘ map f✝ ∘ g✝) (Comp.mk ∘ map f'✝ ∘ g'✝) x✝ = Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)

case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : _root_.flip t α✝ α'✝
toLawfulBifunctor✝ : LawfulBifunctor t
id_bitraverse✝ : ∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x
comp_bitraverse✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') (x : t α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
bitraverse_eq_bimap_id✝ :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
binaturality✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β') (x : t α α'),
    (fun {α} ↦ η.app α) (bitraverse f f' x) = bitraverse ((fun {α} ↦ η.app α) ∘ f) ((fun {α} ↦ η.app α) ∘ f') x
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)

case binaturality
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : _root_.flip t α✝ α'✝
toLawfulBifunctor✝ : LawfulBifunctor t
id_bitraverse✝ : ∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x
comp_bitraverse✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') (x : t α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
bitraverse_eq_bimap_id✝ :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
binaturality✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β') (x : t α α'),
    (fun {α} ↦ η.app α) (bitraverse f f' x) = bitraverse ((fun {α} ↦ η.app α) ∘ f) ((fun {α} ↦ η.app α) ∘ f') x
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ x✝) = bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) x✝