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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} Cᵒᵖ Dᵒᵖ
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
⊢ Eq.{v_2 + 1} (α :=
    unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₁)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃))) ⟶
      unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
          (op
            (unop
              (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                (op d₂) (op c₂))))
          (op c₄)))
    (Quiver.Hom.unop (f.op ⊙ᵣₘ Quiver.Hom.op (g ⊗ₘ h)) ≫ Iso.hom (Iso.unop (Iso.symm (αᵣ (op d₂) (op c₂) (op c₄)))))
    (Iso.hom (Iso.unop (Iso.symm (αᵣ (op d₁) (op c₁) (op c₃)))) ≫
      Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (f.op ⊙ᵣₘ 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
            (unop
              (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                (op d₂) (op c₂))))
          (op c₄))) ⟶
    op
      (unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₁)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃)))))
  (Quiver.Hom.op
    (Quiver.Hom.unop (f.op ⊙ᵣₘ Quiver.Hom.op (g ⊗ₘ h)) ≫ Iso.hom (Iso.unop (Iso.symm (αᵣ (op d₂) (op c₂) (op c₄))))))
  (Quiver.Hom.op
    (Iso.hom (Iso.unop (Iso.symm (αᵣ (op d₁) (op c₁) (op c₃)))) ≫
      Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (f.op ⊙ᵣₘ 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} Cᵒᵖ Dᵒᵖ
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
⊢ Eq.{v_2 + 1} (α :=
    op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
            (op
              (unop
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                  (op d₂) (op c₂))))
            (op c₄))) ⟶
      op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₁)
            (op (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃)))))
    (Quiver.Hom.op
      (Quiver.Hom.unop (f.op ⊙ᵣₘ Quiver.Hom.op (g ⊗ₘ h)) ≫ Iso.hom (Iso.unop (Iso.symm (αᵣ (op d₂) (op c₂) (op c₄))))))
    (Quiver.Hom.op
      (Iso.hom (Iso.unop (Iso.symm (αᵣ (op d₁) (op c₁) (op c₃)))) ≫
        Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (f.op ⊙ᵣₘ g.op)) ⊙ᵣₘ h.op)))
have this : Eq.{v_2 + 1} (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₂)
        (op c₂))
      (op c₄) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₁)
        (op c₁))
      (op c₃))
  (Iso.inv (αᵣ (op d₂) (op c₂) (op c₄)) ≫ (f.op ⊙ᵣₘ g.op ⊗ₘ h.op) ≫ Iso.hom (αᵣ (op d₁) (op c₁) (op c₃)))
  (Iso.inv (αᵣ (op d₂) (op c₂) (op c₄)) ≫ Iso.hom (αᵣ (op d₂) (op c₂) (op c₄)) ≫ ((f.op ⊙ᵣₘ g.op) ⊙ᵣₘ h.op))
Tactic: haveI := (αᵣ (op _) (op _) (op _)).inv ≫=
      MonoidalRightAction.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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} Cᵒᵖ Dᵒᵖ
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
this :
  Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₂)
          (op c₂))
        (op c₄) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₁)
          (op c₁))
        (op c₃))
    (Iso.inv (αᵣ (op d₂) (op c₂) (op c₄)) ≫ (f.op ⊙ᵣₘ g.op ⊗ₘ h.op) ≫ Iso.hom (αᵣ (op d₁) (op c₁) (op c₃)))
    (Iso.inv (αᵣ (op d₂) (op c₂) (op c₄)) ≫ Iso.hom (αᵣ (op d₂) (op c₂) (op c₄)) ≫ ((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
              (unop
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                  (op d₂) (op c₂))))
            (op c₄))) ⟶
      op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₁)
            (op (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃)))))
    (Quiver.Hom.op
      (Quiver.Hom.unop (f.op ⊙ᵣₘ Quiver.Hom.op (g ⊗ₘ h)) ≫ Iso.hom (Iso.unop (Iso.symm (αᵣ (op d₂) (op c₂) (op c₄))))))
    (Quiver.Hom.op
      (Iso.hom (Iso.unop (Iso.symm (αᵣ (op d₁) (op c₁) (op c₃)))) ≫
        Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (f.op ⊙ᵣₘ g.op)) ⊙ᵣₘ h.op)))
have this₁ : Eq.{v_2 + 1} (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₂)
        (op c₂))
      (op c₄) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₁)
        (op c₁))
      (op c₃))
  (Iso.inv (αᵣ (op d₂) (op c₂) (op c₄)) ≫ (f.op ⊙ᵣₘ g.op ⊗ₘ h.op) ≫ Iso.hom (αᵣ (op d₁) (op c₁) (op c₃)))
  ((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 : MonoidalRightAction.{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 d)
          (op (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) ⟶
      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 d')
          (op (tensorUnit.{v_1, u_1} C (𝒞 := inst)))))
      (Quiver.Hom.unop (x.op ⊵ᵣ op (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) (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 d)
          (op (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
  (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 d')
          (op (tensorUnit.{v_1, u_1} C (𝒞 := inst)))))
      (Quiver.Hom.unop (x.op ⊵ᵣ op (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
      (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 : 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} (α :=
    unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_4)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) x x_1))) ⟶
      unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_4)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) x x_2))))
    (Quiver.Hom.unop (op x_4 ⊴ᵣ Quiver.Hom.op (x ◁ x_3)))
    (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_4) (op x) (op x_1)))) ≫
      Quiver.Hom.unop
          (op
              (unop
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                  (op x_4) (op x))) ⊴ᵣ
            x_3.op) ≫
        Iso.inv (Iso.unop (Iso.symm (αᵣ (op x_4) (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 x_4)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) x x_2)))) ⟶
    op
      (unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_4)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) x x_1)))))
  (Quiver.Hom.op (Quiver.Hom.unop (op x_4 ⊴ᵣ Quiver.Hom.op (x ◁ x_3))))
  (Quiver.Hom.op
    (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_4) (op x) (op x_1)))) ≫
      Quiver.Hom.unop
          (op
              (unop
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                  (op x_4) (op x))) ⊴ᵣ
            x_3.op) ≫
        Iso.inv (Iso.unop (Iso.symm (αᵣ (op x_4) (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 : MonoidalRightAction.{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 x_1)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))) ⟶
      unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_1)
          (op x)))
    (Quiver.Hom.unop (op x_1 ⊴ᵣ Quiver.Hom.op (Iso.hom (λ_ x))))
    (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_1) (op (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (op x)))) ≫
      Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (Iso.unop (Iso.symm (ρᵣ (op x_1))))) ⊵ᵣ op x))
have a : Eq.{v_2 + 1} (α :=
  op
      (unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_1)
          (op x))) ⟶
    op
      (unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_1)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x)))))
  (Quiver.Hom.op (Quiver.Hom.unop (op x_1 ⊴ᵣ Quiver.Hom.op (Iso.hom (λ_ x)))))
  (Quiver.Hom.op
    (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_1) (op (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (op x)))) ≫
      Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (Iso.unop (Iso.symm (ρᵣ (op x_1))))) ⊵ᵣ op x)))
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 : MonoidalRightAction.{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_1)
            (op x))) ⟶
      op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_1)
            (op (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x)))))
    (Quiver.Hom.op (Quiver.Hom.unop (op x_1 ⊴ᵣ Quiver.Hom.op (Iso.hom (λ_ x)))))
    (Quiver.Hom.op
      (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_1) (op (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (op x)))) ≫
        Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (Iso.unop (Iso.symm (ρᵣ (op x_1))))) ⊵ᵣ op x)))
have a : Eq.{v_2 + 1} (α :=
  op
      (unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_1)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x)))) ⟶
    op
      (unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_1)
          (op x))))
  (inv (Quiver.Hom.op (Quiver.Hom.unop (op x_1 ⊴ᵣ Quiver.Hom.op (Iso.hom (λ_ x))))))
  (inv
    (Quiver.Hom.op
      (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_1) (op (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (op x)))) ≫
        Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (Iso.unop (Iso.symm (ρᵣ (op x_1))))) ⊵ᵣ op 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.unop (op x_1 ⊴ᵣ Quiver.Hom.op (Iso.hom (ρ_ x))) =
    Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_1) (op x) (op (tensorUnit.{v_1, u_1} C (𝒞 := inst)))))) ≫
      Iso.hom
        (Iso.unop
          (Iso.symm
            (ρᵣ
              (op
                (unop
                  (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                    (op x_1) (op x)))))))
have a : Quiver.Hom.op (Quiver.Hom.unop (op x_1 ⊴ᵣ Quiver.Hom.op (Iso.hom (ρ_ x)))) =
  (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_1) (op x) (op (tensorUnit.{v_1, u_1} C (𝒞 := inst)))))) ≫
      Iso.hom
        (Iso.unop
          (Iso.symm
            (ρᵣ
              (op
                (unop
                  (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                    (op x_1) (op x)))))))).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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} Cᵒᵖ Dᵒᵖ
x : C
x_1 : D
⊢ Quiver.Hom.op (Quiver.Hom.unop (op x_1 ⊴ᵣ Quiver.Hom.op (Iso.hom (ρ_ x)))) =
    (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_1) (op x) (op (tensorUnit.{v_1, u_1} C (𝒞 := inst)))))) ≫
        Iso.hom
          (Iso.unop
            (Iso.symm
              (ρᵣ
                (op
                  (unop
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                      (op x_1) (op x)))))))).op
have a : Eq.{v_2 + 1} (α :=
  op
      (unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_1)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst)))))) ⟶
    op
      (unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_1)
          (op x))))
  (inv (Quiver.Hom.op (Quiver.Hom.unop (op x_1 ⊴ᵣ Quiver.Hom.op (Iso.hom (ρ_ x))))))
  (inv
    (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_1) (op x) (op (tensorUnit.{v_1, u_1} C (𝒞 := inst)))))) ≫
        Iso.hom
          (Iso.unop
            (Iso.symm
              (ρᵣ
                (op
                  (unop
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                      (op x_1) (op x)))))))).op)
Tactic: apply IsIso.inv_eq_inv.mp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Arrow (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Eq (α := tensorObj (𝒞 := instCategoryArrow) X₁ X₂ ⟶ tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂)
    ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)
have refine : Eq (α := (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left ⟶ (tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂).left)
  (Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))) (Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂))
Tactic: refine Arrow.hom_ext _ _ ?_ (by simp [whisker_exchange_assoc])
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Arrow (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Eq (α := (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left ⟶ (tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂).left)
    (Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))) (Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂))
have h₀ : Eq (α := obj.{v, v, u, u} (obj (curriedTensor C) X₁.right) X₂.left ⟶ (tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂).left)
  (CategoryStruct.comp (Y :=
    pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
      (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
    (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
    (Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))))
  (CategoryStruct.comp (Y :=
    pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
      (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
    (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
    (Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)))
Tactic: apply pushout.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Arrow (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
h₀ :
  Eq (α := obj.{v, v, u, u} (obj (curriedTensor C) X₁.right) X₂.left ⟶ (tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂).left)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
        (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
        (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)))
⊢ Eq (α := (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left ⟶ (tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂).left)
    (Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))) (Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂))
have h₁ : Eq (α := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.right ⟶ (tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂).left)
  (CategoryStruct.comp (Y :=
    pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
      (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
    (pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
    (Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))))
  (CategoryStruct.comp (Y :=
    pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
      (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
    (pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
    (Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)))
Tactic: apply pushout.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Arrow (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Eq (α :=
    tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂) X₃ ⟶
      tensorObj (𝒞 := instCategoryArrow) Y₁ (tensorObj (𝒞 := instCategoryArrow) Y₂ Y₃))
    (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)) (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))
have refine : Eq (α :=
  obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.right ⟶
    (tensorObj (𝒞 := instCategoryArrow) Y₁ (tensorObj (𝒞 := instCategoryArrow) Y₂ Y₃)).left)
  (CategoryStruct.comp (Y :=
    pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.left)
      (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
      (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
    (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
      (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
    (Arrow.Hom.left (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃))))
  (CategoryStruct.comp (Y :=
    pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.left)
      (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
      (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
    (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
      (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
    (Arrow.Hom.left (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))))
Tactic: refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp [whisker_exchange_assoc]) ?_) (by simp)