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
⊢ LawfulBitraversable Sum

Tactic:
constructor <;> intros <;> casesm _ ⊕ _

Goal state after:
case id_bitraverse.inl
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type u_1
x✝ : α✝
⊢ bitraverse pure pure (Sum.inl x✝) = pure (Sum.inl x✝)

case id_bitraverse.inr
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type u_1
x✝ : β✝
⊢ bitraverse pure pure (Sum.inr x✝) = pure (Sum.inr x✝)

case comp_bitraverse.inl
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u_1
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : α✝
⊢ bitraverse (Comp.mk ∘ map f✝ ∘ g✝) (Comp.mk ∘ map f'✝ ∘ g'✝) (Sum.inl x✝) =
    Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ (Sum.inl x✝))

case comp_bitraverse.inr
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u_1
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : α'✝
⊢ bitraverse (Comp.mk ∘ map f✝ ∘ g✝) (Comp.mk ∘ map f'✝ ∘ g'✝) (Sum.inr x✝) =
    Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ (Sum.inr x✝))

case bitraverse_eq_bimap_id.inl
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : α✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) (Sum.inl x✝) = pure (bimap f✝ f'✝ (Sum.inl x✝))

case bitraverse_eq_bimap_id.inr
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) (Sum.inr x✝) = pure (bimap f✝ f'✝ (Sum.inr x✝))

case binaturality.inl
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : α✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ (Sum.inl x✝)) =
    bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) (Sum.inl x✝)

case binaturality.inr
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : α'✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ (Sum.inr x✝)) =
    bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) (Sum.inr x✝)