-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
h : f ≈ g
refl :
  ∀ {X Y : F C} (f : X ⟶ᵐ Y),
    Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 f)
      (projectMapAux f_1 f)
symm :
  ∀ {X Y : F C} (f g : X ⟶ᵐ Y),
    HomEquiv f g →
      ∀
        (hfg' :
          Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 f)
            (projectMapAux f_1 g)),
        Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 g)
          (projectMapAux f_1 f)
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 f)
    (projectMapAux f_1 g)
have trans : ∀ {X Y : F C} {f g h : X ⟶ᵐ Y},
  HomEquiv f g →
    HomEquiv g h →
      ∀
        (hfg :
          Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 f)
            (projectMapAux f_1 g))
        (hgh :
          Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 g)
            (projectMapAux f_1 h)),
        Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 f)
          (projectMapAux f_1 h)
Tactic: induction h with
    | refl => rfl
    | symm _ _ _ hfg' => exact hfg'.symm
    | trans _ _ hfg hgh => exact hfg.trans hgh
    | comp _ _ hf hg => dsimp only [projectMapAux]; rw [hf, hg]
    | whiskerLeft _ _ _ _ hf => dsimp only [projectMapAux, projectObj]; rw [hf]
    | whiskerRight _ _ _ _ hf => dsimp only [projectMapAux, projectObj]; rw [hf]
    | tensor _ _ hfg hfg' => dsimp only [projectMapAux]; rw [hfg, hfg']
    | tensorHom_def _ _ =>
        dsimp only [projectMapAux, projectObj]; rw [MonoidalCategory.tensorHom_def]
    | comp_id => dsimp only [projectMapAux]; rw [Category.comp_id]
    | id_comp => dsimp only [projectMapAux]; rw [Category.id_comp]
    | assoc => dsimp only [projectMapAux]; rw [Category.assoc]
    | id_tensorHom_id => dsimp only [projectMapAux]; rw [MonoidalCategory.id_tensorHom_id]; rfl
    | tensorHom_comp_tensorHom =>
      dsimp only [projectMapAux]; rw [MonoidalCategory.tensorHom_comp_tensorHom]
    | whiskerLeft_id =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.whiskerLeft_id]
    | id_whiskerRight =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.id_whiskerRight]
    | α_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
    | α_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
    | associator_naturality =>
        dsimp only [projectMapAux]; rw [MonoidalCategory.associator_naturality]
    | ρ_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
    | ρ_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
    | ρ_naturality =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.rightUnitor_naturality]
    | l_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
    | l_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
    | l_naturality =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.leftUnitor_naturality]
    | pentagon =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.pentagon]
    | triangle =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.triangle]
Cleared hypotheses: h