awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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 β
⊢ α = β
have 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 α
Cleared hypotheses: α, H
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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 β
⊢ { base' := base' : Hom.{u, v, u', v'} f g } = β
have 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 }
Tactic: cases β
Cleared hypotheses: β, H
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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
⊢ { base' := base' : Hom.{u, v, u', v'} f g } = { base' := base'_1 }
have mk' : { base' := base' : Hom.{u, v, u', v'} f g } = { base' := base' }
Tactic: cases H
Cleared hypotheses: base'_1, H
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
α : f = g
⊢ 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 ⋯)
have 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 sorry)) (eqToHom sorry)
Tactic: cases α
Cleared hypotheses: g, α
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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'
⊢ Eq.{v' + 1} (α := f ≫ g ⟶ f' ≫ g') (hComp (eqToHom α) (eqToHom β)) (eqToHom ⋯)
have refl : Eq.{v' + 1} (α := f ≫ g ⟶ f ≫ g') (hComp (eqToHom sorry) (eqToHom β)) (eqToHom sorry)
Tactic: cases α
Cleared hypotheses: f', α
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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'
⊢ Eq.{v' + 1} (α := f ≫ g ⟶ f ≫ g') (hComp (eqToHom ⋯) (eqToHom β)) (eqToHom ⋯)
have refl : Eq.{v' + 1} (α := f ≫ g ⟶ f ≫ g) (hComp (eqToHom sorry) (eqToHom sorry)) (eqToHom sorry)
Tactic: cases β
Cleared hypotheses: g', β
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ Eq (α := 𝟙 a ≫ f ⟶ 𝟙 a ≫ f') (hComp (𝟙 (𝟙 a)) η) (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)
have 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 sorry ≫ η ≫ eqToHom sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ 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 ⋯))
have 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 sorry ≫ η ≫ eqToHom sorry))
Tactic: simp only [hComp, Hom.base_id, base_mk, ← heq_eq_eq, eqToHom_comp_heq_iff, comp_eqToHom_heq_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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.{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 ⋯))
have 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 sorry ≫ η ≫ eqToHom sorry))
Tactic: rw [homEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ Eq (α := f ≫ 𝟙 b ⟶ f' ≫ 𝟙 b) (hComp η (𝟙 (𝟙 b))) (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)
have 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 sorry ≫ η ≫ eqToHom sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ 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 ⋯))
have 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 sorry ≫ η ≫ eqToHom sorry))
Tactic: simp only [hComp, Hom.base_id, base_mk, ← heq_eq_eq, eqToHom_comp_heq_iff, comp_eqToHom_heq_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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)
      (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 ⋯))
have 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 sorry ≫ η ≫ eqToHom sorry))
Tactic: rw [homEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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'
⊢ hComp (hComp η θ) κ = eqToHom ⋯ ≫ hComp η (hComp θ κ) ≫ eqToHom ⋯
have H : Hom.base (hComp (hComp η θ) κ) = Hom.base (eqToHom sorry ≫ hComp η (hComp θ κ) ≫ eqToHom sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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 (hComp (hComp η θ) κ) = Hom.base (eqToHom ⋯ ≫ hComp η (hComp θ κ) ≫ eqToHom ⋯)
have H : CatEnriched.hComp (eqToHom sorry ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom sorry) (Hom.base κ) ≍
  CatEnriched.hComp (Hom.base η) (eqToHom sorry ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom sorry)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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'
| CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
have enter : Hom.base κ
Tactic: enter [1, 2]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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'
| CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
have enter : CatEnriched.hComp (eqToHom sorry ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom sorry) (Hom.base κ)
Tactic: enter [1, 2]; exact ((id_comp _).trans (comp_id _)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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 κ)
| CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
have enter₁ : Hom.base κ
Tactic: enter [1, 2]; exact ((id_comp _).trans (comp_id _)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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'
⊢ CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
have 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 sorry ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom sorry)
    (𝟙 ((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 sorry ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom sorry))
Tactic: conv => enter [1, 2]; exact ((id_comp _).trans (comp_id _)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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'
| 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 ⋯))
have enter : Hom.base η
Tactic: enter [2, 1]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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'
| 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 ⋯))
have enter : CatEnriched.hComp (Hom.base η) (eqToHom sorry ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom sorry)
Tactic: enter [2, 1]; exact ((id_comp _).trans (comp_id _)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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 ⋯)
| 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 ⋯))
have enter₁ : Hom.base η
Tactic: enter [2, 1]; exact ((id_comp _).trans (comp_id _)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.CatEnriched (goal)
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'
⊢ 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 ⋯))
have 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 sorry ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom sorry)
    (𝟙 ((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 sorry ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom sorry) :
    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))
Tactic: conv => enter [2, 1]; exact ((id_comp _).trans (comp_id _)).symm