awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.End (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x : C
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_2, v_2, u_2, u_2} D D) (unmop (Functor.obj (curriedActionMop C D) x))
      (unmop
        (tensorObj (𝒞 := monoidalOppositeCategory)
          ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory))
          (Functor.obj (curriedActionMop C D) x))))
    (Quiver.Hom.unmop (Iso.inv (λ_ (Functor.obj (curriedActionMop C D) x))))
    (Quiver.Hom.unmop
      (CategoryStruct.comp (Y :=
        Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))
        (Functor.map (curriedActionMop C D) (Iso.inv (λ_ x)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := monoidalOppositeCategory)
            (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
            (Functor.obj (curriedActionMop C D) x))
          (Quiver.Hom.mop
            { app := fun (x_1 : D) ↦ Iso.hom (αₗ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x x_1), naturality := ⋯ })
          (Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D)) ▷ Functor.obj (curriedActionMop C D) x))))
have h : ∀ (t : D),
  Eq.{v_2 + 1} (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (unmop (Functor.obj (curriedActionMop C D) x)) t ⟶
      Functor.obj.{v_2, v_2, u_2, u_2}
        (unmop
          (tensorObj (𝒞 := monoidalOppositeCategory)
            ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory))
            (Functor.obj (curriedActionMop C D) x)))
        t)
    (NatTrans.app (Quiver.Hom.unmop (Iso.inv (λ_ (Functor.obj (curriedActionMop C D) x)))) t)
    (NatTrans.app
      (Quiver.Hom.unmop
        (CategoryStruct.comp (Y :=
          Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))
          (Functor.map (curriedActionMop C D) (Iso.inv (λ_ x)))
          (CategoryStruct.comp (Y :=
            tensorObj (𝒞 := monoidalOppositeCategory)
              (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
              (Functor.obj (curriedActionMop C D) x))
            (Quiver.Hom.mop
              { app := fun (x_1 : D) ↦ Iso.hom (αₗ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x x_1), naturality := sorry })
            (Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D)) ▷ Functor.obj (curriedActionMop C D) x))))
      t)
Tactic: ext t
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.End (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x : C
⊢ Eq (α :=
    Quiver.Hom (V := (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (Functor.obj (curriedActionMop C D) x)
      (tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
        ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory))))
    (Iso.inv (ρ_ (Functor.obj (curriedActionMop C D) x)))
    (CategoryStruct.comp (Y :=
      Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
      (Functor.map (curriedActionMop C D) (Iso.inv (ρ_ x)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
          (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Quiver.Hom.mop
          { app := fun (x_1 : D) ↦ Iso.hom (αₗ x (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x_1), naturality := ⋯ })
        (Functor.obj (curriedActionMop C D) x ◁ Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D)))))
have h : Eq (α :=
  Quiver.Hom (V := Functor.{v_2, v_2, u_2, u_2} D D) (unmop (Functor.obj (curriedActionMop C D) x))
    (unmop
      (tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
        ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory)))))
  (Quiver.Hom.unmop (Iso.inv (ρ_ (Functor.obj (curriedActionMop C D) x))))
  (Quiver.Hom.unmop
    (CategoryStruct.comp (Y :=
      Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
      (Functor.map (curriedActionMop C D) (Iso.inv (ρ_ x)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
          (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Quiver.Hom.mop
          { app := fun (x_1 : D) ↦ Iso.hom (αₗ x (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x_1), naturality := sorry })
        (Functor.obj (curriedActionMop C D) x ◁ Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D))))))
Tactic: apply MonoidalOpposite.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.End (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x : C
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_2, v_2, u_2, u_2} D D) (unmop (Functor.obj (curriedActionMop C D) x))
      (unmop
        (tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
          ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory)))))
    (Quiver.Hom.unmop (Iso.inv (ρ_ (Functor.obj (curriedActionMop C D) x))))
    (Quiver.Hom.unmop
      (CategoryStruct.comp (Y :=
        Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Functor.map (curriedActionMop C D) (Iso.inv (ρ_ x)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
            (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
          (Quiver.Hom.mop
            { app := fun (x_1 : D) ↦ Iso.hom (αₗ x (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x_1), naturality := ⋯ })
          (Functor.obj (curriedActionMop C D) x ◁ Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D))))))
have h : ∀ (t : D),
  Eq.{v_2 + 1} (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (unmop (Functor.obj (curriedActionMop C D) x)) t ⟶
      Functor.obj.{v_2, v_2, u_2, u_2}
        (unmop
          (tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
            ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory))))
        t)
    (NatTrans.app (Quiver.Hom.unmop (Iso.inv (ρ_ (Functor.obj (curriedActionMop C D) x)))) t)
    (NatTrans.app
      (Quiver.Hom.unmop
        (CategoryStruct.comp (Y :=
          Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
          (Functor.map (curriedActionMop C D) (Iso.inv (ρ_ x)))
          (CategoryStruct.comp (Y :=
            tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
              (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
            (Quiver.Hom.mop
              { app := fun (x_1 : D) ↦ Iso.hom (αₗ x (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x_1), naturality := sorry })
            (Functor.obj (curriedActionMop C D) x ◁ Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D))))))
      t)
Tactic: ext t
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.End (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
c₁ c₁' c₂ c₂' : C
c₃ c₃' : D
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂)).unmop.obj c₃ ⟶ (F.obj c₁').unmop.obj ((F.obj c₂').unmop.obj c₃'))
    (CategoryStruct.comp (Y := (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₁' c₂')).unmop.obj c₃')
      (CategoryStruct.comp (Y :=
        (fun (c : C) (d : D) ↦ (F.obj c).unmop.obj d) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁' c₂') c₃)
        ((fun {c c' : C} (f : c ⟶ c') (d : D) ↦ (F.map f).unmop.app d) (f ⊗ₘ g) c₃)
        ((fun (c : C) (x x_1 : D) (f : x ⟶ x_1) ↦ (F.obj c).unmop.map f) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁' c₂') c₃
          c₃' h))
      (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c₁' c₂')) c₃'))))
    (CategoryStruct.comp (Y := (F.obj c₁).unmop.obj ((F.obj c₂).unmop.obj c₃))
      (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c₁ c₂)) c₃)))
      (CategoryStruct.comp (Y := (fun (c : C) (d : D) ↦ (F.obj c).unmop.obj d) c₁' ((F.obj c₂).unmop.obj c₃))
        ((fun {c c' : C} (f : c ⟶ c') (d : D) ↦ (F.map f).unmop.app d) f ((F.obj c₂).unmop.obj c₃))
        ((fun (c : C) (x x_1 : D) (f : x ⟶ x_1) ↦ (F.obj c).unmop.map f) c₁' ((F.obj c₂).unmop.obj c₃)
          ((F.obj c₂').unmop.obj c₃')
          (CategoryStruct.comp (Y := (fun (c : C) (d : D) ↦ (F.obj c).unmop.obj d) c₂' c₃)
            ((fun {c c' : C} (f : c ⟶ c') (d : D) ↦ (F.map f).unmop.app d) g c₃)
            ((fun (c : C) (x x_1 : D) (f : x ⟶ x_1) ↦ (F.obj c).unmop.map f) c₂' c₃ c₃' h)))))
have e : Eq.{v_2 + 1} (α :=
  (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂)).unmop.obj c₃ ⟶
    (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₁') (F.obj c₂')).unmop.obj c₃)
  ((fun
        (t :
          F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) ⟶
            tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₁') (F.obj c₂')) ↦
      t.unmop.app c₃)
    (Functor.OplaxMonoidal.δ F c₁ c₂ ≫ (F.map f ⊗ₘ F.map g)))
  ((fun
        (t :
          F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) ⟶
            tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₁') (F.obj c₂')) ↦
      t.unmop.app c₃)
    (F.map (f ⊗ₘ g) ≫ Functor.OplaxMonoidal.δ F c₁' c₂'))
Tactic: have e := congrArg (fun t ↦ t.unmop.app c₃) <|
      Functor.OplaxMonoidal.δ_natural F f g
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.End (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
c x y : C
f : x ⟶ y
d : D
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c x)).unmop.obj d ⟶
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c y)).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (c ◁ f))) d)
    (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c x)) d)) ≫
      (F.obj c).unmop.map ((F.map f).unmop.app d) ≫
        Iso.inv (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c y)) d)))
have e : Eq.{v_2 + 1} (α :=
  (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c) (F.obj x)).unmop.obj d ⟶
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c y)).unmop.obj d)
  ((fun
        (t :
          tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c) (F.obj x) ⟶
            F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c y)) ↦
      t.unmop.app d)
    (F.obj c ◁ F.map f ≫ Functor.LaxMonoidal.μ F c y))
  ((fun
        (t :
          tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c) (F.obj x) ⟶
            F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c y)) ↦
      t.unmop.app d)
    (Functor.LaxMonoidal.μ F c x ≫ F.map (c ◁ f)))
Tactic: have e := congrArg (fun t ↦ t.unmop.app d) <|
      Functor.LaxMonoidal.μ_natural_right F c f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.End (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
x y c : C
f : x ⟶ y
d : D
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x c)).unmop.obj d ⟶
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) y c)).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (f ▷ c))) d)
    (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F x c)) d)) ≫
      (F.map f).unmop.app ((F.obj c).unmop.obj d) ≫
        Iso.inv (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F y c)) d)))
have e : Eq.{v_2 + 1} (α :=
  (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj x) (F.obj c)).unmop.obj d ⟶
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) y c)).unmop.obj d)
  ((fun
        (t :
          tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj x) (F.obj c) ⟶
            F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) y c)) ↦
      t.unmop.app d)
    (F.map f ▷ F.obj c ≫ Functor.LaxMonoidal.μ F y c))
  ((fun
        (t :
          tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj x) (F.obj c) ⟶
            F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) y c)) ↦
      t.unmop.app d)
    (Functor.LaxMonoidal.μ F x c ≫ F.map (f ▷ c)))
Tactic: have e := congrArg (fun t ↦ t.unmop.app d) <|
      Functor.LaxMonoidal.μ_natural_left F f c
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.End (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
c₁ c₂ c₃ : C
d : D
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)).unmop.obj d ⟶
      (F.obj c₁).unmop.obj ((F.obj c₂).unmop.obj ((F.obj c₃).unmop.obj d)))
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (α_ c₁ c₂ c₃)))) d ≫
      Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))) d)) ≫
        (F.obj c₁).unmop.map (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c₂ c₃)) d))))
    (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)) d)) ≫
      Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c₁ c₂)) ((F.obj c₃).unmop.obj d))))
have e : Eq.{v_2 + 1} (α :=
  (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)).unmop.obj d ⟶
    (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₁)
            (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₂) (F.obj c₃))).unmop.obj
      d)
  ((fun
        (t :
          F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃) ⟶
            tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₁)
              (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₂) (F.obj c₃))) ↦
      t.unmop.app d)
    (Functor.OplaxMonoidal.δ F (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃ ≫
      Functor.OplaxMonoidal.δ F c₁ c₂ ▷ F.obj c₃ ≫ Iso.hom (α_ (F.obj c₁) (F.obj c₂) (F.obj c₃))))
  ((fun
        (t :
          F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃) ⟶
            tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₁)
              (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₂) (F.obj c₃))) ↦
      t.unmop.app d)
    (F.map (Iso.hom (α_ c₁ c₂ c₃)) ≫
      Functor.OplaxMonoidal.δ F c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃) ≫
        F.obj c₁ ◁ Functor.OplaxMonoidal.δ F c₂ c₃))
Tactic: have e := congrArg (fun t ↦ t.unmop.app d) <|
      Functor.OplaxMonoidal.associativity F c₁ c₂ c₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.End (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
c₁ c₂ c₃ : C
d : D
e :
  Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)).unmop.obj d ⟶
      (F.obj c₁).unmop.obj ((F.obj c₂).unmop.obj ((F.obj c₃).unmop.obj d)))
    (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)) d ≫
      NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₁ c₂)) ((F.obj c₃).unmop.obj d) ≫
        𝟙 ((F.obj c₁).unmop.obj ((F.obj c₂).unmop.obj ((F.obj c₃).unmop.obj d))))
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (α_ c₁ c₂ c₃)))) d ≫
      NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))) d ≫
        (F.obj c₁).unmop.map (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₂ c₃)) d))
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)).unmop.obj d ⟶
      (F.obj c₁).unmop.obj ((F.obj c₂).unmop.obj ((F.obj c₃).unmop.obj d)))
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (α_ c₁ c₂ c₃)))) d ≫
      Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))) d)) ≫
        (F.obj c₁).unmop.map (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c₂ c₃)) d))))
    (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)) d)) ≫
      Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c₁ c₂)) ((F.obj c₃).unmop.obj d))))
have e₁ : Eq (α :=
  (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)).unmop.obj d ⟶
    (F.obj c₁).unmop.obj ((F.obj c₂).unmop.obj ((F.obj c₃).unmop.obj d)))
  (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)) d ≫
    NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₁ c₂)) ((F.obj c₃).unmop.obj d))
  (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (α_ c₁ c₂ c₃)))) d ≫
    NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))) d ≫
      (F.obj c₁).unmop.map (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₂ c₃)) d))
Tactic: simp only [Category.comp_id] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.End (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
c : C
d : D
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)).unmop.obj d ⟶
      (F.obj c).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (λ_ c)))) d)
    (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)) d)) ≫
      Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.εIso F)) ((F.obj c).unmop.obj d))))
have e : Eq (α :=
  (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)).unmop.obj d ⟶
    (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory)
            ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := MonoidalOpposite.monoidalOppositeCategory))
            (F.obj c)).unmop.obj
      d)
  (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (λ_ c)))) d ≫
    (fun
          (t :
            F.obj c ⟶
              tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory)
                ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := MonoidalOpposite.monoidalOppositeCategory))
                (F.obj c)) ↦
        t.unmop.app d)
      (Iso.inv (λ_ (F.obj c))))
  (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (λ_ c)))) d ≫
    (fun
          (t :
            F.obj c ⟶
              tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory)
                ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := MonoidalOpposite.monoidalOppositeCategory))
                (F.obj c)) ↦
        t.unmop.app d)
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c))
        (F.map (Iso.inv (λ_ c)))
        (Functor.OplaxMonoidal.δ F (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c ≫ Functor.OplaxMonoidal.η F ▷ F.obj c)))
Tactic: have e := (F.map (λ_ c).hom).unmop.app d ≫=
      (congrArg (fun t ↦ t.unmop.app d) <|
        Functor.OplaxMonoidal.left_unitality F c)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.End (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
c : C
d : D
e :
  Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)).unmop.obj d ⟶
      (F.obj c).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (λ_ c)))) d ≫ 𝟙 ((F.obj c).unmop.obj d))
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (λ_ c)))) d ≫
      CategoryStruct.comp (Y :=
        (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)).unmop.obj d)
        (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.inv (λ_ c)))) d)
        (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)) d ≫
          NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.η F)) ((F.obj c).unmop.obj d)))
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)).unmop.obj d ⟶
      (F.obj c).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (λ_ c)))) d)
    (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)) d)) ≫
      Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.εIso F)) ((F.obj c).unmop.obj d))))
have e₁ : Eq (α :=
  (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)).unmop.obj d ⟶
    (F.obj c).unmop.obj d)
  (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (λ_ c)))) d)
  (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)) d ≫
    NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.η F)) ((F.obj c).unmop.obj d))
Tactic: simp only [Category.comp_id, ← NatTrans.comp_app_assoc, ← unmop_comp,
      ← F.map_comp_assoc, Iso.hom_inv_id, Functor.map_id, Category.id_comp] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.End (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
c : C
d : D
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))).unmop.obj d ⟶
      (F.obj c).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (ρ_ c)))) d)
    (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) d)) ≫
      (F.obj c).unmop.map (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.εIso F)) d))))
have e : Eq (α :=
  (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))).unmop.obj d ⟶
    (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c)
            ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := MonoidalOpposite.monoidalOppositeCategory))).unmop.obj
      d)
  (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (ρ_ c)))) d ≫
    (fun
          (t :
            F.obj c ⟶
              tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c)
                ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := MonoidalOpposite.monoidalOppositeCategory))) ↦
        t.unmop.app d)
      (Iso.inv (ρ_ (F.obj c))))
  (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (ρ_ c)))) d ≫
    (fun
          (t :
            F.obj c ⟶
              tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c)
                ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := MonoidalOpposite.monoidalOppositeCategory))) ↦
        t.unmop.app d)
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (F.map (Iso.inv (ρ_ c)))
        (Functor.OplaxMonoidal.δ F c (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≫ F.obj c ◁ Functor.OplaxMonoidal.η F)))
Tactic: have e := (F.map (ρ_ c).hom).unmop.app d ≫=
      (congrArg (fun t ↦ t.unmop.app d) <|
        Functor.OplaxMonoidal.right_unitality F c)