awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.{v' + 1} (α := f ≫ g ⟶ f ≫ g) (hComp (𝟙 f) (𝟙 g)) (𝟙 (f ≫ g))

Tactic:
simp [hComp, Hom.id_eq]

Premises used: CategoryTheory.CatEnrichedOrdinary.Hom.id_eq, CategoryTheory.CatEnrichedOrdinary.hComp
-- 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 f' : a ⟶ b
α : f = f'
g g' : b ⟶ c
β : g = g'
refl : Eq.{v' + 1} (α := f ≫ g ⟶ f ≫ g') (hComp (eqToHom ⋯) (eqToHom β)) (eqToHom ⋯)
⊢ Eq.{v' + 1} (α := f ≫ g ⟶ f' ≫ g') (hComp (eqToHom α) (eqToHom β)) (eqToHom ⋯)

Tactic:
cases α
-- 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 g' : b ⟶ c
β : g = g'
refl : Eq.{v' + 1} (α := f ≫ g ⟶ f ≫ g) (hComp (eqToHom ⋯) (eqToHom ⋯)) (eqToHom ⋯)
⊢ Eq.{v' + 1} (α := f ≫ g ⟶ f ≫ g') (hComp (eqToHom ⋯) (eqToHom β)) (eqToHom ⋯)

Tactic:
cases β
-- 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.{v' + 1} (α := f ≫ g ⟶ f ≫ g) (hComp (eqToHom ⋯) (eqToHom ⋯)) (eqToHom ⋯)

Tactic:
simp
-- 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₁ f₂ f₃ : a ⟶ b
g₁ g₂ g₃ : b ⟶ c
η : f₁ ⟶ f₂
η' : f₂ ⟶ f₃
θ : g₁ ⟶ g₂
θ' : g₂ ⟶ g₃
⊢ Eq.{v' + 1} (α := f₁ ≫ g₁ ⟶ f₃ ≫ g₃) (hComp η θ ≫ hComp η' θ') (hComp (η ≫ η') (θ ≫ θ'))

Tactic:
simp [hComp, ← CatEnriched.hComp_comp, Hom.comp_eq]

Premises used: CategoryTheory.CatEnrichedOrdinary.Hom.comp_eq, CategoryTheory.CatEnrichedOrdinary.hComp, CategoryTheory.CatEnriched.hComp_comp
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
H :
  Eq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (𝟙 a ≫ f) : a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (𝟙 a ≫ f') : a.toBase ⟶ b.toBase))
    (Hom.base (hComp (𝟙 (𝟙 a)) η)) (Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯))
⊢ Eq (α := 𝟙 a ≫ f ⟶ 𝟙 a ≫ f') (hComp (𝟙 (𝟙 a)) η) (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
H :
  HEq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      (CategoryStruct.comp (Y := a.toBase) ((homEquiv : (a_1 : a ⟶ a) → a.toBase ⟶ a.toBase) (𝟙 a))
          ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f) :
        a.toBase ⟶ b.toBase)
      (CategoryStruct.comp (Y := a.toBase) ((homEquiv : (a_1 : a ⟶ a) → a.toBase ⟶ a.toBase) (𝟙 a))
          ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f') :
        a.toBase ⟶ b.toBase))
    (CatEnriched.hComp (𝟙 ((homEquiv : (a_1 : a ⟶ a) → a.toBase ⟶ a.toBase) (𝟙 a))) (Hom.base η) :
      Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
        (CategoryStruct.comp (Y := a.toBase) ((homEquiv : (a_1 : a ⟶ a) → a.toBase ⟶ a.toBase) (𝟙 a))
            ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f) :
          a.toBase ⟶ b.toBase)
        (CategoryStruct.comp (Y := a.toBase) ((homEquiv : (a_1 : a ⟶ a) → a.toBase ⟶ a.toBase) (𝟙 a))
            ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f') :
          a.toBase ⟶ b.toBase))
    (β :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (𝟙 a ≫ f) : a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (𝟙 a ≫ f') : a.toBase ⟶ b.toBase))
    (Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯))
⊢ Eq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (𝟙 a ≫ f) : a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (𝟙 a ≫ f') : a.toBase ⟶ b.toBase))
    (Hom.base (hComp (𝟙 (𝟙 a)) η)) (Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯))

Tactic:
simp only [hComp, Hom.base_id, base_mk, ← heq_eq_eq, eqToHom_comp_heq_iff, comp_eqToHom_heq_iff]

Premises used: heq_eq_eq, CategoryTheory.eqToHom_comp_heq_iff, CategoryTheory.comp_eqToHom_heq_iff, CategoryTheory.CatEnrichedOrdinary.base_mk, CategoryTheory.CatEnrichedOrdinary.hComp, CategoryTheory.CatEnrichedOrdinary.Hom.base_id
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
H :
  HEq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase) (𝟙 a.toBase ≫ (homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f)
      (𝟙 a.toBase ≫ (homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f'))
    (CatEnriched.hComp (𝟙 (𝟙 a.toBase)) (Hom.base η)) (β :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (𝟙 a ≫ f) : a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (𝟙 a ≫ f') : a.toBase ⟶ b.toBase))
    (Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯))
⊢ HEq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      (CategoryStruct.comp (Y := a.toBase) ((homEquiv : (a_1 : a ⟶ a) → a.toBase ⟶ a.toBase) (𝟙 a))
          ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f) :
        a.toBase ⟶ b.toBase)
      (CategoryStruct.comp (Y := a.toBase) ((homEquiv : (a_1 : a ⟶ a) → a.toBase ⟶ a.toBase) (𝟙 a))
          ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f') :
        a.toBase ⟶ b.toBase))
    (CatEnriched.hComp (𝟙 ((homEquiv : (a_1 : a ⟶ a) → a.toBase ⟶ a.toBase) (𝟙 a))) (Hom.base η) :
      Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
        (CategoryStruct.comp (Y := a.toBase) ((homEquiv : (a_1 : a ⟶ a) → a.toBase ⟶ a.toBase) (𝟙 a))
            ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f) :
          a.toBase ⟶ b.toBase)
        (CategoryStruct.comp (Y := a.toBase) ((homEquiv : (a_1 : a ⟶ a) → a.toBase ⟶ a.toBase) (𝟙 a))
            ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f') :
          a.toBase ⟶ b.toBase))
    (β :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (𝟙 a ≫ f) : a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (𝟙 a ≫ f') : a.toBase ⟶ b.toBase))
    (Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯))

Tactic:
rw [homEquiv_id]

Premises used: CategoryTheory.CatEnrichedOrdinary.homEquiv_id
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ HEq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase) (𝟙 a.toBase ≫ (homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f)
      (𝟙 a.toBase ≫ (homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f'))
    (CatEnriched.hComp (𝟙 (𝟙 a.toBase)) (Hom.base η)) (β :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (𝟙 a ≫ f) : a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (𝟙 a ≫ f') : a.toBase ⟶ b.toBase))
    (Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯))

Tactic:
simp [CatEnriched.id_hComp_heq]

Premises used: CategoryTheory.CatEnriched.id_hComp_heq
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ HEq (α := 𝟙 a ≫ f ⟶ 𝟙 a ≫ f') (hComp (𝟙 (𝟙 a)) η) η

Tactic:
simp [id_hComp]

Premises used: CategoryTheory.CatEnrichedOrdinary.id_hComp
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
H :
  Eq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (f ≫ 𝟙 b) : a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (f' ≫ 𝟙 b) : a.toBase ⟶ b.toBase))
    (Hom.base (hComp η (𝟙 (𝟙 b)))) (Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯))
⊢ Eq (α := f ≫ 𝟙 b ⟶ f' ≫ 𝟙 b) (hComp η (𝟙 (𝟙 b))) (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
H :
  HEq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f)
          ((homEquiv : (a : b ⟶ b) → b.toBase ⟶ b.toBase) (𝟙 b)) :
        a.toBase ⟶ b.toBase)
      (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f')
          ((homEquiv : (a : b ⟶ b) → b.toBase ⟶ b.toBase) (𝟙 b)) :
        a.toBase ⟶ b.toBase))
    (CatEnriched.hComp (Hom.base η) (𝟙 ((homEquiv : (a : b ⟶ b) → b.toBase ⟶ b.toBase) (𝟙 b)))) (β :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (f ≫ 𝟙 b) : a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (f' ≫ 𝟙 b) : a.toBase ⟶ b.toBase))
    (Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯))
⊢ Eq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (f ≫ 𝟙 b) : a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (f' ≫ 𝟙 b) : a.toBase ⟶ b.toBase))
    (Hom.base (hComp η (𝟙 (𝟙 b)))) (Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯))

Tactic:
simp only [hComp, Hom.base_id, base_mk, ← heq_eq_eq, eqToHom_comp_heq_iff, comp_eqToHom_heq_iff]

Premises used: heq_eq_eq, CategoryTheory.eqToHom_comp_heq_iff, CategoryTheory.comp_eqToHom_heq_iff, CategoryTheory.CatEnrichedOrdinary.base_mk, CategoryTheory.CatEnrichedOrdinary.hComp, CategoryTheory.CatEnrichedOrdinary.Hom.base_id
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
H :
  HEq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f ≫ 𝟙 b.toBase : a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f' ≫ 𝟙 b.toBase : a.toBase ⟶ b.toBase))
    (CatEnriched.hComp (Hom.base η) (𝟙 (𝟙 b.toBase))) (β :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (f ≫ 𝟙 b) : a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (f' ≫ 𝟙 b) : a.toBase ⟶ b.toBase))
    (Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯))
⊢ HEq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f)
          ((homEquiv : (a : b ⟶ b) → b.toBase ⟶ b.toBase) (𝟙 b)) :
        a.toBase ⟶ b.toBase)
      (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f')
          ((homEquiv : (a : b ⟶ b) → b.toBase ⟶ b.toBase) (𝟙 b)) :
        a.toBase ⟶ b.toBase))
    (CatEnriched.hComp (Hom.base η) (𝟙 ((homEquiv : (a : b ⟶ b) → b.toBase ⟶ b.toBase) (𝟙 b)))) (β :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (f ≫ 𝟙 b) : a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (f' ≫ 𝟙 b) : a.toBase ⟶ b.toBase))
    (Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯))

Tactic:
rw [homEquiv_id]

Premises used: CategoryTheory.CatEnrichedOrdinary.homEquiv_id
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ HEq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f ≫ 𝟙 b.toBase : a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f' ≫ 𝟙 b.toBase : a.toBase ⟶ b.toBase))
    (CatEnriched.hComp (Hom.base η) (𝟙 (𝟙 b.toBase))) (β :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (f ≫ 𝟙 b) : a.toBase ⟶ b.toBase)
      ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) (f' ≫ 𝟙 b) : a.toBase ⟶ b.toBase))
    (Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯))

Tactic:
simp [CatEnriched.hComp_id_heq]

Premises used: CategoryTheory.CatEnriched.hComp_id_heq
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ HEq (α := f ≫ 𝟙 b ⟶ f' ≫ 𝟙 b) (hComp η (𝟙 (𝟙 b))) η

Tactic:
simp [hComp_id]

Premises used: CategoryTheory.CatEnrichedOrdinary.hComp_id
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := X ⟶ X) (𝟙 X) (eqToHom ⋯)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
H : Hom.base (hComp (hComp η θ) κ) = Hom.base (eqToHom ⋯ ≫ hComp η (hComp θ κ) ≫ eqToHom ⋯)
⊢ hComp (hComp η θ) κ = eqToHom ⋯ ≫ hComp η (hComp θ κ) ≫ eqToHom ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
H :
  CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
⊢ Hom.base (hComp (hComp η θ) κ) = Hom.base (eqToHom ⋯ ≫ hComp η (hComp θ κ) ≫ eqToHom ⋯)

Tactic:
simp only [hComp, base_mk, Hom.base_comp, Hom.base_eqToHom,
    ← heq_eq_eq, heq_eqToHom_comp_iff, heq_comp_eqToHom_iff,
    eqToHom_comp_heq_iff, comp_eqToHom_heq_iff]

Premises used: heq_eq_eq, CategoryTheory.heq_comp_eqToHom_iff, CategoryTheory.eqToHom_comp_heq_iff, CategoryTheory.comp_eqToHom_heq_iff, CategoryTheory.CatEnrichedOrdinary.Hom.base_comp, CategoryTheory.CatEnrichedOrdinary.base_mk, CategoryTheory.CatEnrichedOrdinary.hComp, CategoryTheory.CatEnrichedOrdinary.Hom.base_eqToHom, CategoryTheory.heq_eqToHom_comp_iff
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
enter : Hom.base κ
| CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
enter [1, 2]
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ Hom.base κ =
    𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h) ≫
      Hom.base κ ≫ 𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h')

Tactic:
((id_comp _).trans (comp_id _)).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm, Eq.trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
enter : CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ)
enter₁ enter₂ : Hom.base κ
| CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
enter [1, 2]; exact ((id_comp _).trans (comp_id _)).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm, Eq.trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
H :
  HEq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := c.toBase) ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f ≫ g))
          ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h) :
        a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := c.toBase) ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f' ≫ g'))
          ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h') :
        a.toBase ⟶ d.toBase))
    (CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯)
      (𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h) ≫
        Hom.base κ ≫ 𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h')))
    (CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯))
⊢ CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
conv => enter [1, 2]; exact ((id_comp _).trans (comp_id _)).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm, Eq.trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
enter : Hom.base η
| HEq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := c.toBase) ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f ≫ g))
          ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h) :
        a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := c.toBase) ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f' ≫ g'))
          ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h') :
        a.toBase ⟶ d.toBase))
    (CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯)
      (𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h) ≫
        Hom.base κ ≫ 𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h')))
    (CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯))

Tactic:
enter [2, 1]
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ Hom.base η =
    𝟙 ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f) ≫
      Hom.base η ≫ 𝟙 ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f')

Tactic:
((id_comp _).trans (comp_id _)).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm, Eq.trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
enter : CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
enter₁ enter₂ : Hom.base η
| HEq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := c.toBase) ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f ≫ g))
          ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h) :
        a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := c.toBase) ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f' ≫ g'))
          ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h') :
        a.toBase ⟶ d.toBase))
    (CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯)
      (𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h) ≫
        Hom.base κ ≫ 𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h')))
    (CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯))

Tactic:
enter [2, 1]; exact ((id_comp _).trans (comp_id _)).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm, Eq.trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
H :
  HEq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := c.toBase) ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f ≫ g))
          ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h) :
        a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := c.toBase) ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f' ≫ g'))
          ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h') :
        a.toBase ⟶ d.toBase))
    (CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯)
      (𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h) ≫
        Hom.base κ ≫ 𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h')))
    (β :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f)
          ((homEquiv : (a : b ⟶ d) → b.toBase ⟶ d.toBase) (g ≫ h)) :
        a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f')
          ((homEquiv : (a : b ⟶ d) → b.toBase ⟶ d.toBase) (g' ≫ h')) :
        a.toBase ⟶ d.toBase))
    (CatEnriched.hComp
        (𝟙 ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f) ≫
          Hom.base η ≫ 𝟙 ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f'))
        (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯) :
      Quiver.Hom.{v', u'} (V := a.toBase ⟶ d.toBase)
        (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f)
            ((homEquiv : (a : b ⟶ d) → b.toBase ⟶ d.toBase) (g ≫ h)) :
          a.toBase ⟶ d.toBase)
        (CategoryStruct.comp (Y := b.toBase) ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f')
            ((homEquiv : (a : b ⟶ d) → b.toBase ⟶ d.toBase) (g' ≫ h')) :
          a.toBase ⟶ d.toBase))
⊢ HEq (α :=
    Quiver.Hom.{v', u'} (V := a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := c.toBase) ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f ≫ g))
          ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h) :
        a.toBase ⟶ d.toBase)
      (CategoryStruct.comp (Y := c.toBase) ((homEquiv : (a_1 : a ⟶ c) → a.toBase ⟶ c.toBase) (f' ≫ g'))
          ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h') :
        a.toBase ⟶ d.toBase))
    (CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯)
      (𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h) ≫
        Hom.base κ ≫ 𝟙 ((homEquiv : (a : c ⟶ d) → c.toBase ⟶ d.toBase) h')))
    (CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯))

Tactic:
conv => enter [2, 1]; exact ((id_comp _).trans (comp_id _)).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm, Eq.trans, CategoryTheory.Category.id_comp