awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ HEq (α :=
    f ≫
        Functor.obj (Cat.Hom.toFunctor (eId Cat b))
          { down := { as := () : Discrete Unit } : ULift.{u_2, 0} (ULiftHom (Discrete Unit)) } ⟶
      f' ≫
        Functor.obj (Cat.Hom.toFunctor (eId Cat b))
          { down := { as := () : Discrete Unit } : ULift.{u_2, 0} (ULiftHom (Discrete Unit)) })
    (hComp η (Functor.map (Cat.Hom.toFunctor (eId Cat b)) (𝟙 { down := { as := () } }))) η

Tactic:
exact congr_arg_heq (·.toFunctor.map η) (e_comp_id (V := Cat) a b)

Premises used: CategoryTheory.e_comp_id, congr_arg_heq, CategoryTheory.Cat
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ Eq (α := f ≫ 𝟙 b ⟶ f' ≫ 𝟙 b) (hComp η (𝟙 (𝟙 b))) (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)

Tactic:
simp [← heq_eq_eq, hComp_id_heq]

Premises used: heq_eq_eq, CategoryTheory.CatEnriched.hComp_id_heq
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c d : CatEnriched C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ hComp (hComp η θ) κ ≍ hComp η (hComp θ κ)

Tactic:
congr_arg_heq (·.toFunctor.map (X := (_, _, _)) (Y := (_, _, _)) (η, θ, κ))
    (e_assoc (V := Cat) a b c d)

Premises used: congr_arg_heq, CategoryTheory.CatEnriched.hComp, CategoryTheory.Cat, CategoryTheory.e_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c d : CatEnriched C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ hComp (hComp η θ) κ = eqToHom ⋯ ≫ hComp η (hComp θ κ) ≫ eqToHom ⋯

Tactic:
simp [← heq_eq_eq, hComp_assoc_heq]

Premises used: heq_eq_eq, CategoryTheory.CatEnriched.hComp_assoc_heq
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
⊢ ∀ {a b c d : CatEnriched C} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
    hComp (𝟙 (f ≫ g)) η = Iso.hom (eqToIso ⋯) ≫ hComp (𝟙 f) (hComp (𝟙 g) η) ≫ Iso.inv (eqToIso ⋯)

Tactic:
simp [← id_hComp_id, hComp_assoc]

Premises used: CategoryTheory.CatEnriched.id_hComp_id, CategoryTheory.CatEnriched.hComp_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
⊢ ∀ {a b c d : CatEnriched C} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
    hComp η (𝟙 (g ≫ h)) = Iso.inv (eqToIso ⋯) ≫ hComp (hComp η (𝟙 g)) (𝟙 h) ≫ Iso.hom (eqToIso ⋯)

Tactic:
simp [hComp_assoc]

Premises used: CategoryTheory.CatEnriched.hComp_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
⊢ ∀ {a b c d : CatEnriched C} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
    hComp (hComp (𝟙 f) η) (𝟙 h) = Iso.hom (eqToIso ⋯) ≫ hComp (𝟙 f) (hComp η (𝟙 h)) ≫ Iso.inv (eqToIso ⋯)

Tactic:
simp [hComp_assoc]

Premises used: CategoryTheory.CatEnriched.hComp_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c d e : CatEnriched C
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
generalize_proofs :
  ∀ (h1 : (f ≫ g) ≫ h = f ≫ g ≫ h) (h2 : (f ≫ g ≫ h) ≫ i = f ≫ (g ≫ h) ≫ i) (h3 : (g ≫ h) ≫ i = g ≫ h ≫ i)
    (h4 : ((f ≫ g) ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i) (pf : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i),
    hComp (Iso.hom (eqToIso h1)) (𝟙 i) ≫ Iso.hom (eqToIso h2) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h3)) =
      Iso.hom (eqToIso h4) ≫ Iso.hom (eqToIso pf)
⊢ Eq (α := ((f ≫ g) ≫ h) ≫ i ⟶ f ≫ g ≫ h ≫ i)
    (CategoryStruct.comp (Y := (f ≫ g ≫ h) ≫ i) (hComp (Iso.hom (eqToIso ⋯)) (𝟙 i))
      (CategoryStruct.comp (Y := f ≫ (g ≫ h) ≫ i) (Iso.hom (eqToIso ⋯)) (hComp (𝟙 f) (Iso.hom (eqToIso ⋯)))))
    (CategoryStruct.comp (Y := (f ≫ g) ≫ h ≫ i) (Iso.hom (eqToIso ⋯)) (Iso.hom (eqToIso ⋯)))

Tactic:
generalize_proofs h1 h2 h3 h4
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c d e : CatEnriched C
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
h1 : (f ≫ g) ≫ h = f ≫ g ≫ h
h2 : (f ≫ g ≫ h) ≫ i = f ≫ (g ≫ h) ≫ i
h3 : (g ≫ h) ≫ i = g ≫ h ≫ i
h4 : ((f ≫ g) ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i
pf : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i
revert :
  ∀ (h1 : (f ≫ g) ≫ h = f ≫ g ≫ h) (h2 : (f ≫ g ≫ h) ≫ i = f ≫ (g ≫ h) ≫ i) (h3 : (g ≫ h) ≫ i = g ≫ h ≫ i)
    (h4 : ((f ≫ g) ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i),
    hComp (Iso.hom (eqToIso h1)) (𝟙 i) ≫ Iso.hom (eqToIso h2) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h3)) =
      Iso.hom (eqToIso h4) ≫ Iso.hom (eqToIso pf)
⊢ hComp (Iso.hom (eqToIso h1)) (𝟙 i) ≫ Iso.hom (eqToIso h2) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h3)) =
    Iso.hom (eqToIso h4) ≫ Iso.hom (eqToIso pf)

Tactic:
revert h1 h2 h3 h4
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c d e : CatEnriched C
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
pf : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i
generalize :
  ∀ (x : a ⟶ d) (w : b ⟶ e) (h1 : x = f ≫ g ≫ h) (h2 : (f ≫ g ≫ h) ≫ i = f ≫ w) (h3 : w = g ≫ h ≫ i)
    (h4 : x ≫ i = (f ≫ g) ≫ h ≫ i),
    hComp (Iso.hom (eqToIso h1)) (𝟙 i) ≫ Iso.hom (eqToIso h2) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h3)) =
      Iso.hom (eqToIso h4) ≫ Iso.hom (eqToIso pf)
⊢ ∀ (h1 : (f ≫ g) ≫ h = f ≫ g ≫ h) (h2 : (f ≫ g ≫ h) ≫ i = f ≫ (g ≫ h) ≫ i) (h3 : (g ≫ h) ≫ i = g ≫ h ≫ i)
    (h4 : ((f ≫ g) ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i),
    hComp (Iso.hom (eqToIso h1)) (𝟙 i) ≫ Iso.hom (eqToIso h2) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h3)) =
      Iso.hom (eqToIso h4) ≫ Iso.hom (eqToIso pf)

Tactic:
generalize (f ≫ g) ≫ h = x, (g ≫ h) ≫ i = w

Premises used: CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c d e : CatEnriched C
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
pf : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i
h2 : (f ≫ g ≫ h) ≫ i = f ≫ g ≫ h ≫ i
h4 : (f ≫ g ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i
⊢ hComp (Iso.hom (eqToIso ⋯)) (𝟙 i) ≫ Iso.hom (eqToIso h2) ≫ hComp (𝟙 f) (Iso.hom (eqToIso ⋯)) =
    Iso.hom (eqToIso h4) ≫ Iso.hom (eqToIso pf)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g : b ⟶ c
generalize_proofs :
  ∀ (h1 : (f ≫ 𝟙 b) ≫ g = f ≫ 𝟙 b ≫ g) (h2 : 𝟙 b ≫ g = g) (h3 : f ≫ 𝟙 b = f),
    Iso.hom (eqToIso h1) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h2)) = hComp (Iso.hom (eqToIso h3)) (𝟙 g)
⊢ Eq.{u_3 + 1} (α := (f ≫ 𝟙 b) ≫ g ⟶ f ≫ g)
    (CategoryStruct.comp (Y := f ≫ 𝟙 b ≫ g) (Iso.hom (eqToIso ⋯)) (hComp (𝟙 f) (Iso.hom (eqToIso ⋯))) :
      (f ≫ 𝟙 b) ≫ g ⟶ f ≫ g)
    (hComp (Iso.hom (eqToIso ⋯)) (𝟙 g) : (f ≫ 𝟙 b) ≫ g ⟶ f ≫ g)

Tactic:
generalize_proofs h1 h2 h3
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g : b ⟶ c
h1 : (f ≫ 𝟙 b) ≫ g = f ≫ 𝟙 b ≫ g
h2 : 𝟙 b ≫ g = g
h3 : f ≫ 𝟙 b = f
revert :
  ∀ (h1 : (f ≫ 𝟙 b) ≫ g = f ≫ 𝟙 b ≫ g) (h2 : 𝟙 b ≫ g = g) (h3 : f ≫ 𝟙 b = f),
    Iso.hom (eqToIso h1) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h2)) = hComp (Iso.hom (eqToIso h3)) (𝟙 g)
⊢ Iso.hom (eqToIso h1) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h2)) = hComp (Iso.hom (eqToIso h3)) (𝟙 g)

Tactic:
revert h1 h2 h3
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g : b ⟶ c
generalize :
  ∀ (g_1 : b ⟶ c) (f_1 : a ⟶ b) (h1 : f_1 ≫ g = f ≫ g_1) (h2 : g_1 = g) (h3 : f_1 = f),
    Iso.hom (eqToIso h1) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h2)) = hComp (Iso.hom (eqToIso h3)) (𝟙 g)
⊢ ∀ (h1 : (f ≫ 𝟙 b) ≫ g = f ≫ 𝟙 b ≫ g) (h2 : 𝟙 b ≫ g = g) (h3 : f ≫ 𝟙 b = f),
    Iso.hom (eqToIso h1) ≫ hComp (𝟙 f) (Iso.hom (eqToIso h2)) = hComp (Iso.hom (eqToIso h3)) (𝟙 g)

Tactic:
generalize 𝟙 _ ≫ g = g, f ≫ 𝟙 _ = f

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : EnrichedCategory Cat C
a b c : CatEnriched C
g : b ⟶ c
f : a ⟶ b
h1 : f ≫ g = f ≫ g
⊢ Iso.hom (eqToIso h1) ≫ hComp (𝟙 f) (Iso.hom (eqToIso ⋯)) = hComp (Iso.hom (eqToIso ⋯)) (𝟙 g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a : CatEnrichedOrdinary C
simp :
  Eq.{u' + 1} (α := a.toBase ⟶ a.toBase)
    ((Cat.fromChosenTerminalEquiv :
          (a_1 : (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] a) : Type u')) →
            a.toBase ⟶ a.toBase)
        ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
              (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a a) :
            (a_1 : MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] a) →
              (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] a) : Type u'))
          ((eHomEquiv Cat : (a_1 : a ⟶ a) → MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] a) (𝟙 a))) :
      a.toBase ⟶ a.toBase)
    (𝟙 a.toBase : a.toBase ⟶ a.toBase)
⊢ Eq.{u' + 1} (α := a.toBase ⟶ a.toBase)
    ((Equiv.trans (eHomEquiv Cat)
            (Equiv.trans
              (Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
                (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a a))
              Cat.fromChosenTerminalEquiv) :
          (a_1 : a ⟶ a) → a.toBase ⟶ a.toBase)
        (𝟙 a) :
      a.toBase ⟶ a.toBase)
    (𝟙 a.toBase : a.toBase ⟶ a.toBase)

Tactic:
simp only [Equiv.trans_apply]

Premises used: Equiv.trans_apply
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a : CatEnrichedOrdinary C
rw :
  Eq.{u' + 1} (α := a.toBase ⟶ a.toBase)
    ((Cat.fromChosenTerminalEquiv :
          (a_1 : (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] a) : Type u')) →
            a.toBase ⟶ a.toBase)
        ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
              (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a a) :
            (a_1 : MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] a) →
              (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] a) : Type u'))
          (eId Cat a)) :
      a.toBase ⟶ a.toBase)
    (𝟙 a.toBase : a.toBase ⟶ a.toBase)
⊢ Eq.{u' + 1} (α := a.toBase ⟶ a.toBase)
    ((Cat.fromChosenTerminalEquiv :
          (a_1 : (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] a) : Type u')) →
            a.toBase ⟶ a.toBase)
        ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
              (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a a) :
            (a_1 : MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] a) →
              (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] a) : Type u'))
          ((eHomEquiv Cat : (a_1 : a ⟶ a) → MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] a) (𝟙 a))) :
      a.toBase ⟶ a.toBase)
    (𝟙 a.toBase : a.toBase ⟶ a.toBase)

Tactic:
rw [eHomEquiv_id]

Premises used: CategoryTheory.eHomEquiv_id
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a : CatEnrichedOrdinary C
⊢ Eq.{u' + 1} (α := a.toBase ⟶ a.toBase)
    ((Cat.fromChosenTerminalEquiv :
          (a_1 : (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] a) : Type u')) →
            a.toBase ⟶ a.toBase)
        ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
              (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a a) :
            (a_1 : MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] a) →
              (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] a) : Type u'))
          (eId Cat a)) :
      a.toBase ⟶ a.toBase)
    (𝟙 a.toBase : a.toBase ⟶ a.toBase)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g : b ⟶ c
unfold :
  Eq.{u' + 1} (α := a.toBase ⟶ c.toBase)
    ((Equiv.trans (eHomEquiv Cat)
            (Equiv.trans
              (Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
                (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a c))
              Cat.fromChosenTerminalEquiv) :
          (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase)
        (f ≫ g) :
      a.toBase ⟶ c.toBase)
    (CategoryStruct.comp (Y := b.toBase)
        ((Equiv.trans (eHomEquiv Cat)
              (Equiv.trans
                (Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
                  (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a b))
                Cat.fromChosenTerminalEquiv) :
            (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase)
          f)
        ((Equiv.trans (eHomEquiv Cat)
              (Equiv.trans
                (Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
                  (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ b c))
                Cat.fromChosenTerminalEquiv) :
            (a : b ⟶ c) → b.toBase ⟶ c.toBase)
          g) :
      a.toBase ⟶ c.toBase)
⊢ Eq.{u' + 1} (α := a.toBase ⟶ c.toBase)
    ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f ≫ g) : a.toBase ⟶ c.toBase)
    (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f)
        ((homEquiv : (a : b ⟶ c) → b.toBase ⟶ c.toBase) g) :
      a.toBase ⟶ c.toBase)

Tactic:
unfold homEquiv

Premises used: CategoryTheory.CatEnrichedOrdinary.homEquiv
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g : b ⟶ c
⊢ Eq.{u' + 1} (α := a.toBase ⟶ c.toBase)
    ((Cat.fromChosenTerminalEquiv :
          (a_1 : (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] c) : Type u')) →
            a.toBase ⟶ c.toBase)
        ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
              (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a c) :
            (a_1 : MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] c) →
              (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] c) : Type u'))
          (CategoryStruct.comp (Y :=
            MonoidalCategoryStruct.tensorObj (𝒞 := Cat.category)
              (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
              (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category)))
            (Iso.inv (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))))
            (MonoidalCategoryStruct.tensorHom
                ((eHomEquiv Cat : (a_1 : a ⟶ b) → MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] b) f)
                ((eHomEquiv Cat : (a : b ⟶ c) → MonoidalCategoryStruct.tensorUnit Cat ⟶ b ⟶[Cat] c) g) ≫
              eComp Cat a b c))) :
      a.toBase ⟶ c.toBase)
    (CategoryStruct.comp (Y := b.toBase)
        ((Cat.fromChosenTerminalEquiv :
            (a_1 : (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] b) : Type u')) →
              a.toBase ⟶ b.toBase)
          ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
                (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ a b) :
              (a_1 : MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] b) →
                (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(a ⟶[Cat] b) : Type u'))
            ((eHomEquiv Cat : (a_1 : a ⟶ b) → MonoidalCategoryStruct.tensorUnit Cat ⟶ a ⟶[Cat] b) f)))
        ((Cat.fromChosenTerminalEquiv :
            (a : (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(b ⟶[Cat] c) : Type u')) →
              b.toBase ⟶ c.toBase)
          ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat (𝒞 := Cat.category))
                (@EnrichedCategory.Hom _ Cat.category SemiCartesianMonoidalCategory.toMonoidalCategory _ _ b c) :
              (a : MonoidalCategoryStruct.tensorUnit Cat ⟶ b ⟶[Cat] c) →
                (↑(MonoidalCategoryStruct.tensorUnit Cat) : Type u') ⥤ (↑(b ⟶[Cat] c) : Type u'))
            ((eHomEquiv Cat : (a : b ⟶ c) → MonoidalCategoryStruct.tensorUnit Cat ⟶ b ⟶[Cat] c) g))) :
      a.toBase ⟶ c.toBase)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
α : f ⟶ g
⊢ Hom.mk (Hom.base α) = α

Tactic:
rfl

Premises used: CategoryTheory.CatEnrichedOrdinary.Hom.base, CategoryTheory.CatEnrichedOrdinary.Hom.mk, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
α :
  Quiver.Hom.{v', u'} (V := X.toBase ⟶ Y.toBase)
    ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase)
    ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) g : X.toBase ⟶ Y.toBase)
⊢ Hom.base (Hom.mk α) = α

Tactic:
rfl

Premises used: CategoryTheory.CatEnrichedOrdinary.Hom.base, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f : X ⟶ Y
⊢ Eq.{v' + 1} (α := f ⟶ f) (𝟙 f) (mk (𝟙 ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f : X ⟶ Y
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := X.toBase ⟶ Y.toBase)
      ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase)
      ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase))
    (base (𝟙 f) :
      Quiver.Hom.{v', u'} (V := X.toBase ⟶ Y.toBase)
        ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase)
        ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase))
    (𝟙 ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f) :
      Quiver.Hom.{v', u'} (V := X.toBase ⟶ Y.toBase)
        ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase)
        ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase))

Tactic:
rfl

Premises used: CategoryTheory.CatEnrichedOrdinary.Hom.base, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g h : X ⟶ Y
α : f ⟶ g
β : g ⟶ h
⊢ α ≫ β = mk (base α ≫ base β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g h : X ⟶ Y
α : f ⟶ g
β : g ⟶ h
⊢ base (α ≫ β) = base α ≫ base β

Tactic:
rfl

Premises used: CategoryTheory.CatEnrichedOrdinary.Hom.base, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g h : X ⟶ Y
α :
  Quiver.Hom.{v', u'} (V := X.toBase ⟶ Y.toBase)
    ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase)
    ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) g : X.toBase ⟶ Y.toBase)
β :
  Quiver.Hom.{v', u'} (V := X.toBase ⟶ Y.toBase)
    ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) g : X.toBase ⟶ Y.toBase)
    ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) h : X.toBase ⟶ Y.toBase)
⊢ mk (α ≫ β) = mk α ≫ mk β

Tactic:
rfl

Premises used: CategoryTheory.CatEnrichedOrdinary.Hom.base, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
α β : f ⟶ g
H : base α = base β
mk' :
  ∀
    (base' :
      Quiver.Hom.{v', u'} (V := X.toBase ⟶ Y.toBase)
        ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase)
        ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) g : X.toBase ⟶ Y.toBase))
    (H : { base' := base' : Hom.{u, v, u', v'} f g }.base = base β), { base' := base' : Hom.{u, v, u', v'} f g } = β
⊢ α = β

Tactic:
cases α
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
β : f ⟶ g
base' :
  Quiver.Hom.{v', u'} (V := X.toBase ⟶ Y.toBase)
    ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase)
    ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) g : X.toBase ⟶ Y.toBase)
H : { base' := base' : Hom.{u, v, u', v'} f g }.base = base β
mk' :
  ∀
    (base'_1 :
      Quiver.Hom.{v', u'} (V := X.toBase ⟶ Y.toBase)
        ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase)
        ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) g : X.toBase ⟶ Y.toBase))
    (H : { base' := base' : Hom.{u, v, u', v'} f g }.base = { base' := base'_1 }.base),
    { base' := base' : Hom.{u, v, u', v'} f g } = { base' := base'_1 }
⊢ { base' := base' : Hom.{u, v, u', v'} f g } = β

Tactic:
cases β
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
base' base'_1 :
  Quiver.Hom.{v', u'} (V := X.toBase ⟶ Y.toBase)
    ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase)
    ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) g : X.toBase ⟶ Y.toBase)
H : { base' := base' : Hom.{u, v, u', v'} f g }.base = { base' := base'_1 }.base
mk' : { base' := base' : Hom.{u, v, u', v'} f g } = { base' := base' }
⊢ { base' := base' : Hom.{u, v, u', v'} f g } = { base' := base'_1 }

Tactic:
cases H
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
base' :
  Quiver.Hom.{v', u'} (V := X.toBase ⟶ Y.toBase)
    ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase)
    ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) g : X.toBase ⟶ Y.toBase)
⊢ { base' := base' : Hom.{u, v, u', v'} f g } = { base' := base' }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
α : f = g
refl :
  Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := X.toBase ⟶ Y.toBase)
      ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase)
      ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase))
    (base (eqToHom ⋯)) (eqToHom ⋯)
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := X.toBase ⟶ Y.toBase)
      ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase)
      ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) g : X.toBase ⟶ Y.toBase))
    (base (eqToHom α)) (eqToHom ⋯)

Tactic:
cases α
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f : X ⟶ Y
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := X.toBase ⟶ Y.toBase)
      ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase)
      ((homEquiv : (a : X ⟶ Y) → X.toBase ⟶ Y.toBase) f : X.toBase ⟶ Y.toBase))
    (base (eqToHom ⋯)) (eqToHom ⋯)

Tactic:
rfl