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
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 η ≫ 𝟙 ((homEquiv : (a_1 : a ⟶ b) → a.toBase ⟶ b.toBase) f'))
        (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))
  (eqToHom sorry ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (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))
  (eqToHom sorry ≫ CatEnriched.hComp (Hom.base η) (CatEnriched.hComp (Hom.base θ) (Hom.base κ)) ≫ eqToHom sorry)
Tactic: rw [← CatEnriched.hComp_comp, id_eq_eqToHom, CatEnriched.eqToHom_hComp_eqToHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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
⊢ normalizeAux p f = normalizeAux p g
have mk : ∀ (η' : Hom₂ f g), normalizeAux p f = normalizeAux p g
Tactic: rcases η with ⟨η'⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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
⊢ normalizeAux p f = normalizeAux p g
have 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
Tactic: apply @congr_fun _ _ fun p => normalizeAux p f
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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
⊢ 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
have mk₂ : (x : Path.{v, u} a a_1) → Path.{v, u} a b_1
Tactic: apply Eq.trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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
⊢ 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)
have mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x (f_1 ≫ g_1) = normalizeAux x (f_1 ≫ h)
Tactic: funext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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
⊢ 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)
have mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x (Hom.comp f_1 h) = normalizeAux x (Hom.comp g_1 h)
Tactic: funext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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
⊢ 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
have mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x f_1 = normalizeAux x f_1
Tactic: funext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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
⊢ 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)
have mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x ((f_1 ≫ g_1) ≫ h) = normalizeAux x (f_1 ≫ g_1 ≫ h)
Tactic: funext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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
⊢ 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)
have mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x (f_1 ≫ g_1 ≫ h) = normalizeAux x ((f_1 ≫ g_1) ≫ h)
Tactic: funext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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
⊢ 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
have mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x (f_1 ≫ 𝟙 b_1) = normalizeAux x f_1
Tactic: funext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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
⊢ 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)
have mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x f_1 = normalizeAux x (f_1 ≫ 𝟙 b_1)
Tactic: funext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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
⊢ 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
have mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x (𝟙 a_1 ≫ f_1) = normalizeAux x f_1
Tactic: funext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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
⊢ 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)
have mk : ∀ (x : Path.{v, u} a a_1), normalizeAux x f_1 = normalizeAux x (𝟙 a_1 ≫ f_1)
Tactic: funext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
η' : Hom₂ f g
⊢ 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
have mk : ∀ {a_1 b : FreeBicategory B} {f g h : a_1 ⟶ b} (η : Hom₂ f g) (θ : Hom₂ g h),
  (Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g) →
    (Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g)
        fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h) →
      Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
        fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h
Tactic: induction η' with
  | vcomp _ _ _ _ => apply Eq.trans <;> assumption
  | whisker_left _ _ ih => funext; apply congr_fun ih
  | whisker_right _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih _) rfl
  | _ => funext; rfl
Cleared hypotheses: η'
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
η' : Hom₂ f g
mk :
  ∀ {a_1 b : FreeBicategory B} {f g h : a_1 ⟶ b} (η : Hom₂ f g) (θ : Hom₂ g h),
    (Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
        fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g) →
      (Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g)
          fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h) →
        Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
          fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h
⊢ 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
have mk₁ : ∀ {a_1 b c : FreeBicategory B} (f : a_1 ⟶ b) {g h : b ⟶ c} (η : Hom₂ g h)
  (ih :
    Eq (α := (x : Path.{v, u} a b) → Path.{v, u} a c) (fun (p : Path.{v, u} a b) ↦ normalizeAux p g)
      fun (p : Path.{v, u} a b) ↦ normalizeAux p h),
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a c) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ g))
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ h)
Tactic: induction η' with
  | vcomp _ _ _ _ => apply Eq.trans <;> assumption
  | whisker_left _ _ ih => funext; apply congr_fun ih
  | whisker_right _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih _) rfl
  | _ => funext; rfl
Cleared hypotheses: η'
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
η' : Hom₂ f g
mk :
  ∀ {a_1 b : FreeBicategory B} {f g h : a_1 ⟶ b} (η : Hom₂ f g) (θ : Hom₂ g h),
    (Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
        fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g) →
      (Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g)
          fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h) →
        Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
          fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h
mk₁ :
  ∀ {a_1 b c : FreeBicategory B} (f : a_1 ⟶ b) {g h : b ⟶ c} (η : Hom₂ g h)
    (ih :
      Eq (α := (x : Path.{v, u} a b) → Path.{v, u} a c) (fun (p : Path.{v, u} a b) ↦ normalizeAux p g)
        fun (p : Path.{v, u} a b) ↦ normalizeAux p h),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a c) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ g))
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ h)
⊢ 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
have mk₂ : ∀ {a_1 b c : FreeBicategory B} {f g : a_1 ⟶ b} (h : b ⟶ c) (η : Hom₂ f g)
  (ih :
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g),
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a c) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (Hom.comp f h))
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (Hom.comp g h)
Tactic: induction η' with
  | vcomp _ _ _ _ => apply Eq.trans <;> assumption
  | whisker_left _ _ ih => funext; apply congr_fun ih
  | whisker_right _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih _) rfl
  | _ => funext; rfl
Cleared hypotheses: η'
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
η' : Hom₂ f g
mk :
  ∀ {a_1 b : FreeBicategory B} {f g h : a_1 ⟶ b} (η : Hom₂ f g) (θ : Hom₂ g h),
    (Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
        fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g) →
      (Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g)
          fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h) →
        Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
          fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h
mk₁ :
  ∀ {a_1 b c : FreeBicategory B} (f : a_1 ⟶ b) {g h : b ⟶ c} (η : Hom₂ g h)
    (ih :
      Eq (α := (x : Path.{v, u} a b) → Path.{v, u} a c) (fun (p : Path.{v, u} a b) ↦ normalizeAux p g)
        fun (p : Path.{v, u} a b) ↦ normalizeAux p h),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a c) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ g))
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ h)
mk₂ :
  ∀ {a_1 b c : FreeBicategory B} {f g : a_1 ⟶ b} (h : b ⟶ c) (η : Hom₂ f g)
    (ih :
      Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
        fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a c) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (Hom.comp f h))
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (Hom.comp g h)
⊢ 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
have mk₃ : ∀ {a_1 b : FreeBicategory B} (f : a_1 ⟶ b),
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f
Tactic: induction η' with
  | vcomp _ _ _ _ => apply Eq.trans <;> assumption
  | whisker_left _ _ ih => funext; apply congr_fun ih
  | whisker_right _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih _) rfl
  | _ => funext; rfl
Cleared hypotheses: η'
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
η' : Hom₂ f g
mk :
  ∀ {a_1 b : FreeBicategory B} {f g h : a_1 ⟶ b} (η : Hom₂ f g) (θ : Hom₂ g h),
    (Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
        fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g) →
      (Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g)
          fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h) →
        Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
          fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h
mk₁ :
  ∀ {a_1 b c : FreeBicategory B} (f : a_1 ⟶ b) {g h : b ⟶ c} (η : Hom₂ g h)
    (ih :
      Eq (α := (x : Path.{v, u} a b) → Path.{v, u} a c) (fun (p : Path.{v, u} a b) ↦ normalizeAux p g)
        fun (p : Path.{v, u} a b) ↦ normalizeAux p h),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a c) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ g))
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ h)
mk₂ :
  ∀ {a_1 b c : FreeBicategory B} {f g : a_1 ⟶ b} (h : b ⟶ c) (η : Hom₂ f g)
    (ih :
      Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
        fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a c) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (Hom.comp f h))
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (Hom.comp g h)
mk₃ :
  ∀ {a_1 b : FreeBicategory B} (f : a_1 ⟶ b),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f
⊢ 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
have mk₄ : ∀ {a_1 b c d : FreeBicategory B} (f : a_1 ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a d) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p ((f ≫ g) ≫ h))
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ g ≫ h)
Tactic: induction η' with
  | vcomp _ _ _ _ => apply Eq.trans <;> assumption
  | whisker_left _ _ ih => funext; apply congr_fun ih
  | whisker_right _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih _) rfl
  | _ => funext; rfl
Cleared hypotheses: η'
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
η' : Hom₂ f g
mk :
  ∀ {a_1 b : FreeBicategory B} {f g h : a_1 ⟶ b} (η : Hom₂ f g) (θ : Hom₂ g h),
    (Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
        fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g) →
      (Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g)
          fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h) →
        Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
          fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h
mk₁ :
  ∀ {a_1 b c : FreeBicategory B} (f : a_1 ⟶ b) {g h : b ⟶ c} (η : Hom₂ g h)
    (ih :
      Eq (α := (x : Path.{v, u} a b) → Path.{v, u} a c) (fun (p : Path.{v, u} a b) ↦ normalizeAux p g)
        fun (p : Path.{v, u} a b) ↦ normalizeAux p h),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a c) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ g))
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ h)
mk₂ :
  ∀ {a_1 b c : FreeBicategory B} {f g : a_1 ⟶ b} (h : b ⟶ c) (η : Hom₂ f g)
    (ih :
      Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
        fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a c) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (Hom.comp f h))
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (Hom.comp g h)
mk₃ :
  ∀ {a_1 b : FreeBicategory B} (f : a_1 ⟶ b),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f
mk₄ :
  ∀ {a_1 b c d : FreeBicategory B} (f : a_1 ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a d) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p ((f ≫ g) ≫ h))
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ g ≫ h)
⊢ 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
have mk₅ : ∀ {a_1 b c d : FreeBicategory B} (f : a_1 ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a d) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ g ≫ h))
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p ((f ≫ g) ≫ h)
Tactic: induction η' with
  | vcomp _ _ _ _ => apply Eq.trans <;> assumption
  | whisker_left _ _ ih => funext; apply congr_fun ih
  | whisker_right _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih _) rfl
  | _ => funext; rfl
Cleared hypotheses: η'
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
η' : Hom₂ f g
mk :
  ∀ {a_1 b : FreeBicategory B} {f g h : a_1 ⟶ b} (η : Hom₂ f g) (θ : Hom₂ g h),
    (Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
        fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g) →
      (Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g)
          fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h) →
        Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
          fun (p : Path.{v, u} a a_1) ↦ normalizeAux p h
mk₁ :
  ∀ {a_1 b c : FreeBicategory B} (f : a_1 ⟶ b) {g h : b ⟶ c} (η : Hom₂ g h)
    (ih :
      Eq (α := (x : Path.{v, u} a b) → Path.{v, u} a c) (fun (p : Path.{v, u} a b) ↦ normalizeAux p g)
        fun (p : Path.{v, u} a b) ↦ normalizeAux p h),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a c) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ g))
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ h)
mk₂ :
  ∀ {a_1 b c : FreeBicategory B} {f g : a_1 ⟶ b} (h : b ⟶ c) (η : Hom₂ f g)
    (ih :
      Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
        fun (p : Path.{v, u} a a_1) ↦ normalizeAux p g),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a c) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (Hom.comp f h))
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (Hom.comp g h)
mk₃ :
  ∀ {a_1 b : FreeBicategory B} (f : a_1 ⟶ b),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f)
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f
mk₄ :
  ∀ {a_1 b c d : FreeBicategory B} (f : a_1 ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a d) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p ((f ≫ g) ≫ h))
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ g ≫ h)
mk₅ :
  ∀ {a_1 b c d : FreeBicategory B} (f : a_1 ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
    Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a d) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ g ≫ h))
      fun (p : Path.{v, u} a a_1) ↦ normalizeAux p ((f ≫ g) ≫ h)
⊢ 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
have mk₆ : ∀ {a_1 b : FreeBicategory B} (f : a_1 ⟶ b),
  Eq (α := (x : Path.{v, u} a a_1) → Path.{v, u} a b) (fun (p : Path.{v, u} a a_1) ↦ normalizeAux p (f ≫ 𝟙 b))
    fun (p : Path.{v, u} a a_1) ↦ normalizeAux p f
Tactic: induction η' with
  | vcomp _ _ _ _ => apply Eq.trans <;> assumption
  | whisker_left _ _ ih => funext; apply congr_fun ih
  | whisker_right _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih _) rfl
  | _ => funext; rfl
Cleared hypotheses: η'