awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Arrow.{v, u} C
f : X ⟶ Y
⊢ Eq (α := tensorObj (𝒞 := instCategoryArrow) ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)) X ⟶ Y)
    ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow) ◁ f ≫ Iso.hom (λ_ Y)) (Iso.hom (λ_ X) ≫ f)
have refine : Eq (α :=
  obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
      X.right ⟶
    Y.left)
  (CategoryStruct.comp (Y :=
    pushout (X :=
      obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        X.left)
      (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
      (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
    (pushout.inr
      (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
      (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
    (Arrow.Hom.left ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow) ◁ f ≫ Iso.hom (λ_ Y))))
  (CategoryStruct.comp (Y :=
    pushout (X :=
      obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        X.left)
      (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
      (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
    (pushout.inr
      (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
      (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
    (Arrow.Hom.left (Iso.hom (λ_ X) ≫ f)))
Tactic: refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp) ?_) (by simp)
-- 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 : Arrow.{v, u} C
f : X ⟶ Y
⊢ Eq (α := tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)) ⟶ Y)
    (f ▷ (𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow) ≫ Iso.hom (ρ_ Y)) (Iso.hom (ρ_ X) ≫ f)
have refine : Eq (α :=
  obj.{v, v, u, u} (obj (curriedTensor C) X.right)
      (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))) ⟶
    Y.left)
  (CategoryStruct.comp (Y :=
    pushout (X :=
      obj.{v, v, u, u} (obj (curriedTensor C) X.left)
        (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
      (NatTrans.app (map (curriedTensor C) X.hom) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
      (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
    (pushout.inl
      (NatTrans.app (map (curriedTensor C) X.hom) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
      (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
    (Arrow.Hom.left (f ▷ (𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow) ≫ Iso.hom (ρ_ Y))))
  (CategoryStruct.comp (Y :=
    pushout (X :=
      obj.{v, v, u, u} (obj (curriedTensor C) X.left)
        (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
      (NatTrans.app (map (curriedTensor C) X.hom) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
      (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
    (pushout.inl
      (NatTrans.app (map (curriedTensor C) X.hom) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
      (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
    (Arrow.Hom.left (Iso.hom (ρ_ X) ≫ f)))
Tactic: refine Arrow.hom_ext _ _ (pushout.hom_ext ?_ (by simp)) (by simp)
-- 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
W X Y Z : Arrow.{v, u} C
⊢ Iso.hom (α_ W X Y) ▷ Z ≫ Iso.hom (α_ W (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ W ◁ Iso.hom (α_ X Y Z) =
    Iso.hom (α_ (tensorObj (𝒞 := instCategoryArrow) W X) Y Z) ≫
      Iso.hom (α_ W X (tensorObj (𝒞 := instCategoryArrow) Y Z))
have refine : CategoryStruct.comp (Y :=
    pushout (X :=
      obj.{v, v, u, u}
        (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).left)
        Z.left)
      (NatTrans.app
        (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).hom)
        Z.left)
      (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).left)
        Z.hom))
    (pushout.inr
      (NatTrans.app
        (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).hom)
        Z.left)
      (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).left)
        Z.hom))
    (Arrow.Hom.left
      (Iso.hom (α_ W X Y) ▷ Z ≫ Iso.hom (α_ W (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ W ◁ Iso.hom (α_ X Y Z))) =
  pushout.inr
      (NatTrans.app
        (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).hom)
        Z.left)
      (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).left)
        Z.hom) ≫
    Arrow.Hom.left
      (Iso.hom (α_ (tensorObj (𝒞 := instCategoryArrow) W X) Y Z) ≫
        Iso.hom (α_ W X (tensorObj (𝒞 := instCategoryArrow) Y Z)))
Tactic: refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp) ?_) (by simp)
-- 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 : Arrow.{v, u} C
⊢ Eq (α :=
    tensorObj (𝒞 := instCategoryArrow)
        (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))) Y ⟶
      tensorObj (𝒞 := instCategoryArrow) X Y)
    (Iso.hom (α_ X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)) Y) ≫ X ◁ Iso.hom (λ_ Y)) (Iso.hom (ρ_ X) ▷ Y)
have refine : Eq (α :=
  obj.{v, v, u, u}
      (obj (curriedTensor C)
        (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
      Y.right ⟶
    (tensorObj (𝒞 := instCategoryArrow) X Y).left)
  (CategoryStruct.comp (Y :=
    pushout (X :=
      obj.{v, v, u, u}
        (obj (curriedTensor C)
          (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
        Y.left)
      (NatTrans.app
        (map (curriedTensor C)
          (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
        Y.left)
      (map
        (obj (curriedTensor C)
          (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
        Y.hom))
    (pushout.inr
      (NatTrans.app
        (map (curriedTensor C)
          (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
        Y.left)
      (map
        (obj (curriedTensor C)
          (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
        Y.hom))
    (Arrow.Hom.left (Iso.hom (α_ X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)) Y) ≫ X ◁ Iso.hom (λ_ Y))))
  (CategoryStruct.comp (Y :=
    pushout (X :=
      obj.{v, v, u, u}
        (obj (curriedTensor C)
          (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
        Y.left)
      (NatTrans.app
        (map (curriedTensor C)
          (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
        Y.left)
      (map
        (obj (curriedTensor C)
          (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
        Y.hom))
    (pushout.inr
      (NatTrans.app
        (map (curriedTensor C)
          (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
        Y.left)
      (map
        (obj (curriedTensor C)
          (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
        Y.hom))
    (Arrow.Hom.left (Iso.hom (ρ_ X) ▷ Y)))
Tactic: refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp) ?_) (by simp)
-- 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 : Arrow.{v, u} C
⊢ Eq (α :=
    tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) X Y) Z ⟶
      tensorObj (𝒞 := instCategoryArrow) Y (tensorObj (𝒞 := instCategoryArrow) Z X))
    (Iso.hom (α_ X Y Z) ≫ Iso.hom (braiding X (tensorObj (𝒞 := instCategoryArrow) Y Z)) ≫ Iso.hom (α_ Y Z X))
    (Iso.hom (braiding X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (braiding X Z))
have refine : Eq (α :=
  obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.right ⟶
    (tensorObj (𝒞 := instCategoryArrow) Y (tensorObj (𝒞 := instCategoryArrow) Z X)).left)
  (CategoryStruct.comp (Y :=
    pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.left)
      (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
      (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
    (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
      (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
    (Arrow.Hom.left
      (Iso.hom (α_ X Y Z) ≫ Iso.hom (braiding X (tensorObj (𝒞 := instCategoryArrow) Y Z)) ≫ Iso.hom (α_ Y Z X))))
  (CategoryStruct.comp (Y :=
    pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.left)
      (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
      (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
    (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
      (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
    (Arrow.Hom.left (Iso.hom (braiding X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (braiding X Z))))
Tactic: refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp) ?_) (by simp)
-- 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 : Arrow.{v, u} C
⊢ Eq (α :=
    tensorObj (𝒞 := instCategoryArrow) X (tensorObj (𝒞 := instCategoryArrow) Y Z) ⟶
      tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) Z X) Y)
    (Iso.inv (α_ X Y Z) ≫ Iso.hom (braiding (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ Iso.inv (α_ Z X Y))
    (X ◁ Iso.hom (braiding Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (braiding X Z) ▷ Y)
have refine : Eq (α :=
  obj.{v, v, u, u} (obj (curriedTensor C) X.right) (tensorObj (𝒞 := instCategoryArrow) Y Z).left ⟶
    (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) Z X) Y).left)
  (CategoryStruct.comp (Y :=
    pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
      (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
      (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
    (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
      (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
    (Arrow.Hom.left
      (Iso.inv (α_ X Y Z) ≫ Iso.hom (braiding (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ Iso.inv (α_ Z X Y))))
  (CategoryStruct.comp (Y :=
    pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
      (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
      (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
    (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
      (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
    (Arrow.Hom.left (X ◁ Iso.hom (braiding Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (braiding X Z) ▷ Y)))
Tactic: refine Arrow.hom_ext _ _ (pushout.hom_ext ?_ (by simp)) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft
have rw : (Q.actLeft ≫ f.inv) ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_left_act_hom, ← Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id,
          whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actLeft ≫ f.inv) ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
⊢ Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft
have rw₁ : Q.actLeft ≫ f.inv ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_left_act_hom, ← Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id,
          whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actLeft ≫ f.inv) ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₁ : Q.actLeft ≫ f.inv ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
⊢ Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft
have rw₂ : Q.actLeft ≫ f.inv ≫ f.hom = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_left_act_hom, ← Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id,
          whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actLeft ≫ f.inv) ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₁ : Q.actLeft ≫ f.inv ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₂ : Q.actLeft ≫ f.inv ≫ f.hom = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
⊢ Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft
have rw₃ : Q.actLeft ≫ 𝟙 Q.X = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_left_act_hom, ← Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id,
          whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actLeft ≫ f.inv) ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₁ : Q.actLeft ≫ f.inv ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₂ : Q.actLeft ≫ f.inv ≫ f.hom = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₃ : Q.actLeft ≫ 𝟙 Q.X = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
⊢ Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft
have rw₄ : Q.actLeft = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_left_act_hom, ← Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id,
          whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actLeft ≫ f.inv) ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₁ : Q.actLeft ≫ f.inv ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₂ : Q.actLeft ≫ f.inv ≫ f.hom = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₃ : Q.actLeft ≫ 𝟙 Q.X = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₄ : Q.actLeft = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
⊢ Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft
have rw₅ : Q.actLeft = X.X ◁ f.inv ≫ X.X ◁ f.hom ≫ Q.actLeft
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_left_act_hom, ← Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id,
          whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actLeft ≫ f.inv) ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₁ : Q.actLeft ≫ f.inv ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₂ : Q.actLeft ≫ f.inv ≫ f.hom = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₃ : Q.actLeft ≫ 𝟙 Q.X = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₄ : Q.actLeft = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₅ : Q.actLeft = X.X ◁ f.inv ≫ X.X ◁ f.hom ≫ Q.actLeft
⊢ Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft
have rw₆ : Q.actLeft = (X.X ◁ f.inv ≫ X.X ◁ f.hom) ≫ Q.actLeft
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_left_act_hom, ← Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id,
          whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actLeft ≫ f.inv) ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₁ : Q.actLeft ≫ f.inv ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₂ : Q.actLeft ≫ f.inv ≫ f.hom = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₃ : Q.actLeft ≫ 𝟙 Q.X = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₄ : Q.actLeft = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₅ : Q.actLeft = X.X ◁ f.inv ≫ X.X ◁ f.hom ≫ Q.actLeft
rw₆ : Q.actLeft = (X.X ◁ f.inv ≫ X.X ◁ f.hom) ≫ Q.actLeft
⊢ Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft
have rw₇ : Q.actLeft = X.X ◁ (f.inv ≫ f.hom) ≫ Q.actLeft
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_left_act_hom, ← Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id,
          whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actLeft ≫ f.inv) ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₁ : Q.actLeft ≫ f.inv ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₂ : Q.actLeft ≫ f.inv ≫ f.hom = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₃ : Q.actLeft ≫ 𝟙 Q.X = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₄ : Q.actLeft = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₅ : Q.actLeft = X.X ◁ f.inv ≫ X.X ◁ f.hom ≫ Q.actLeft
rw₆ : Q.actLeft = (X.X ◁ f.inv ≫ X.X ◁ f.hom) ≫ Q.actLeft
rw₇ : Q.actLeft = X.X ◁ (f.inv ≫ f.hom) ≫ Q.actLeft
⊢ Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft
have rw₈ : Q.actLeft = X.X ◁ 𝟙 Q.X ≫ Q.actLeft
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_left_act_hom, ← Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id,
          whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actLeft ≫ f.inv) ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₁ : Q.actLeft ≫ f.inv ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₂ : Q.actLeft ≫ f.inv ≫ f.hom = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₃ : Q.actLeft ≫ 𝟙 Q.X = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₄ : Q.actLeft = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₅ : Q.actLeft = X.X ◁ f.inv ≫ X.X ◁ f.hom ≫ Q.actLeft
rw₆ : Q.actLeft = (X.X ◁ f.inv ≫ X.X ◁ f.hom) ≫ Q.actLeft
rw₇ : Q.actLeft = X.X ◁ (f.inv ≫ f.hom) ≫ Q.actLeft
rw₈ : Q.actLeft = X.X ◁ 𝟙 Q.X ≫ Q.actLeft
⊢ Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft
have rw₉ : Q.actLeft = 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X.X Q.X) ≫ Q.actLeft
Tactic: rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_left_act_hom, ← Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id,
          whiskerLeft_id, Category.id_comp]