awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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_1 : ∀ (X : C), eId V X ≫ G_map X X = eId V (F_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 (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_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 := F_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 := F_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 }
have e_map : F_map = G_map
Tactic: congr
-- 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_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_1 : ∀ (X : C), eId V X ≫ G_map X X = eId V (F_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 (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_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 := F_obj, map := G_map, map_id := map_id_1, map_comp := map_comp_1 }.map X Y
⊢ F_map = G_map
have e_map : ∀ (X Y : C), F_map X Y = G_map X Y
Tactic: ext X Y
-- 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
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
C : Type u₁
inst_5 : EnrichedCategory.{w', v', u₁} W C
D : Type u₂
inst_6 : EnrichedCategory.{w', v', u₂} W D
E : Type u₃
inst_7 : EnrichedCategory.{w', v', u₃} W E
F : EnrichedFunctor.{w', v', u₁, u₂} W C D
X Y Z : ForgetEnrichment.{w', v', u₁} W C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ForgetEnrichment.homOf W
      (ForgetEnrichment.homTo W (f ≫ g) ≫ F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Z)) =
    ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) ≫
      ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z))
have dsimp : ForgetEnrichment.homOf W
    (((Iso.inv (λ_ (tensorUnit.{w', v'} W (𝒞 := inst_3))) ≫
          (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g)) ≫
        eComp W (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
      F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Z)) =
  ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) ≫
    ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z))
Tactic: dsimp
-- 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
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
C : Type u₁
inst_5 : EnrichedCategory.{w', v', u₁} W C
D : Type u₂
inst_6 : EnrichedCategory.{w', v', u₂} W D
E : Type u₃
inst_7 : EnrichedCategory.{w', v', u₃} W E
F : EnrichedFunctor.{w', v', u₁, u₂} W C D
X Y Z : ForgetEnrichment.{w', v', u₁} W C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ForgetEnrichment.homOf W
      (((Iso.inv (λ_ (tensorUnit.{w', v'} W (𝒞 := inst_3))) ≫
            (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g)) ≫
          eComp W (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
        F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Z)) =
    ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) ≫
      ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z))
have apply_fun : ForgetEnrichment.homTo W
    (ForgetEnrichment.homOf W
      (((Iso.inv (λ_ (tensorUnit.{w', v'} W (𝒞 := inst_3))) ≫
            (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g)) ≫
          eComp W (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
        F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Z))) =
  ForgetEnrichment.homTo W
    (ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) ≫
      ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)))
Tactic: apply_fun ForgetEnrichment.homTo W
-- 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
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
C : Type u₁
inst_5 : EnrichedCategory.{w', v', u₁} W C
D : Type u₂
inst_6 : EnrichedCategory.{w', v', u₂} W D
E : Type u₃
inst_7 : EnrichedCategory.{w', v', u₃} W E
F : EnrichedFunctor.{w', v', u₁, u₂} W C D
X Y Z : ForgetEnrichment.{w', v', u₁} W C
f : X ⟶ Y
g : Y ⟶ Z
apply_fun :
  ForgetEnrichment.homTo W
      (ForgetEnrichment.homOf W
        (((Iso.inv (λ_ (tensorUnit.{w', v'} W (𝒞 := inst_3))) ≫
              (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g)) ≫
            eComp W (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
          F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Z))) =
    ForgetEnrichment.homTo W
      (ForgetEnrichment.homOf W
          (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) ≫
        ForgetEnrichment.homOf W
          (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)))
⊢ ForgetEnrichment.homOf W
      (((Iso.inv (λ_ (tensorUnit.{w', v'} W (𝒞 := inst_3))) ≫
            (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g)) ≫
          eComp W (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
        F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Z)) =
    ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) ≫
      ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z))
have inj : Function.Injective.{w' + 1, w' + 1} (α :=
  Quiver.Hom (V := ForgetEnrichment.{w', v', u₂} W D) (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X)))
    (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z))))
  (ForgetEnrichment.homTo W)
Tactic: apply_fun ForgetEnrichment.homTo W
-- 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
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
C : Type u₁
inst_5 : EnrichedCategory.{w', v', u₁} W C
D : Type u₂
inst_6 : EnrichedCategory.{w', v', u₂} W D
E : Type u₃
inst_7 : EnrichedCategory.{w', v', u₃} W E
F : EnrichedFunctor.{w', v', u₁, u₂} W C D
X Y Z : ForgetEnrichment.{w', v', u₁} W C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ForgetEnrichment.homTo W
      (ForgetEnrichment.homOf W
        (((Iso.inv (λ_ (tensorUnit.{w', v'} W (𝒞 := inst_3))) ≫
              (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g)) ≫
            eComp W (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
          F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Z))) =
    ForgetEnrichment.homTo W
      (ForgetEnrichment.homOf W
          (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) ≫
        ForgetEnrichment.homOf W
          (ForgetEnrichment.homTo W g ≫ F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)))
have simp : (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g) ≫
    (F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) ⊗ₘ
        F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
      eComp W (F.obj (ForgetEnrichment.to W X)) (F.obj (ForgetEnrichment.to W Y)) (F.obj (ForgetEnrichment.to W Z)) =
  (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g) ≫
    (F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) ⊗ₘ
        F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
      eComp W (ForgetEnrichment.to.{w', v', u₂} W (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X))))
        (ForgetEnrichment.to.{w', v', u₂} W (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Y))))
        (ForgetEnrichment.to.{w', v', u₂} W (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z))))
Tactic: simp only [Iso.cancel_iso_inv_left, Category.assoc, ← tensorHom_comp_tensorHom,
        ForgetEnrichment.homTo_homOf, EnrichedFunctor.map_comp, ForgetEnrichment.homTo_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (hypothesis)
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
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
C : Type u₁
inst_5 : EnrichedCategory.{w', v', u₁} W C
D : Type u₂
inst_6 : EnrichedCategory.{w', v', u₂} W D
E : Type u₃
inst_7 : EnrichedCategory.{w', v', u₃} W E
F : EnrichedFunctor.{w', v', u₁, u₂} W C D
X Y Z : ForgetEnrichment.{w', v', u₁} W C
f_1 : X ⟶ Y
g_1 : Y ⟶ Z
f g :
  Quiver.Hom (V := ForgetEnrichment.{w', v', u₂} W D) (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X)))
    (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z)))
w : ForgetEnrichment.homTo W f = ForgetEnrichment.homTo W g
⊢ f = g
have w₁ : ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f) = ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g)
Tactic: apply_fun ForgetEnrichment.homOf W at w
Cleared hypotheses: w
-- 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
D : Type u₂
inst_3 : EnrichedCategory.{w, v, u₂} V D
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
α β : F ⟶ G
h : ∀ (X : C), α.out.app X = β.out.app X
⊢ α = β
have rcases : ∀ (α : F.forget ⟶ G.forget) (h : ∀ (X : C), { out := α : EnrichedNatTrans F G }.out.app X = β.out.app X),
  { out := α : EnrichedNatTrans F G } = β
Tactic: rcases α with ⟨α⟩
Cleared hypotheses: α, h
-- 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
D : Type u₂
inst_3 : EnrichedCategory.{w, v, u₂} V D
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
β : F ⟶ G
α : F.forget ⟶ G.forget
h : ∀ (X : C), { out := α : EnrichedNatTrans F G }.out.app X = β.out.app X
⊢ { out := α : EnrichedNatTrans F G } = β
have rcases : ∀ (β : F.forget ⟶ G.forget) (h : ∀ (X : C), { out := α : EnrichedNatTrans F G }.out.app X = { out := β }.out.app X),
  { out := α : EnrichedNatTrans F G } = { out := β }
Tactic: rcases β with ⟨β⟩
Cleared hypotheses: β, h
-- 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
D : Type u₂
inst_3 : EnrichedCategory.{w, v, u₂} V D
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
α β : F.forget ⟶ G.forget
h : ∀ (X : C), { out := α : EnrichedNatTrans F G }.out.app X = { out := β }.out.app X
⊢ { out := α : EnrichedNatTrans F G } = { out := β }
have e_out : α = β
Tactic: congr
-- 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
D : Type u₂
inst_3 : EnrichedCategory.{w, v, u₂} V D
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
α β : F.forget ⟶ G.forget
h : ∀ (X : C), { out := α : EnrichedNatTrans F G }.out.app X = { out := β }.out.app X
⊢ α = β
have e_out : ∀ (x : ForgetEnrichment.{w, v, u₁} V C), α.app x = β.app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (hypothesis)
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
D : Type u₂
inst_3 : EnrichedCategory.{w, v, u₂} V D
inst_4 : BraidedCategory.{w, v} V
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
X_1 Y_1 : Vᵒᵖ
f : X_1 ⟶ Y_1
σ : GradedNatTrans (Functor.obj (Center.ofBraided V) (unop X_1)) F G
X Y : C
⊢ Iso.hom
        (HalfBraiding.β
          (Sigma.snd (β := fun (X : V) ↦ HalfBraiding.{w, v} X) (Functor.obj (Center.ofBraided V) (unop Y_1)))
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (F.map X Y ⊗ₘ f.unop ≫ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
have p : Iso.hom
      (HalfBraiding.β
        (Sigma.snd (β := fun (X : V) ↦ HalfBraiding.{w, v} X) (Functor.obj (Center.ofBraided V) (unop X_1)))
        (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
    (F.map X Y ⊗ₘ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
  (σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
Tactic: have p := σ.naturality X Y
-- 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
D : Type u₂
inst_3 : EnrichedCategory.{w, v, u₂} V D
inst_4 : BraidedCategory.{w, v} V
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
X_1 Y_1 : Vᵒᵖ
f : X_1 ⟶ Y_1
σ : GradedNatTrans (Functor.obj (Center.ofBraided V) (unop X_1)) F G
X Y : C
p :
  Iso.hom
        (HalfBraiding.β
          (Sigma.snd (β := fun (X : V) ↦ HalfBraiding.{w, v} X) (Functor.obj (Center.ofBraided V) (unop X_1)))
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (F.map X Y ⊗ₘ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
⊢ Iso.hom
        (HalfBraiding.β
          (Sigma.snd (β := fun (X : V) ↦ HalfBraiding.{w, v} X) (Functor.obj (Center.ofBraided V) (unop Y_1)))
          (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (F.map X Y ⊗ₘ f.unop ≫ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
have dsimp : Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
    (F.map X Y ⊗ₘ f.unop ≫ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
  (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
Tactic: dsimp at p ⊢
-- 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
D : Type u₂
inst_3 : EnrichedCategory.{w, v, u₂} V D
inst_4 : BraidedCategory.{w, v} V
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
X_1 Y_1 : Vᵒᵖ
f : X_1 ⟶ Y_1
σ : GradedNatTrans (Functor.obj (Center.ofBraided V) (unop X_1)) F G
X Y : C
p :
  Iso.hom (β_ (unop X_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (F.map X Y ⊗ₘ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
⊢ Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (F.map X Y ⊗ₘ f.unop ≫ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
have rw : Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
    ((𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ f.unop ≫ σ.app Y) ≫
        (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y)))) ≫
      eComp V (F.obj X) (F.obj Y) (G.obj Y) =
  (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
Tactic: rw [← id_tensor_comp_tensor_id (f.unop ≫ σ.app Y) _, id_tensor_comp, Category.assoc,
          Category.assoc, ← braiding_naturality_assoc, id_tensor_comp_tensor_id_assoc, p,
          tensorHom_comp_tensorHom_assoc, Category.id_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
D : Type u₂
inst_3 : EnrichedCategory.{w, v, u₂} V D
inst_4 : BraidedCategory.{w, v} V
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
X_1 Y_1 : Vᵒᵖ
f : X_1 ⟶ Y_1
σ : GradedNatTrans (Functor.obj (Center.ofBraided V) (unop X_1)) F G
X Y : C
p :
  Iso.hom (β_ (unop X_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (F.map X Y ⊗ₘ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
rw :
  Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      ((𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ f.unop ≫ σ.app Y) ≫
          (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y)))) ≫
        eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
⊢ Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (F.map X Y ⊗ₘ f.unop ≫ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
have rw₁ : Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
    (((𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ f.unop) ≫
          (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ σ.app Y)) ≫
        (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y)))) ≫
      eComp V (F.obj X) (F.obj Y) (G.obj Y) =
  (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
Tactic: rw [← id_tensor_comp_tensor_id (f.unop ≫ σ.app Y) _, id_tensor_comp, Category.assoc,
          Category.assoc, ← braiding_naturality_assoc, id_tensor_comp_tensor_id_assoc, p,
          tensorHom_comp_tensorHom_assoc, Category.id_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
D : Type u₂
inst_3 : EnrichedCategory.{w, v, u₂} V D
inst_4 : BraidedCategory.{w, v} V
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
X_1 Y_1 : Vᵒᵖ
f : X_1 ⟶ Y_1
σ : GradedNatTrans (Functor.obj (Center.ofBraided V) (unop X_1)) F G
X Y : C
p :
  Iso.hom (β_ (unop X_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (F.map X Y ⊗ₘ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
rw :
  Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      ((𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ f.unop ≫ σ.app Y) ≫
          (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y)))) ≫
        eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
rw₁ :
  Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (((𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ f.unop) ≫
            (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ σ.app Y)) ≫
          (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y)))) ≫
        eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
⊢ Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (F.map X Y ⊗ₘ f.unop ≫ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
have rw₂ : Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
    ((𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ f.unop) ≫
        (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ σ.app Y)) ≫
      (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y))) ≫
        eComp V (F.obj X) (F.obj Y) (G.obj Y) =
  (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
Tactic: rw [← id_tensor_comp_tensor_id (f.unop ≫ σ.app Y) _, id_tensor_comp, Category.assoc,
          Category.assoc, ← braiding_naturality_assoc, id_tensor_comp_tensor_id_assoc, p,
          tensorHom_comp_tensorHom_assoc, Category.id_comp]