[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
