awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, v, u, u} C C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ Eq (α := F.obj V₁.V ⟶ V₂.V)
    (F.map f.f ≫ (Equiv.symm (adj.homEquiv V₂.V V₂.V) : (a : V₂.V ⟶ G.obj V₂.V) → F.obj V₂.V ⟶ V₂.V) V₂.str)
    ((Equiv.symm (adj.homEquiv V₁.V V₁.V) : (a : V₁.V ⟶ G.obj V₁.V) → F.obj V₁.V ⟶ V₁.V) V₁.str ≫ f.f)
have rw : Eq (α := F.obj V₁.V ⟶ V₂.V)
  ((Equiv.symm (adj.homEquiv V₁.V V₂.V) : (a : V₁.V ⟶ G.obj V₂.V) → F.obj V₁.V ⟶ V₂.V) (f.f ≫ V₂.str) :
    F.obj V₁.V ⟶ V₂.V)
  ((Equiv.symm (adj.homEquiv V₁.V V₁.V) : (a : V₁.V ⟶ G.obj V₁.V) → F.obj V₁.V ⟶ V₁.V) V₁.str ≫ f.f : F.obj V₁.V ⟶ V₂.V)
Tactic: rw [← Adjunction.homEquiv_naturality_left_symm, ← Adjunction.homEquiv_naturality_right_symm,
    f.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, v, u, u} C C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
rw :
  Eq (α := F.obj V₁.V ⟶ V₂.V)
    ((Equiv.symm (adj.homEquiv V₁.V V₂.V) : (a : V₁.V ⟶ G.obj V₂.V) → F.obj V₁.V ⟶ V₂.V) (f.f ≫ V₂.str) :
      F.obj V₁.V ⟶ V₂.V)
    ((Equiv.symm (adj.homEquiv V₁.V V₁.V) : (a : V₁.V ⟶ G.obj V₁.V) → F.obj V₁.V ⟶ V₁.V) V₁.str ≫ f.f :
      F.obj V₁.V ⟶ V₂.V)
⊢ Eq (α := F.obj V₁.V ⟶ V₂.V)
    (F.map f.f ≫ (Equiv.symm (adj.homEquiv V₂.V V₂.V) : (a : V₂.V ⟶ G.obj V₂.V) → F.obj V₂.V ⟶ V₂.V) V₂.str)
    ((Equiv.symm (adj.homEquiv V₁.V V₁.V) : (a : V₁.V ⟶ G.obj V₁.V) → F.obj V₁.V ⟶ V₁.V) V₁.str ≫ f.f)
have rw₁ : Eq (α := F.obj V₁.V ⟶ V₂.V)
  ((Equiv.symm (adj.homEquiv V₁.V V₂.V) : (a : V₁.V ⟶ G.obj V₂.V) → F.obj V₁.V ⟶ V₂.V) (f.f ≫ V₂.str) :
    F.obj V₁.V ⟶ V₂.V)
  ((Equiv.symm (adj.homEquiv V₁.V V₂.V) : (a : V₁.V ⟶ G.obj V₂.V) → F.obj V₁.V ⟶ V₂.V) (V₁.str ≫ G.map f.f) :
    F.obj V₁.V ⟶ V₂.V)
Tactic: rw [← Adjunction.homEquiv_naturality_left_symm, ← Adjunction.homEquiv_naturality_right_symm,
    f.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, v, u, u} C C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
rw :
  Eq (α := F.obj V₁.V ⟶ V₂.V)
    ((Equiv.symm (adj.homEquiv V₁.V V₂.V) : (a : V₁.V ⟶ G.obj V₂.V) → F.obj V₁.V ⟶ V₂.V) (f.f ≫ V₂.str) :
      F.obj V₁.V ⟶ V₂.V)
    ((Equiv.symm (adj.homEquiv V₁.V V₁.V) : (a : V₁.V ⟶ G.obj V₁.V) → F.obj V₁.V ⟶ V₁.V) V₁.str ≫ f.f :
      F.obj V₁.V ⟶ V₂.V)
rw₁ :
  Eq (α := F.obj V₁.V ⟶ V₂.V)
    ((Equiv.symm (adj.homEquiv V₁.V V₂.V) : (a : V₁.V ⟶ G.obj V₂.V) → F.obj V₁.V ⟶ V₂.V) (f.f ≫ V₂.str) :
      F.obj V₁.V ⟶ V₂.V)
    ((Equiv.symm (adj.homEquiv V₁.V V₂.V) : (a : V₁.V ⟶ G.obj V₂.V) → F.obj V₁.V ⟶ V₂.V) (V₁.str ≫ G.map f.f) :
      F.obj V₁.V ⟶ V₂.V)
⊢ Eq (α := F.obj V₁.V ⟶ V₂.V)
    (F.map f.f ≫ (Equiv.symm (adj.homEquiv V₂.V V₂.V) : (a : V₂.V ⟶ G.obj V₂.V) → F.obj V₂.V ⟶ V₂.V) V₂.str)
    ((Equiv.symm (adj.homEquiv V₁.V V₁.V) : (a : V₁.V ⟶ G.obj V₁.V) → F.obj V₁.V ⟶ V₁.V) V₁.str ≫ f.f)
have rw₂ : Eq (α := F.obj V₁.V ⟶ V₂.V)
  ((Equiv.symm (adj.homEquiv V₁.V V₂.V) : (a : V₁.V ⟶ G.obj V₂.V) → F.obj V₁.V ⟶ V₂.V) (f.f ≫ V₂.str) :
    F.obj V₁.V ⟶ V₂.V)
  ((Equiv.symm (adj.homEquiv V₁.V V₂.V) : (a : V₁.V ⟶ G.obj V₂.V) → F.obj V₁.V ⟶ V₂.V) (f.f ≫ V₂.str) :
    F.obj V₁.V ⟶ V₂.V)
Tactic: rw [← Adjunction.homEquiv_naturality_left_symm, ← Adjunction.homEquiv_naturality_right_symm,
    f.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, v, u, u} C C
adj : F ⊣ G
A : Algebra F
⊢ (Algebra.toCoalgebraOf adj).map ((AlgCoalgEquiv.unitIso adj).hom.app A) ≫
      (AlgCoalgEquiv.counitIso adj).hom.app ((Algebra.toCoalgebraOf adj).obj A) =
    𝟙 ((Algebra.toCoalgebraOf adj).obj A)
have w : autoParam
  (((Algebra.toCoalgebraOf adj).map ((AlgCoalgEquiv.unitIso adj).hom.app A) ≫
        (AlgCoalgEquiv.counitIso adj).hom.app ((Algebra.toCoalgebraOf adj).obj A)).f =
    Coalgebra.Hom.f (𝟙 ((Algebra.toCoalgebraOf adj).obj A)))
  Coalgebra.ext._auto_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Endomorphism (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f g : (End X)ˣ
⊢ { hom := (↑(f * g) : End X), inv := (f * g).inv, hom_inv_id := ⋯, inv_hom_id := ⋯ : X ≅ X } =
    { hom := (↑f : End X), inv := f.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ : X ≅ X } *
      { hom := (↑g : End X), inv := g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ : X ≅ X }
have mk : ∀ (val inv : End X) (val_inv : val * inv = 1) (inv_val : inv * val = 1),
  { hom := (↑({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } * g) : End X),
      inv := ({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } * g).inv, hom_inv_id := sorry,
      inv_hom_id := sorry : X ≅ X } =
    { hom := (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } : End X),
        inv := { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ }.inv, hom_inv_id := sorry,
        inv_hom_id := sorry : X ≅ X } *
      { hom := (↑g : End X), inv := g.inv, hom_inv_id := sorry, inv_hom_id := sorry : X ≅ X }
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Endomorphism (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
g : (End X)ˣ
val inv : End X
val_inv : val * inv = 1
inv_val : inv * val = 1
⊢ { hom := (↑({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } * g) : End X),
      inv := ({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } * g).inv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ : X ≅ X } =
    { hom := (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } : End X),
        inv := { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ }.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ : X ≅ X } *
      { hom := (↑g : End X), inv := g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ : X ≅ X }
have mk : ∀ (val_1 inv_1 : End X) (val_inv_1 : val_1 * inv_1 = 1) (inv_val_1 : inv_1 * val_1 = 1),
  {
      hom :=
        (↑({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } *
              { val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 : (End X)ˣ }) :
          End X),
      inv :=
        ({ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } *
            { val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 : (End X)ˣ }).inv,
      hom_inv_id := sorry, inv_hom_id := sorry : X ≅ X } =
    { hom := (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ } : End X),
        inv := { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : (End X)ˣ }.inv, hom_inv_id := sorry,
        inv_hom_id := sorry : X ≅ X } *
      { hom := (↑{ val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 : (End X)ˣ } : End X),
        inv := { val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 : (End X)ˣ }.inv,
        hom_inv_id := sorry, inv_hom_id := sorry : X ≅ X }
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W X Y Z : C
⊢ Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := V)
      (tensorObj.{w, v} (𝒞 := inst)
        (tensorObj.{w, v} (𝒞 := inst) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
        (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W Z))
    (Iso.hom
        (α_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z)) ≫
      @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X ◁ eComp V X Y Z ≫ eComp V W X Z)
    (eComp V W X Y ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z ≫ eComp V W Y Z)
have rw : Eq.{w + 1} (α :=
  Quiver.Hom.{w, v} (V := V)
    (tensorObj.{w, v} (𝒞 := inst)
      (tensorObj.{w, v} (𝒞 := inst) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
        (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z))
    (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W Z))
  (Iso.hom
      (α_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
        (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z)) ≫
    Iso.inv
        (α_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z)) ≫
      eComp V W X Y ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z ≫ eComp V W Y Z)
  (eComp V W X Y ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z ≫ eComp V W Y Z)
Tactic: rw [← e_assoc V W X Y Z, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W X Y Z : C
rw :
  Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := V)
      (tensorObj.{w, v} (𝒞 := inst)
        (tensorObj.{w, v} (𝒞 := inst) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
        (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W Z))
    (Iso.hom
        (α_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z)) ≫
      Iso.inv
          (α_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
            (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
            (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z)) ≫
        eComp V W X Y ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z ≫ eComp V W Y Z)
    (eComp V W X Y ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z ≫ eComp V W Y Z)
⊢ Eq.{w + 1} (α :=
    Quiver.Hom.{w, v} (V := V)
      (tensorObj.{w, v} (𝒞 := inst)
        (tensorObj.{w, v} (𝒞 := inst) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
        (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W Z))
    (Iso.hom
        (α_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z)) ≫
      @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X ◁ eComp V X Y Z ≫ eComp V W X Z)
    (eComp V W X Y ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z ≫ eComp V W Y Z)
have rw₁ : Eq.{w + 1} (α :=
  Quiver.Hom.{w, v} (V := V)
    (tensorObj.{w, v} (𝒞 := inst)
      (tensorObj.{w, v} (𝒞 := inst) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W X)
        (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
      (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z))
    (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ W Z))
  (eComp V W X Y ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z ≫ eComp V W Y Z)
  (eComp V W X Y ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z ≫ eComp V W Y Z)
Tactic: rw [← e_assoc V W X Y Z, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ CategoryStruct.comp (Y :=
      tensorObj.{w', v'} (𝒞 := inst_3) (tensorUnit.{w', v'} W (𝒞 := inst_3))
        (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)))
      (Iso.inv (λ_ (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))))
      ((ε F ≫ F.map (eId V X)) ▷ F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ≫
        μ F (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X X)
            (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ≫
          F.map (eComp V X X Y)) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
have simp : F.map (Iso.inv (λ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))) ≫
    F.map (eId V X ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ≫ F.map (eComp V X X Y) =
  𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
Tactic: simp only [comp_whiskerRight, Category.assoc, Functor.LaxMonoidal.μ_natural_left_assoc,
      Functor.LaxMonoidal.left_unitality_inv_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ F.map (Iso.inv (λ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))) ≫
      F.map (eId V X ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ≫ F.map (eComp V X X Y) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
have simp_rw : F.map
    (Iso.inv (λ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      eId V X ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ≫ eComp V X X Y) =
  𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
Tactic: simp_rw [← F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ F.map
      (Iso.inv (λ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
        eId V X ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ≫ eComp V X X Y) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
have h : Eq.{w + 1} (α :=
  Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
    (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
  (Iso.inv (λ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
    eId V X ▷ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ≫ eComp V X X Y)
  (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
Tactic: convert! F.map_id _
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ CategoryStruct.comp (Y :=
      tensorObj.{w', v'} (𝒞 := inst_3) (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
        (tensorUnit.{w', v'} W (𝒞 := inst_3)))
      (Iso.inv (ρ_ (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))))
      (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ◁ (ε F ≫ F.map (eId V Y)) ≫
        μ F (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
            (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Y) ≫
          F.map (eComp V X Y Y)) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
have simp : F.map (Iso.inv (ρ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))) ≫
    F.map (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ◁ eId V Y) ≫ F.map (eComp V X Y Y) =
  𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
Tactic: simp only [MonoidalCategory.whiskerLeft_comp, Category.assoc,
      Functor.LaxMonoidal.μ_natural_right_assoc,
      Functor.LaxMonoidal.right_unitality_inv_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ F.map (Iso.inv (ρ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))) ≫
      F.map (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ◁ eId V Y) ≫ F.map (eComp V X Y Y) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
have simp_rw : F.map
    (Iso.inv (ρ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ◁ eId V Y ≫ eComp V X Y Y) =
  𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
Tactic: simp_rw [← F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
F : Functor.{w, w', v, v'} V W
inst_5 : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ F.map
      (Iso.inv (ρ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
        @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ◁ eId V Y ≫ eComp V X Y Y) =
    𝟙 (F.obj (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
have h : Eq.{w + 1} (α :=
  Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
    (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
  (Iso.inv (ρ_ (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
    @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y ◁ eId V Y ≫ eComp V X Y Y)
  (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y))
Tactic: convert! F.map_id _
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
Goal:
C : Type u₁
W : Type v
inst : Category.{w, v} W
inst_1 : MonoidalCategory.{w, v} W
inst_2 : EnrichedCategory.{w, v, u₁} W C
X Y Z : C
f : tensorUnit.{w, v} W (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y
g : tensorUnit.{w, v} W (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ Y Z
⊢ homOf W (Iso.inv (λ_ (tensorUnit.{w, v} W (𝒞 := inst))) ≫ (f ⊗ₘ g) ≫ eComp W X Y Z) = homOf W f ≫ homOf W g
have rw : homOf W ((Iso.inv (λ_ (tensorUnit.{w, v} W (𝒞 := inst))) ≫ (f ⊗ₘ g)) ≫ eComp W X Y Z) = homOf W f ≫ homOf W g
Tactic: rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C_1 : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C_1
C : Type u₁
D : Type u₂
inst_3 : EnrichedCategory.{w, v, u₁} V C
inst_4 : EnrichedCategory.{w, v, u₂} V D
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
h_obj : ∀ (X : C), F.obj X = G.obj X
X Y : C
⊢ Eq.{v + 1} (α := V) (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj X) (F.obj Y))
    (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G.obj X) (G.obj Y))
have rw : Eq.{v + 1} (α := V) (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G.obj X) (F.obj Y))
  (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G.obj X) (G.obj Y))
Tactic: rw [h_obj, h_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C_1 : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C_1
C : Type u₁
D : Type u₂
inst_3 : EnrichedCategory.{w, v, u₁} V C
inst_4 : EnrichedCategory.{w, v, u₂} V D
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
h_obj : ∀ (X : C), F.obj X = G.obj X
X Y : C
rw :
  Eq.{v + 1} (α := V) (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G.obj X) (F.obj Y))
    (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G.obj X) (G.obj Y))
⊢ Eq.{v + 1} (α := V) (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj X) (F.obj Y))
    (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G.obj X) (G.obj Y))
have rw₁ : Eq.{v + 1} (α := V) (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G.obj X) (G.obj Y))
  (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G.obj X) (G.obj Y))
Tactic: rw [h_obj, h_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
D : Type u₂
inst_2 : EnrichedCategory.{w, v, u₁} V C
inst_3 : EnrichedCategory.{w, v, u₂} V D
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
F_obj : C → D
F_map :
  (X Y : C) →
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F_obj X) (F_obj Y))
map_id : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ₘ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_obj : C → D
G_map :
  (X Y : C) →
    Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (G_obj X) (G_obj Y))
map_id_1 : ∀ (X : C), eId V X ≫ G_map X X = eId V (G_obj X)
map_comp_1 : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ₘ G_map Y Z) ≫ eComp V (G_obj X) (G_obj Y) (G_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
        X =
      { obj := G_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 :
            EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
        X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D }.map X
          Y ≫
        eqToHom ⋯ =
      { obj := G_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 }.map X Y
⊢ { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D } =
    { obj := G_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 }
have obtain : ∀
  (G_map :
    (X Y : C) →
      Quiver.Hom.{w, v} (V := V) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F_obj X) (F_obj Y)))
  (map_id_2 : ∀ (X : C), eId V X ≫ G_map X X = eId V (F_obj X))
  (map_comp_2 :
    ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ₘ G_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z))
  (h_obj :
    ∀ (X : C),
      { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
          X =
        { obj := F_obj, map := G_map, map_id := map_id_2, map_comp := map_comp_2 :
              EnrichedFunctor.{w, v, u₁, u₂} V C D }.obj
          X)
  (h_map :
    ∀ (X Y : C),
      { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D }.map
            X Y ≫
          eqToHom sorry =
        { obj := F_obj, map := G_map, map_id := map_id_2, map_comp := map_comp_2 }.map X Y),
  { obj := F_obj, map := F_map, map_id := map_id, map_comp := map_comp : EnrichedFunctor.{w, v, u₁, u₂} V C D } =
    { obj := F_obj, map := G_map, map_id := map_id_2, map_comp := map_comp_2 }
Tactic: obtain rfl : F_obj = G_obj := funext fun X ↦ h_obj X
Cleared hypotheses: G_obj, G_map, map_id_1, map_comp_1, h_obj, h_map