[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A✝ B X✝ X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A✝
A X : C
inst✝ : Exponentiable A
⊢ uncurry (𝟙 (A ⟹ X)) = NatTrans.app (exp.ev A) X
[PROOFSTEP]
rw [uncurry_eq, prod.map_id_id, id_comp]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A✝ B X✝ X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A✝
A X : C
inst✝ : Exponentiable A
⊢ curry (𝟙 (A ⨯ (𝟭 C).obj X)) = NatTrans.app (exp.coev A) X
[PROOFSTEP]
rw [curry_eq, (exp A).map_id (A ⨯ _)]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A✝ B X✝ X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A✝
A X : C
inst✝ : Exponentiable A
⊢ NatTrans.app (exp.coev A) ((𝟭 C).obj X) ≫ 𝟙 (A ⟹ A ⨯ (𝟭 C).obj X) = NatTrans.app (exp.coev A) X
[PROOFSTEP]
apply comp_id
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
inst✝ : Exponentiable (⊤_ C)
Z✝ : C
g : Z✝ ⟶ (⊤_ C) ⟹ X
⊢ (fun {Y} f => CartesianClosed.curry ((prod.leftUnitor Y).hom ≫ f))
      ((fun {Y} f => (prod.leftUnitor Y).inv ≫ CartesianClosed.uncurry f) g) =
    g
[PROOFSTEP]
rw [curry_eq_iff, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
inst✝ : Exponentiable (⊤_ C)
Z✝ : C
g : Z✝ ⟶ X
⊢ (fun {Y} f => (prod.leftUnitor Y).inv ≫ CartesianClosed.uncurry f)
      ((fun {Y} f => CartesianClosed.curry ((prod.leftUnitor Y).hom ≫ f)) g) =
    g
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
inst✝ : Exponentiable (⊤_ C)
Z✝ Z'✝ : C
f : Z'✝ ⟶ Z✝
g : Z✝ ⟶ (⊤_ C) ⟹ X
⊢ (fun {Y} f => (prod.leftUnitor Y).inv ≫ CartesianClosed.uncurry f) (f ≫ g) =
    f ≫ (fun {Y} f => (prod.leftUnitor Y).inv ≫ CartesianClosed.uncurry f) g
[PROOFSTEP]
dsimp [-prod.leftUnitor_inv]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
inst✝ : Exponentiable (⊤_ C)
Z✝ Z'✝ : C
f : Z'✝ ⟶ Z✝
g : Z✝ ⟶ (⊤_ C) ⟹ X
⊢ (prod.leftUnitor Z'✝).inv ≫ CartesianClosed.uncurry (f ≫ g) = f ≫ (prod.leftUnitor Z✝).inv ≫ CartesianClosed.uncurry g
[PROOFSTEP]
rw [uncurry_natural_left, prod.leftUnitor_inv_naturality_assoc f]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
f : B ⟶ A
inst✝ : Exponentiable B
X : C
⊢ CartesianClosed.uncurry (NatTrans.app (pre f) X) = prod.map f (𝟙 (A ⟹ X)) ≫ NatTrans.app (exp.ev A) X
[PROOFSTEP]
rw [uncurry_eq, prod_map_pre_app_comp_ev]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A✝ B X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A✝
A : C
inst✝ : Exponentiable A
⊢ pre (𝟙 A) = 𝟙 (exp A)
[PROOFSTEP]
simp [pre]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Exponentiable A
A₁ A₂ A₃ : C
inst✝² : Exponentiable A₁
inst✝¹ : Exponentiable A₂
inst✝ : Exponentiable A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ pre (f ≫ g) = pre g ≫ pre f
[PROOFSTEP]
rw [pre, pre, pre, transferNatTransSelf_comp, prod.functor.map_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
⊢ prod.snd ≫ IsInitial.to t (A ⨯ I) = 𝟙 (A ⨯ I)
[PROOFSTEP]
have : (prod.snd : A ⨯ I ⟶ I) = CartesianClosed.uncurry (t.to _)
[GOAL]
case this
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
⊢ prod.snd = CartesianClosed.uncurry (IsInitial.to t (A ⟹ I))
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
this : prod.snd = CartesianClosed.uncurry (IsInitial.to t (A ⟹ I))
⊢ prod.snd ≫ IsInitial.to t (A ⨯ I) = 𝟙 (A ⨯ I)
[PROOFSTEP]
rw [← curry_eq_iff]
[GOAL]
case this
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
⊢ CartesianClosed.curry prod.snd = IsInitial.to t (A ⟹ I)
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
this : prod.snd = CartesianClosed.uncurry (IsInitial.to t (A ⟹ I))
⊢ prod.snd ≫ IsInitial.to t (A ⨯ I) = 𝟙 (A ⨯ I)
[PROOFSTEP]
apply t.hom_ext
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
this : prod.snd = CartesianClosed.uncurry (IsInitial.to t (A ⟹ I))
⊢ prod.snd ≫ IsInitial.to t (A ⨯ I) = 𝟙 (A ⨯ I)
[PROOFSTEP]
rw [this, ← uncurry_natural_right, ← eq_curry_iff]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
this : prod.snd = CartesianClosed.uncurry (IsInitial.to t (A ⟹ I))
⊢ IsInitial.to t (A ⟹ I) ≫ (exp A).map (IsInitial.to t (A ⨯ I)) = CartesianClosed.curry (𝟙 (A ⨯ I))
[PROOFSTEP]
apply t.hom_ext
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I : C
t : IsInitial I
inst✝ : CartesianClosed C
⊢ default ≫ CartesianClosed.curry ((mulZero t).hom ≫ IsInitial.to t B) = 𝟙 (I ⟹ B)
[PROOFSTEP]
rw [← curry_natural_left, curry_eq_iff, ← cancel_epi (mulZero t).inv]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I : C
t : IsInitial I
inst✝ : CartesianClosed C
⊢ (mulZero t).inv ≫ prod.map (𝟙 I) default ≫ (mulZero t).hom ≫ IsInitial.to t B =
    (mulZero t).inv ≫ CartesianClosed.uncurry (𝟙 (I ⟹ B))
[PROOFSTEP]
apply t.hom_ext
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr) ≫
      CartesianClosed.uncurry (coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr)) =
    𝟙 ((Z ⨯ X) ⨿ Z ⨯ Y)
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.inl ≫
      coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr) ≫
        CartesianClosed.uncurry (coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr)) =
    coprod.inl ≫ 𝟙 ((Z ⨯ X) ⨿ Z ⨯ Y)
case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.inr ≫
      coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr) ≫
        CartesianClosed.uncurry (coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr)) =
    coprod.inr ≫ 𝟙 ((Z ⨯ X) ⨿ Z ⨯ Y)
[PROOFSTEP]
rw [coprod.inl_desc_assoc, comp_id, ← uncurry_natural_left, coprod.inl_desc, uncurry_curry]
[GOAL]
case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.inr ≫
      coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr) ≫
        CartesianClosed.uncurry (coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr)) =
    coprod.inr ≫ 𝟙 ((Z ⨯ X) ⨿ Z ⨯ Y)
[PROOFSTEP]
rw [coprod.inr_desc_assoc, comp_id, ← uncurry_natural_left, coprod.inr_desc, uncurry_curry]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ CartesianClosed.uncurry (coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr)) ≫
      coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr) =
    𝟙 (Z ⨯ X ⨿ Y)
[PROOFSTEP]
rw [← uncurry_natural_right, ← eq_curry_iff]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr) ≫
      (exp Z).map (coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr)) =
    CartesianClosed.curry (𝟙 (Z ⨯ X ⨿ Y))
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.inl ≫
      coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr) ≫
        (exp Z).map (coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr)) =
    coprod.inl ≫ CartesianClosed.curry (𝟙 (Z ⨯ X ⨿ Y))
case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.inr ≫
      coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr) ≫
        (exp Z).map (coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr)) =
    coprod.inr ≫ CartesianClosed.curry (𝟙 (Z ⨯ X ⨿ Y))
[PROOFSTEP]
rw [coprod.inl_desc_assoc, ← curry_natural_right, coprod.inl_desc, ← curry_natural_left, comp_id]
[GOAL]
case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.inr ≫
      coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr) ≫
        (exp Z).map (coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr)) =
    coprod.inr ≫ CartesianClosed.curry (𝟙 (Z ⨯ X ⨿ Y))
[PROOFSTEP]
rw [coprod.inr_desc_assoc, ← curry_natural_right, coprod.inr_desc, ← curry_natural_left, comp_id]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
⊢ IsIso f
[PROOFSTEP]
haveI : Mono (prod.lift (𝟙 A) f ≫ (zeroMul t).hom) := mono_comp _ _
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this : Mono (prod.lift (𝟙 A) f ≫ (zeroMul t).hom)
⊢ IsIso f
[PROOFSTEP]
rw [zeroMul_hom, prod.lift_snd] at this 
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this : Mono f
⊢ IsIso f
[PROOFSTEP]
haveI : IsSplitEpi f := IsSplitEpi.mk' ⟨t.to _, t.hom_ext _ _⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this✝ : Mono f
this : IsSplitEpi f
⊢ IsIso f
[PROOFSTEP]
apply isIso_of_mono_of_isSplitEpi
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B✝ X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ IsInitial.to t B = h ≫ IsInitial.to t B
⊢ g = h
[PROOFSTEP]
haveI := strict_initial t g
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B✝ X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ IsInitial.to t B = h ≫ IsInitial.to t B
this : IsIso g
⊢ g = h
[PROOFSTEP]
haveI := strict_initial t h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B✝ X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ IsInitial.to t B = h ≫ IsInitial.to t B
this✝ : IsIso g
this : IsIso h
⊢ g = h
[PROOFSTEP]
exact eq_of_inv_eq_inv (t.hom_ext _ _)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
haveI q : Exponentiable (e.inverse.obj X) := inferInstance
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
have : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X)) := q.isAdj
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
have : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
[GOAL]
case this
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
⊢ e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝ : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
apply NatIso.ofComponents _ _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
⊢ (X_1 : C) → (e.functor ⋙ prod.functor.obj X ⋙ e.inverse).obj X_1 ≅ (prod.functor.obj (e.inverse.obj X)).obj X_1
[PROOFSTEP]
intro Y
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
Y : C
⊢ (e.functor ⋙ prod.functor.obj X ⋙ e.inverse).obj Y ≅ (prod.functor.obj (e.inverse.obj X)).obj Y
[PROOFSTEP]
apply asIso (prodComparison e.inverse X (e.functor.obj Y)) ≪≫ _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
Y : C
⊢ e.inverse.obj X ⨯ e.inverse.obj (e.functor.obj Y) ≅ (prod.functor.obj (e.inverse.obj X)).obj Y
[PROOFSTEP]
apply prod.mapIso (Iso.refl _) (e.unitIso.app Y).symm
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
⊢ ∀ {X_1 Y : C} (f : X_1 ⟶ Y),
    (e.functor ⋙ prod.functor.obj X ⋙ e.inverse).map f ≫
        (asIso (prodComparison e.inverse X (e.functor.obj Y)) ≪≫
            prod.mapIso (Iso.refl (e.inverse.obj X)) (e.unitIso.app Y).symm).hom =
      (asIso (prodComparison e.inverse X (e.functor.obj X_1)) ≪≫
            prod.mapIso (Iso.refl (e.inverse.obj X)) (e.unitIso.app X_1).symm).hom ≫
        (prod.functor.obj (e.inverse.obj X)).map f
[PROOFSTEP]
intro Y Z g
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
Y Z : C
g : Y ⟶ Z
⊢ (e.functor ⋙ prod.functor.obj X ⋙ e.inverse).map g ≫
      (asIso (prodComparison e.inverse X (e.functor.obj Z)) ≪≫
          prod.mapIso (Iso.refl (e.inverse.obj X)) (e.unitIso.app Z).symm).hom =
    (asIso (prodComparison e.inverse X (e.functor.obj Y)) ≪≫
          prod.mapIso (Iso.refl (e.inverse.obj X)) (e.unitIso.app Y).symm).hom ≫
      (prod.functor.obj (e.inverse.obj X)).map g
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
Y Z : C
g : Y ⟶ Z
⊢ e.inverse.map (prod.map (𝟙 X) (e.functor.map g)) ≫
      prodComparison e.inverse X (e.functor.obj Z) ≫ prod.map (𝟙 (e.inverse.obj X)) (NatTrans.app e.unitIso.inv Z) =
    (prodComparison e.inverse X (e.functor.obj Y) ≫ prod.map (𝟙 (e.inverse.obj X)) (NatTrans.app e.unitIso.inv Y)) ≫
      prod.map (𝟙 (e.inverse.obj X)) g
[PROOFSTEP]
simp [prodComparison, prod.comp_lift, ← e.inverse.map_comp, ← e.inverse.map_comp_assoc]
  -- I wonder if it would be a good idea to make `map_comp` a simp lemma the other way round
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝ : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
have : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse) := Adjunction.leftAdjointOfNatIso this.symm
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝¹ : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this✝ : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
this : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
have : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse) :=
  Adjunction.leftAdjointOfComp e.inverse _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝² : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this✝¹ : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
this✝ : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
have : (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse) ⋙ e.functor ≅ prod.functor.obj X :=
  by
  apply isoWhiskerRight e.counitIso (prod.functor.obj X ⋙ e.inverse ⋙ e.functor) ≪≫ _
  change prod.functor.obj X ⋙ e.inverse ⋙ e.functor ≅ prod.functor.obj X
  apply isoWhiskerLeft (prod.functor.obj X) e.counitIso
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝² : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this✝¹ : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
this✝ : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
⊢ (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse) ⋙ e.functor ≅ prod.functor.obj X
[PROOFSTEP]
apply isoWhiskerRight e.counitIso (prod.functor.obj X ⋙ e.inverse ⋙ e.functor) ≪≫ _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝² : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this✝¹ : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
this✝ : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
⊢ 𝟭 D ⋙ prod.functor.obj X ⋙ e.inverse ⋙ e.functor ≅ prod.functor.obj X
[PROOFSTEP]
change prod.functor.obj X ⋙ e.inverse ⋙ e.functor ≅ prod.functor.obj X
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝² : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this✝¹ : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
this✝ : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
⊢ prod.functor.obj X ⋙ e.inverse ⋙ e.functor ≅ prod.functor.obj X
[PROOFSTEP]
apply isoWhiskerLeft (prod.functor.obj X) e.counitIso
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝³ : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this✝² : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
this✝¹ : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this✝ : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this : (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse) ⋙ e.functor ≅ prod.functor.obj X
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
skip
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝³ : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this✝² : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
this✝¹ : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this✝ : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this : (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse) ⋙ e.functor ≅ prod.functor.obj X
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
apply Adjunction.leftAdjointOfNatIso this
