awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under.{v₂, u₂} j
⊢ Functor.map (ihom (F₁.obj k.right)) (f₃.app k.right) =
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
          (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
        (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
          (eHomEquiv C : (a : F₃.obj k.right ⟶ F₃'.obj k.right) → 𝟙_ C ⟶ F₃.obj k.right ⟶[C] F₃'.obj k.right)
            (f₃.app k.right))
        (eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right)))
have w : CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
      (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
        (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
      (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
        (eHomEquiv C : (a : F₃.obj k.right ⟶ F₃'.obj k.right) → 𝟙_ C ⟶ F₃.obj k.right ⟶[C] F₃'.obj k.right)
          (f₃.app k.right))
      (eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right))) =
  Functor.map (ihom (F₁.obj k.right)) (f₃.app k.right)
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete (goal)
Goal:
I : Type u₂
inst : Category.{v₂, u₂} I
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalClosed.{v₁, u₁} C
inst_4 :
  ∀ (F : Functor.{u₂, v₁, u₂, u₁} (Discrete I) C),
    HasRightKanExtension.{u₂, u₂, v₁, u₁, v₂, u₂} (Discrete.functor _root_.id) F
A B : Functor.{v₂, v₁, u₂, u₁} I C
f : A ⟶ B
h :
  IsIso (X := obj (obj (whiskeringLeft (Discrete I) I C) (incl I)) A)
    (map (obj (whiskeringLeft (Discrete I) I C) (incl I)) f)
⊢ IsIso f
have simp : ∀
  (h :
    ∀ (X : Discrete I),
      IsIso (X := (obj (obj (whiskeringLeft (Discrete I) I C) (incl I)) A).obj X)
        (NatTrans.app (map (obj (whiskeringLeft (Discrete I) I C) (incl I)) f) X))
  (X : I), IsIso (f.app X)
Tactic: simp only [NatTrans.isIso_iff_isIso_app] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid (goal)
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
⊢ (obj (𝟭 (Functor.{v, v_1, u, u_1} D C)) G).map f ≫ NatTrans.app (ihom.coev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.coev (F.obj X)) (G.obj X) ≫ ((tensorLeft F ⋙ F.closedIhom).obj G).map f
have dsimp : G.map f ≫ NatTrans.app (ihom.coev (F.obj Y)) (G.obj Y) =
  NatTrans.app (ihom.coev (F.obj X)) (G.obj X) ≫ (F.closedIhom.obj (tensorObj (𝒞 := category) F G)).map f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid (goal)
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ NatTrans.app (ihom.coev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.coev (F.obj X)) (G.obj X) ≫ (F.closedIhom.obj (tensorObj (𝒞 := category) F G)).map f
have simp : Eq (α := G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
  (NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ map (ihom (F.obj Y)) (F.obj Y ◁ G.map f) :
    obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj X) ⟶
      obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
  (CategoryStruct.comp (Y :=
      obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (G.obj X)))
      (NatTrans.app (ihom.coev (F.obj X)) (G.obj X))
      (NatTrans.app (pre (CategoryTheory.inv (F.map f))) ((tensorObj (𝒞 := category) F G).obj X) ≫
        map (ihom (F.obj Y)) (F.map f ⊗ₘ G.map f)) :
    G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
Tactic: simp only [ihom.coev_naturality, closedIhom_obj_map, Monoidal.tensorObj_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid (goal)
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
⊢ Eq (α := G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ map (ihom (F.obj Y)) (F.obj Y ◁ G.map f) :
      obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj X) ⟶
        obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (CategoryStruct.comp (Y :=
        obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (G.obj X)))
        (NatTrans.app (ihom.coev (F.obj X)) (G.obj X))
        (NatTrans.app (pre (CategoryTheory.inv (F.map f))) ((tensorObj (𝒞 := category) F G).obj X) ≫
          map (ihom (F.obj Y)) (F.map f ⊗ₘ G.map f)) :
      G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
have dsimp : Eq (α := G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
  (NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ map (ihom (F.obj Y)) (F.obj Y ◁ G.map f) :
    G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
  (CategoryStruct.comp (Y :=
      obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (G.obj X)))
      (NatTrans.app (ihom.coev (F.obj X)) (G.obj X))
      (NatTrans.app (pre (CategoryTheory.inv (F.map f))) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (G.obj X)) ≫
        map (ihom (F.obj Y)) (F.map f ⊗ₘ G.map f)) :
    G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid (goal)
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
⊢ Eq (α := G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ map (ihom (F.obj Y)) (F.obj Y ◁ G.map f) :
      G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (CategoryStruct.comp (Y :=
        obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (G.obj X)))
        (NatTrans.app (ihom.coev (F.obj X)) (G.obj X))
        (NatTrans.app (pre (CategoryTheory.inv (F.map f))) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (G.obj X)) ≫
          map (ihom (F.obj Y)) (F.map f ⊗ₘ G.map f)) :
      G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
have rw : Eq (α := G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
  (NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ map (ihom (F.obj Y)) (F.obj Y ◁ G.map f) :
    G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
  (NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫
      map (ihom (F.obj Y)) (CategoryTheory.inv (F.map f) ▷ G.obj X ≫ F.map f ▷ G.obj X ≫ F.obj Y ◁ G.map f) :
    G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
Tactic: rw [coev_app_comp_pre_app_assoc, ← Functor.map_comp, tensorHom_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid (goal)
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
⊢ ((F.closedIhom ⋙ tensorLeft F).obj G).map f ≫ NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ (obj (𝟭 (Functor.{v, v_1, u, u_1} D C)) G).map f
have dsimp : (F.map f ⊗ₘ (F.closedIhom.obj G).map f) ≫ NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y) =
  NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid (goal)
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
⊢ (F.map f ⊗ₘ (F.closedIhom.obj G).map f) ≫ NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f
have simp : Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (G.obj X)) ⟶ G.obj Y)
  (CategoryStruct.comp (Y :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (G.obj Y)))
    (F.map f ⊗ₘ map (ihom (F.obj X)) (G.map f) ≫ NatTrans.app (pre (CategoryTheory.inv (F.map f))) (G.obj Y))
    (NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y)))
  (NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f)
Tactic: simp only [closedIhom_obj_map, pre_comm_ihom_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid (goal)
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
⊢ Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (G.obj X)) ⟶ G.obj Y)
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (G.obj Y)))
      (F.map f ⊗ₘ map (ihom (F.obj X)) (G.map f) ≫ NatTrans.app (pre (CategoryTheory.inv (F.map f))) (G.obj Y))
      (NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y)))
    (NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f)
have rw : Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (G.obj X)) ⟶ G.obj Y)
  (CategoryStruct.comp (Y :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (G.obj Y)))
    (F.map f ▷ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (G.obj X) ≫
      F.obj Y ◁ (map (ihom (F.obj X)) (G.map f) ≫ NatTrans.app (pre (CategoryTheory.inv (F.map f))) (G.obj Y)))
    (NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y)))
  (NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f)
Tactic: rw [tensorHom_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F X_1 Y : C ⥤ Type (max w v u)
f : X_1 ⟶ Y
X : C
a : (F.functorHom X_1).obj X
c d : C
g : c ⟶ d
h : obj (Opposite.unop (obj (Functor.rightOp coyoneda) X)) c
this :
  F.map g ≫
      a.app d
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) g) :
            (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj c)) →
              (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj d))
          h) =
    a.app c h ≫ X_1.map g
⊢ F.map g ≫
      a.app d
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (Functor.map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) g) :
              (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj c)) →
                (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj d))
            h) ≫
        f.app d =
    (a.app c h ≫ f.app c) ≫ Y.map g
have change : (F.map g ≫ a.app d (h ≫ g)) ≫ f.app d = (a.app c h ≫ f.app c) ≫ Y.map g
Tactic: change (F.map g ≫ a.app _ (h ≫ g)) ≫ _ = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
⊢ Functor.map (𝟭 (C ⥤ Type (max w v u))) f ≫
      Equiv.invFun (functorHomEquiv.{w, v, u} F H (obj (tensorLeft F) H)) (𝟙 (tensorObj (𝒞 := category) F H)) =
    Equiv.invFun (functorHomEquiv.{w, v, u} F G (obj (tensorLeft F) G)) (𝟙 (tensorObj (𝒞 := category) F G)) ≫
      (tensorLeft F ⋙ rightAdj.{w, v, u} F).map f
have w : ∀ (x : C) (x_1 : (obj (𝟭 (C ⥤ Type (max w v u))) G).obj x),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Functor.map (𝟭 (C ⥤ Type (max w v u))) f ≫
            Equiv.invFun (functorHomEquiv.{w, v, u} F H (obj (tensorLeft F) H)) (𝟙 (tensorObj (𝒞 := category) F H)))
          x))
      x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Equiv.invFun (functorHomEquiv.{w, v, u} F G (obj (tensorLeft F) G)) (𝟙 (tensorObj (𝒞 := category) F G)) ≫
                (tensorLeft F ⋙ rightAdj.{w, v, u} F).map f).app
            x)).toFun
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
x : C
x_1 : (obj (𝟭 (C ⥤ Type (max w v u))) G).obj x
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Functor.map (𝟭 (C ⥤ Type (max w v u))) f ≫
            Equiv.invFun (functorHomEquiv.{w, v, u} F H (obj (tensorLeft F) H)) (𝟙 (tensorObj (𝒞 := category) F H)))
          x))
      x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Equiv.invFun (functorHomEquiv.{w, v, u} F G (obj (tensorLeft F) G)) (𝟙 (tensorObj (𝒞 := category) F G)) ≫
                (tensorLeft F ⋙ rightAdj.{w, v, u} F).map f).app
            x)).toFun
      x_1
have w : Eq (α := F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))
  (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app
              (f ≫
                (Equiv.symm (functorHomEquiv.{w, v, u} F H (tensorObj (𝒞 := category) F H)) :
                    (a : F ⊗ H ⟶ F ⊗ H) → H ⟶ F.functorHom (F ⊗ H))
                  (𝟙 (tensorObj (𝒞 := category) F H)))
              x) :
          TypeCat.Fun (G.obj x) (F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))) :
        (a : G.obj x) → F.HomObj (F ⊗ H) (coyoneda.obj (Opposite.op x)))
      x_1 :
    F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))
  (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app
              ((Equiv.symm (functorHomEquiv.{w, v, u} F G (tensorObj (𝒞 := category) F G)) :
                    (a : F ⊗ G ⟶ F ⊗ G) → G ⟶ F.functorHom (F ⊗ G))
                  (𝟙 (tensorObj (𝒞 := category) F G)) ≫
                (rightAdj.{w, v, u} F).map (F ◁ f))
              x) :
          TypeCat.Fun (G.obj x) (F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))) :
        (a : G.obj x) → F.HomObj (F ⊗ H) (coyoneda.obj (Opposite.op x)))
      x_1 :
    F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalClosed.{v₁, u₁} C
h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)
B : C
hB : i.essImage B
A : C
⊢ i.essImage (A ⟹ B)
have rcases : ∀ (B' : D) (iB' : i.obj B' ≅ B), i.essImage (A ⟹ B)
Tactic: rcases hB with ⟨B', ⟨iB'⟩⟩
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalClosed.{v₁, u₁} C
⊢ ExponentialIdeal.{v₁, u₁, u₁} (D := Subterminals.{v₁, u₁} C) (subterminalInclusion C)
have h : ∀ (B : Subterminals.{v₁, u₁} C) (A : C),
  Functor.essImage.{v₁, v₁, u₁, u₁} (C := Subterminals.{v₁, u₁} C) (subterminalInclusion C)
    (A ⟹ Functor.obj (subterminalInclusion C) B)
Tactic: apply ExponentialIdeal.mk'
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalClosed.{v₁, u₁} C
B : Subterminals.{v₁, u₁} C
A : C
⊢ Functor.essImage.{v₁, v₁, u₁, u₁} (C := Subterminals.{v₁, u₁} C) (subterminalInclusion C)
    (A ⟹ Functor.obj (subterminalInclusion C) B)
have h : ∀ (Z : C) (g h : Z ⟶ A ⟹ B.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)), g = h
Tactic: refine ⟨⟨A ⟹ B.1, fun Z g h => ?_⟩, ⟨Iso.refl _⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalClosed.{v₁, u₁} C
A : C
inst_4 : Reflective i
inst_5 : ExponentialIdeal i
⊢ i ⋙ ihom A ⋙ reflector i ⋙ i ≅ i ⋙ ihom A
have symm : i ⋙ ihom A ≅ i ⋙ ihom A ⋙ reflector i ⋙ i
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalClosed.{v₁, u₁} C
A : C
inst_4 : Reflective i
inst_5 : ExponentialIdeal i
⊢ i ⋙ ihom A ≅ i ⋙ ihom A ⋙ reflector i ⋙ i
have apply : (X : D) → (i ⋙ ihom A).obj X ≅ (i ⋙ ihom A ⋙ reflector i ⋙ i).obj X
Tactic: apply NatIso.ofComponents _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalClosed.{v₁, u₁} C
A : C
inst_4 : Reflective i
inst_5 : ExponentialIdeal i
apply : (X : D) → (i ⋙ ihom A).obj X ≅ (i ⋙ ihom A ⋙ reflector i ⋙ i).obj X
⊢ i ⋙ ihom A ≅ i ⋙ ihom A ⋙ reflector i ⋙ i
have apply₁ : ∀ {X Y : D} (f : X ⟶ Y),
  (i ⋙ ihom A).map f ≫ Iso.hom (asIso (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (A ⟹ i.obj Y))) =
    Iso.hom (asIso (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (A ⟹ i.obj X))) ≫
      (i ⋙ ihom A ⋙ reflector i ⋙ i).map f
Tactic: apply NatIso.ofComponents _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalClosed.{v₁, u₁} C
A : C
inst_4 : Reflective i
inst_5 : ExponentialIdeal i
X : D
⊢ (i ⋙ ihom A).obj X ≅ (i ⋙ ihom A ⋙ reflector i ⋙ i).obj X
have this : IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (A ⟹ i.obj X)) (Y := (reflector i ⋙ i).obj (A ⟹ i.obj X))
  (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (A ⟹ i.obj X))
Tactic: haveI := Functor.essImage.unit_isIso (ExponentialIdeal.exp_closed (i.obj_mem_essImage X) A)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalClosed.{v₁, u₁} C
inst_4 : Reflective i
h : (A : C) → i ⋙ ihom A ⋙ reflector i ⋙ i ≅ i ⋙ ihom A
⊢ ExponentialIdeal i
have h₁ : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)
Tactic: apply ExponentialIdeal.mk'
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
⊢ IsLimit.{0, v₁, 0, u₂} (asEmptyCone ((reflector i).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
have t : IsLimit (i.mapCone (asEmptyCone ((reflector i).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))
Tactic: apply isLimitOfReflects i
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
⊢ IsLimit (i.mapCone (asEmptyCone ((reflector i).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))
have t : Cone.pt.{0, v₁, 0, u₁} (asEmptyCone (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≅
  (i.mapCone (asEmptyCone ((reflector i).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))).pt
Tactic: apply isLimitChangeEmptyCone _ isTerminalTensorUnit
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
⊢ IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Y :=
    (reflector i ⋙ i).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
have this : HasFiniteProducts.{v₁, u₂} D
Tactic: have := reflective_products i
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
this : HasFiniteProducts.{v₁, u₂} D
⊢ IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Y :=
    (reflector i ⋙ i).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
have refine : terminal.{v₁, u₁} C ≅ tensorUnit.{v₁, u₁} C (𝒞 := inst)
Tactic: refine Functor.essImage.unit_isIso ⟨terminal D, ⟨PreservesTerminal.iso i |>.trans ?_⟩⟩