-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
H : Rel η θ
vcomp_right :
  ∀ {a b : B} {f g h : Hom.{v₁, u₁} a b} (η : Hom₂ f g) (θ₁ θ₂ : Hom₂ g h),
    Rel θ₁ θ₂ → liftHom₂ F θ₁ = liftHom₂ F θ₂ → liftHom₂ F (η.vcomp θ₁) = liftHom₂ F (η.vcomp θ₂)
vcomp_left :
  ∀ {a b : B} {f g h : Hom.{v₁, u₁} a b} (η₁ η₂ : Hom₂ f g) (θ : Hom₂ g h),
    Rel η₁ η₂ → liftHom₂ F η₁ = liftHom₂ F η₂ → liftHom₂ F (η₁.vcomp θ) = liftHom₂ F (η₂.vcomp θ)
id_comp : ∀ {a b : B} {f g : Hom.{v₁, u₁} a b} (η : Hom₂ f g), liftHom₂ F ((Hom₂.id f).vcomp η) = liftHom₂ F η
comp_id : ∀ {a b : B} {f g : Hom.{v₁, u₁} a b} (η : Hom₂ f g), liftHom₂ F (η.vcomp (Hom₂.id g)) = liftHom₂ F η
assoc :
  ∀ {a b : B} {f g h i : Hom.{v₁, u₁} a b} (η : Hom₂ f g) (θ : Hom₂ g h) (ι : Hom₂ h i),
    liftHom₂ F ((η.vcomp θ).vcomp ι) = liftHom₂ F (η.vcomp (θ.vcomp ι))
whisker_left :
  ∀ {a b c : B} (f : Hom.{v₁, u₁} a b) (g h : Hom.{v₁, u₁} b c) (η η' : Hom₂ g h),
    Rel η η' → liftHom₂ F η = liftHom₂ F η' → liftHom₂ F (Hom₂.whisker_left f η) = liftHom₂ F (Hom₂.whisker_left f η')
whisker_left_id :
  ∀ {a b c : B} (f : Hom.{v₁, u₁} a b) (g : Hom.{v₁, u₁} b c),
    liftHom₂ F (Hom₂.whisker_left f (Hom₂.id g)) = liftHom₂ F (Hom₂.id (f.comp g))
whisker_left_comp :
  ∀ {a b c : B} (f : Hom.{v₁, u₁} a b) {g h i : Hom.{v₁, u₁} b c} (η : Hom₂ g h) (θ : Hom₂ h i),
    liftHom₂ F (Hom₂.whisker_left f (η.vcomp θ)) = liftHom₂ F ((Hom₂.whisker_left f η).vcomp (Hom₂.whisker_left f θ))
id_whisker_left :
  ∀ {a b : B} {f g : Hom.{v₁, u₁} a b} (η : Hom₂ f g),
    liftHom₂ F (Hom₂.whisker_left (Hom.id a) η) =
      liftHom₂ F ((Hom₂.left_unitor f).vcomp (η.vcomp (Hom₂.left_unitor_inv g)))
comp_whisker_left :
  ∀ {a b c d : B} (f : Hom.{v₁, u₁} a b) (g : Hom.{v₁, u₁} b c) {h h' : Hom.{v₁, u₁} c d} (η : Hom₂ h h'),
    liftHom₂ F (Hom₂.whisker_left (f.comp g) η) =
      liftHom₂ F
        ((Hom₂.associator f g h).vcomp
          ((Hom₂.whisker_left f (Hom₂.whisker_left g η)).vcomp (Hom₂.associator_inv f g h')))
whisker_right :
  ∀ {a b c : B} (f g : Hom.{v₁, u₁} a b) (h : Hom.{v₁, u₁} b c) (η η' : Hom₂ f g),
    Rel η η' → liftHom₂ F η = liftHom₂ F η' → liftHom₂ F (Hom₂.whisker_right h η) = liftHom₂ F (Hom₂.whisker_right h η')
id_whisker_right :
  ∀ {a b c : B} (f : Hom.{v₁, u₁} a b) (g : Hom.{v₁, u₁} b c),
    liftHom₂ F (Hom₂.whisker_right g (Hom₂.id f)) = liftHom₂ F (Hom₂.id (f.comp g))
comp_whisker_right :
  ∀ {a b c : B} {f g h : Hom.{v₁, u₁} a b} (i : Hom.{v₁, u₁} b c) (η : Hom₂ f g) (θ : Hom₂ g h),
    liftHom₂ F (Hom₂.whisker_right i (η.vcomp θ)) = liftHom₂ F ((Hom₂.whisker_right i η).vcomp (Hom₂.whisker_right i θ))
whisker_right_id :
  ∀ {a b : B} {f g : Hom.{v₁, u₁} a b} (η : Hom₂ f g),
    liftHom₂ F (Hom₂.whisker_right (Hom.id b) η) =
      liftHom₂ F ((Hom₂.right_unitor f).vcomp (η.vcomp (Hom₂.right_unitor_inv g)))
whisker_right_comp :
  ∀ {a b c d : B} {f f' : Hom.{v₁, u₁} a b} (g : Hom.{v₁, u₁} b c) (h : Hom.{v₁, u₁} c d) (η : Hom₂ f f'),
    liftHom₂ F (Hom₂.whisker_right (g.comp h) η) =
      liftHom₂ F
        ((Hom₂.associator_inv f g h).vcomp
          ((Hom₂.whisker_right h (Hom₂.whisker_right g η)).vcomp (Hom₂.associator f' g h)))
whisker_assoc :
  ∀ {a b c d : B} (f : Hom.{v₁, u₁} a b) {g g' : Hom.{v₁, u₁} b c} (η : Hom₂ g g') (h : Hom.{v₁, u₁} c d),
    liftHom₂ F (Hom₂.whisker_right h (Hom₂.whisker_left f η)) =
      liftHom₂ F
        ((Hom₂.associator f g h).vcomp
          ((Hom₂.whisker_left f (Hom₂.whisker_right h η)).vcomp (Hom₂.associator_inv f g' h)))
whisker_exchange :
  ∀ {a b c : B} {f g : Hom.{v₁, u₁} a b} {h i : Hom.{v₁, u₁} b c} (η : Hom₂ f g) (θ : Hom₂ h i),
    liftHom₂ F ((Hom₂.whisker_left f θ).vcomp (Hom₂.whisker_right i η)) =
      liftHom₂ F ((Hom₂.whisker_right h η).vcomp (Hom₂.whisker_left g θ))
associator_hom_inv :
  ∀ {a b c d : B} (f : Hom.{v₁, u₁} a b) (g : Hom.{v₁, u₁} b c) (h : Hom.{v₁, u₁} c d),
    liftHom₂ F ((Hom₂.associator f g h).vcomp (Hom₂.associator_inv f g h)) = liftHom₂ F (Hom₂.id ((f.comp g).comp h))
associator_inv_hom :
  ∀ {a b c d : B} (f : Hom.{v₁, u₁} a b) (g : Hom.{v₁, u₁} b c) (h : Hom.{v₁, u₁} c d),
    liftHom₂ F ((Hom₂.associator_inv f g h).vcomp (Hom₂.associator f g h)) = liftHom₂ F (Hom₂.id (f.comp (g.comp h)))
left_unitor_hom_inv :
  ∀ {a b : B} (f : Hom.{v₁, u₁} a b),
    liftHom₂ F ((Hom₂.left_unitor f).vcomp (Hom₂.left_unitor_inv f)) = liftHom₂ F (Hom₂.id (Hom.comp (Hom.id a) f))
left_unitor_inv_hom :
  ∀ {a b : B} (f : Hom.{v₁, u₁} a b),
    liftHom₂ F ((Hom₂.left_unitor_inv f).vcomp (Hom₂.left_unitor f)) = liftHom₂ F (Hom₂.id f)
right_unitor_hom_inv :
  ∀ {a b : B} (f : Hom.{v₁, u₁} a b),
    liftHom₂ F ((Hom₂.right_unitor f).vcomp (Hom₂.right_unitor_inv f)) = liftHom₂ F (Hom₂.id (f.comp (Hom.id b)))
right_unitor_inv_hom :
  ∀ {a b : B} (f : Hom.{v₁, u₁} a b),
    liftHom₂ F ((Hom₂.right_unitor_inv f).vcomp (Hom₂.right_unitor f)) = liftHom₂ F (Hom₂.id f)
⊢ liftHom₂ F η = liftHom₂ F θ
have pentagon : ∀ {a b c d e : B} (f : Hom.{v₁, u₁} a b) (g : Hom.{v₁, u₁} b c) (h : Hom.{v₁, u₁} c d) (i : Hom.{v₁, u₁} d e),
  liftHom₂ F
      ((Hom₂.whisker_right i (Hom₂.associator f g h)).vcomp
        ((Hom₂.associator f (g.comp h) i).vcomp (Hom₂.whisker_left f (Hom₂.associator g h i)))) =
    liftHom₂ F ((Hom₂.associator (f.comp g) h i).vcomp (Hom₂.associator f g (h.comp i)))
Tactic: induction H
Cleared hypotheses: H