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 : 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))
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))
⊢ 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) X
      (tensorObj.{v, u} (𝒞 := inst) (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)))
  (Iso.inv (α_ X (tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
    (X ◁ hom (ρ_ Y)) ▷ tensorUnit.{v, u} C (𝒞 := inst))
  (Iso.inv (α_ X (tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))) (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]
-- 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 X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X' Y') Z')
    ((f ⊗ₘ g) ⊗ₘ h) (hom (α_ X Y Z) ≫ (f ⊗ₘ g ⊗ₘ h) ≫ Iso.inv (α_ X' Y' Z'))
have rw : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X' Y') Z')
  ((f ⊗ₘ g) ⊗ₘ h) (hom (α_ X Y Z) ≫ Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ g) ⊗ₘ h))
Tactic: rw [associator_inv_naturality, hom_inv_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 X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X' Y') Z')
    ((f ⊗ₘ g) ⊗ₘ h) (hom (α_ X Y Z) ≫ Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ g) ⊗ₘ h))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X' Y') Z')
    ((f ⊗ₘ g) ⊗ₘ h) (hom (α_ X Y Z) ≫ (f ⊗ₘ g ⊗ₘ h) ≫ Iso.inv (α_ X' Y' Z'))
have rw₁ : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X' Y') Z')
  ((f ⊗ₘ g) ⊗ₘ h) ((f ⊗ₘ g) ⊗ₘ h)
Tactic: rw [associator_inv_naturality, hom_inv_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 X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) X' (tensorObj.{v, u} (𝒞 := inst) Y' Z'))
    (f ⊗ₘ g ⊗ₘ h) (Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ g) ⊗ₘ h) ≫ hom (α_ X' Y' Z'))
have rw : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) X' (tensorObj.{v, u} (𝒞 := inst) Y' Z'))
  (f ⊗ₘ g ⊗ₘ h) (Iso.inv (α_ X Y Z) ≫ hom (α_ X Y Z) ≫ (f ⊗ₘ g ⊗ₘ h))
Tactic: rw [associator_naturality, 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 X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) X' (tensorObj.{v, u} (𝒞 := inst) Y' Z'))
    (f ⊗ₘ g ⊗ₘ h) (Iso.inv (α_ X Y Z) ≫ hom (α_ X Y Z) ≫ (f ⊗ₘ g ⊗ₘ h))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) X' (tensorObj.{v, u} (𝒞 := inst) Y' Z'))
    (f ⊗ₘ g ⊗ₘ h) (Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ g) ⊗ₘ h) ≫ hom (α_ X' Y' Z'))
have rw₁ : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) X' (tensorObj.{v, u} (𝒞 := inst) Y' Z'))
  (f ⊗ₘ g ⊗ₘ h) (f ⊗ₘ g ⊗ₘ h)
Tactic: rw [associator_naturality, 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 Z Z' : C
h : Z ⟶ Z'
⊢ (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) ⊗ₘ h) ≫ hom (α_ X Y Z') = hom (α_ X Y Z) ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ h)
have rw : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z'))
  (((𝟙 X ⊗ₘ 𝟙 Y) ⊗ₘ h) ≫ hom (α_ X Y Z')) (hom (α_ X Y Z) ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ h))
Tactic: rw [← id_tensorHom_id, associator_naturality]
-- 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 Z' : C
h : Z ⟶ Z'
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z'))
    (((𝟙 X ⊗ₘ 𝟙 Y) ⊗ₘ h) ≫ hom (α_ X Y Z')) (hom (α_ X Y Z) ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ h))
⊢ (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) ⊗ₘ h) ≫ hom (α_ X Y Z') = hom (α_ X Y Z) ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ h)
have rw₁ : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z'))
  (hom (α_ X Y Z) ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ h)) (hom (α_ X Y Z) ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ h))
Tactic: rw [← id_tensorHom_id, associator_naturality]
-- 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 X' : C
f : X ⟶ X'
⊢ (f ⊗ₘ 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.inv (α_ X' Y Z) = Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z)
have rw : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X' Y) Z)
  ((f ⊗ₘ 𝟙 Y ⊗ₘ 𝟙 Z) ≫ Iso.inv (α_ X' Y Z)) (Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z))
Tactic: rw [← id_tensorHom_id, associator_inv_naturality]
-- 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 X' : C
f : X ⟶ X'
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X' Y) Z)
    ((f ⊗ₘ 𝟙 Y ⊗ₘ 𝟙 Z) ≫ Iso.inv (α_ X' Y Z)) (Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z))
⊢ (f ⊗ₘ 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.inv (α_ X' Y Z) = Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z)
have rw₁ : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X' Y) Z)
  (Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z)) (Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z))
Tactic: rw [← id_tensorHom_id, associator_inv_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X_1 Y_1 Z X Y : C
f g : X ⟶ Y
h :
  Eq (α :=
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (Functor.obj (tensoringLeft C) X) (Functor.obj (tensoringLeft C) Y))
    (Functor.map (tensoringLeft C) f) (Functor.map (tensoringLeft C) g)
⊢ f = g
have h₁ : Eq (α := (Y_2 : C) → tensorObj.{v, u} (𝒞 := inst) X Y_2 ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y_2) (fun (Y_2 : C) ↦ f ▷ Y_2)
  fun (Y_2 : C) ↦ g ▷ Y_2
Tactic: injections h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X_1 Y_1 Z X Y : C
f g : X ⟶ Y
h :
  Eq (α := (Y_2 : C) → tensorObj.{v, u} (𝒞 := inst) X Y_2 ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y_2)
    (fun (Y_2 : C) ↦ f ▷ Y_2) fun (Y_2 : C) ↦ g ▷ Y_2
⊢ f = g
have h₁ : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst)) ⟶
    tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst)))
  (f ▷ tensorUnit.{v, u} C (𝒞 := inst)) (g ▷ tensorUnit.{v, u} C (𝒞 := inst))
Tactic: replace h := congr_fun h (𝟙_ C)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X_1 Y_1 Z X Y : C
f g : X ⟶ Y
h :
  Eq (α :=
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (Functor.obj (tensoringRight C) X) (Functor.obj (tensoringRight C) Y))
    (Functor.map (tensoringRight C) f) (Functor.map (tensoringRight C) g)
⊢ f = g
have h₁ : Eq (α :=
  (j : C) →
    Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) j) X ⟶
      Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) j) Y)
  (fun (j : C) ↦ Functor.map (Functor.obj (curriedTensor C) j) f) fun (j : C) ↦
  Functor.map (Functor.obj (curriedTensor C) j) g
Tactic: injections h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X_1 Y_1 Z X Y : C
f g : X ⟶ Y
h :
  Eq (α :=
    (j : C) →
      Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) j) X ⟶
        Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) j) Y)
    (fun (j : C) ↦ Functor.map (Functor.obj (curriedTensor C) j) f) fun (j : C) ↦
    Functor.map (Functor.obj (curriedTensor C) j) g
⊢ f = g
have h₁ : Eq (α :=
  Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) (tensorUnit.{v, u} C (𝒞 := inst))) X ⟶
    Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) (tensorUnit.{v, u} C (𝒞 := inst))) Y)
  (Functor.map (Functor.obj (curriedTensor C) (tensorUnit.{v, u} C (𝒞 := inst))) f)
  (Functor.map (Functor.obj (curriedTensor C) (tensorUnit.{v, u} C (𝒞 := inst))) g)
Tactic: replace h := congr_fun h (𝟙_ C)
Cleared hypotheses: h
-- 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 : ObjectProperty.{v, u} C
tensorUnit : P (MonoidalCategoryStruct.tensorUnit.{v, u} C (𝒞 := inst))
tensorObj : ∀ (X Y : C), P X → P Y → P (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) X Y)
X₁ Y₁ X₂ Y₂ : P.FullSubcategory
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
⊢ Eq.{v + 1} (α :=
    FullSubcategory.mk (P := P)
        (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (X₁.obj (P := P)) (X₂.obj (P := P))) ⋯ ⟶
      FullSubcategory.mk (P := P)
        (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (Y₁.obj (P := P)) (Y₂.obj (P := P))) ⋯)
    (homMk (P := P) (x.hom ⊗ₘ x_1.hom))
    (CategoryStruct.comp (Y :=
      FullSubcategory.mk (P := P)
        (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (Y₁.obj (P := P)) (X₂.obj (P := P))) ⋯)
      (homMk (P := P) (x.hom ▷ X₂.obj (P := P))) (homMk (P := P) (Y₁.obj (P := P) ◁ x_1.hom)))
have h : Eq.{v + 1} (α :=
  (FullSubcategory.mk (P := P) (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (X₁.obj (P := P)) (X₂.obj (P := P)))
          sorry).obj
      (P := P) ⟶
    (FullSubcategory.mk (P := P)
          (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (Y₁.obj (P := P)) (Y₂.obj (P := P))) sorry).obj
      (P := P))
  (InducedCategory.Hom.hom (homMk (P := P) (x.hom ⊗ₘ x_1.hom)))
  (InducedCategory.Hom.hom
    (CategoryStruct.comp (Y :=
      FullSubcategory.mk (P := P)
        (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (Y₁.obj (P := P)) (X₂.obj (P := P))) sorry)
      (homMk (P := P) (x.hom ▷ X₂.obj (P := P))) (homMk (P := P) (Y₁.obj (P := P) ◁ x_1.hom))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Center.{v₁, u₁} C
f g : X ⟶ Y
w : f.f = g.f
⊢ f = g
have mk : ∀ (f : X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ⟶ Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
  (comm :
    ∀ (U : C),
      f ▷ U ≫ (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
        (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫ U ◁ f)
  (w : { f := f, comm := comm : X.Hom Y }.f = g.f), { f := f, comm := comm : X.Hom Y } = g
Tactic: cases f
Cleared hypotheses: f, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Center.{v₁, u₁} C
g : X ⟶ Y
f : X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ⟶ Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)
comm :
  ∀ (U : C),
    f ▷ U ≫ (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
      (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫ U ◁ f
w : { f := f, comm := comm : X.Hom Y }.f = g.f
⊢ { f := f, comm := comm : X.Hom Y } = g
have mk : ∀ (f_1 : X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ⟶ Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
  (comm_1 :
    ∀ (U : C),
      f_1 ▷ U ≫ (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
        (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫ U ◁ f_1)
  (w : { f := f, comm := comm : X.Hom Y }.f = { f := f_1, comm := comm_1 }.f),
  { f := f, comm := comm : X.Hom Y } = { f := f_1, comm := comm_1 }
Tactic: cases g
Cleared hypotheses: g, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Center.{v₁, u₁} C
f : X ⟶ Y
inst_2 : IsIso f.f
⊢ IsIso f
have change : IsIso (isoMk f).hom
Tactic: change IsIso (isoMk f).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y₁ Y₂ : Center.{v₁, u₁} C
f : Y₁ ⟶ Y₂
U : C
⊢ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ f.f) ▷ U ≫
      ((X.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X.tensorObj Y₁).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁ X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ f.f
have dsimp : (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ f.f) ▷ U ≫
    Iso.hom
        (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
          U) ≫
      X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
          (Y₂.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
        Iso.inv
            (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
              (Y₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
          (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
              Y₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
            Iso.hom
              (α_ U (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) =
  (Iso.hom
        (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
          U) ≫
      X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
          (Y₁.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
        Iso.inv
            (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
              (Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
          (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
              Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
            Iso.hom
              (α_ U (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))) ≫
    U ◁ X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ f.f
Tactic: dsimp only [tensorObj_fst, tensorObj_snd_β, Iso.trans_hom, whiskerLeftIso_hom,
    Iso.symm_hom, whiskerRightIso_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ X₂ : Center.{v₁, u₁} C
f : X₁ ⟶ X₂
Y : Center.{v₁, u₁} C
U : C
⊢ f.f ▷ Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ▷ U ≫
      ((X₂.tensorObj Y).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj Y).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁ f.f ▷ Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)
have dsimp : f.f ▷ Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ▷ U ≫
    Iso.hom
        (α_ (X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
          U) ≫
      X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
          (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
        Iso.inv
            (α_ (X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
              (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
          (X₂.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
              Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
            Iso.hom
              (α_ U (X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) =
  (Iso.hom
        (α_ (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
          U) ≫
      X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
          (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
        Iso.inv
            (α_ (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
              (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
          (X₁.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
              Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
            Iso.hom
              (α_ U (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))) ≫
    U ◁ f.f ▷ Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)
Tactic: dsimp only [tensorObj_fst, tensorObj_snd_β, Iso.trans_hom, whiskerLeftIso_hom,
    Iso.symm_hom, whiskerRightIso_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : Center.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
U : C
⊢ (f.f ⊗ₘ g.f) ▷ U ≫ ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫ U ◁ (f.f ⊗ₘ g.f)
have rw : (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
        Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f) ▷
      U ≫
    ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
  ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
    U ◁
      (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
        Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
Tactic: rw [tensorHom_def, comp_whiskerRight_assoc, whiskerLeft_comm, whiskerRight_comm_assoc,
      MonoidalCategory.whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : Center.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
U : C
rw :
  (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f) ▷
        U ≫
      ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
⊢ (f.f ⊗ₘ g.f) ▷ U ≫ ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫ U ◁ (f.f ⊗ₘ g.f)
have rw₁ : f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ▷ U ≫
    (Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f) ▷ U ≫
      ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
  ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
    U ◁
      (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
        Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
Tactic: rw [tensorHom_def, comp_whiskerRight_assoc, whiskerLeft_comm, whiskerRight_comm_assoc,
      MonoidalCategory.whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : Center.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
U : C
rw :
  (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f) ▷
        U ≫
      ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
rw₁ :
  f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ▷ U ≫
      (Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f) ▷ U ≫
        ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
⊢ (f.f ⊗ₘ g.f) ▷ U ≫ ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫ U ◁ (f.f ⊗ₘ g.f)
have rw₂ : f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ▷ U ≫
    ((Y₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁ Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f =
  ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
    U ◁
      (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
        Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
Tactic: rw [tensorHom_def, comp_whiskerRight_assoc, whiskerLeft_comm, whiskerRight_comm_assoc,
      MonoidalCategory.whiskerLeft_comp]