[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ Category.{?u.391, u + 1} (KleisliCat m)
[PROOFSTEP]
refine' { id_comp := _, comp_id := _, assoc := _ }
[GOAL]
case refine'_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {X Y : KleisliCat m} (f : X ⟶ Y), 𝟙 X ≫ f = f
[PROOFSTEP]
intros
[GOAL]
case refine'_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {X Y : KleisliCat m} (f : X ⟶ Y), f ≫ 𝟙 Y = f
[PROOFSTEP]
intros
[GOAL]
case refine'_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {W X Y Z : KleisliCat m} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
intros
[GOAL]
case refine'_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f✝ = f✝
[PROOFSTEP]
refine funext (fun x => ?_)
[GOAL]
case refine'_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
⊢ f✝ ≫ 𝟙 Y✝ = f✝
[PROOFSTEP]
refine funext (fun x => ?_)
[GOAL]
case refine'_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
W✝ X✝ Y✝ Z✝ : KleisliCat m
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
[PROOFSTEP]
refine funext (fun x => ?_)
[GOAL]
case refine'_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
x : X✝
⊢ (𝟙 X✝ ≫ f✝) x = f✝ x
[PROOFSTEP]
simp [CategoryStruct.id, CategoryStruct.comp, (· >=> ·)]
[GOAL]
case refine'_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
x : X✝
⊢ (f✝ ≫ 𝟙 Y✝) x = f✝ x
[PROOFSTEP]
simp [CategoryStruct.id, CategoryStruct.comp, (· >=> ·)]
[GOAL]
case refine'_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
W✝ X✝ Y✝ Z✝ : KleisliCat m
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
x : W✝
⊢ ((f✝ ≫ g✝) ≫ h✝) x = (f✝ ≫ g✝ ≫ h✝) x
[PROOFSTEP]
simp [CategoryStruct.id, CategoryStruct.comp, (· >=> ·)]
