awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : C
x_1 : D
⊢ Eq.{v_2 + 1} (α :=
    op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x)
            (op x_1))) ⟶
      op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
            (op (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) (op x_1))))
    (Quiver.Hom.op (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (ρ_ x)) ⊵ₗ op x_1)))
    (Quiver.Hom.op
      (Iso.hom (Iso.unop (Iso.symm (αₗ (op x) (op (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (op x_1)))) ≫
        Quiver.Hom.unop (op x ⊴ₗ Quiver.Hom.op (Iso.hom (Iso.unop (Iso.symm (λₗ (op x_1))))))))
have a : Eq.{v_2 + 1} (α :=
  op
      (unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) (op x_1))) ⟶
    op
      (unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x)
          (op x_1))))
  (inv (Quiver.Hom.op (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (ρ_ x)) ⊵ₗ op x_1))))
  (inv
    (Quiver.Hom.op
      (Iso.hom (Iso.unop (Iso.symm (αₗ (op x) (op (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (op x_1)))) ≫
        Quiver.Hom.unop (op x ⊴ₗ Quiver.Hom.op (Iso.hom (Iso.unop (Iso.symm (λₗ (op x_1)))))))))
Tactic: apply IsIso.inv_eq_inv.mp
-- 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
c c' : Cᵒᵖ
d d' : Dᵒᵖ
f : unop d' ⟶ unop d
g : unop c' ⟶ unop c
⊢ Eq (α :=
    op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d) (unop c)) ⟶
      op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d') (unop c')))
    (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g)))
    (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊵ᵣ unop c) ≫ Quiver.Hom.op (unop d' ⊴ᵣ Quiver.Hom.unop (op g)))
have a : Eq (α :=
  unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d') (unop c'))) ⟶
    unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d) (unop c))))
  (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 c) ≫ Quiver.Hom.op (unop d' ⊴ᵣ 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d₁ d₂ : Dᵒᵖ
c₁ c₂ c₃ c₄ : Cᵒᵖ
f : unop d₂ ⟶ unop d₁
g : unop c₂ ⟶ unop c₁
h : unop c₄ ⟶ unop c₃
⊢ Eq (α :=
    op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₁)
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c₁ c₃))) ⟶
      op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
          (unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₂) (unop c₂))))
          (unop c₄)))
    (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g ⊗ₘ op h)) ≫
      Iso.hom (Iso.op (Iso.symm (αᵣ (unop d₂) (unop c₂) (unop c₄)))))
    (Iso.hom (Iso.op (Iso.symm (αᵣ (unop d₁) (unop c₁) (unop c₃)))) ≫
      Quiver.Hom.op
        (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ 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 (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₂) (unop c₂))))
          (unop c₄))) ⟶
    unop
      (op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₁)
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c₁ c₃)))))
  (Quiver.Hom.unop
    (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g ⊗ₘ op h)) ≫
      Iso.hom (Iso.op (Iso.symm (αᵣ (unop d₂) (unop c₂) (unop c₄))))))
  (Quiver.Hom.unop
    (Iso.hom (Iso.op (Iso.symm (αᵣ (unop d₁) (unop c₁) (unop c₃)))) ≫
      Quiver.Hom.op
        (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d₁ d₂ : Dᵒᵖ
c₁ c₂ c₃ c₄ : Cᵒᵖ
f : unop d₂ ⟶ unop d₁
g : unop c₂ ⟶ unop c₁
h : unop c₄ ⟶ unop c₃
⊢ Eq (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₂) (unop c₂))))
            (unop c₄))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₁)
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c₁ c₃)))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g ⊗ₘ op h)) ≫
        Iso.hom (Iso.op (Iso.symm (αᵣ (unop d₂) (unop c₂) (unop c₄))))))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (αᵣ (unop d₁) (unop c₁) (unop c₃)))) ≫
        Quiver.Hom.op
          (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ 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 _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₂) (unop c₂)) (unop c₄) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₁) (unop c₁)) (unop c₃))
  (Iso.inv (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ (unop d₁) (unop c₁) (unop c₃)))
  (Iso.inv (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ Iso.hom (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h))
Tactic: haveI := (αᵣ (unop _) (unop _) (unop _)).inv ≫=
          MonoidalRightAction.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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d₁ d₂ : Dᵒᵖ
c₁ c₂ c₃ c₄ : Cᵒᵖ
f : unop d₂ ⟶ unop d₁
g : unop c₂ ⟶ unop c₁
h : unop c₄ ⟶ unop c₃
this :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₂) (unop c₂)) (unop c₄) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₁) (unop c₁)) (unop c₃))
    (Iso.inv (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ (unop d₁) (unop c₁) (unop c₃)))
    (Iso.inv (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ Iso.hom (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h))
⊢ Eq (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₂) (unop c₂))))
            (unop c₄))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₁)
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c₁ c₃)))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g ⊗ₘ op h)) ≫
        Iso.hom (Iso.op (Iso.symm (αᵣ (unop d₂) (unop c₂) (unop c₄))))))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (αᵣ (unop d₁) (unop c₁) (unop c₃)))) ≫
        Quiver.Hom.op
          (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ 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 _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₂) (unop c₂)) (unop c₄) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₁) (unop c₁)) (unop c₃))
  (Iso.inv (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ (unop d₁) (unop c₁) (unop c₃)))
  ((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 : MonoidalRightAction.{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 d)
          (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)))) ⟶
      d')
    (Iso.hom (Iso.op (Iso.symm (ρᵣ (unop d)))) ≫ x)
    (Quiver.Hom.op (x.unop ⊵ᵣ unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) ≫
      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 d)
          (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))))))
  (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρᵣ (unop d)))) ≫ x))
  (Quiver.Hom.unop
    (Quiver.Hom.op (x.unop ⊵ᵣ unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) ≫
      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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x x_1 x_2 : Cᵒᵖ
x_3 : x_1 ⟶ x_2
x_4 : Dᵒᵖ
⊢ Eq.{v_2 + 1} (α :=
    op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_4)
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1))) ⟶
      op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_4)
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_2))))
    (Quiver.Hom.op (unop x_4 ⊴ᵣ Quiver.Hom.unop (x ◁ x_3)))
    (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_4) (unop x) (unop x_1)))) ≫
      Quiver.Hom.op
          (unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_4) (unop x))) ⊴ᵣ
            x_3.unop) ≫
        Iso.inv (Iso.op (Iso.symm (αᵣ (unop x_4) (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 x_4)
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_2)))) ⟶
    unop
      (op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_4)
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)))))
  (Quiver.Hom.unop (Quiver.Hom.op (unop x_4 ⊴ᵣ Quiver.Hom.unop (x ◁ x_3))))
  (Quiver.Hom.unop
    (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_4) (unop x) (unop x_1)))) ≫
      Quiver.Hom.op
          (unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_4) (unop x))) ⊴ᵣ
            x_3.unop) ≫
        Iso.inv (Iso.op (Iso.symm (αᵣ (unop x_4) (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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x x_1 x_2 : Cᵒᵖ
x_3 : Dᵒᵖ
⊢ Quiver.Hom.op (unop x_3 ⊴ᵣ Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2))) ≫
      Iso.hom
          (Iso.op (Iso.symm (αᵣ (unop x_3) (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2))))) ≫
        Iso.hom
          (Iso.op
            (Iso.symm
              (αᵣ
                (unop
                  (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3) (unop x))))
                (unop x_1) (unop x_2)))) =
    Iso.hom
        (Iso.op (Iso.symm (αᵣ (unop x_3) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2)))) ≫
      Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_3) (unop x) (unop x_1))))) ⊵ᵣ 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
            (op
              (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
                (unop
                  (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3) (unop x))))
                (unop x_1))))
          (unop x_2))) ⟶
    unop
      (op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3)
          (unop
            (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)
              x_2)))))
  (Quiver.Hom.unop
    (Quiver.Hom.op (unop x_3 ⊴ᵣ Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2))) ≫
      Iso.hom
          (Iso.op (Iso.symm (αᵣ (unop x_3) (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2))))) ≫
        Iso.hom
          (Iso.op
            (Iso.symm
              (αᵣ
                (unop
                  (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3) (unop x))))
                (unop x_1) (unop x_2))))))
  (Quiver.Hom.unop
    (Iso.hom
        (Iso.op (Iso.symm (αᵣ (unop x_3) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2)))) ≫
      Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_3) (unop x) (unop x_1))))) ⊵ᵣ 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : Cᵒᵖ
x_1 : Dᵒᵖ
⊢ Eq.{v_2 + 1} (α :=
    op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
          (unop
            (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)) x))) ⟶
      op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1) (unop x)))
    (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (λ_ x))))
    (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_1) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) (unop x)))) ≫
      Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρᵣ (unop x_1))))) ⊵ᵣ unop x))
have a : Eq.{v_2 + 1} (α :=
  unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1) (unop x))) ⟶
    unop
      (op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
          (unop
            (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)) x)))))
  (Quiver.Hom.unop (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (λ_ x)))))
  (Quiver.Hom.unop
    (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_1) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) (unop x)))) ≫
      Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρᵣ (unop x_1))))) ⊵ᵣ unop x)))
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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : Cᵒᵖ
x_1 : Dᵒᵖ
⊢ Eq.{v_2 + 1} (α :=
    unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1) (unop x))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
            (unop
              (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)) x)))))
    (Quiver.Hom.unop (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (λ_ x)))))
    (Quiver.Hom.unop
      (Iso.hom
          (Iso.op (Iso.symm (αᵣ (unop x_1) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) (unop x)))) ≫
        Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρᵣ (unop x_1))))) ⊵ᵣ unop x)))
have a : Eq.{v_2 + 1} (α :=
  unop
      (op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
          (unop
            (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)) x)))) ⟶
    unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1) (unop x))))
  (inv (Quiver.Hom.unop (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (λ_ x))))))
  (inv
    (Quiver.Hom.unop
      (Iso.hom
          (Iso.op (Iso.symm (αᵣ (unop x_1) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) (unop x)))) ≫
        Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρᵣ (unop x_1))))) ⊵ᵣ unop x))))
Tactic: apply IsIso.inv_eq_inv.mp
-- 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : Cᵒᵖ
x_1 : Dᵒᵖ
⊢ Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (ρ_ x))) =
    Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_1) (unop x) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)))))) ≫
      Iso.hom
        (Iso.op
          (Iso.symm
            (ρᵣ
              (unop
                (op
                  (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1) (unop x)))))))
have a : Quiver.Hom.unop (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (ρ_ x)))) =
  (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_1) (unop x) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)))))) ≫
      Iso.hom
        (Iso.op
          (Iso.symm
            (ρᵣ
              (unop
                (op
                  (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
                    (unop x)))))))).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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : Cᵒᵖ
x_1 : Dᵒᵖ
⊢ Quiver.Hom.unop (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (ρ_ x)))) =
    (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_1) (unop x) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)))))) ≫
        Iso.hom
          (Iso.op
            (Iso.symm
              (ρᵣ
                (unop
                  (op
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
                      (unop x)))))))).unop
have a : Eq.{v_2 + 1} (α :=
  unop
      (op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
          (unop
            (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)))))) ⟶
    unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1) (unop x))))
  (inv (Quiver.Hom.unop (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (ρ_ x))))))
  (inv
    (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_1) (unop x) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)))))) ≫
        Iso.hom
          (Iso.op
            (Iso.symm
              (ρᵣ
                (unop
                  (op
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
                      (unop x)))))))).unop)
Tactic: apply IsIso.inv_eq_inv.mp
-- 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} Cᵒᵖ Dᵒᵖ
c c' : C
d d' : D
f : d ⟶ d'
g : c ⟶ c'
⊢ Eq.{v_2 + 1} (α :=
    unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d)
          (op c)) ⟶
      unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d')
          (op c')))
    (Quiver.Hom.unop (f.op ⊙ᵣₘ g.op))
    (CategoryStruct.comp (Y :=
      unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d')
          (op c)))
      (Quiver.Hom.unop (f.op ⊵ᵣ op c)) (Quiver.Hom.unop (op d' ⊴ᵣ g.op)))
have a : Eq.{v_2 + 1} (α :=
  op
      (unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d')
          (op c'))) ⟶
    op
      (unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d)
          (op c))))
  (Quiver.Hom.op (Quiver.Hom.unop (f.op ⊙ᵣₘ g.op)))
  (Quiver.Hom.op
    (CategoryStruct.comp (Y :=
      unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d')
          (op c)))
      (Quiver.Hom.unop (f.op ⊵ᵣ op c)) (Quiver.Hom.unop (op d' ⊴ᵣ g.op))))
Tactic: apply Quiver.Hom.op_inj