awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) 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 ≫ 𝟙 ((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) c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))).unmop.obj d)
        (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.inv (ρ_ c)))) d)
        (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) d ≫
          (F.obj c).unmop.map (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.η F)) 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 ⟶
    (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 c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) d ≫
    (F.obj c).unmop.map (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.η F)) 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 (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 : MonoidalRightAction.{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 (curriedAction C D) x)
      (tensorObj (𝒞 := Functor.category) ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)) (𝒞 := Functor.category))
        (Functor.obj (curriedAction C D) x)))
    (Iso.inv (λ_ (Functor.obj (curriedAction C D) x)))
    (CategoryStruct.comp (Y :=
      Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))
      (Functor.map (curriedAction C D) (Iso.inv (λ_ x)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
          (Functor.obj (curriedAction C D) x))
        { app := fun (x_1 : D) ↦ Iso.hom (αᵣ x_1 (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x), naturality := ⋯ }
        (Iso.hom (actionUnitNatIso C D) ▷ Functor.obj (curriedAction C D) x)))
have w : ∀ (t : D),
  Eq.{v_2 + 1} (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (Functor.obj (curriedAction C D) x) t ⟶
      Functor.obj.{v_2, v_2, u_2, u_2}
        (tensorObj (𝒞 := Functor.category) ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)) (𝒞 := Functor.category))
          (Functor.obj (curriedAction C D) x))
        t)
    (NatTrans.app (Iso.inv (λ_ (Functor.obj (curriedAction C D) x))) t)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))
        (Functor.map (curriedAction C D) (Iso.inv (λ_ x)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
            (Functor.obj (curriedAction C D) x))
          { app := fun (x_1 : D) ↦ Iso.hom (αᵣ x_1 (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x), naturality := sorry }
          (Iso.hom (actionUnitNatIso C D) ▷ Functor.obj (curriedAction 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 : MonoidalRightAction.{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 (curriedAction C D) x)
      (tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) x)
        ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)) (𝒞 := Functor.category))))
    (Iso.inv (ρ_ (Functor.obj (curriedAction C D) x)))
    (CategoryStruct.comp (Y :=
      Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
      (Functor.map (curriedAction C D) (Iso.inv (ρ_ x)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) x)
          (Functor.obj (curriedAction C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        { app := fun (x_1 : D) ↦ Iso.hom (αᵣ x_1 x (tensorUnit.{v_1, u_1} C (𝒞 := inst))), naturality := ⋯ }
        (Functor.obj (curriedAction C D) x ◁ Iso.hom (actionUnitNatIso C D))))
have w : ∀ (t : D),
  Eq.{v_2 + 1} (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (Functor.obj (curriedAction C D) x) t ⟶
      Functor.obj.{v_2, v_2, u_2, u_2}
        (tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) x)
          ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)) (𝒞 := Functor.category)))
        t)
    (NatTrans.app (Iso.inv (ρ_ (Functor.obj (curriedAction C D) x))) t)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Functor.map (curriedAction C D) (Iso.inv (ρ_ x)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) x)
            (Functor.obj (curriedAction C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
          { app := fun (x_1 : D) ↦ Iso.hom (αᵣ x_1 x (tensorUnit.{v_1, u_1} C (𝒞 := inst))), naturality := sorry }
          (Functor.obj (curriedAction C D) x ◁ 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₁' : D
c₂ c₂' c₃ c₃' : C
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
⊢ Eq (α := (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)).obj c₁ ⟶ (F.obj c₃').obj ((F.obj c₂').obj c₁'))
    (CategoryStruct.comp (Y := (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₂' c₃')).obj c₁')
      (CategoryStruct.comp (Y := (fun (d : D) (c : C) ↦ (F.obj c).obj d) c₁' (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))
        ((fun {d d' : D} (f : d ⟶ d') (c : C) ↦ (F.obj c).map f) f (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))
        ((fun (d : D) (x x_1 : C) (f : x ⟶ x_1) ↦ (F.map f).app d) c₁' (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)
          (tensorObj.{v_1, u_1} (𝒞 := inst) c₂' c₃') (g ⊗ₘ h)))
      (Iso.hom (Iso.symm (Iso.app (Functor.Monoidal.μIso F c₂' c₃') c₁'))))
    (CategoryStruct.comp (Y := (F.obj c₃).obj ((F.obj c₂).obj c₁))
      (Iso.hom (Iso.symm (Iso.app (Functor.Monoidal.μIso F c₂ c₃) c₁)))
      (CategoryStruct.comp (Y := (fun (d : D) (c : C) ↦ (F.obj c).obj d) ((F.obj c₂').obj c₁') c₃)
        ((fun {d d' : D} (f : d ⟶ d') (c : C) ↦ (F.obj c).map f)
          (CategoryStruct.comp (Y := (fun (d : D) (c : C) ↦ (F.obj c).obj d) c₁' c₂)
            ((fun {d d' : D} (f : d ⟶ d') (c : C) ↦ (F.obj c).map f) f c₂)
            ((fun (d : D) (x x_1 : C) (f : x ⟶ x_1) ↦ (F.map f).app d) c₁' c₂ c₂' g))
          c₃)
        ((fun (d : D) (x x_1 : C) (f : x ⟶ x_1) ↦ (F.map f).app d) ((F.obj c₂').obj c₁') c₃ c₃' h)))
have e : Eq.{v_2 + 1} (α :=
  (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)).obj c₁ ⟶
    (tensorObj (𝒞 := Functor.category) (F.obj c₂') (F.obj c₃')).obj c₁)
  ((fun
        (t :
          F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃) ⟶ tensorObj (𝒞 := Functor.category) (F.obj c₂') (F.obj c₃')) ↦
      t.app c₁)
    (Functor.OplaxMonoidal.δ F c₂ c₃ ≫ (F.map g ⊗ₘ F.map h)))
  ((fun
        (t :
          F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃) ⟶ tensorObj (𝒞 := Functor.category) (F.obj c₂') (F.obj c₃')) ↦
      t.app c₁)
    (F.map (g ⊗ₘ h) ≫ Functor.OplaxMonoidal.δ F c₂' c₃'))
Tactic: have e := congrArg (fun t ↦ t.app c₁) <|
      Functor.OplaxMonoidal.δ_natural F g h
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Opposites (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
c c' : Cᵒᵖ
d d' : Dᵒᵖ
f : unop c' ⟶ unop c
g : unop d' ⟶ unop d
⊢ Eq (α :=
    op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c) (unop d)) ⟶
      op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c') (unop d')))
    (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ₗₘ Quiver.Hom.unop (op g)))
    (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊵ₗ unop d) ≫ Quiver.Hom.op (unop c' ⊴ₗ Quiver.Hom.unop (op g)))
have a : Eq (α :=
  unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c') (unop d'))) ⟶
    unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c) (unop d))))
  (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ₗₘ Quiver.Hom.unop (op g))))
  (Quiver.Hom.unop
    (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊵ₗ unop d) ≫ Quiver.Hom.op (unop c' ⊴ₗ Quiver.Hom.unop (op g))))
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Opposites (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
c₁ c₂ c₃ c₄ : Cᵒᵖ
d₁ d₂ : Dᵒᵖ
f : unop c₂ ⟶ unop c₁
g : unop c₄ ⟶ unop c₃
h : unop d₂ ⟶ unop d₁
⊢ Eq (α :=
    op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c₁ c₃)) (unop d₁)) ⟶
      op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₂)
          (unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₄) (unop d₂))))))
    (Quiver.Hom.op (Quiver.Hom.unop (op f ⊗ₘ op g) ⊙ₗₘ Quiver.Hom.unop (op h)) ≫
      Iso.hom (Iso.op (Iso.symm (αₗ (unop c₂) (unop c₄) (unop d₂)))))
    (Iso.hom (Iso.op (Iso.symm (αₗ (unop c₁) (unop c₃) (unop d₁)))) ≫
      Quiver.Hom.op
        (Quiver.Hom.unop (op f) ⊙ₗₘ
          Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (op g) ⊙ₗₘ Quiver.Hom.unop (op h)))))
have a : Eq (α :=
  unop
      (op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₂)
          (unop
            (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₄) (unop d₂)))))) ⟶
    unop
      (op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c₁ c₃)) (unop d₁))))
  (Quiver.Hom.unop
    (Quiver.Hom.op (Quiver.Hom.unop (op f ⊗ₘ op g) ⊙ₗₘ Quiver.Hom.unop (op h)) ≫
      Iso.hom (Iso.op (Iso.symm (αₗ (unop c₂) (unop c₄) (unop d₂))))))
  (Quiver.Hom.unop
    (Iso.hom (Iso.op (Iso.symm (αₗ (unop c₁) (unop c₃) (unop d₁)))) ≫
      Quiver.Hom.op
        (Quiver.Hom.unop (op f) ⊙ₗₘ
          Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (op g) ⊙ₗₘ Quiver.Hom.unop (op h))))))
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Opposites (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
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c₁ c₂ c₃ c₄ : Cᵒᵖ
d₁ d₂ : Dᵒᵖ
f : unop c₂ ⟶ unop c₁
g : unop c₄ ⟶ unop c₃
h : unop d₂ ⟶ unop d₁
⊢ Eq (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₂)
            (unop
              (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₄) (unop d₂)))))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c₁ c₃)) (unop d₁))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (op f ⊗ₘ op g) ⊙ₗₘ Quiver.Hom.unop (op h)) ≫
        Iso.hom (Iso.op (Iso.symm (αₗ (unop c₂) (unop c₄) (unop d₂))))))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (αₗ (unop c₁) (unop c₃) (unop d₁)))) ≫
        Quiver.Hom.op
          (Quiver.Hom.unop (op f) ⊙ₗₘ
            Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (op g) ⊙ₗₘ Quiver.Hom.unop (op h))))))
have this : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₂)
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₄) (unop d₂)) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₁)
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₃) (unop d₁)))
  (Iso.inv (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ (unop c₁) (unop c₃) (unop d₁)))
  (Iso.inv (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ Iso.hom (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ (f ⊙ₗₘ g ⊙ₗₘ h))
Tactic: haveI := (αₗ (unop _) (unop _) (unop _)).inv ≫=
          MonoidalLeftAction.actionAssocIso_hom_naturality f g h
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Opposites (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
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c₁ c₂ c₃ c₄ : Cᵒᵖ
d₁ d₂ : Dᵒᵖ
f : unop c₂ ⟶ unop c₁
g : unop c₄ ⟶ unop c₃
h : unop d₂ ⟶ unop d₁
this :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₂)
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₄) (unop d₂)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₁)
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₃) (unop d₁)))
    (Iso.inv (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ (unop c₁) (unop c₃) (unop d₁)))
    (Iso.inv (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ Iso.hom (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ (f ⊙ₗₘ g ⊙ₗₘ h))
⊢ Eq (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₂)
            (unop
              (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₄) (unop d₂)))))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c₁ c₃)) (unop d₁))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (op f ⊗ₘ op g) ⊙ₗₘ Quiver.Hom.unop (op h)) ≫
        Iso.hom (Iso.op (Iso.symm (αₗ (unop c₂) (unop c₄) (unop d₂))))))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (αₗ (unop c₁) (unop c₃) (unop d₁)))) ≫
        Quiver.Hom.op
          (Quiver.Hom.unop (op f) ⊙ₗₘ
            Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (op g) ⊙ₗₘ Quiver.Hom.unop (op h))))))
have this₁ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₂)
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₄) (unop d₂)) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₁)
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₃) (unop d₁)))
  (Iso.inv (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ (unop c₁) (unop c₃) (unop d₁)))
  (f ⊙ₗₘ g ⊙ₗₘ h)
Tactic: simp only [Iso.inv_hom_id_assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Opposites (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
d d' : Dᵒᵖ
x : d ⟶ d'
⊢ Eq (α :=
    op
        (@actionObj.{v_1, u_1, v_2, u_2} C _ inst inst_2 toMonoidalCategoryStruct _
          (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) (unop d)) ⟶
      d')
    (Iso.hom (Iso.op (Iso.symm (λₗ (unop d)))) ≫ x)
    (Quiver.Hom.op (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)) ⊴ₗ x.unop) ≫
      Iso.hom (Iso.op (Iso.symm (λₗ (unop d')))))
have a : Eq (α :=
  unop d' ⟶
    unop
      (op
        (@actionObj.{v_1, u_1, v_2, u_2} C _ inst inst_2 toMonoidalCategoryStruct _
          (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) (unop d))))
  (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (λₗ (unop d)))) ≫ x))
  (Quiver.Hom.unop
    (Quiver.Hom.op (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)) ⊴ₗ x.unop) ≫
      Iso.hom (Iso.op (Iso.symm (λₗ (unop d'))))))
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Opposites (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
c c' x : Cᵒᵖ
x_1 : c ⟶ c'
x_2 : Dᵒᵖ
⊢ Eq.{v_2 + 1} (α :=
    op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c x)) (unop x_2)) ⟶
      op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c' x)) (unop x_2)))
    (Quiver.Hom.op (Quiver.Hom.unop (x_1 ▷ x) ⊵ₗ unop x_2))
    (Iso.hom (Iso.op (Iso.symm (αₗ (unop c) (unop x) (unop x_2)))) ≫
      Quiver.Hom.op
          (x_1.unop ⊵ₗ
            unop
              (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x) (unop x_2)))) ≫
        Iso.inv (Iso.op (Iso.symm (αₗ (unop c') (unop x) (unop x_2)))))
have a : Eq.{v_2 + 1} (α :=
  unop
      (op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c' x)) (unop x_2))) ⟶
    unop
      (op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c x)) (unop x_2))))
  (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (x_1 ▷ x) ⊵ₗ unop x_2)))
  (Quiver.Hom.unop
    (Iso.hom (Iso.op (Iso.symm (αₗ (unop c) (unop x) (unop x_2)))) ≫
      Quiver.Hom.op
          (x_1.unop ⊵ₗ
            unop
              (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x) (unop x_2)))) ≫
        Iso.inv (Iso.op (Iso.symm (αₗ (unop c') (unop x) (unop x_2))))))
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Opposites (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 x_1 x_2 : Cᵒᵖ
x_3 : Dᵒᵖ
⊢ Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2)) ⊵ₗ unop x_3) ≫
      Iso.hom
          (Iso.op (Iso.symm (αₗ (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2)) (unop x_3)))) ≫
        Quiver.Hom.op (unop x ⊴ₗ Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αₗ (unop x_1) (unop x_2) (unop x_3)))))) =
    Iso.hom
        (Iso.op (Iso.symm (αₗ (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2) (unop x_3)))) ≫
      Iso.hom
        (Iso.op
          (Iso.symm
            (αₗ (unop x) (unop x_1)
              (unop
                (op
                  (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_2)
                    (unop x_3)))))))
have a : Quiver.Hom.unop
    (Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2)) ⊵ₗ unop x_3) ≫
      Iso.hom
          (Iso.op (Iso.symm (αₗ (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2)) (unop x_3)))) ≫
        Quiver.Hom.op (unop x ⊴ₗ Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αₗ (unop x_1) (unop x_2) (unop x_3))))))) =
  (Iso.hom (Iso.op (Iso.symm (αₗ (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2) (unop x_3)))) ≫
      Iso.hom
        (Iso.op
          (Iso.symm
            (αₗ (unop x) (unop x_1)
              (unop
                (op
                  (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_2)
                    (unop x_3)))))))).unop
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Opposites (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 x_1 x_2 : Cᵒᵖ
x_3 : Dᵒᵖ
⊢ Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2)) ⊵ₗ unop x_3) ≫
        Iso.hom
            (Iso.op
              (Iso.symm (αₗ (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2)) (unop x_3)))) ≫
          Quiver.Hom.op
            (unop x ⊴ₗ Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αₗ (unop x_1) (unop x_2) (unop x_3))))))) =
    (Iso.hom
          (Iso.op (Iso.symm (αₗ (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2) (unop x_3)))) ≫
        Iso.hom
          (Iso.op
            (Iso.symm
              (αₗ (unop x) (unop x_1)
                (unop
                  (op
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_2)
                      (unop x_3)))))))).unop
have a : Eq.{v_2 + 1} (α :=
  unop
      (op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
          (unop
            (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1) x_2))
          (unop x_3))) ⟶
    unop
      (op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x)
          (unop
            (op
              (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
                (unop
                  (op
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_2)
                      (unop x_3))))))))))
  (inv
    (Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2)) ⊵ₗ unop x_3) ≫
        Iso.hom
            (Iso.op
              (Iso.symm (αₗ (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2)) (unop x_3)))) ≫
          Quiver.Hom.op
            (unop x ⊴ₗ Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αₗ (unop x_1) (unop x_2) (unop x_3)))))))))
  (inv
    (Iso.hom
          (Iso.op (Iso.symm (αₗ (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2) (unop x_3)))) ≫
        Iso.hom
          (Iso.op
            (Iso.symm
              (αₗ (unop x) (unop x_1)
                (unop
                  (op
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_2)
                      (unop x_3)))))))).unop)
Tactic: apply IsIso.inv_eq_inv.mp