awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
f : Y ⟶ Z
inst_2 : IsIso f
rw : X ◁ (f ≫ inv f) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)
rw₁ : X ◁ 𝟙 Y = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)
⊢ X ◁ f ≫ X ◁ inv f = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)
have rw₂ : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Y)
  (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)) (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y))
Tactic: rw [← whiskerLeft_comp, IsIso.hom_inv_id, whiskerLeft_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
Z : C
⊢ f ▷ Z ≫ inv f ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
have rw : (f ≫ inv f) ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
Tactic: rw [← comp_whiskerRight, IsIso.hom_inv_id, id_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
Z : C
rw : (f ≫ inv f) ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
⊢ f ▷ Z ≫ inv f ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
have rw₁ : 𝟙 X ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
Tactic: rw [← comp_whiskerRight, IsIso.hom_inv_id, id_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
Z : C
rw : (f ≫ inv f) ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
rw₁ : 𝟙 X ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
⊢ f ▷ Z ≫ inv f ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
have rw₂ : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) X Z)
  (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)) (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z))
Tactic: rw [← comp_whiskerRight, IsIso.hom_inv_id, id_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
f : Y ⟶ Z
inst_2 : IsIso f
⊢ X ◁ inv f ≫ X ◁ f = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
have rw : X ◁ (inv f ≫ f) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
Tactic: rw [← whiskerLeft_comp, IsIso.inv_hom_id, whiskerLeft_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
f : Y ⟶ Z
inst_2 : IsIso f
rw : X ◁ (inv f ≫ f) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
⊢ X ◁ inv f ≫ X ◁ f = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
have rw₁ : X ◁ 𝟙 Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
Tactic: rw [← whiskerLeft_comp, IsIso.inv_hom_id, whiskerLeft_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
f : Y ⟶ Z
inst_2 : IsIso f
rw : X ◁ (inv f ≫ f) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
rw₁ : X ◁ 𝟙 Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
⊢ X ◁ inv f ≫ X ◁ f = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
have rw₂ : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) X Z)
  (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)) (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z))
Tactic: rw [← whiskerLeft_comp, IsIso.inv_hom_id, whiskerLeft_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
Z : C
⊢ inv f ▷ Z ≫ f ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)
have rw : (inv f ≫ f) ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)
Tactic: rw [← comp_whiskerRight, IsIso.inv_hom_id, id_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
Z : C
rw : (inv f ≫ f) ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)
⊢ inv f ▷ Z ≫ f ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)
have rw₁ : 𝟙 Y ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)
Tactic: rw [← comp_whiskerRight, IsIso.inv_hom_id, id_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
Z : C
rw : (inv f ≫ f) ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)
rw₁ : 𝟙 Y ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)
⊢ inv f ▷ Z ≫ f ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)
have rw₂ : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) Y Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z)
  (𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)) (𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z))
Tactic: rw [← comp_whiskerRight, IsIso.inv_hom_id, id_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z)
    (X ◁ if h : P then f h else f' h) (if h : P then X ◁ f h else X ◁ f' h)
have pos : ∀ (h : P), Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (X ◁ f h) (X ◁ f h)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
pos : ∀ (h : P), Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (X ◁ f h) (X ◁ f h)
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z)
    (X ◁ if h : P then f h else f' h) (if h : P then X ◁ f h else X ◁ f' h)
have neg : ∀ (h : ¬P), Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (X ◁ f' h) (X ◁ f' h)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z)
    ((if h : P then f h else f' h) ▷ Z) (if h : P then f h ▷ Z else f' h ▷ Z)
have pos : ∀ (h : P), Eq (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z) (f h ▷ Z) (f h ▷ Z)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
pos : ∀ (h : P), Eq (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z) (f h ▷ Z) (f h ▷ Z)
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z)
    ((if h : P then f h else f' h) ▷ Z) (if h : P then f h ▷ Z else f' h ▷ Z)
have neg : ∀ (h : ¬P), Eq (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z) (f' h ▷ Z) (f' h ▷ Z)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (f ⊗ₘ if h : P then g h else g' h)
    (if h : P then f ⊗ₘ g h else f ⊗ₘ g' h)
have pos : ∀ (h : P), Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (f ⊗ₘ g h) (f ⊗ₘ g h)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
pos : ∀ (h : P), Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (f ⊗ₘ g h) (f ⊗ₘ g h)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (f ⊗ₘ if h : P then g h else g' h)
    (if h : P then f ⊗ₘ g h else f ⊗ₘ g' h)
have neg : ∀ (h : ¬P), Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (f ⊗ₘ g' h) (f ⊗ₘ g' h)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Y W ⟶ tensorObj.{v, u} (𝒞 := inst) Z X) ((if h : P then g h else g' h) ⊗ₘ f)
    (if h : P then g h ⊗ₘ f else g' h ⊗ₘ f)
have pos : ∀ (h : P), Eq (α := tensorObj.{v, u} (𝒞 := inst) Y W ⟶ tensorObj.{v, u} (𝒞 := inst) Z X) (g h ⊗ₘ f) (g h ⊗ₘ f)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
pos : ∀ (h : P), Eq (α := tensorObj.{v, u} (𝒞 := inst) Y W ⟶ tensorObj.{v, u} (𝒞 := inst) Z X) (g h ⊗ₘ f) (g h ⊗ₘ f)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Y W ⟶ tensorObj.{v, u} (𝒞 := inst) Z X) ((if h : P then g h else g' h) ⊗ₘ f)
    (if h : P then g h ⊗ₘ f else g' h ⊗ₘ f)
have neg : ∀ (h : ¬P), Eq (α := tensorObj.{v, u} (𝒞 := inst) Y W ⟶ tensorObj.{v, u} (𝒞 := inst) Z X) (g' h ⊗ₘ f) (g' h ⊗ₘ f)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
f : Y = Z
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (X ◁ eqToHom f) (eqToHom ⋯)
have refl : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Y) (X ◁ eqToHom sorry) (eqToHom sorry)
Tactic: cases f
Cleared hypotheses: Z, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X = Y
Z : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z) (eqToHom f ▷ Z) (eqToHom ⋯)
have refl : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (eqToHom sorry ▷ Z) (eqToHom sorry)
Tactic: cases f
Cleared hypotheses: Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X Y Z : C
⊢ Iso.inv (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫
      Iso.inv (α_ W X Y) ▷ Z ≫ hom (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) =
    W ◁ hom (α_ X Y Z) ≫ Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z))
have rw : (W ◁ Iso.inv (α_ X Y Z) ≫
      Iso.inv (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫
        Iso.inv (α_ W X Y) ▷ Z ≫ hom (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z)) ≫
    Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) =
  (W ◁ Iso.inv (α_ X Y Z) ≫ W ◁ hom (α_ X Y Z) ≫ Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z))) ≫
    Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z)
Tactic: rw [← cancel_epi (W ◁ (α_ X Y Z).inv), ← cancel_mono (α_ (W ⊗ X) Y Z).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X Y Z : C
⊢ hom (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
      W ◁ Iso.inv (α_ X Y Z) ≫ Iso.inv (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) =
    Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫ hom (α_ W X Y) ▷ Z
have rw : (Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
      hom (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
        W ◁ Iso.inv (α_ X Y Z) ≫ Iso.inv (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z)) ≫
    Iso.inv (α_ W X Y) ▷ Z =
  (Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
      Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫ hom (α_ W X Y) ▷ Z) ≫
    Iso.inv (α_ W X Y) ▷ Z
Tactic: rw [← cancel_epi (α_ W X (Y ⊗ Z)).inv, ← cancel_mono ((α_ W X Y).inv ▷ Z)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) Y) ⟶
      tensorObj.{v, u} (𝒞 := inst) X Y)
    (Iso.inv (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫ hom (ρ_ X) ▷ Y) (X ◁ hom (λ_ Y))
have rw : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) Y) ⟶
    tensorObj.{v, u} (𝒞 := inst) X Y)
  (Iso.inv (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫ hom (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫ X ◁ hom (λ_ Y))
  (X ◁ hom (λ_ Y))
Tactic: rw [← triangle, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
rw :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) Y) ⟶
      tensorObj.{v, u} (𝒞 := inst) X Y)
    (Iso.inv (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫
      hom (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫ X ◁ hom (λ_ Y))
    (X ◁ hom (λ_ Y))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) Y) ⟶
      tensorObj.{v, u} (𝒞 := inst) X Y)
    (Iso.inv (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫ hom (ρ_ X) ▷ Y) (X ◁ hom (λ_ Y))
have rw₁ : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) Y) ⟶
    tensorObj.{v, u} (𝒞 := inst) X Y)
  (X ◁ hom (λ_ Y)) (X ◁ hom (λ_ Y))
Tactic: rw [← triangle, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
⊢ hom (λ_ X) ▷ Y = hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
have rw : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst))
      (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) X Y))
  (tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y)
  (tensorUnit.{v, u} C (𝒞 := inst) ◁
    (hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))))
Tactic: rw [← whiskerLeft_iff, whiskerLeft_comp, ← cancel_epi (α_ _ _ _).hom, ←
      cancel_epi ((α_ _ _ _).hom ▷ _), pentagon_assoc, triangle, ← associator_naturality_middle, ←
      comp_whiskerRight_assoc, triangle, associator_naturality_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst))
        (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) X Y))
    (tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y)
    (tensorUnit.{v, u} C (𝒞 := inst) ◁
      (hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))))
⊢ hom (λ_ X) ▷ Y = hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
have rw₁ : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst))
      (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) X Y))
  (tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y)
  (tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫
    tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y)))
Tactic: rw [← whiskerLeft_iff, whiskerLeft_comp, ← cancel_epi (α_ _ _ _).hom, ←
      cancel_epi ((α_ _ _ _).hom ▷ _), pentagon_assoc, triangle, ← associator_naturality_middle, ←
      comp_whiskerRight_assoc, triangle, associator_naturality_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst))
        (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) X Y))
    (tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y)
    (tensorUnit.{v, u} C (𝒞 := inst) ◁
      (hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))))
rw₁ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst))
        (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) X Y))
    (tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y)
    (tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫
      tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y)))
⊢ hom (λ_ X) ▷ Y = hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
have rw₂ : hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ≫
    tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y =
  hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ≫
    tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫
      tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
Tactic: rw [← whiskerLeft_iff, whiskerLeft_comp, ← cancel_epi (α_ _ _ _).hom, ←
      cancel_epi ((α_ _ _ _).hom ▷ _), pentagon_assoc, triangle, ← associator_naturality_middle, ←
      comp_whiskerRight_assoc, triangle, associator_naturality_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst))
        (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) X Y))
    (tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y)
    (tensorUnit.{v, u} C (𝒞 := inst) ◁
      (hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))))
rw₁ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst))
        (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) X Y))
    (tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y)
    (tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫
      tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y)))
rw₂ :
  hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ≫
      tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y =
    hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ≫
      tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫
        tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
⊢ hom (λ_ X) ▷ Y = hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
have rw₃ : hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)) X) ▷ Y ≫
    hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ≫
      tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y =
  hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)) X) ▷ Y ≫
    hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ≫
      tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫
        tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
Tactic: rw [← whiskerLeft_iff, whiskerLeft_comp, ← cancel_epi (α_ _ _ _).hom, ←
      cancel_epi ((α_ _ _ _).hom ▷ _), pentagon_assoc, triangle, ← associator_naturality_middle, ←
      comp_whiskerRight_assoc, triangle, associator_naturality_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
⊢ X ◁ hom (ρ_ Y) = Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))) ≫ hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
have rw : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst)
      (tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))))
      (tensorUnit.{v, u} C (𝒞 := inst)) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) (tensorUnit.{v, u} C (𝒞 := inst)))
  ((X ◁ hom (ρ_ Y)) ▷ tensorUnit.{v, u} C (𝒞 := inst))
  ((Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))) ≫ hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X Y))) ▷
    tensorUnit.{v, u} C (𝒞 := inst))
Tactic: rw [← whiskerRight_iff, comp_whiskerRight, ← cancel_epi (α_ _ _ _).inv, ←
      cancel_epi (X ◁ (α_ _ _ _).inv), pentagon_inv_assoc, triangle_assoc_comp_right, ←
      associator_inv_naturality_middle, ← whiskerLeft_comp_assoc, triangle_assoc_comp_right,
      associator_inv_naturality_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst)
        (tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))))
        (tensorUnit.{v, u} C (𝒞 := inst)) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) (tensorUnit.{v, u} C (𝒞 := inst)))
    ((X ◁ hom (ρ_ Y)) ▷ tensorUnit.{v, u} C (𝒞 := inst))
    ((Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))) ≫ hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X Y))) ▷
      tensorUnit.{v, u} C (𝒞 := inst))
⊢ X ◁ hom (ρ_ Y) = Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))) ≫ hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
have rw₁ : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst)
      (tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))))
      (tensorUnit.{v, u} C (𝒞 := inst)) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) (tensorUnit.{v, u} C (𝒞 := inst)))
  ((X ◁ hom (ρ_ Y)) ▷ tensorUnit.{v, u} C (𝒞 := inst))
  (Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))) ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
    hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X Y)) ▷ tensorUnit.{v, u} C (𝒞 := inst))
Tactic: rw [← whiskerRight_iff, comp_whiskerRight, ← cancel_epi (α_ _ _ _).inv, ←
      cancel_epi (X ◁ (α_ _ _ _).inv), pentagon_inv_assoc, triangle_assoc_comp_right, ←
      associator_inv_naturality_middle, ← whiskerLeft_comp_assoc, triangle_assoc_comp_right,
      associator_inv_naturality_right]