[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α₀ α₁ α₂ : Type u₀
β : Type u₁
f : α₀ → α₁
f' : α₁ → α₂
x : F α₀ β
⊢ fst f' (fst f x) = fst (f' ∘ f) x
[PROOFSTEP]
simp [fst, bimap_bimap]
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α₀ α₁ : Type u₀
β₀ β₁ : Type u₁
f : α₀ → α₁
f' : β₀ → β₁
x : F α₀ β₀
⊢ fst f (snd f' x) = bimap f f' x
[PROOFSTEP]
simp [fst, bimap_bimap]
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α₀ α₁ : Type u₀
β₀ β₁ : Type u₁
f : α₀ → α₁
f' : β₀ → β₁
x : F α₀ β₀
⊢ snd f' (fst f x) = bimap f f' x
[PROOFSTEP]
simp [snd, bimap_bimap]
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
β₀ β₁ β₂ : Type u₁
g : β₀ → β₁
g' : β₁ → β₂
x : F α β₀
⊢ snd g' (snd g x) = snd (g' ∘ g) x
[PROOFSTEP]
simp [snd, bimap_bimap]
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ LawfulBifunctor Prod
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ ∀ {α : Type ?u.3875} {β : Type ?u.3874} (x : α × β), bimap id id x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type ?u.3875} {β₀ β₁ β₂ : Type ?u.3874} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
    (x : α₀ × β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
α✝ : Type ?u.3875
β✝ : Type ?u.3874
x✝ : α✝ × β✝
⊢ bimap id id x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
α₀✝ α₁✝ α₂✝ : Type ?u.3875
β₀✝ β₁✝ β₂✝ : Type ?u.3874
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : α₀✝ × β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ LawfulBifunctor Const
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ ∀ {α : Type ?u.4176} {β : Type ?u.4177} (x : Const α β), bimap id id x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type ?u.4176} {β₀ β₁ β₂ : Type ?u.4177} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
    (x : Const α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
α✝ : Type ?u.4176
β✝ : Type ?u.4177
x✝ : Const α✝ β✝
⊢ bimap id id x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
α₀✝ α₁✝ α₂✝ : Type ?u.4176
β₀✝ β₁✝ β₂✝ : Type ?u.4177
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : Const α₀✝ β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
⊢ LawfulBifunctor (_root_.flip F)
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
⊢ ∀ {α : Type u₁} {β : Type u₀} (x : _root_.flip F α β), bimap id id x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type u₁} {β₀ β₁ β₂ : Type u₀} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
    (x : _root_.flip F α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α✝ : Type u₁
β✝ : Type u₀
x✝ : _root_.flip F α✝ β✝
⊢ bimap id id x✝ = x✝
[PROOFSTEP]
simp [bimap, functor_norm]
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α₀✝ α₁✝ α₂✝ : Type u₁
β₀✝ β₁✝ β₂✝ : Type u₀
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : _root_.flip F α₀✝ β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝
[PROOFSTEP]
simp [bimap, functor_norm]
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ LawfulBifunctor Sum
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ ∀ {α : Type ?u.4990} {β : Type ?u.4989} (x : α ⊕ β), bimap id id x = x
[PROOFSTEP]
aesop
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝ : Bifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type ?u.4990} {β₀ β₁ β₂ : Type ?u.4989} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
    (x : α₀ ⊕ β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
[PROOFSTEP]
aesop
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
⊢ LawfulFunctor (F α)
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
⊢ ∀ {α_1 β : Type u₁}, mapConst = map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
⊢ ∀ {α_1 : Type u₁} (x : F α α_1), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_3
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
⊢ ∀ {α_1 β γ : Type u₁} (g : α_1 → β) (h : β → γ) (x : F α α_1), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
α✝ β✝ : Type u₁
⊢ mapConst = map ∘ Function.const β✝
[PROOFSTEP]
simp [mapConst, Functor.map, functor_norm]
[GOAL]
case refine'_2
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
α✝ : Type u₁
x✝ : F α α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
simp [mapConst, Functor.map, functor_norm]
[GOAL]
case refine'_3
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
α✝ β✝ γ✝ : Type u₁
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : F α α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
simp [mapConst, Functor.map, functor_norm]
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
⊢ LawfulBifunctor (bicompl F G H)
[PROOFSTEP]
constructor
[GOAL]
case id_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
⊢ ∀ {α : Type u_1} {β : Type u_2} (x : bicompl F G H α β), bimap id id x = x
[PROOFSTEP]
intros
[GOAL]
case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type u_1} {β₀ β₁ β₂ : Type u_2} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
    (x : bicompl F G H α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
[PROOFSTEP]
intros
[GOAL]
case id_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
α✝ : Type u_1
β✝ : Type u_2
x✝ : bicompl F G H α✝ β✝
⊢ bimap id id x✝ = x✝
[PROOFSTEP]
simp [bimap, map_id, map_comp_map, functor_norm]
[GOAL]
case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
α₀✝ α₁✝ α₂✝ : Type u_1
β₀✝ β₁✝ β₂✝ : Type u_2
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : bicompl F G H α₀✝ β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝
[PROOFSTEP]
simp [bimap, map_id, map_comp_map, functor_norm]
[GOAL]
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
⊢ LawfulBifunctor (bicompr G F)
[PROOFSTEP]
constructor
[GOAL]
case id_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
⊢ ∀ {α : Type u₀} {β : Type u₁} (x : bicompr G F α β), bimap id id x = x
[PROOFSTEP]
intros
[GOAL]
case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type u₀} {β₀ β₁ β₂ : Type u₁} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
    (x : bicompr G F α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
[PROOFSTEP]
intros
[GOAL]
case id_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
α✝ : Type u₀
β✝ : Type u₁
x✝ : bicompr G F α✝ β✝
⊢ bimap id id x✝ = x✝
[PROOFSTEP]
simp [bimap, functor_norm]
[GOAL]
case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
α₀✝ α₁✝ α₂✝ : Type u₀
β₀✝ β₁✝ β₂✝ : Type u₁
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : bicompr G F α₀✝ β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝
[PROOFSTEP]
simp [bimap, functor_norm]
