[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : op X ⟶ op Y
⊢ (yoneda.obj X).map f (𝟙 X) = NatTrans.app (yoneda.map f.unop) (op Y) (𝟙 Y)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : op X ⟶ op Y
⊢ f.unop ≫ 𝟙 X = 𝟙 Y ≫ f.unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
p : yoneda.map f = yoneda.map g
⊢ f = g
[PROOFSTEP]
convert congr_fun (congr_app p (op X)) (𝟙 X) using 1
[GOAL]
case h.e'_2.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
p : yoneda.map f = yoneda.map g
e_1✝ : (X ⟶ Y) = (yoneda.obj Y).obj (op X)
⊢ f = NatTrans.app (yoneda.map f) (op X) (𝟙 X)
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
p : yoneda.map f = yoneda.map g
e_1✝ : (X ⟶ Y) = (yoneda.obj Y).obj (op X)
⊢ g = NatTrans.app (yoneda.map g) (op X) (𝟙 X)
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_2.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
p : yoneda.map f = yoneda.map g
e_1✝ : (X ⟶ Y) = (yoneda.obj Y).obj (op X)
⊢ f = 𝟙 X ≫ f
[PROOFSTEP]
simp
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
p : yoneda.map f = yoneda.map g
e_1✝ : (X ⟶ Y) = (yoneda.obj Y).obj (op X)
⊢ g = 𝟙 X ≫ g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : coyoneda.obj X ⟶ coyoneda.obj Y
⊢ coyoneda.map ((fun {X} x f => (NatTrans.app f X.unop (𝟙 X.unop)).op) Y f) = f
[PROOFSTEP]
simp only [coyoneda]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : coyoneda.obj X ⟶ coyoneda.obj Y
⊢ (NatTrans.mk fun Y_1 g => (NatTrans.app f X.unop (𝟙 X.unop)).op.unop ≫ g) = f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X x✝² : Cᵒᵖ
x✝¹ x✝ : X ⟶ x✝²
p : coyoneda.map x✝¹ = coyoneda.map x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
have t := congr_fun (congr_app p X.unop) (𝟙 _)
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X x✝² : Cᵒᵖ
x✝¹ x✝ : X ⟶ x✝²
p : coyoneda.map x✝¹ = coyoneda.map x✝
t : NatTrans.app (coyoneda.map x✝¹) X.unop (𝟙 X.unop) = NatTrans.app (coyoneda.map x✝) X.unop (𝟙 X.unop)
⊢ x✝¹ = x✝
[PROOFSTEP]
simpa using congr_arg Quiver.Hom.op t
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ ((reprW F).app X).hom f = F.map f.op (reprx F)
[PROOFSTEP]
change F.reprF.app X f = (F.reprF.app (op F.reprX) ≫ F.map f.op) (𝟙 F.reprX)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ NatTrans.app (reprF F) X f = (NatTrans.app (reprF F) (op (reprX F)) ≫ F.map f.op) (𝟙 (reprX F))
[PROOFSTEP]
rw [← F.reprF.naturality]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ NatTrans.app (reprF F) X f = ((yoneda.obj (reprX F)).map f.op ≫ NatTrans.app (reprF F) (op X.unop)) (𝟙 (reprX F))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ NatTrans.app (reprF F) X f = NatTrans.app (reprF F) X (f ≫ 𝟙 (reprX F))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ ((coreprW F).app X).hom f = F.map f (coreprx F)
[PROOFSTEP]
change F.coreprF.app X f = (F.coreprF.app F.coreprX ≫ F.map f) (𝟙 F.coreprX)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ NatTrans.app (coreprF F) X f = (NatTrans.app (coreprF F) (coreprX F) ≫ F.map f) (𝟙 (coreprX F))
[PROOFSTEP]
rw [← F.coreprF.naturality]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ NatTrans.app (coreprF F) X f = ((coyoneda.obj (op (coreprX F))).map f ≫ NatTrans.app (coreprF F) X) (𝟙 (coreprX F))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ NatTrans.app (coreprF F) X f = NatTrans.app (coreprF F) X (𝟙 (coreprX F) ≫ f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ ⦃X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)⦄ (f : X ⟶ Y),
    (yonedaPairing C).map f ≫ (fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) }) Y =
      (fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) }) X ≫ (yonedaEvaluation C).map f
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
⊢ (yonedaPairing C).map f ≫ (fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) }) Y =
    (fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) }) X ≫ (yonedaEvaluation C).map f
[PROOFSTEP]
simp only [yonedaEvaluation]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
⊢ ((yonedaPairing C).map f ≫ fun x => { down := NatTrans.app x Y.fst (𝟙 Y.fst.unop) }) =
    (fun x => { down := NatTrans.app x X.fst (𝟙 X.fst.unop) }) ≫
      (evaluationUncurried Cᵒᵖ (Type v₁) ⋙ uliftFunctor.{u₁, v₁}).map f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
a✝ : (yonedaPairing C).obj X
⊢ ((yonedaPairing C).map f ≫ fun x => { down := NatTrans.app x Y.fst (𝟙 Y.fst.unop) }) a✝ =
    ((fun x => { down := NatTrans.app x X.fst (𝟙 X.fst.unop) }) ≫
        (evaluationUncurried Cᵒᵖ (Type v₁) ⋙ uliftFunctor.{u₁, v₁}).map f)
      a✝
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
a✝ : (yonedaPairing C).obj X
⊢ { down := NatTrans.app f.snd Y.fst (NatTrans.app a✝ Y.fst (𝟙 Y.fst.unop ≫ f.fst.unop)) } =
    { down := NatTrans.app f.snd Y.fst (X.snd.map f.fst (NatTrans.app a✝ X.fst (𝟙 X.fst.unop))) }
[PROOFSTEP]
erw [Category.id_comp, ← FunctorToTypes.naturality]
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
a✝ : (yonedaPairing C).obj X
⊢ { down := NatTrans.app f.snd Y.fst (NatTrans.app a✝ Y.fst f.fst.unop) } =
    { down := NatTrans.app f.snd Y.fst (NatTrans.app a✝ Y.fst ((yoneda.obj X.fst.unop).map f.fst (𝟙 X.fst.unop))) }
[PROOFSTEP]
simp only [Category.comp_id, yoneda_obj_map]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
x : (yonedaEvaluation C).obj F
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).fst.unop.map f ≫ (fun X a => F.snd.map a.op x.down) Y =
      (fun X a => F.snd.map a.op x.down) X ≫ ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).snd.map f
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
x : (yonedaEvaluation C).obj F
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).fst.unop.map f ≫ (fun X a => F.snd.map a.op x.down) Y =
    (fun X a => F.snd.map a.op x.down) X ≫ ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).snd.map f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
x : (yonedaEvaluation C).obj F
X Y : Cᵒᵖ
f : X ⟶ Y
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).fst.unop.obj X
⊢ (((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).fst.unop.map f ≫ (fun X a => F.snd.map a.op x.down) Y) a✝ =
    ((fun X a => F.snd.map a.op x.down) X ≫ ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).snd.map f) a✝
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
x : (yonedaEvaluation C).obj F
X Y : Cᵒᵖ
f : X ⟶ Y
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).fst.unop.obj X
⊢ F.snd.map (a✝.op ≫ f) x.down = F.snd.map f (F.snd.map a✝.op x.down)
[PROOFSTEP]
rw [FunctorToTypes.map_comp_apply]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ ⦃X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)⦄ (f : X ⟶ Y),
    (yonedaEvaluation C).map f ≫ (fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down) Y =
      (fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down) X ≫ (yonedaPairing C).map f
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
⊢ (yonedaEvaluation C).map f ≫ (fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down) Y =
    (fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down) X ≫ (yonedaPairing C).map f
[PROOFSTEP]
simp only [yoneda]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
⊢ ((yonedaEvaluation C).map f ≫ fun x => NatTrans.mk fun X a => Y.snd.map a.op x.down) =
    (fun x => NatTrans.mk fun X_1 a => X.snd.map a.op x.down) ≫ (yonedaPairing C).map f
[PROOFSTEP]
ext
[GOAL]
case h.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
a✝¹ : (yonedaEvaluation C).obj X
Y✝ : Cᵒᵖ
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj Y).fst.unop.obj Y✝
⊢ NatTrans.app (((yonedaEvaluation C).map f ≫ fun x => NatTrans.mk fun X a => Y.snd.map a.op x.down) a✝¹) Y✝ a✝ =
    NatTrans.app (((fun x => NatTrans.mk fun X_1 a => X.snd.map a.op x.down) ≫ (yonedaPairing C).map f) a✝¹) Y✝ a✝
[PROOFSTEP]
dsimp
[GOAL]
case h.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
a✝¹ : (yonedaEvaluation C).obj X
Y✝ : Cᵒᵖ
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj Y).fst.unop.obj Y✝
⊢ Y.snd.map a✝.op (NatTrans.app f.snd Y.fst (X.snd.map f.fst a✝¹.down)) =
    NatTrans.app f.snd Y✝ (X.snd.map (f.fst ≫ a✝.op) a✝¹.down)
[PROOFSTEP]
rw [← FunctorToTypes.naturality X.snd Y.snd f.snd, FunctorToTypes.map_comp_apply]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ((NatTrans.mk fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) }) ≫
      NatTrans.mk fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down) =
    𝟙 (yonedaPairing C)
[PROOFSTEP]
ext
[GOAL]
case w.h.h.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
a✝¹ : (yonedaPairing C).obj x✝
Y✝ : Cᵒᵖ
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj x✝).fst.unop.obj Y✝
⊢ NatTrans.app
      (NatTrans.app
        ((NatTrans.mk fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) }) ≫
          NatTrans.mk fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down)
        x✝ a✝¹)
      Y✝ a✝ =
    NatTrans.app (NatTrans.app (𝟙 (yonedaPairing C)) x✝ a✝¹) Y✝ a✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
a✝¹ : (yonedaPairing C).obj x✝
Y✝ : Cᵒᵖ
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj x✝).fst.unop.obj Y✝
⊢ x✝.snd.map a✝.op (NatTrans.app a✝¹ x✝.fst (𝟙 x✝.fst.unop)) = NatTrans.app a✝¹ Y✝ a✝
[PROOFSTEP]
erw [← FunctorToTypes.naturality, obj_map_id]
[GOAL]
case w.h.h.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
a✝¹ : (yonedaPairing C).obj x✝
Y✝ : Cᵒᵖ
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj x✝).fst.unop.obj Y✝
⊢ NatTrans.app a✝¹ Y✝ (NatTrans.app (yoneda.map a✝.op.unop) (op Y✝.unop) (𝟙 Y✝.unop)) = NatTrans.app a✝¹ Y✝ a✝
[PROOFSTEP]
simp only [yoneda_map_app, Quiver.Hom.unop_op]
[GOAL]
case w.h.h.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
a✝¹ : (yonedaPairing C).obj x✝
Y✝ : Cᵒᵖ
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj x✝).fst.unop.obj Y✝
⊢ NatTrans.app a✝¹ Y✝ (𝟙 Y✝.unop ≫ a✝) = NatTrans.app a✝¹ Y✝ a✝
[PROOFSTEP]
erw [Category.id_comp]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ((NatTrans.mk fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down) ≫
      NatTrans.mk fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) }) =
    𝟙 (yonedaEvaluation C)
[PROOFSTEP]
ext
[GOAL]
case w.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
a✝ : (yonedaEvaluation C).obj x✝
⊢ NatTrans.app
      ((NatTrans.mk fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down) ≫
        NatTrans.mk fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) })
      x✝ a✝ =
    NatTrans.app (𝟙 (yonedaEvaluation C)) x✝ a✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
a✝ : (yonedaEvaluation C).obj x✝
⊢ { down := x✝.snd.map (𝟙 x✝.fst) a✝.down } = a✝
[PROOFSTEP]
rw [FunctorToTypes.map_id_apply, ULift.up_down]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ F.map g.op (↑yonedaEquiv f) = ↑yonedaEquiv (yoneda.map g ≫ f)
[PROOFSTEP]
change (f.app (op X) ≫ F.map g.op) (𝟙 X) = f.app (op Y) (𝟙 Y ≫ g)
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (NatTrans.app f (op X) ≫ F.map g.op) (𝟙 X) = NatTrans.app f (op Y) (𝟙 Y ≫ g)
[PROOFSTEP]
rw [← f.naturality]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ ((yoneda.obj X).map g.op ≫ NatTrans.app f (op Y)) (𝟙 X) = NatTrans.app f (op Y) (𝟙 Y ≫ g)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ NatTrans.app f (op Y) (g ≫ 𝟙 X) = NatTrans.app f (op Y) (𝟙 Y ≫ g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ ↑yonedaEquiv (yoneda.map f) = f
[PROOFSTEP]
rw [yonedaEquiv_apply]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ NatTrans.app (yoneda.map f) (op X) (𝟙 X) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type v₁
t : F.obj X
⊢ ↑yonedaEquiv.symm (F.map f t) = yoneda.map f.unop ≫ ↑yonedaEquiv.symm t
[PROOFSTEP]
obtain ⟨u, rfl⟩ := yonedaEquiv.surjective t
[GOAL]
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type v₁
u : yoneda.obj X.unop ⟶ F
⊢ ↑yonedaEquiv.symm (F.map f (↑yonedaEquiv u)) = yoneda.map f.unop ≫ ↑yonedaEquiv.symm (↑yonedaEquiv u)
[PROOFSTEP]
rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]
[GOAL]
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ yoneda.op ⋙ coyoneda ≅ evaluation Cᵒᵖ (Type u₁)
[PROOFSTEP]
refine
  eqToIso ?_ ≪≫
    curry.mapIso (yonedaLemma C ≪≫ isoWhiskerLeft (evaluationUncurried Cᵒᵖ (Type u₁)) uliftFunctorTrivial) ≪≫ eqToIso ?_
[GOAL]
case refine_1
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ yoneda.op ⋙ coyoneda = curry.obj (yonedaPairing C)
[PROOFSTEP]
apply Functor.ext
[GOAL]
case refine_1.h_map
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ autoParam
    (∀ (X Y : Cᵒᵖ) (f : X ⟶ Y),
      (yoneda.op ⋙ coyoneda).map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          (curry.obj (yonedaPairing C)).map f ≫
            eqToHom (_ : (curry.obj (yonedaPairing C)).obj Y = (yoneda.op ⋙ coyoneda).obj Y))
    _auto✝
[PROOFSTEP]
intro X Y f
[GOAL]
case refine_1.h_map
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (yoneda.op ⋙ coyoneda).map f =
    eqToHom (_ : ?F.obj X = ?G.obj X) ≫
      (curry.obj (yonedaPairing C)).map f ≫
        eqToHom (_ : (curry.obj (yonedaPairing C)).obj Y = (yoneda.op ⋙ coyoneda).obj Y)
[PROOFSTEP]
ext
[GOAL]
case refine_1.h_map.w.h.h
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : Cᵒᵖ ⥤ Type u₁
a✝ : ((yoneda.op ⋙ coyoneda).obj X).obj x✝
⊢ NatTrans.app ((yoneda.op ⋙ coyoneda).map f) x✝ a✝ =
    NatTrans.app
      (eqToHom (_ : ?F.obj X = ?G.obj X) ≫
        (curry.obj (yonedaPairing C)).map f ≫
          eqToHom (_ : (curry.obj (yonedaPairing C)).obj Y = (yoneda.op ⋙ coyoneda).obj Y))
      x✝ a✝
[PROOFSTEP]
simp
[GOAL]
case refine_1.h_obj
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ ∀ (X : Cᵒᵖ), (yoneda.op ⋙ coyoneda).obj X = (curry.obj (yonedaPairing C)).obj X
[PROOFSTEP]
aesop_cat
[GOAL]
case refine_2
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁)) = evaluation Cᵒᵖ (Type u₁)
[PROOFSTEP]
apply Functor.ext
[GOAL]
case refine_2.h_map
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ autoParam
    (∀ (X Y : Cᵒᵖ) (f : X ⟶ Y),
      (curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          (evaluation Cᵒᵖ (Type u₁)).map f ≫
            eqToHom
              (_ :
                (evaluation Cᵒᵖ (Type u₁)).obj Y = (curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).obj Y))
    _auto✝
[PROOFSTEP]
intro X Y f
[GOAL]
case refine_2.h_map
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).map f =
    eqToHom (_ : ?F.obj X = ?G.obj X) ≫
      (evaluation Cᵒᵖ (Type u₁)).map f ≫
        eqToHom
          (_ : (evaluation Cᵒᵖ (Type u₁)).obj Y = (curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).obj Y)
[PROOFSTEP]
ext
[GOAL]
case refine_2.h_map.w.h.h
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : Cᵒᵖ ⥤ Type u₁
a✝ : ((curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).obj X).obj x✝
⊢ NatTrans.app ((curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).map f) x✝ a✝ =
    NatTrans.app
      (eqToHom (_ : ?F.obj X = ?G.obj X) ≫
        (evaluation Cᵒᵖ (Type u₁)).map f ≫
          eqToHom
            (_ :
              (evaluation Cᵒᵖ (Type u₁)).obj Y = (curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).obj Y))
      x✝ a✝
[PROOFSTEP]
simp
[GOAL]
case refine_2.h_obj
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ ∀ (X : Cᵒᵖ), (curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).obj X = (evaluation Cᵒᵖ (Type u₁)).obj X
[PROOFSTEP]
intro X
[GOAL]
case refine_2.h_obj
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X : Cᵒᵖ
⊢ (curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).obj X = (evaluation Cᵒᵖ (Type u₁)).obj X
[PROOFSTEP]
simp only [curry, yoneda, coyoneda, curryObj, yonedaPairing]
[GOAL]
case refine_2.h_obj
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X : Cᵒᵖ
⊢ Functor.mk
      { obj := fun Y => (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁)).obj (X, Y),
        map := fun {X_1 Y} g => (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁)).map (𝟙 X, g) } =
    (evaluation Cᵒᵖ (Type u₁)).obj X
[PROOFSTEP]
aesop_cat
[GOAL]
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op ≅ 𝟭 (Cᵒᵖ ⥤ Type u₁)
[PROOFSTEP]
refine
  eqToIso ?_ ≪≫
    curry.mapIso
        (isoWhiskerLeft (Prod.swap _ _)
          (yonedaLemma C ≪≫ isoWhiskerLeft (evaluationUncurried Cᵒᵖ (Type u₁)) uliftFunctorTrivial : _)) ≪≫
      eqToIso ?_
[GOAL]
case refine_1
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op =
    curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ yonedaPairing C)
[PROOFSTEP]
apply Functor.ext
[GOAL]
case refine_1.h_map
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ autoParam
    (∀ (X Y : Cᵒᵖ ⥤ Type u₁) (f : X ⟶ Y),
      (yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          (curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ yonedaPairing C)).map f ≫
            eqToHom
              (_ :
                (curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ yonedaPairing C)).obj Y =
                  (yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).obj Y))
    _auto✝
[PROOFSTEP]
intro X Y f
[GOAL]
case refine_1.h_map
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : Cᵒᵖ ⥤ Type u₁
f : X ⟶ Y
⊢ (yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).map f =
    eqToHom (_ : ?F.obj X = ?G.obj X) ≫
      (curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ yonedaPairing C)).map f ≫
        eqToHom
          (_ :
            (curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ yonedaPairing C)).obj Y =
              (yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).obj Y)
[PROOFSTEP]
aesop_cat
[GOAL]
case refine_2
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁)) = 𝟭 (Cᵒᵖ ⥤ Type u₁)
[PROOFSTEP]
apply Functor.ext
[GOAL]
case refine_2.h_map
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ autoParam
    (∀ (X Y : Cᵒᵖ ⥤ Type u₁) (f : X ⟶ Y),
      (curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          (𝟭 (Cᵒᵖ ⥤ Type u₁)).map f ≫
            eqToHom
              (_ :
                (𝟭 (Cᵒᵖ ⥤ Type u₁)).obj Y =
                  (curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).obj Y))
    _auto✝
[PROOFSTEP]
aesop_cat


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
hX : Closed X
hY : Closed Y
⊢ IsLeftAdjoint (tensorLeft (X ⊗ Y))
[PROOFSTEP]
haveI := hX.isAdj
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
hX : Closed X
hY : Closed Y
this : IsLeftAdjoint (tensorLeft X)
⊢ IsLeftAdjoint (tensorLeft (X ⊗ Y))
[PROOFSTEP]
haveI := hY.isAdj
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
hX : Closed X
hY : Closed Y
this✝ : IsLeftAdjoint (tensorLeft X)
this : IsLeftAdjoint (tensorLeft Y)
⊢ IsLeftAdjoint (tensorLeft (X ⊗ Y))
[PROOFSTEP]
exact Adjunction.leftAdjointOfNatIso (MonoidalCategory.tensorLeftTensor _ _).symm
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X x✝ : C
⊢ Function.LeftInverse (fun a => (λ_ X).hom ≫ a) fun a => (λ_ X).inv ≫ a
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X x✝ : C
⊢ Function.RightInverse (fun a => (λ_ X).hom ≫ a) fun a => (λ_ X).inv ≫ a
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X'✝ X✝ Y✝ : C
f : X'✝ ⟶ X✝
g : X✝ ⟶ (𝟭 C).obj Y✝
⊢ ↑((fun X x =>
              { toFun := fun a => (λ_ X).inv ≫ a, invFun := fun a => (λ_ X).hom ≫ a,
                left_inv := (_ : ∀ (x_1 : (tensorLeft (𝟙_ C)).obj X ⟶ x), (λ_ X).hom ≫ (λ_ X).inv ≫ x_1 = x_1),
                right_inv := (_ : ∀ (x_1 : X ⟶ (𝟭 C).obj x), (λ_ X).inv ≫ (λ_ X).hom ≫ x_1 = x_1) })
            X'✝ Y✝).symm
      (f ≫ g) =
    (tensorLeft (𝟙_ C)).map f ≫
      ↑((fun X x =>
                { toFun := fun a => (λ_ X).inv ≫ a, invFun := fun a => (λ_ X).hom ≫ a,
                  left_inv := (_ : ∀ (x_1 : (tensorLeft (𝟙_ C)).obj X ⟶ x), (λ_ X).hom ≫ (λ_ X).inv ≫ x_1 = x_1),
                  right_inv := (_ : ∀ (x_1 : X ⟶ (𝟭 C).obj x), (λ_ X).inv ≫ (λ_ X).hom ≫ x_1 = x_1) })
              X✝ Y✝).symm
        g
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X'✝ X✝ Y✝ : C
f : X'✝ ⟶ X✝
g : X✝ ⟶ (𝟭 C).obj Y✝
⊢ (λ_ X'✝).hom ≫ f ≫ g = (𝟙 (𝟙_ C) ⊗ f) ≫ (λ_ X✝).hom ≫ g
[PROOFSTEP]
rw [leftUnitor_naturality_assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A B X X' Y Y' Z : C
inst✝ : Closed A
⊢ uncurry (𝟙 ((ihom A).obj X)) = NatTrans.app (ihom.ev A) X
[PROOFSTEP]
rw [uncurry_eq, tensor_id, id_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A B X X' Y Y' Z : C
inst✝ : Closed A
⊢ curry (𝟙 (A ⊗ (𝟭 C).obj X)) = NatTrans.app (ihom.coev A) X
[PROOFSTEP]
rw [curry_eq, (ihom A).map_id (A ⊗ _)]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A B X X' Y Y' Z : C
inst✝ : Closed A
⊢ NatTrans.app (ihom.coev A) ((𝟭 C).obj X) ≫ 𝟙 ((ihom A).obj (A ⊗ (𝟭 C).obj X)) = NatTrans.app (ihom.coev A) X
[PROOFSTEP]
apply comp_id
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X✝ X' Y Y' Z : C
inst✝¹ : Closed A
inst✝ : Closed B
f : B ⟶ A
X : C
⊢ uncurry (NatTrans.app (pre f) X) = (f ⊗ 𝟙 ((ihom A).obj X)) ≫ NatTrans.app (ihom.ev A) X
[PROOFSTEP]
rw [uncurry_eq, id_tensor_pre_app_comp_ev]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
A✝ B X X' Y Y' Z : C
inst✝² : Closed A✝
inst✝¹ : Closed B
A : C
inst✝ : Closed A
⊢ pre (𝟙 A) = 𝟙 (ihom A)
[PROOFSTEP]
simp only [pre, Functor.map_id]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
A✝ B X X' Y Y' Z : C
inst✝² : Closed A✝
inst✝¹ : Closed B
A : C
inst✝ : Closed A
⊢ ↑(transferNatTransSelf (ihom.adjunction A) (ihom.adjunction A)) (𝟙 ((tensoringLeft C).obj A)) = 𝟙 (ihom A)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
A✝ B X X' Y Y' Z : C
inst✝² : Closed A✝
inst✝¹ : Closed B
A : C
inst✝ : Closed A
⊢ ↑(transferNatTransSelf (ihom.adjunction A) (ihom.adjunction A)) (𝟙 (tensorLeft A)) = 𝟙 (ihom A)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
A B X X' Y Y' Z : C
inst✝⁴ : Closed A
inst✝³ : Closed B
A₁ A₂ A₃ : C
inst✝² : Closed A₁
inst✝¹ : Closed A₂
inst✝ : Closed A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ pre (f ≫ g) = pre g ≫ pre f
[PROOFSTEP]
rw [pre, pre, pre, transferNatTransSelf_comp, (tensoringLeft C).map_comp]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : Closed A
inst✝² : Closed B
W X Y Z : C
inst✝¹ : Closed W
inst✝ : Closed X
f : W ⟶ X
g : Y ⟶ Z
⊢ NatTrans.app (pre f) Y ≫ (ihom W).map g = (ihom X).map g ≫ NatTrans.app (pre f) Z
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
A B X✝ X' Y Y' Z : C
inst✝³ : Closed A
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
h : MonoidalClosed D
X : C
⊢ IsLeftAdjoint (tensorLeft X)
[PROOFSTEP]
haveI q : Closed (F.obj X) := inferInstance
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
A B X✝ X' Y Y' Z : C
inst✝³ : Closed A
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
h : MonoidalClosed D
X : C
q : Closed (F.obj X)
⊢ IsLeftAdjoint (tensorLeft X)
[PROOFSTEP]
haveI : IsLeftAdjoint (tensorLeft (F.obj X)) := q.isAdj
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
A B X✝ X' Y Y' Z : C
inst✝³ : Closed A
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
h : MonoidalClosed D
X : C
q : Closed (F.obj X)
this : IsLeftAdjoint (tensorLeft (F.obj X))
⊢ IsLeftAdjoint (tensorLeft X)
[PROOFSTEP]
have i := compInvIso (MonoidalFunctor.commTensorLeft F X)
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
A B X✝ X' Y Y' Z : C
inst✝³ : Closed A
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
h : MonoidalClosed D
X : C
q : Closed (F.obj X)
this : IsLeftAdjoint (tensorLeft (F.obj X))
i : (F.toFunctor ⋙ tensorLeft (F.obj X)) ⋙ Functor.inv F.toFunctor ≅ tensorLeft X
⊢ IsLeftAdjoint (tensorLeft X)
[PROOFSTEP]
exact Adjunction.leftAdjointOfNatIso i


[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : HasFiniteProducts C
inst✝ : CartesianClosed C
h : ∀ (B : D) (A : C), (A ⟹ i.obj B) ∈ Functor.essImage i
B✝ : C
hB : B✝ ∈ Functor.essImage i
A : C
⊢ (A ⟹ B✝) ∈ Functor.essImage i
[PROOFSTEP]
rcases hB with ⟨B', ⟨iB'⟩⟩
[GOAL]
case intro.intro
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : HasFiniteProducts C
inst✝ : CartesianClosed C
h : ∀ (B : D) (A : C), (A ⟹ i.obj B) ∈ Functor.essImage i
B✝ A : C
B' : D
iB' : i.obj B' ≅ B✝
⊢ (A ⟹ B✝) ∈ Functor.essImage i
[PROOFSTEP]
exact Functor.essImage.ofIso ((exp A).mapIso iB') (h B' A)
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : HasFiniteProducts C
inst✝ : CartesianClosed C
⊢ ExponentialIdeal (subterminalInclusion C)
[PROOFSTEP]
apply ExponentialIdeal.mk'
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : HasFiniteProducts C
inst✝ : CartesianClosed C
⊢ ∀ (B : Subterminals C) (A : C), (A ⟹ (subterminalInclusion C).obj B) ∈ Functor.essImage (subterminalInclusion C)
[PROOFSTEP]
intro B A
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : HasFiniteProducts C
inst✝ : CartesianClosed C
B : Subterminals C
A : C
⊢ (A ⟹ (subterminalInclusion C).obj B) ∈ Functor.essImage (subterminalInclusion C)
[PROOFSTEP]
refine' ⟨⟨A ⟹ B.1, fun Z g h => _⟩, ⟨Iso.refl _⟩⟩
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : HasFiniteProducts C
inst✝ : CartesianClosed C
B : Subterminals C
A Z : C
g h : Z ⟶ A ⟹ B.obj
⊢ g = h
[PROOFSTEP]
exact uncurry_injective (B.2 (CartesianClosed.uncurry g) (CartesianClosed.uncurry h))
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝³ : HasFiniteProducts C
inst✝² : CartesianClosed C
A : C
inst✝¹ : Reflective i
inst✝ : ExponentialIdeal i
⊢ i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A
[PROOFSTEP]
symm
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝³ : HasFiniteProducts C
inst✝² : CartesianClosed C
A : C
inst✝¹ : Reflective i
inst✝ : ExponentialIdeal i
⊢ i ⋙ exp A ≅ i ⋙ exp A ⋙ leftAdjoint i ⋙ i
[PROOFSTEP]
apply NatIso.ofComponents _ _
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝³ : HasFiniteProducts C
inst✝² : CartesianClosed C
A : C
inst✝¹ : Reflective i
inst✝ : ExponentialIdeal i
⊢ (X : D) → (i ⋙ exp A).obj X ≅ (i ⋙ exp A ⋙ leftAdjoint i ⋙ i).obj X
[PROOFSTEP]
intro X
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝³ : HasFiniteProducts C
inst✝² : CartesianClosed C
A : C
inst✝¹ : Reflective i
inst✝ : ExponentialIdeal i
X : D
⊢ (i ⋙ exp A).obj X ≅ (i ⋙ exp A ⋙ leftAdjoint i ⋙ i).obj X
[PROOFSTEP]
haveI := Functor.essImage.unit_isIso (ExponentialIdeal.exp_closed (i.obj_mem_essImage X) A)
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝³ : HasFiniteProducts C
inst✝² : CartesianClosed C
A : C
inst✝¹ : Reflective i
inst✝ : ExponentialIdeal i
X : D
this : IsIso (NatTrans.app (Adjunction.ofRightAdjoint i).unit (A ⟹ i.obj X))
⊢ (i ⋙ exp A).obj X ≅ (i ⋙ exp A ⋙ leftAdjoint i ⋙ i).obj X
[PROOFSTEP]
apply asIso ((Adjunction.ofRightAdjoint i).unit.app (A ⟹ i.obj X))
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝³ : HasFiniteProducts C
inst✝² : CartesianClosed C
A : C
inst✝¹ : Reflective i
inst✝ : ExponentialIdeal i
⊢ ∀ {X Y : D} (f : X ⟶ Y),
    (i ⋙ exp A).map f ≫ (asIso (NatTrans.app (Adjunction.ofRightAdjoint i).unit (A ⟹ i.obj Y))).hom =
      (asIso (NatTrans.app (Adjunction.ofRightAdjoint i).unit (A ⟹ i.obj X))).hom ≫
        (i ⋙ exp A ⋙ leftAdjoint i ⋙ i).map f
[PROOFSTEP]
simp [asIso]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝² : HasFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : Reflective i
h : (A : C) → i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A
⊢ ExponentialIdeal i
[PROOFSTEP]
apply ExponentialIdeal.mk'
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝² : HasFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : Reflective i
h : (A : C) → i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A
⊢ ∀ (B : D) (A : C), (A ⟹ i.obj B) ∈ Functor.essImage i
[PROOFSTEP]
intro B A
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝² : HasFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : Reflective i
h : (A : C) → i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A
B : D
A : C
⊢ (A ⟹ i.obj B) ∈ Functor.essImage i
[PROOFSTEP]
exact ⟨_, ⟨(h A).app B⟩⟩
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
⊢ ExponentialIdeal i
[PROOFSTEP]
let ir := Adjunction.ofRightAdjoint i
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
⊢ ExponentialIdeal i
[PROOFSTEP]
let L : C ⥤ D := leftAdjoint i
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
⊢ ExponentialIdeal i
[PROOFSTEP]
let η : 𝟭 C ⟶ L ⋙ i := ir.unit
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
⊢ ExponentialIdeal i
[PROOFSTEP]
let ε : i ⋙ L ⟶ 𝟭 D := ir.counit
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
⊢ ExponentialIdeal i
[PROOFSTEP]
apply ExponentialIdeal.mk'
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
⊢ ∀ (B : D) (A : C), (A ⟹ i.obj B) ∈ Functor.essImage i
[PROOFSTEP]
intro B A
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
⊢ (A ⟹ i.obj B) ∈ Functor.essImage i
[PROOFSTEP]
let q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B
[GOAL]
case q
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
⊢ i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B
case h
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B := ?q
⊢ (A ⟹ i.obj B) ∈ Functor.essImage i
[PROOFSTEP]
apply CartesianClosed.curry (ir.homEquiv _ _ _)
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
⊢ (leftAdjoint i).obj (A ⨯ i.obj (L.obj (A ⟹ i.obj B))) ⟶ B
case h
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  CartesianClosed.curry (↑(Adjunction.homEquiv ir (A ⨯ i.obj (L.obj (A ⟹ i.obj B))) B) ?m.26486)
⊢ (A ⟹ i.obj B) ∈ Functor.essImage i
[PROOFSTEP]
apply _ ≫ (ir.homEquiv _ _).symm ((exp.ev A).app (i.obj B))
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
⊢ (leftAdjoint i).obj (A ⨯ i.obj (L.obj (A ⟹ i.obj B))) ⟶
    (leftAdjoint i).obj ((exp A ⋙ prod.functor.obj A).obj (i.obj B))
case h
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  CartesianClosed.curry
    (↑(Adjunction.homEquiv ir (A ⨯ i.obj (L.obj (A ⟹ i.obj B))) B)
      (?m.26547 ≫
        ↑(Adjunction.homEquiv ir ((exp A ⋙ prod.functor.obj A).obj (i.obj B)) B).symm
          (NatTrans.app (exp.ev A) (i.obj B))))
⊢ (A ⟹ i.obj B) ∈ Functor.essImage i
[PROOFSTEP]
refine' prodComparison L A _ ≫ Limits.prod.map (𝟙 _) (ε.app _) ≫ inv (prodComparison _ _ _)
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  CartesianClosed.curry
    (↑(Adjunction.homEquiv ir (A ⨯ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          prod.map (𝟙 (L.obj A)) (NatTrans.app ε (L.obj (A ⟹ i.obj B))) ≫
            inv (prodComparison (leftAdjoint i) A (A ⟹ i.obj B))) ≫
        ↑(Adjunction.homEquiv ir ((exp A ⋙ prod.functor.obj A).obj (i.obj B)) B).symm
          (NatTrans.app (exp.ev A) (i.obj B))))
⊢ (A ⟹ i.obj B) ∈ Functor.essImage i
[PROOFSTEP]
have : η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B) := by
  dsimp
  rw [← curry_natural_left, curry_eq_iff, uncurry_id_eq_ev, ← ir.homEquiv_naturality_left, ir.homEquiv_apply_eq, assoc,
    assoc, prodComparison_natural_assoc, L.map_id, ← prod.map_id_comp_assoc, ir.left_triangle_components,
    prod.map_id_id, id_comp]
  apply IsIso.hom_inv_id_assoc
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  CartesianClosed.curry
    (↑(Adjunction.homEquiv ir (A ⨯ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          prod.map (𝟙 (L.obj A)) (NatTrans.app ε (L.obj (A ⟹ i.obj B))) ≫
            inv (prodComparison (leftAdjoint i) A (A ⟹ i.obj B))) ≫
        ↑(Adjunction.homEquiv ir ((exp A ⋙ prod.functor.obj A).obj (i.obj B)) B).symm
          (NatTrans.app (exp.ev A) (i.obj B))))
⊢ NatTrans.app η (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  CartesianClosed.curry
    (↑(Adjunction.homEquiv ir (A ⨯ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          prod.map (𝟙 (L.obj A)) (NatTrans.app ε (L.obj (A ⟹ i.obj B))) ≫
            inv (prodComparison (leftAdjoint i) A (A ⟹ i.obj B))) ≫
        ↑(Adjunction.homEquiv ir ((exp A ⋙ prod.functor.obj A).obj (i.obj B)) B).symm
          (NatTrans.app (exp.ev A) (i.obj B))))
⊢ NatTrans.app (Adjunction.ofRightAdjoint i).unit (A ⟹ i.obj B) ≫
      CartesianClosed.curry
        (↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint i) (A ⨯ i.obj ((leftAdjoint i).obj (A ⟹ i.obj B))) B)
          ((prodComparison (leftAdjoint i) A (i.obj ((leftAdjoint i).obj (A ⟹ i.obj B))) ≫
              prod.map (𝟙 ((leftAdjoint i).obj A))
                  (NatTrans.app (Adjunction.ofRightAdjoint i).counit ((leftAdjoint i).obj (A ⟹ i.obj B))) ≫
                inv (prodComparison (leftAdjoint i) A (A ⟹ i.obj B))) ≫
            ↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint i) (A ⨯ A ⟹ i.obj B) B).symm
              (NatTrans.app (exp.ev A) (i.obj B)))) =
    𝟙 (A ⟹ i.obj B)
[PROOFSTEP]
rw [← curry_natural_left, curry_eq_iff, uncurry_id_eq_ev, ← ir.homEquiv_naturality_left, ir.homEquiv_apply_eq, assoc,
  assoc, prodComparison_natural_assoc, L.map_id, ← prod.map_id_comp_assoc, ir.left_triangle_components, prod.map_id_id,
  id_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  CartesianClosed.curry
    (↑(Adjunction.homEquiv ir (A ⨯ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          prod.map (𝟙 (L.obj A)) (NatTrans.app ε (L.obj (A ⟹ i.obj B))) ≫
            inv (prodComparison (leftAdjoint i) A (A ⟹ i.obj B))) ≫
        ↑(Adjunction.homEquiv ir ((exp A ⋙ prod.functor.obj A).obj (i.obj B)) B).symm
          (NatTrans.app (exp.ev A) (i.obj B))))
⊢ prodComparison (leftAdjoint i) A (A ⟹ i.obj B) ≫
      inv (prodComparison (leftAdjoint i) A (A ⟹ i.obj B)) ≫
        ↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint i) (A ⨯ A ⟹ i.obj B) B).symm
          (NatTrans.app (exp.ev A) (i.obj B)) =
    ↑(Adjunction.homEquiv ir (A ⨯ A ⟹ i.obj B) B).symm (NatTrans.app (exp.ev A) (i.obj B))
[PROOFSTEP]
apply IsIso.hom_inv_id_assoc
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  CartesianClosed.curry
    (↑(Adjunction.homEquiv ir (A ⨯ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          prod.map (𝟙 (L.obj A)) (NatTrans.app ε (L.obj (A ⟹ i.obj B))) ≫
            inv (prodComparison (leftAdjoint i) A (A ⟹ i.obj B))) ≫
        ↑(Adjunction.homEquiv ir ((exp A ⋙ prod.functor.obj A).obj (i.obj B)) B).symm
          (NatTrans.app (exp.ev A) (i.obj B))))
this : NatTrans.app η (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B)
⊢ (A ⟹ i.obj B) ∈ Functor.essImage i
[PROOFSTEP]
haveI : IsSplitMono (η.app (A ⟹ i.obj B)) := IsSplitMono.mk' ⟨_, this⟩
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i)
ir : leftAdjoint i ⊣ i := Adjunction.ofRightAdjoint i
L : C ⥤ D := leftAdjoint i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  CartesianClosed.curry
    (↑(Adjunction.homEquiv ir (A ⨯ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          prod.map (𝟙 (L.obj A)) (NatTrans.app ε (L.obj (A ⟹ i.obj B))) ≫
            inv (prodComparison (leftAdjoint i) A (A ⟹ i.obj B))) ≫
        ↑(Adjunction.homEquiv ir ((exp A ⋙ prod.functor.obj A).obj (i.obj B)) B).symm
          (NatTrans.app (exp.ev A) (i.obj B))))
this✝ : NatTrans.app η (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B)
this : IsSplitMono (NatTrans.app η (A ⟹ i.obj B))
⊢ (A ⟹ i.obj B) ∈ Functor.essImage i
[PROOFSTEP]
apply mem_essImage_of_unit_isSplitMono
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
src✝ : MonoidalCategory D := monoidalOfHasFiniteProducts D
B : D
⊢ MonoidalCategory.tensorLeft B ⊣ i ⋙ exp (i.obj B) ⋙ leftAdjoint i
[PROOFSTEP]
apply Adjunction.restrictFullyFaithful i i (exp.adjunction (i.obj B))
[GOAL]
case comm1
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
src✝ : MonoidalCategory D := monoidalOfHasFiniteProducts D
B : D
⊢ i ⋙ prod.functor.obj (i.obj B) ≅ MonoidalCategory.tensorLeft B ⋙ i
[PROOFSTEP]
symm
[GOAL]
case comm1
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
src✝ : MonoidalCategory D := monoidalOfHasFiniteProducts D
B : D
⊢ MonoidalCategory.tensorLeft B ⋙ i ≅ i ⋙ prod.functor.obj (i.obj B)
[PROOFSTEP]
refine' NatIso.ofComponents (fun X => _) (fun f => _)
[GOAL]
case comm1.refine'_1
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
src✝ : MonoidalCategory D := monoidalOfHasFiniteProducts D
B X : D
⊢ (MonoidalCategory.tensorLeft B ⋙ i).obj X ≅ (i ⋙ prod.functor.obj (i.obj B)).obj X
[PROOFSTEP]
haveI := Adjunction.rightAdjointPreservesLimits.{0, 0} (Adjunction.ofRightAdjoint i)
[GOAL]
case comm1.refine'_1
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
src✝ : MonoidalCategory D := monoidalOfHasFiniteProducts D
B X : D
this : PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
⊢ (MonoidalCategory.tensorLeft B ⋙ i).obj X ≅ (i ⋙ prod.functor.obj (i.obj B)).obj X
[PROOFSTEP]
apply asIso (prodComparison i B X)
[GOAL]
case comm1.refine'_2
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
src✝ : MonoidalCategory D := monoidalOfHasFiniteProducts D
B X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ (MonoidalCategory.tensorLeft B ⋙ i).map f ≫ ((fun X => asIso (prodComparison i B X)) Y✝).hom =
    ((fun X => asIso (prodComparison i B X)) X✝).hom ≫ (i ⋙ prod.functor.obj (i.obj B)).map f
[PROOFSTEP]
dsimp [asIso]
[GOAL]
case comm1.refine'_2
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
src✝ : MonoidalCategory D := monoidalOfHasFiniteProducts D
B X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ i.map (prod.map (𝟙 B) f) ≫ prodComparison i B Y✝ = prodComparison i B X✝ ≫ prod.map (𝟙 (i.obj B)) (i.map f)
[PROOFSTEP]
rw [prodComparison_natural, Functor.map_id]
[GOAL]
case comm2
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
src✝ : MonoidalCategory D := monoidalOfHasFiniteProducts D
B : D
⊢ i ⋙ exp (i.obj B) ≅ (i ⋙ exp (i.obj B) ⋙ leftAdjoint i) ⋙ i
[PROOFSTEP]
apply (exponentialIdealReflective i _).symm
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ ↑(bijection i A B ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)).symm
      (𝟙 ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)) =
    prodComparison (leftAdjoint i) A B
[PROOFSTEP]
have : PreservesLimits i := (Adjunction.ofRightAdjoint i).rightAdjointPreservesLimits
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
this : PreservesLimits i
⊢ ↑(bijection i A B ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)).symm
      (𝟙 ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)) =
    prodComparison (leftAdjoint i) A B
[PROOFSTEP]
have := preservesSmallestLimitsOfPreservesLimits i
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
this✝ : PreservesLimits i
this : PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
⊢ ↑(bijection i A B ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)).symm
      (𝟙 ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)) =
    prodComparison (leftAdjoint i) A B
[PROOFSTEP]
dsimp [bijection]
  -- Porting note: added
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
this✝ : PreservesLimits i
this : PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
⊢ ↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint i) (A ⨯ B) ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)).symm
      (prod.lift prod.snd prod.fst ≫
        ↑(Adjunction.homEquiv (exp.adjunction B) A (i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B))).symm
            (↑(unitCompPartialBijective A
                    (_ : (B ⟹ i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)) ∈ Functor.essImage i)).symm
              (↑(Adjunction.homEquiv (exp.adjunction B) (i.obj ((leftAdjoint i).obj A))
                    (i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)))
                (prod.lift prod.snd prod.fst ≫
                  ↑(Adjunction.homEquiv (exp.adjunction (i.obj ((leftAdjoint i).obj A))) B
                            (i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B))).symm
                      (↑(unitCompPartialBijective B
                              (_ :
                                (i.obj ((leftAdjoint i).obj A) ⟹
                                    i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)) ∈
                                  Functor.essImage i)).symm
                        (↑(Adjunction.homEquiv (exp.adjunction (i.obj ((leftAdjoint i).obj A)))
                              (i.obj ((leftAdjoint i).obj B)) (i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)))
                          ((PreservesLimitPair.iso i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)).inv ≫
                            i.map (𝟙 ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)) ≫
                              𝟙 (i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B))))) ≫
                    𝟙 (i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B))))) ≫
          𝟙 (i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B))) =
    prodComparison (leftAdjoint i) A B
[PROOFSTEP]
erw [homEquiv_symm_apply_eq, homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
this✝ : PreservesLimits i
this : PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
⊢ ↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint i) (A ⨯ B) ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)).symm
      (prod.lift prod.snd prod.fst ≫
        CartesianClosed.uncurry
            (↑(unitCompPartialBijective A
                    (_ : (B ⟹ i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)) ∈ Functor.essImage i)).symm
              (CartesianClosed.curry
                (prod.lift prod.snd prod.fst ≫
                  CartesianClosed.uncurry
                      (↑(unitCompPartialBijective B
                              (_ :
                                (i.obj ((leftAdjoint i).obj A) ⟹
                                    i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)) ∈
                                  Functor.essImage i)).symm
                        (CartesianClosed.curry
                          ((PreservesLimitPair.iso i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)).inv ≫
                            i.map (𝟙 ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)) ≫
                              𝟙 (i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B))))) ≫
                    𝟙 (i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B))))) ≫
          𝟙 (i.obj ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B))) =
    prodComparison (leftAdjoint i) A B
[PROOFSTEP]
rw [comp_id, comp_id, comp_id, i.map_id, comp_id, unitCompPartialBijective_symm_apply,
  unitCompPartialBijective_symm_apply, uncurry_natural_left, uncurry_curry, uncurry_natural_left, uncurry_curry,
  prod.lift_map_assoc, comp_id, prod.lift_map_assoc, comp_id]
  -- Porting note: added
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
this✝ : PreservesLimits i
this : PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
⊢ ↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint i) (A ⨯ B) ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)).symm
      (prod.lift prod.snd (prod.fst ≫ NatTrans.app (Adjunction.ofRightAdjoint i).unit A) ≫
        prod.lift prod.snd (prod.fst ≫ NatTrans.app (Adjunction.ofRightAdjoint i).unit B) ≫
          (PreservesLimitPair.iso i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)).inv) =
    prodComparison (leftAdjoint i) A B
[PROOFSTEP]
dsimp only [Functor.comp_obj]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
this✝ : PreservesLimits i
this : PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
⊢ ↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint i) (A ⨯ B) ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)).symm
      (prod.lift prod.snd (prod.fst ≫ NatTrans.app (Adjunction.ofRightAdjoint i).unit A) ≫
        prod.lift prod.snd (prod.fst ≫ NatTrans.app (Adjunction.ofRightAdjoint i).unit B) ≫
          (PreservesLimitPair.iso i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)).inv) =
    prodComparison (leftAdjoint i) A B
[PROOFSTEP]
rw [prod.comp_lift_assoc, prod.lift_snd, prod.lift_fst_assoc, prod.lift_fst_comp_snd_comp, ←
  Adjunction.eq_homEquiv_apply, Adjunction.homEquiv_unit, Iso.comp_inv_eq, assoc]
  -- Porting note: rw became erw
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
this✝ : PreservesLimits i
this : PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
⊢ prod.map (NatTrans.app (Adjunction.ofRightAdjoint i).unit A) (NatTrans.app (Adjunction.ofRightAdjoint i).unit B) =
    NatTrans.app (Adjunction.ofRightAdjoint i).unit (A ⨯ B) ≫
      i.map (prodComparison (leftAdjoint i) A B) ≫
        (PreservesLimitPair.iso i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)).hom
[PROOFSTEP]
erw [PreservesLimitPair.iso_hom i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
this✝ : PreservesLimits i
this : PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
⊢ prod.map (NatTrans.app (Adjunction.ofRightAdjoint i).unit A) (NatTrans.app (Adjunction.ofRightAdjoint i).unit B) =
    NatTrans.app (Adjunction.ofRightAdjoint i).unit (A ⨯ B) ≫
      i.map (prodComparison (leftAdjoint i) A B) ≫ prodComparison i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)
[PROOFSTEP]
apply prod.hom_ext
[GOAL]
case h₁
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
this✝ : PreservesLimits i
this : PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
⊢ prod.map (NatTrans.app (Adjunction.ofRightAdjoint i).unit A) (NatTrans.app (Adjunction.ofRightAdjoint i).unit B) ≫
      prod.fst =
    (NatTrans.app (Adjunction.ofRightAdjoint i).unit (A ⨯ B) ≫
        i.map (prodComparison (leftAdjoint i) A B) ≫ prodComparison i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)) ≫
      prod.fst
[PROOFSTEP]
rw [Limits.prod.map_fst, assoc, assoc, prodComparison_fst, ← i.map_comp, prodComparison_fst]
[GOAL]
case h₁
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
this✝ : PreservesLimits i
this : PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
⊢ prod.fst ≫ NatTrans.app (Adjunction.ofRightAdjoint i).unit A =
    NatTrans.app (Adjunction.ofRightAdjoint i).unit (A ⨯ B) ≫ i.map ((leftAdjoint i).map prod.fst)
[PROOFSTEP]
apply (Adjunction.ofRightAdjoint i).unit.naturality
[GOAL]
case h₂
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
this✝ : PreservesLimits i
this : PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
⊢ prod.map (NatTrans.app (Adjunction.ofRightAdjoint i).unit A) (NatTrans.app (Adjunction.ofRightAdjoint i).unit B) ≫
      prod.snd =
    (NatTrans.app (Adjunction.ofRightAdjoint i).unit (A ⨯ B) ≫
        i.map (prodComparison (leftAdjoint i) A B) ≫ prodComparison i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)) ≫
      prod.snd
[PROOFSTEP]
rw [Limits.prod.map_snd, assoc, assoc, prodComparison_snd, ← i.map_comp, prodComparison_snd]
[GOAL]
case h₂
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
this✝ : PreservesLimits i
this : PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
⊢ prod.snd ≫ NatTrans.app (Adjunction.ofRightAdjoint i).unit B =
    NatTrans.app (Adjunction.ofRightAdjoint i).unit (A ⨯ B) ≫ i.map ((leftAdjoint i).map prod.snd)
[PROOFSTEP]
apply (Adjunction.ofRightAdjoint i).unit.naturality
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
X X' : D
f : (leftAdjoint i).obj (A ⨯ B) ⟶ X
g : X ⟶ X'
⊢ ↑(bijection i A B X') (f ≫ g) = ↑(bijection i A B X) f ≫ g
[PROOFSTEP]
dsimp [bijection]
  -- Porting note: added
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
X X' : D
f : (leftAdjoint i).obj (A ⨯ B) ⟶ X
g : X ⟶ X'
⊢ i.preimage
      ((PreservesLimitPair.iso i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)).hom ≫
        ↑(Adjunction.homEquiv (exp.adjunction (i.obj ((leftAdjoint i).obj A))) (i.obj ((leftAdjoint i).obj B))
                  (i.obj X')).symm
            (↑(unitCompPartialBijective B (_ : (i.obj ((leftAdjoint i).obj A) ⟹ i.obj X') ∈ Functor.essImage i))
              (↑(Adjunction.homEquiv (exp.adjunction (i.obj ((leftAdjoint i).obj A))) B (i.obj X'))
                (prod.lift prod.snd prod.fst ≫
                  ↑(Adjunction.homEquiv (exp.adjunction B) (i.obj ((leftAdjoint i).obj A)) (i.obj X')).symm
                      (↑(unitCompPartialBijective A (_ : (B ⟹ i.obj X') ∈ Functor.essImage i))
                        (↑(Adjunction.homEquiv (exp.adjunction B) A (i.obj X'))
                          (prod.lift prod.snd prod.fst ≫
                            ↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint i) (A ⨯ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                    𝟙 (i.obj X')))) ≫
          𝟙 (i.obj X')) =
    i.preimage
        ((PreservesLimitPair.iso i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)).hom ≫
          ↑(Adjunction.homEquiv (exp.adjunction (i.obj ((leftAdjoint i).obj A))) (i.obj ((leftAdjoint i).obj B))
                    (i.obj X)).symm
              (↑(unitCompPartialBijective B (_ : (i.obj ((leftAdjoint i).obj A) ⟹ i.obj X) ∈ Functor.essImage i))
                (↑(Adjunction.homEquiv (exp.adjunction (i.obj ((leftAdjoint i).obj A))) B (i.obj X))
                  (prod.lift prod.snd prod.fst ≫
                    ↑(Adjunction.homEquiv (exp.adjunction B) (i.obj ((leftAdjoint i).obj A)) (i.obj X)).symm
                        (↑(unitCompPartialBijective A (_ : (B ⟹ i.obj X) ∈ Functor.essImage i))
                          (↑(Adjunction.homEquiv (exp.adjunction B) A (i.obj X))
                            (prod.lift prod.snd prod.fst ≫
                              ↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint i) (A ⨯ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                      𝟙 (i.obj X)))) ≫
            𝟙 (i.obj X)) ≫
      g
[PROOFSTEP]
erw [homEquiv_symm_apply_eq, homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq, homEquiv_symm_apply_eq,
  homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
X X' : D
f : (leftAdjoint i).obj (A ⨯ B) ⟶ X
g : X ⟶ X'
⊢ i.preimage
      ((PreservesLimitPair.iso i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)).hom ≫
        CartesianClosed.uncurry
            (↑(unitCompPartialBijective B (_ : (i.obj ((leftAdjoint i).obj A) ⟹ i.obj X') ∈ Functor.essImage i))
              (CartesianClosed.curry
                (prod.lift prod.snd prod.fst ≫
                  CartesianClosed.uncurry
                      (↑(unitCompPartialBijective A (_ : (B ⟹ i.obj X') ∈ Functor.essImage i))
                        (CartesianClosed.curry
                          (prod.lift prod.snd prod.fst ≫
                            ↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint i) (A ⨯ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                    𝟙 (i.obj X')))) ≫
          𝟙 (i.obj X')) =
    i.preimage
        ((PreservesLimitPair.iso i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)).hom ≫
          CartesianClosed.uncurry
              (↑(unitCompPartialBijective B (_ : (i.obj ((leftAdjoint i).obj A) ⟹ i.obj X) ∈ Functor.essImage i))
                (CartesianClosed.curry
                  (prod.lift prod.snd prod.fst ≫
                    CartesianClosed.uncurry
                        (↑(unitCompPartialBijective A (_ : (B ⟹ i.obj X) ∈ Functor.essImage i))
                          (CartesianClosed.curry
                            (prod.lift prod.snd prod.fst ≫
                              ↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint i) (A ⨯ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                      𝟙 (i.obj X)))) ≫
            𝟙 (i.obj X)) ≫
      g
[PROOFSTEP]
apply i.map_injective
[GOAL]
case a
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
X X' : D
f : (leftAdjoint i).obj (A ⨯ B) ⟶ X
g : X ⟶ X'
⊢ i.map
      (i.preimage
        ((PreservesLimitPair.iso i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)).hom ≫
          CartesianClosed.uncurry
              (↑(unitCompPartialBijective B (_ : (i.obj ((leftAdjoint i).obj A) ⟹ i.obj X') ∈ Functor.essImage i))
                (CartesianClosed.curry
                  (prod.lift prod.snd prod.fst ≫
                    CartesianClosed.uncurry
                        (↑(unitCompPartialBijective A (_ : (B ⟹ i.obj X') ∈ Functor.essImage i))
                          (CartesianClosed.curry
                            (prod.lift prod.snd prod.fst ≫
                              ↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint i) (A ⨯ B) X') (f ≫ g) ≫
                                𝟙 (i.obj X')))) ≫
                      𝟙 (i.obj X')))) ≫
            𝟙 (i.obj X'))) =
    i.map
      (i.preimage
          ((PreservesLimitPair.iso i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)).hom ≫
            CartesianClosed.uncurry
                (↑(unitCompPartialBijective B (_ : (i.obj ((leftAdjoint i).obj A) ⟹ i.obj X) ∈ Functor.essImage i))
                  (CartesianClosed.curry
                    (prod.lift prod.snd prod.fst ≫
                      CartesianClosed.uncurry
                          (↑(unitCompPartialBijective A (_ : (B ⟹ i.obj X) ∈ Functor.essImage i))
                            (CartesianClosed.curry
                              (prod.lift prod.snd prod.fst ≫
                                ↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint i) (A ⨯ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                        𝟙 (i.obj X)))) ≫
              𝟙 (i.obj X)) ≫
        g)
[PROOFSTEP]
rw [i.image_preimage, i.map_comp, i.image_preimage, comp_id, comp_id, comp_id, comp_id, comp_id, comp_id,
  Adjunction.homEquiv_naturality_right, ← assoc, curry_natural_right _ (i.map g), unitCompPartialBijective_natural,
  uncurry_natural_right, ← assoc, curry_natural_right, unitCompPartialBijective_natural, uncurry_natural_right, assoc]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ prodComparison (leftAdjoint i) A B ≫
      ↑(bijection i A B ((leftAdjoint i).obj (A ⨯ B))) (𝟙 ((leftAdjoint i).obj (A ⨯ B))) =
    𝟙 ((leftAdjoint i).obj (A ⨯ B))
[PROOFSTEP]
rw [← (bijection i _ _ _).injective.eq_iff, bijection_natural, ← bijection_symm_apply_id, Equiv.apply_symm_apply,
  id_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : HasFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ ↑(bijection i A B ((leftAdjoint i).obj (A ⨯ B))) (𝟙 ((leftAdjoint i).obj (A ⨯ B))) ≫
      prodComparison (leftAdjoint i) A B =
    𝟙 ((leftAdjoint i).obj A ⨯ (leftAdjoint i).obj B)
[PROOFSTEP]
rw [← bijection_natural, id_comp, ← bijection_symm_apply_id, Equiv.apply_symm_apply]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : HasFiniteProducts C
inst✝⁴ : Reflective i
inst✝³ : CartesianClosed C
inst✝² : HasFiniteProducts D
inst✝¹ : ExponentialIdeal i
J : Type
inst✝ : Fintype J
⊢ PreservesLimitsOfShape (Discrete J) (leftAdjoint i)
[PROOFSTEP]
letI := preservesBinaryProductsOfExponentialIdeal i
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : HasFiniteProducts C
inst✝⁴ : Reflective i
inst✝³ : CartesianClosed C
inst✝² : HasFiniteProducts D
inst✝¹ : ExponentialIdeal i
J : Type
inst✝ : Fintype J
this : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i) := preservesBinaryProductsOfExponentialIdeal i
⊢ PreservesLimitsOfShape (Discrete J) (leftAdjoint i)
[PROOFSTEP]
letI := leftAdjointPreservesTerminalOfReflective.{0} i
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : HasFiniteProducts C
inst✝⁴ : Reflective i
inst✝³ : CartesianClosed C
inst✝² : HasFiniteProducts D
inst✝¹ : ExponentialIdeal i
J : Type
inst✝ : Fintype J
this✝ : PreservesLimitsOfShape (Discrete WalkingPair) (leftAdjoint i) := preservesBinaryProductsOfExponentialIdeal i
this : PreservesLimitsOfShape (Discrete PEmpty) (leftAdjoint i) := leftAdjointPreservesTerminalOfReflective i
⊢ PreservesLimitsOfShape (Discrete J) (leftAdjoint i)
[PROOFSTEP]
apply preservesFiniteProductsOfPreservesBinaryAndTerminal (leftAdjoint i) J


[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
h : L ⊣ F
A : C
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) L
inst✝¹ : Full F
inst✝ : Faithful F
B : D
⊢ IsIso (NatTrans.app (frobeniusMorphism F h A) B)
[PROOFSTEP]
dsimp [frobeniusMorphism]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
h : L ⊣ F
A : C
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) L
inst✝¹ : Full F
inst✝ : Faithful F
B : D
⊢ IsIso (prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
⊢ prod.map (𝟙 (F.obj A)) (NatTrans.app (expComparison F A) B) ≫ NatTrans.app (exp.ev (F.obj A)) (F.obj B) =
    inv (prodComparison F A (A ⟹ B)) ≫ F.map (NatTrans.app (exp.ev A) B)
[PROOFSTEP]
convert transferNatTrans_counit _ _ (prodComparisonNatIso F A).inv B using 2
[GOAL]
case h.e'_3.h.h.e'_6.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
e_1✝ :
  (F.obj A ⨯ (exp A ⋙ F).obj B ⟶ (𝟭 D).obj (F.obj B)) =
    ((prod.functor.obj (F.obj A)).obj ((exp A ⋙ F).obj B) ⟶ (𝟭 D).obj (F.obj B))
e_3✝ : (F.obj A ⨯ F.obj (A ⟹ B)) = (F ⋙ prod.functor.obj (F.obj A)).obj (A ⟹ B)
e_4✝ : F.obj (A ⨯ A ⟹ B) = (prod.functor.obj A ⋙ F).obj (A ⟹ B)
⊢ inv (prodComparison F A (A ⟹ B)) = NatTrans.app (prodComparisonNatIso F A).inv (A ⟹ B)
[PROOFSTEP]
apply IsIso.inv_eq_of_hom_inv_id
[GOAL]
case h.e'_3.h.h.e'_6.h.hom_inv_id
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
e_1✝ :
  (F.obj A ⨯ (exp A ⋙ F).obj B ⟶ (𝟭 D).obj (F.obj B)) =
    ((prod.functor.obj (F.obj A)).obj ((exp A ⋙ F).obj B) ⟶ (𝟭 D).obj (F.obj B))
e_3✝ : (F.obj A ⨯ F.obj (A ⟹ B)) = (F ⋙ prod.functor.obj (F.obj A)).obj (A ⟹ B)
e_4✝ : F.obj (A ⨯ A ⟹ B) = (prod.functor.obj A ⋙ F).obj (A ⟹ B)
⊢ prodComparison F A (A ⟹ B) ≫ NatTrans.app (prodComparisonNatIso F A).inv (A ⟹ B) = 𝟙 (F.obj (A ⨯ A ⟹ B))
[PROOFSTEP]
simp only [Limits.prodComparisonNatIso_inv, asIso_inv, NatIso.isIso_inv_app, IsIso.hom_inv_id]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
⊢ F.map (NatTrans.app (exp.coev A) B) ≫ NatTrans.app (expComparison F A) (A ⨯ B) =
    NatTrans.app (exp.coev (F.obj A)) (F.obj B) ≫ (exp (F.obj A)).map (inv (prodComparison F A B))
[PROOFSTEP]
convert unit_transferNatTrans _ _ (prodComparisonNatIso F A).inv B using 3
[GOAL]
case h.e'_3.h.h.e'_7.h.h.e'_8.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (A ⨯ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj ((prod.functor.obj A).obj B))
e_4✝ :
  (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj B) =
    (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (F.obj A ⟹ F.obj (A ⨯ B)) = (F.obj A ⟹ (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (prod.functor.obj (F.obj A)).obj (F.obj B) = (prod.functor.obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⨯ B) = (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ inv (prodComparison F A B) = NatTrans.app (prodComparisonNatIso F A).inv ((𝟭 C).obj B)
[PROOFSTEP]
apply IsIso.inv_eq_of_hom_inv_id
[GOAL]
case h.e'_3.h.h.e'_7.h.h.e'_8.h.hom_inv_id
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (A ⨯ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj ((prod.functor.obj A).obj B))
e_4✝ :
  (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj B) =
    (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (F.obj A ⟹ F.obj (A ⨯ B)) = (F.obj A ⟹ (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (prod.functor.obj (F.obj A)).obj (F.obj B) = (prod.functor.obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⨯ B) = (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ prodComparison F A B ≫ NatTrans.app (prodComparisonNatIso F A).inv ((𝟭 C).obj B) = 𝟙 (F.obj (A ⨯ B))
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_3.h.h.e'_7.h.h.e'_8.h.hom_inv_id
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (A ⨯ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj ((prod.functor.obj A).obj B))
e_4✝ :
  (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj B) =
    (prod.functor.obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (F.obj A ⟹ F.obj (A ⨯ B)) = (F.obj A ⟹ (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (prod.functor.obj (F.obj A)).obj (F.obj B) = (prod.functor.obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⨯ B) = (prod.functor.obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ prodComparison F A B ≫ NatTrans.app (inv (NatTrans.mk fun B => prodComparison F A B)) B = 𝟙 (F.obj (A ⨯ B))
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A B : C
⊢ CartesianClosed.uncurry (NatTrans.app (expComparison F A) B) =
    inv (prodComparison F A (A ⟹ B)) ≫ F.map (NatTrans.app (exp.ev A) B)
[PROOFSTEP]
rw [uncurry_eq, expComparison_ev]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A A' : C
f : A' ⟶ A
⊢ expComparison F A ≫ whiskerLeft F (pre (F.map f)) = whiskerRight (pre f) F ≫ expComparison F A'
[PROOFSTEP]
ext B
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A A' : C
f : A' ⟶ A
B : C
⊢ NatTrans.app (expComparison F A ≫ whiskerLeft F (pre (F.map f))) B =
    NatTrans.app (whiskerRight (pre f) F ≫ expComparison F A') B
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A A' : C
f : A' ⟶ A
B : C
⊢ NatTrans.app (expComparison F A) B ≫ NatTrans.app (pre (F.map f)) (F.obj B) =
    F.map (NatTrans.app (pre f) B) ≫ NatTrans.app (expComparison F A') B
[PROOFSTEP]
apply uncurry_injective
[GOAL]
case w.h.a
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
A A' : C
f : A' ⟶ A
B : C
⊢ CartesianClosed.uncurry (NatTrans.app (expComparison F A) B ≫ NatTrans.app (pre (F.map f)) (F.obj B)) =
    CartesianClosed.uncurry (F.map (NatTrans.app (pre f) B) ≫ NatTrans.app (expComparison F A') B)
[PROOFSTEP]
rw [uncurry_natural_left, uncurry_natural_left, uncurry_expComparison, uncurry_pre, prod.map_swap_assoc, ← F.map_id,
  expComparison_ev, ← F.map_id, ← prodComparison_inv_natural_assoc, ← prodComparison_inv_natural_assoc, ← F.map_comp, ←
  F.map_comp, prod_map_pre_app_comp_ev]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
⊢ ↑(transferNatTransSelf (Adjunction.comp h (exp.adjunction A)) (Adjunction.comp (exp.adjunction (F.obj A)) h))
      (frobeniusMorphism F h A) =
    expComparison F A
[PROOFSTEP]
rw [← Equiv.eq_symm_apply]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
⊢ frobeniusMorphism F h A =
    ↑(transferNatTransSelf (Adjunction.comp h (exp.adjunction A)) (Adjunction.comp (exp.adjunction (F.obj A)) h)).symm
      (expComparison F A)
[PROOFSTEP]
ext B : 2
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ NatTrans.app (frobeniusMorphism F h A) B =
    NatTrans.app
      (↑(transferNatTransSelf (Adjunction.comp h (exp.adjunction A))
              (Adjunction.comp (exp.adjunction (F.obj A)) h)).symm
        (expComparison F A))
      B
[PROOFSTEP]
dsimp [frobeniusMorphism, transferNatTransSelf, transferNatTrans, Adjunction.comp]
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) =
    𝟙 (L.obj (F.obj A ⨯ B)) ≫
      (L.map
            (prod.map (𝟙 (F.obj A))
              ((NatTrans.app h.unit B ≫
                  F.map (NatTrans.app (exp.adjunction A).unit (L.obj B)) ≫ 𝟙 (F.obj (A ⟹ A ⨯ L.obj B))) ≫
                𝟙 (F.obj (A ⟹ A ⨯ L.obj B)) ≫
                  NatTrans.app (expComparison F A) (A ⨯ L.obj B) ≫ 𝟙 (F.obj A ⟹ F.obj (A ⨯ L.obj B)))) ≫
          𝟙 (L.obj (F.obj A ⨯ F.obj A ⟹ F.obj (A ⨯ L.obj B))) ≫
            L.map (NatTrans.app (exp.adjunction (F.obj A)).counit (F.obj (A ⨯ L.obj B))) ≫
              NatTrans.app h.counit (A ⨯ L.obj B)) ≫
        𝟙 (A ⨯ L.obj B)
[PROOFSTEP]
simp only [id_comp, comp_id]
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) =
    L.map
        (prod.map (𝟙 (F.obj A))
          ((NatTrans.app h.unit B ≫ F.map (NatTrans.app (exp.adjunction A).unit (L.obj B))) ≫
            NatTrans.app (expComparison F A) (A ⨯ L.obj B))) ≫
      L.map (NatTrans.app (exp.adjunction (F.obj A)).counit (F.obj (A ⨯ L.obj B))) ≫ NatTrans.app h.counit (A ⨯ L.obj B)
[PROOFSTEP]
rw [← L.map_comp_assoc, prod.map_id_comp, assoc]
  -- Porting note: need to use `erw` here.
    -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) =
    L.map
        (prod.map (𝟙 (F.obj A)) (NatTrans.app h.unit B ≫ F.map (NatTrans.app (exp.adjunction A).unit (L.obj B))) ≫
          prod.map (𝟙 (F.obj A)) (NatTrans.app (expComparison F A) (A ⨯ L.obj B)) ≫
            NatTrans.app (exp.adjunction (F.obj A)).counit (F.obj (A ⨯ L.obj B))) ≫
      NatTrans.app h.counit (A ⨯ L.obj B)
[PROOFSTEP]
erw [expComparison_ev]
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) =
    L.map
        (prod.map (𝟙 (F.obj A)) (NatTrans.app h.unit B ≫ F.map (NatTrans.app (exp.adjunction A).unit (L.obj B))) ≫
          inv (prodComparison F A (A ⟹ A ⨯ L.obj B)) ≫ F.map (NatTrans.app (exp.ev A) (A ⨯ L.obj B))) ≫
      NatTrans.app h.counit (A ⨯ L.obj B)
[PROOFSTEP]
rw [prod.map_id_comp, assoc, ← F.map_id, ← prodComparison_inv_natural_assoc, ← F.map_comp]
  -- Porting note: need to use `erw` here.
    -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) =
    L.map
        (prod.map (F.map (𝟙 A)) (NatTrans.app h.unit B) ≫
          inv (prodComparison F A (L.obj B)) ≫
            F.map
              (prod.map (𝟙 A) (NatTrans.app (exp.adjunction A).unit (L.obj B)) ≫
                NatTrans.app (exp.ev A) (A ⨯ L.obj B))) ≫
      NatTrans.app h.counit (A ⨯ L.obj B)
[PROOFSTEP]
erw [exp.ev_coev]
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) =
    L.map
        (prod.map (F.map (𝟙 A)) (NatTrans.app h.unit B) ≫
          inv (prodComparison F A (L.obj B)) ≫ F.map (𝟙 (A ⨯ L.obj B))) ≫
      NatTrans.app h.counit (A ⨯ L.obj B)
[PROOFSTEP]
rw [F.map_id (A ⨯ L.obj B), comp_id]
[GOAL]
case w.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) =
    L.map (prod.map (F.map (𝟙 A)) (NatTrans.app h.unit B) ≫ inv (prodComparison F A (L.obj B))) ≫
      NatTrans.app h.counit (A ⨯ L.obj B)
[PROOFSTEP]
ext
[GOAL]
case w.h.h₁
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ (prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B))) ≫ prod.fst =
    (L.map (prod.map (F.map (𝟙 A)) (NatTrans.app h.unit B) ≫ inv (prodComparison F A (L.obj B))) ≫
        NatTrans.app h.counit (A ⨯ L.obj B)) ≫
      prod.fst
[PROOFSTEP]
rw [assoc, assoc, ← h.counit_naturality, ← L.map_comp_assoc, assoc, inv_prodComparison_map_fst]
[GOAL]
case w.h.h₁
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) ≫ prod.fst =
    L.map (prod.map (F.map (𝟙 A)) (NatTrans.app h.unit B) ≫ prod.fst) ≫ NatTrans.app h.counit A
[PROOFSTEP]
simp
[GOAL]
case w.h.h₂
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ (prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B))) ≫ prod.snd =
    (L.map (prod.map (F.map (𝟙 A)) (NatTrans.app h.unit B) ≫ inv (prodComparison F A (L.obj B))) ≫
        NatTrans.app h.counit (A ⨯ L.obj B)) ≫
      prod.snd
[PROOFSTEP]
rw [assoc, assoc, ← h.counit_naturality, ← L.map_comp_assoc, assoc, inv_prodComparison_map_snd]
[GOAL]
case w.h.h₂
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
B : D
⊢ prodComparison L (F.obj A) B ≫ prod.map (NatTrans.app h.counit A) (𝟙 (L.obj B)) ≫ prod.snd =
    L.map (prod.map (F.map (𝟙 A)) (NatTrans.app h.unit B) ≫ prod.snd) ≫ NatTrans.app h.counit (L.obj B)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (expComparison F A)
⊢ IsIso (frobeniusMorphism F h A)
[PROOFSTEP]
rw [← frobeniusMorphism_mate F h] at i
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
i :
  IsIso
    (↑(transferNatTransSelf (Adjunction.comp h (exp.adjunction A)) (Adjunction.comp (exp.adjunction (F.obj A)) h))
      (frobeniusMorphism F h A))
⊢ IsIso (frobeniusMorphism F h A)
[PROOFSTEP]
exact @transferNatTransSelf_of_iso _ _ _ _ _ _ _ _ _ _ _ i
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (frobeniusMorphism F h A)
⊢ IsIso (expComparison F A)
[PROOFSTEP]
rw [← frobeniusMorphism_mate F h]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (frobeniusMorphism F h A)
⊢ IsIso
    (↑(transferNatTransSelf (Adjunction.comp h (exp.adjunction A)) (Adjunction.comp (exp.adjunction (F.obj A)) h))
      (frobeniusMorphism F h A))
[PROOFSTEP]
infer_instance