-- 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)
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
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 ≫ 𝟙 b)
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 (𝟙 a_1 ≫ 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 : 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 (𝟙 a_1 ≫ 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: η'