[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
x✝ d₂ : D
f : x✝ ⟶ d₂
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    ((fun d =>
                Functor.mk
                  { obj := fun t => ∐ fun x => d,
                    map := fun {X Y} f => Sigma.desc fun g => Sigma.ι (fun x => d) (g ≫ f) })
              x✝).map
          f_1 ≫
        (fun e => Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) Y =
      (fun e => Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) X ≫
        ((fun d =>
                Functor.mk
                  { obj := fun t => ∐ fun x => d,
                    map := fun {X Y} f => Sigma.desc fun g => Sigma.ι (fun x => d) (g ≫ f) })
              d₂).map
          f_1
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
x✝ d₂ : D
f : x✝ ⟶ d₂
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ((fun d =>
              Functor.mk
                { obj := fun t => ∐ fun x => d,
                  map := fun {X Y} f => Sigma.desc fun g => Sigma.ι (fun x => d) (g ≫ f) })
            x✝).map
        f✝ ≫
      (fun e => Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) Y✝ =
    (fun e => Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) X✝ ≫
      ((fun d =>
              Functor.mk
                { obj := fun t => ∐ fun x => d,
                  map := fun {X Y} f => Sigma.desc fun g => Sigma.ι (fun x => d) (g ≫ f) })
            d₂).map
        f✝
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
x✝ d₂ : D
f : x✝ ⟶ d₂
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ((Sigma.desc fun g => Sigma.ι (fun x => x✝) (g ≫ f✝)) ≫ Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) =
    (Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) ≫ Sigma.desc fun g => Sigma.ι (fun x => d₂) (g ≫ f✝)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
x✝ d₂ : D
f : x✝ ⟶ d₂
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
b✝ : c ⟶ X✝
⊢ (Sigma.ι (fun x => x✝) b✝ ≫
      (Sigma.desc fun g => Sigma.ι (fun x => x✝) (g ≫ f✝)) ≫ Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) =
    Sigma.ι (fun x => x✝) b✝ ≫
      (Sigma.desc fun h => f ≫ Sigma.ι (fun x => d₂) h) ≫ Sigma.desc fun g => Sigma.ι (fun x => d₂) (g ≫ f✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : d ⟶ ((evaluation C D).obj c).obj F
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    ((evaluationLeftAdjoint D c).obj d).map f_1 ≫ (fun e => Sigma.desc fun h => f ≫ F.map h) Y =
      (fun e => Sigma.desc fun h => f ≫ F.map h) X ≫ F.map f_1
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : d ⟶ ((evaluation C D).obj c).obj F
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ((evaluationLeftAdjoint D c).obj d).map f✝ ≫ (fun e => Sigma.desc fun h => f ≫ F.map h) Y✝ =
    (fun e => Sigma.desc fun h => f ≫ F.map h) X✝ ≫ F.map f✝
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : d ⟶ ((evaluation C D).obj c).obj F
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ((Sigma.desc fun g => Sigma.ι (fun x => d) (g ≫ f✝)) ≫ Sigma.desc fun h => f ≫ F.map h) =
    (Sigma.desc fun h => f ≫ F.map h) ≫ F.map f✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : d ⟶ ((evaluation C D).obj c).obj F
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
b✝ : c ⟶ X✝
⊢ (Sigma.ι (fun x => d) b✝ ≫ (Sigma.desc fun g => Sigma.ι (fun x => d) (g ≫ f✝)) ≫ Sigma.desc fun h => f ≫ F.map h) =
    Sigma.ι (fun x => d) b✝ ≫ (Sigma.desc fun h => f ≫ F.map h) ≫ F.map f✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
⊢ Function.LeftInverse (fun f => NatTrans.mk fun e => Sigma.desc fun h => f ≫ F.map h) fun f =>
    Sigma.ι (fun x => d) (𝟙 c) ≫ NatTrans.app f c
[PROOFSTEP]
intro f
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : (evaluationLeftAdjoint D c).obj d ⟶ F
⊢ (fun f => NatTrans.mk fun e => Sigma.desc fun h => f ≫ F.map h)
      ((fun f => Sigma.ι (fun x => d) (𝟙 c) ≫ NatTrans.app f c) f) =
    f
[PROOFSTEP]
ext x
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : (evaluationLeftAdjoint D c).obj d ⟶ F
x : C
⊢ NatTrans.app
      ((fun f => NatTrans.mk fun e => Sigma.desc fun h => f ≫ F.map h)
        ((fun f => Sigma.ι (fun x => d) (𝟙 c) ≫ NatTrans.app f c) f))
      x =
    NatTrans.app f x
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : (evaluationLeftAdjoint D c).obj d ⟶ F
x : C
⊢ (Sigma.desc fun h => (Sigma.ι (fun x => d) (𝟙 c) ≫ NatTrans.app f c) ≫ F.map h) = NatTrans.app f x
[PROOFSTEP]
ext g
[GOAL]
case w.h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : (evaluationLeftAdjoint D c).obj d ⟶ F
x : C
g : c ⟶ x
⊢ (Sigma.ι (fun x => d) g ≫ Sigma.desc fun h => (Sigma.ι (fun x => d) (𝟙 c) ≫ NatTrans.app f c) ≫ F.map h) =
    Sigma.ι (fun x => d) g ≫ NatTrans.app f x
[PROOFSTEP]
simp only [colimit.ι_desc, Cofan.mk_ι_app, Category.assoc, ← f.naturality, evaluationLeftAdjoint_obj_map,
  colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Discrete.natTrans_app, Category.id_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : d ⟶ ((evaluation C D).obj c).obj F
⊢ (fun f => Sigma.ι (fun x => d) (𝟙 c) ≫ NatTrans.app f c)
      ((fun f => NatTrans.mk fun e => Sigma.desc fun h => f ≫ F.map h) f) =
    f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : d ⟶ ((evaluation C D).obj c).obj F
⊢ (Sigma.ι (fun x => d) (𝟙 c) ≫ Sigma.desc fun h => f ≫ F.map h) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Mono η ↔ ∀ (c : C), Mono (app η c)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Mono η → ∀ (c : C), Mono (app η c)
[PROOFSTEP]
intro h c
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
h : Mono η
c : C
⊢ Mono (app η c)
[PROOFSTEP]
exact (inferInstance : Mono (((evaluation _ _).obj c).map η))
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ (∀ (c : C), Mono (app η c)) → Mono η
[PROOFSTEP]
intro _
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
a✝ : ∀ (c : C), Mono (app η c)
⊢ Mono η
[PROOFSTEP]
apply NatTrans.mono_of_mono_app
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    ((fun d =>
                Functor.mk
                  { obj := fun t => ∏ fun x => d, map := fun {X Y} f => Pi.lift fun g => Pi.π (fun x => d) (f ≫ g) })
              X✝).map
          f_1 ≫
        (fun t => Pi.lift fun g => Pi.π (fun x => X✝) g ≫ f) Y =
      (fun t => Pi.lift fun g => Pi.π (fun x => X✝) g ≫ f) X ≫
        ((fun d =>
                Functor.mk
                  { obj := fun t => ∏ fun x => d, map := fun {X Y} f => Pi.lift fun g => Pi.π (fun x => d) (f ≫ g) })
              Y✝).map
          f_1
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
X✝¹ Y✝¹ : D
f : X✝¹ ⟶ Y✝¹
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ((fun d =>
              Functor.mk
                { obj := fun t => ∏ fun x => d, map := fun {X Y} f => Pi.lift fun g => Pi.π (fun x => d) (f ≫ g) })
            X✝¹).map
        f✝ ≫
      (fun t => Pi.lift fun g => Pi.π (fun x => X✝¹) g ≫ f) Y✝ =
    (fun t => Pi.lift fun g => Pi.π (fun x => X✝¹) g ≫ f) X✝ ≫
      ((fun d =>
              Functor.mk
                { obj := fun t => ∏ fun x => d, map := fun {X Y} f => Pi.lift fun g => Pi.π (fun x => d) (f ≫ g) })
            Y✝¹).map
        f✝
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
X✝¹ Y✝¹ : D
f : X✝¹ ⟶ Y✝¹
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ((Pi.lift fun g => Pi.π (fun x => X✝¹) (f✝ ≫ g)) ≫ Pi.lift fun g => Pi.π (fun x => X✝¹) g ≫ f) =
    (Pi.lift fun g => Pi.π (fun x => X✝¹) g ≫ f) ≫ Pi.lift fun g => Pi.π (fun x => Y✝¹) (f✝ ≫ g)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
X✝¹ Y✝¹ : D
f : X✝¹ ⟶ Y✝¹
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
b✝ : Y✝ ⟶ c
⊢ ((Pi.lift fun g => Pi.π (fun x => X✝¹) (f✝ ≫ g)) ≫ Pi.lift fun g => Pi.π (fun x => X✝¹) g ≫ f) ≫
      Pi.π (fun x => Y✝¹) b✝ =
    ((Pi.lift fun g => Pi.π (fun x => X✝¹) g ≫ f) ≫ Pi.lift fun g => Pi.π (fun x => Y✝¹) (f✝ ≫ g)) ≫
      Pi.π (fun x => Y✝¹) b✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : ((evaluation C D).obj c).obj F ⟶ d
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    F.map f_1 ≫ (fun t => Pi.lift fun g => F.map g ≫ f) Y =
      (fun t => Pi.lift fun g => F.map g ≫ f) X ≫ ((evaluationRightAdjoint D c).obj d).map f_1
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : ((evaluation C D).obj c).obj F ⟶ d
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ F.map f✝ ≫ (fun t => Pi.lift fun g => F.map g ≫ f) Y✝ =
    (fun t => Pi.lift fun g => F.map g ≫ f) X✝ ≫ ((evaluationRightAdjoint D c).obj d).map f✝
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : ((evaluation C D).obj c).obj F ⟶ d
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (F.map f✝ ≫ Pi.lift fun g => F.map g ≫ f) =
    (Pi.lift fun g => F.map g ≫ f) ≫ Pi.lift fun g => Pi.π (fun x => d) (f✝ ≫ g)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : ((evaluation C D).obj c).obj F ⟶ d
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
b✝ : Y✝ ⟶ c
⊢ (F.map f✝ ≫ Pi.lift fun g => F.map g ≫ f) ≫ Pi.π (fun x => d) b✝ =
    ((Pi.lift fun g => F.map g ≫ f) ≫ Pi.lift fun g => Pi.π (fun x => d) (f✝ ≫ g)) ≫ Pi.π (fun x => d) b✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : ((evaluation C D).obj c).obj F ⟶ d
⊢ (fun f => NatTrans.app f c ≫ Pi.π (fun x => d) (𝟙 c))
      ((fun f => NatTrans.mk fun t => Pi.lift fun g => F.map g ≫ f) f) =
    f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : ((evaluation C D).obj c).obj F ⟶ d
⊢ (Pi.lift fun g => F.map g ≫ f) ≫ Pi.π (fun x => d) (𝟙 c) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
⊢ Function.RightInverse (fun f => NatTrans.app f c ≫ Pi.π (fun x => d) (𝟙 c)) fun f =>
    NatTrans.mk fun t => Pi.lift fun g => F.map g ≫ f
[PROOFSTEP]
intro f
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : F ⟶ (evaluationRightAdjoint D c).obj d
⊢ (fun f => NatTrans.mk fun t => Pi.lift fun g => F.map g ≫ f)
      ((fun f => NatTrans.app f c ≫ Pi.π (fun x => d) (𝟙 c)) f) =
    f
[PROOFSTEP]
ext x
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : F ⟶ (evaluationRightAdjoint D c).obj d
x : C
⊢ NatTrans.app
      ((fun f => NatTrans.mk fun t => Pi.lift fun g => F.map g ≫ f)
        ((fun f => NatTrans.app f c ≫ Pi.π (fun x => d) (𝟙 c)) f))
      x =
    NatTrans.app f x
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : F ⟶ (evaluationRightAdjoint D c).obj d
x : C
⊢ (Pi.lift fun g => F.map g ≫ NatTrans.app f c ≫ Pi.π (fun x => d) (𝟙 c)) = NatTrans.app f x
[PROOFSTEP]
ext g
[GOAL]
case w.h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : F ⟶ (evaluationRightAdjoint D c).obj d
x : C
g : x ⟶ c
⊢ (Pi.lift fun g => F.map g ≫ NatTrans.app f c ≫ Pi.π (fun x => d) (𝟙 c)) ≫ Pi.π (fun x => d) g =
    NatTrans.app f x ≫ Pi.π (fun x => d) g
[PROOFSTEP]
simp only [Discrete.functor_obj, NatTrans.naturality_assoc, evaluationRightAdjoint_obj_obj,
  evaluationRightAdjoint_obj_map, limit.lift_π, Fan.mk_pt, Fan.mk_π_app, Discrete.natTrans_app, Category.comp_id]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Epi η ↔ ∀ (c : C), Epi (app η c)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Epi η → ∀ (c : C), Epi (app η c)
[PROOFSTEP]
intro h c
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
h : Epi η
c : C
⊢ Epi (app η c)
[PROOFSTEP]
exact (inferInstance : Epi (((evaluation _ _).obj c).map η))
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ (∀ (c : C), Epi (app η c)) → Epi η
[PROOFSTEP]
intros
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
a✝ : ∀ (c : C), Epi (app η c)
⊢ Epi η
[PROOFSTEP]
apply NatTrans.epi_of_epi_app
