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 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))
    (eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (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))
    (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (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))
    (eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (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))
    (eqToHom ⋯ ≫
      CatEnriched.hComp (Hom.base η ≫ 𝟙 ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f'))
        (CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯))

Tactic:
rw [← CatEnriched.hComp_comp, id_eq_eqToHom, CatEnriched.eqToHom_hComp_eqToHom]

Premises used: CategoryTheory.CatEnrichedOrdinary.id_eq_eqToHom, CategoryTheory.CatEnriched.eqToHom_hComp_eqToHom, 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 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))
    (eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (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))
    (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (CatEnriched.hComp (Hom.base θ) (Hom.base κ)) ≫ eqToHom ⋯)

Tactic:
simp [CatEnriched.hComp_assoc_heq]

Premises used: CategoryTheory.CatEnriched.hComp_assoc_heq
-- 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'
⊢ hComp (hComp η θ) κ ≍ hComp η (hComp θ κ)

Tactic:
simp [hComp_assoc]

Premises used: CategoryTheory.CatEnrichedOrdinary.hComp_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b : CatEnrichedOrdinary C} {f g : a ⟶ b} (η : f ⟶ g),
    hComp (𝟙 (𝟙 a)) η = Iso.hom (eqToIso ⋯) ≫ η ≫ Iso.inv (eqToIso ⋯)

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 c d : CatEnrichedOrdinary C} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
    Eq (α := (f ≫ g) ≫ h ⟶ (f ≫ g) ≫ h') (hComp (𝟙 (f ≫ g)) η)
      (Iso.hom (eqToIso ⋯) ≫ hComp (𝟙 f) (hComp (𝟙 g) η) ≫ Iso.inv (eqToIso ⋯))

Tactic:
simp [← hComp_assoc]

Premises used: CategoryTheory.CatEnrichedOrdinary.hComp_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b : CatEnrichedOrdinary C} {f g : a ⟶ b} (η : f ⟶ g),
    hComp η (𝟙 (𝟙 b)) = Iso.hom (eqToIso ⋯) ≫ η ≫ Iso.inv (eqToIso ⋯)

Tactic:
simp [hComp_id]

Premises used: CategoryTheory.CatEnrichedOrdinary.hComp_id
-- 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} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
    Eq (α := f ≫ g ≫ h ⟶ f' ≫ g ≫ h) (hComp η (𝟙 (g ≫ h)))
      (Iso.inv (eqToIso ⋯) ≫ hComp (hComp η (𝟙 g)) (𝟙 h) ≫ Iso.hom (eqToIso ⋯))

Tactic:
simp [hComp_assoc]

Premises used: CategoryTheory.CatEnrichedOrdinary.hComp_assoc
-- 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 : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
    Eq (α := (f ≫ g) ≫ h ⟶ (f ≫ g') ≫ h) (hComp (hComp (𝟙 f) η) (𝟙 h))
      (Iso.hom (eqToIso ⋯) ≫ hComp (𝟙 f) (hComp η (𝟙 h)) ≫ Iso.inv (eqToIso ⋯))

Tactic:
simp [hComp_assoc]

Premises used: CategoryTheory.CatEnrichedOrdinary.hComp_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.CatEnriched
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b c d e : CatEnrichedOrdinary C} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
    Eq.{v' + 1} (α := ((f ≫ g) ≫ h) ≫ i ⟶ f ≫ g ≫ h ≫ i)
      (hComp (Iso.hom (eqToIso ⋯)) (𝟙 i) ≫ Iso.hom (eqToIso ⋯) ≫ hComp (𝟙 f) (Iso.hom (eqToIso ⋯)))
      (Iso.hom (eqToIso ⋯) ≫ Iso.hom (eqToIso ⋯))

Tactic:
simp [id_eq_eqToHom, -eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.CatEnrichedOrdinary.id_eq_eqToHom
-- 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 ≫ 𝟙 b) ≫ g ⟶ f ≫ g) (Iso.hom (eqToIso ⋯) ≫ hComp (𝟙 f) (Iso.hom (eqToIso ⋯)))
      (hComp (Iso.hom (eqToIso ⋯)) (𝟙 g))

Tactic:
simp [id_eq_eqToHom, -eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.CatEnrichedOrdinary.id_eq_eqToHom
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a : B
⊢ Prefunctor.obj (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
      { as := a : LocallyDiscrete (Paths B) } =
    a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : B
f g : Discrete (Path.{v, u} a b)
η : f ⟶ g
⊢ Eq (α :=
    Quiver.Hom (V :=
      Prefunctor.obj (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
          { as := a : LocallyDiscrete (Paths B) } ⟶
        Prefunctor.obj (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
          { as := b : LocallyDiscrete (Paths B) })
      (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) f)
      (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) g))
    (PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) η) (eqToHom ⋯)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
p : Path.{v, u} a b
f g : Hom.{v, u} b c
η : f ⟶ g
mk : ∀ (η' : Hom₂ f g), normalizeAux p f = normalizeAux p g
⊢ normalizeAux p f = normalizeAux p g

Tactic:
rcases η with ⟨η'⟩
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
p : Path.{v, u} a b
f g : Hom.{v, u} b c
η : f ⟶ g
η' : Hom₂ f g
mk :
  Eq (α := (x : Path.{v, u} a b) → Path.{v, u} a c) (fun (p : Path.{v, u} a b) ↦ normalizeAux p f)
    fun (p : Path.{v, u} a b) ↦ normalizeAux p g
⊢ normalizeAux p f = normalizeAux p g

Tactic:
apply @congr_fun _ _ fun p => normalizeAux p f

Premises used: congr_fun
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 g_1 h : a_1 ⟶ b_1
η : Hom₂ f_1 g_1
θ : Hom₂ g_1 h
η_ih :
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g_1
θ_ih :
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h
mk :
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g_1
mk₁ :
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h
mk₂ : (x : Path.{v, u} a a_1) → Path.{v, u} a b_1
⊢ Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h

Tactic:
apply Eq.trans

Premises used: Eq.trans
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 g_1 h : a_1 ⟶ b_1
η : Hom₂ f_1 g_1
θ : Hom₂ g_1 h
η_ih :
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g_1
θ_ih :
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h
⊢ Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g_1

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 g_1 h : a_1 ⟶ b_1
η : Hom₂ f_1 g_1
θ : Hom₂ g_1 h
η_ih :
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g_1
θ_ih :
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h
⊢ Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 c_1 : FreeBicategory B
f_1 : a_1 ⟶ b_1
g_1 h : b_1 ⟶ c_1
η : Hom₂ g_1 h
ih :
  Eq (α := (x : Path.{v, u} a b_1) → Path.{v, u} a c_1) (fun (p : Path.{v, u} a b_1) ↦ normalizeAux p g_1)
    fun (p : Path.{v, u} a b_1) ↦ normalizeAux p h
mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x (f_1 ≫ g_1) = normalizeAux x (f_1 ≫ h)
⊢ Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a c_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f_1 ≫ g_1))
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f_1 ≫ h)

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 c_1 : FreeBicategory B
f_1 : a_1 ⟶ b_1
g_1 h : b_1 ⟶ c_1
η : Hom₂ g_1 h
ih :
  Eq (α := (x : Path.{v, u} a b_1) → Path.{v, u} a c_1) (fun (p : Path.{v, u} a b_1) ↦ normalizeAux p g_1)
    fun (p : Path.{v, u} a b_1) ↦ normalizeAux p h
x : Path.{v, u} a a_1
⊢ normalizeAux x (f_1 ≫ g_1) = normalizeAux x (f_1 ≫ h)

Tactic:
apply congr_fun ih

Premises used: congr_fun
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 c_1 : FreeBicategory B
f_1 g_1 : a_1 ⟶ b_1
h : b_1 ⟶ c_1
η : Hom₂ f_1 g_1
ih :
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g_1
mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x (Hom.comp f_1 h) = normalizeAux x (Hom.comp g_1 h)
⊢ Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a c_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (Hom.comp f_1 h))
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (Hom.comp g_1 h)

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 c_1 : FreeBicategory B
f_1 g_1 : a_1 ⟶ b_1
h : b_1 ⟶ c_1
η : Hom₂ f_1 g_1
ih :
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g_1
x : Path.{v, u} a a_1
⊢ normalizeAux x (Hom.comp f_1 h) = normalizeAux x (Hom.comp g_1 h)

Tactic:
apply congr_arg₂ _ (congr_fun ih _) rfl

Premises used: congr_fun, rfl, congr_arg₂
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 : a_1 ⟶ b_1
mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x f_1 = normalizeAux x f_1
⊢ Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f_1

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 : a_1 ⟶ b_1
x : Path.{v, u} a a_1
⊢ normalizeAux x f_1 = normalizeAux x f_1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 c_1 d : FreeBicategory B
f_1 : a_1 ⟶ b_1
g_1 : b_1 ⟶ c_1
h : c_1 ⟶ d
mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x ((f_1 ≫ g_1) ≫ h) = normalizeAux x (f_1 ≫ g_1 ≫ h)
⊢ Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a d) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p ((f_1 ≫ g_1) ≫ h))
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f_1 ≫ g_1 ≫ h)

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 c_1 d : FreeBicategory B
f_1 : a_1 ⟶ b_1
g_1 : b_1 ⟶ c_1
h : c_1 ⟶ d
x : Path.{v, u} a a_1
⊢ normalizeAux x ((f_1 ≫ g_1) ≫ h) = normalizeAux x (f_1 ≫ g_1 ≫ h)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 c_1 d : FreeBicategory B
f_1 : a_1 ⟶ b_1
g_1 : b_1 ⟶ c_1
h : c_1 ⟶ d
mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x (f_1 ≫ g_1 ≫ h) = normalizeAux x ((f_1 ≫ g_1) ≫ h)
⊢ Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a d) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f_1 ≫ g_1 ≫ h))
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p ((f_1 ≫ g_1) ≫ h)

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 c_1 d : FreeBicategory B
f_1 : a_1 ⟶ b_1
g_1 : b_1 ⟶ c_1
h : c_1 ⟶ d
x : Path.{v, u} a a_1
⊢ normalizeAux x (f_1 ≫ g_1 ≫ h) = normalizeAux x ((f_1 ≫ g_1) ≫ h)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 : a_1 ⟶ b_1
mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x (f_1 ≫ 𝟙 b_1) = normalizeAux x f_1
⊢ Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f_1 ≫ 𝟙 b_1))
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f_1

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 : a_1 ⟶ b_1
x : Path.{v, u} a a_1
⊢ normalizeAux x (f_1 ≫ 𝟙 b_1) = normalizeAux x f_1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 : a_1 ⟶ b_1
mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x f_1 = normalizeAux x (f_1 ≫ 𝟙 b_1)
⊢ Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f_1 ≫ 𝟙 b_1)

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 : a_1 ⟶ b_1
x : Path.{v, u} a a_1
⊢ normalizeAux x f_1 = normalizeAux x (f_1 ≫ 𝟙 b_1)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 : a_1 ⟶ b_1
mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x (𝟙 a_1 ≫ f_1) = normalizeAux x f_1
⊢ Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (𝟙 a_1 ≫ f_1))
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f_1

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 : a_1 ⟶ b_1
x : Path.{v, u} a a_1
⊢ normalizeAux x (𝟙 a_1 ≫ f_1) = normalizeAux x f_1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 : a_1 ⟶ b_1
mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x f_1 = normalizeAux x (𝟙 a_1 ≫ f_1)
⊢ Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b_1) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f_1)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (𝟙 a_1 ≫ f_1)

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 : a_1 ⟶ b_1
x : Path.{v, u} a a_1
⊢ normalizeAux x f_1 = normalizeAux x (𝟙 a_1 ≫ f_1)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
p : Path.{v, u} a b
f g : Hom.{v, u} b c
η : f ⟶ g
mk :
  ∀ (η' : Hom₂ f g),
    Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ◁
          Quot.mk Rel η' ≫
        (normalizeIso p g).hom =
      (normalizeIso p f).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
⊢ Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) { as := p } ◁
        η ≫
      (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫ PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)

Tactic:
rcases η with ⟨η'⟩
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 : a_1 ⟶ b_1
p : Path.{v, u} a a_1
⊢ Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) { as := p } ◁
        Quot.mk Rel (Hom₂.id f_1) ≫
      (normalizeIso p f_1).hom =
    (normalizeIso p f_1).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 g_1 h : a_1 ⟶ b_1
η : Hom₂ f_1 g_1
θ : Hom₂ g_1 h
ihf :
  ∀ (p : Path.{v, u} a a_1),
    Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ◁
          Quot.mk Rel η ≫
        (normalizeIso p g_1).hom =
      (normalizeIso p f_1).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
ihg :
  ∀ (p : Path.{v, u} a a_1),
    Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ◁
          Quot.mk Rel θ ≫
        (normalizeIso p h).hom =
      (normalizeIso p g_1).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
p : Path.{v, u} a a_1
mk :
  CategoryStruct.comp (Y :=
        Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ≫
          g_1)
        (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ◁
          η.mk)
        (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ◁
          θ.mk) ≫
      (normalizeIso p h).hom =
    (normalizeIso p f_1).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
⊢ Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) { as := p } ◁
        Quot.mk Rel (η.vcomp θ) ≫
      (normalizeIso p h).hom =
    (normalizeIso p f_1).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)

Tactic:
simp only [mk_vcomp, whiskerLeft_comp]

Premises used: CategoryTheory.Bicategory.whiskerLeft_comp, CategoryTheory.FreeBicategory.mk_vcomp
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 : FreeBicategory B
f_1 g_1 h : a_1 ⟶ b_1
η : Hom₂ f_1 g_1
θ : Hom₂ g_1 h
ihf :
  ∀ (p : Path.{v, u} a a_1),
    Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ◁
          Quot.mk Rel η ≫
        (normalizeIso p g_1).hom =
      (normalizeIso p f_1).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
ihg :
  ∀ (p : Path.{v, u} a a_1),
    Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ◁
          Quot.mk Rel θ ≫
        (normalizeIso p h).hom =
      (normalizeIso p g_1).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
p : Path.{v, u} a a_1
a₁ :
  (normalizeIso p g_1).hom ≫ PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
| Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) { as := p } ◁
      θ.mk ≫
    (normalizeIso p h).hom

Tactic:
rw [ihg]