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