-- 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)
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)
comp :
  ∀ {X Y Z : F C} {f f' : X ⟶ᵐ Y} {g g' : Y ⟶ᵐ Z},
    HomEquiv f f' →
      HomEquiv g g' →
        ∀
          (hf :
            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'))
          (hg :
            Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 g)
              (projectMapAux f_1 g')),
          Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 (f.comp g))
            (projectMapAux f_1 (f'.comp g'))
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f f' : Y ⟶ᵐ Z),
    HomEquiv f f' →
      ∀
        (hf :
          Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 f)
            (projectMapAux f_1 f')),
        Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X.tensor Y) ⟶ projectObj.{v', u, u'} f_1 (X.tensor Z))
          (projectMapAux f_1 (Hom.whiskerLeft X f)) (projectMapAux f_1 (Hom.whiskerLeft X f'))
whiskerRight :
  ∀ {Y Z : F C} (f f' : Y ⟶ᵐ Z) (X : F C),
    HomEquiv f f' →
      ∀
        (hf :
          Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 f)
            (projectMapAux f_1 f')),
        Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (Y.tensor X) ⟶ projectObj.{v', u, u'} f_1 (Z.tensor X))
          (projectMapAux f_1 (f.whiskerRight X)) (projectMapAux f_1 (f'.whiskerRight X))
tensor :
  ∀ {W X Y Z : F C} {f f' : W ⟶ᵐ X} {g g' : Y ⟶ᵐ Z},
    HomEquiv f f' →
      HomEquiv g g' →
        ∀
          (hfg :
            Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 W ⟶ projectObj.{v', u, u'} f_1 X) (projectMapAux f_1 f)
              (projectMapAux f_1 f'))
          (hfg' :
            Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 g)
              (projectMapAux f_1 g')),
          Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (W.tensor Y) ⟶ projectObj.{v', u, u'} f_1 (X.tensor Z))
            (projectMapAux f_1 (f.tensor g)) (projectMapAux f_1 (f'.tensor g'))
tensorHom_def :
  ∀ {X₁ Y₁ X₂ Y₂ : F C} (f : X₁ ⟶ᵐ Y₁) (g : X₂ ⟶ᵐ Y₂),
    Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X₁.tensor X₂) ⟶ projectObj.{v', u, u'} f_1 (Y₁.tensor Y₂))
      (projectMapAux f_1 (f.tensor g)) (projectMapAux f_1 ((f.whiskerRight X₂).comp (Hom.whiskerLeft Y₁ g)))
comp_id :
  ∀ {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.comp (Hom.id Y))) (projectMapAux f_1 f)
id_comp :
  ∀ {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 ((Hom.id X).comp f)) (projectMapAux f_1 f)
assoc :
  ∀ {X Y U V : F C} (f : X ⟶ᵐ U) (g : U ⟶ᵐ V) (h : V ⟶ᵐ Y),
    Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y)
      (projectMapAux f_1 ((f.comp g).comp h)) (projectMapAux f_1 (f.comp (g.comp 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 g)
have id_tensorHom_id : ∀ {X Y : F C},
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X.tensor Y) ⟶ projectObj.{v', u, u'} f_1 (X.tensor Y))
    (projectMapAux f_1 ((Hom.id X).tensor (Hom.id Y))) (projectMapAux f_1 (Hom.id (X.tensor Y)))
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