[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β✝ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ α₂ β : Type u
f : α₀ → F α₁
f' : α₁ → G α₂
x : t α₀ β
⊢ Comp.mk (tfst f' <$> tfst f x) = tfst (Comp.mk ∘ map f' ∘ f) x
[PROOFSTEP]
rw [← comp_bitraverse]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β✝ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ α₂ β : Type u
f : α₀ → F α₁
f' : α₁ → G α₂
x : t α₀ β
⊢ bitraverse (Comp.mk ∘ map f' ∘ f) (Comp.mk ∘ map pure ∘ pure) x = tfst (Comp.mk ∘ map f' ∘ f) x
[PROOFSTEP]
simp only [Function.comp, tfst, map_pure, Pure.pure]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ Comp.mk (tfst f <$> tsnd f' x) = bitraverse (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x
[PROOFSTEP]
rw [← comp_bitraverse]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ bitraverse (Comp.mk ∘ map f ∘ pure) (Comp.mk ∘ map pure ∘ f') x =
    bitraverse (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x
[PROOFSTEP]
simp only [Function.comp, map_pure]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ Comp.mk (tsnd f' <$> tfst f x) = bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x
[PROOFSTEP]
rw [← comp_bitraverse]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ map f' ∘ pure) x =
    bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x
[PROOFSTEP]
simp only [Function.comp, map_pure]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ Comp.mk (tsnd g' <$> tsnd g x) = tsnd (Comp.mk ∘ map g' ∘ g) x
[PROOFSTEP]
rw [← comp_bitraverse]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ bitraverse (Comp.mk ∘ map pure ∘ pure) (Comp.mk ∘ map g' ∘ g) x = tsnd (Comp.mk ∘ map g' ∘ g) x
[PROOFSTEP]
simp only [Function.comp, map_pure]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ bitraverse (fun x => Comp.mk (pure (pure x))) (fun x => Comp.mk (g' <$> g x)) x =
    tsnd (fun x => Comp.mk (g' <$> g x)) x
[PROOFSTEP]
rfl
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β✝ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α α' β : Type u
f : α → α'
x : t α β
⊢ tfst (pure ∘ f) x = pure (fst f x)
[PROOFSTEP]
apply bitraverse_eq_bimap_id
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
β✝ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β β' : Type u
f : β → β'
x : t α β
⊢ tsnd (pure ∘ f) x = pure (snd f x)
[PROOFSTEP]
apply bitraverse_eq_bimap_id
