awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
c X Y : C
x : X ⟶ Y
refine_1 :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₁ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫ L.obj (R.obj c) ◁ L.map (R.map x) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
⊢ Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    ((δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X)) ≫ c ◁ x)
have refine_1₂ : Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
  (δ L (R.obj c) (R.obj X) ≫
    L.obj (R.obj c) ◁ L.map (R.map x) ≫ L.obj (R.obj c) ◁ adj.counit.app Y ≫ adj.counit.app c ▷ Y)
  (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
Tactic: rw [Category.assoc, ← δ_natural_right_assoc,
        tensorHom_def', ← MonoidalCategory.whiskerLeft_comp_assoc,
        Adjunction.counit_naturality, whisker_exchange,
        tensorHom_def_assoc, MonoidalCategory.whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
c X Y : C
x : X ⟶ Y
refine_1 :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₁ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫ L.obj (R.obj c) ◁ L.map (R.map x) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₂ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫
      L.obj (R.obj c) ◁ L.map (R.map x) ≫ L.obj (R.obj c) ◁ adj.counit.app Y ≫ adj.counit.app c ▷ Y)
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
⊢ Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    ((δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X)) ≫ c ◁ x)
have refine_1₃ : Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
  (δ L (R.obj c) (R.obj X) ≫ L.obj (R.obj c) ◁ (L.map (R.map x) ≫ adj.counit.app Y) ≫ adj.counit.app c ▷ Y)
  (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
Tactic: rw [Category.assoc, ← δ_natural_right_assoc,
        tensorHom_def', ← MonoidalCategory.whiskerLeft_comp_assoc,
        Adjunction.counit_naturality, whisker_exchange,
        tensorHom_def_assoc, MonoidalCategory.whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
c X Y : C
x : X ⟶ Y
refine_1 :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₁ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫ L.obj (R.obj c) ◁ L.map (R.map x) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₂ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫
      L.obj (R.obj c) ◁ L.map (R.map x) ≫ L.obj (R.obj c) ◁ adj.counit.app Y ≫ adj.counit.app c ▷ Y)
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₃ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫ L.obj (R.obj c) ◁ (L.map (R.map x) ≫ adj.counit.app Y) ≫ adj.counit.app c ▷ Y)
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
⊢ Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    ((δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X)) ≫ c ◁ x)
have refine_1₄ : Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
  (δ L (R.obj c) (R.obj X) ≫ L.obj (R.obj c) ◁ (adj.counit.app X ≫ x) ≫ adj.counit.app c ▷ Y)
  (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
Tactic: rw [Category.assoc, ← δ_natural_right_assoc,
        tensorHom_def', ← MonoidalCategory.whiskerLeft_comp_assoc,
        Adjunction.counit_naturality, whisker_exchange,
        tensorHom_def_assoc, MonoidalCategory.whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Reflection (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
c X Y : C
x : X ⟶ Y
refine_1 :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₁ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫ L.obj (R.obj c) ◁ L.map (R.map x) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₂ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫
      L.obj (R.obj c) ◁ L.map (R.map x) ≫ L.obj (R.obj c) ◁ adj.counit.app Y ≫ adj.counit.app c ▷ Y)
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₃ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫ L.obj (R.obj c) ◁ (L.map (R.map x) ≫ adj.counit.app Y) ≫ adj.counit.app c ▷ Y)
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
refine_1₄ :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (δ L (R.obj c) (R.obj X) ≫ L.obj (R.obj c) ◁ (adj.counit.app X ≫ x) ≫ adj.counit.app c ▷ Y)
    (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
⊢ Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    ((δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X)) ≫ c ◁ x)
have refine_1₅ : Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
  (δ L (R.obj c) (R.obj X) ≫ adj.counit.app c ▷ L.obj (R.obj X) ≫ c ◁ (adj.counit.app X ≫ x))
  (δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X) ≫ c ◁ x)
Tactic: rw [Category.assoc, ← δ_natural_right_assoc,
        tensorHom_def', ← MonoidalCategory.whiskerLeft_comp_assoc,
        Adjunction.counit_naturality, whisker_exchange,
        tensorHom_def_assoc, MonoidalCategory.whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Transport (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
X Y : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := instCategoryTransported e) ((e' e).functor.obj X) ((e' e).functor.obj Y) ⟶
      (e' e).functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (μ (e' e).functor X Y ≫ (e' e).functor.map (Iso.hom (β_ X Y)))
    (Iso.hom (β_ ((e' e).functor.obj X) ((e' e).functor.obj Y)) ≫ μ (e' e).functor Y X)
have a : Eq (α :=
  (e' e).inverse.obj
      (tensorObj.{v₂, u₂} (𝒞 := instCategoryTransported e) ((e' e).functor.obj X) ((e' e).functor.obj Y)) ⟶
    (e' e).inverse.obj ((e' e).functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
  ((e' e).inverse.map (μ (e' e).functor X Y ≫ (e' e).functor.map (Iso.hom (β_ X Y))))
  ((e' e).inverse.map (Iso.hom (β_ ((e' e).functor.obj X) ((e' e).functor.obj Y)) ≫ μ (e' e).functor Y X))
Tactic: apply (e' e).inverse.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Transport (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
X Y : C
⊢ Eq (α :=
    (e' e).inverse.obj
        (tensorObj.{v₂, u₂} (𝒞 := instCategoryTransported e) ((e' e).functor.obj X) ((e' e).functor.obj Y)) ⟶
      (e' e).inverse.obj ((e' e).functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
    ((e' e).inverse.map (μ (e' e).functor X Y ≫ (e' e).functor.map (Iso.hom (β_ X Y))))
    ((e' e).inverse.map (Iso.hom (β_ ((e' e).functor.obj X) ((e' e).functor.obj Y)) ≫ μ (e' e).functor Y X))
have this : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (((e' e).functor ⋙ (e' e).inverse).obj X) (((e' e).functor ⋙ (e' e).inverse).obj Y) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) (((e' e).functor ⋙ (e' e).inverse).obj Y) (((e' e).functor ⋙ (e' e).inverse).obj X))
  (Iso.hom (β_ (((e' e).functor ⋙ (e' e).inverse).obj X) (((e' e).functor ⋙ (e' e).inverse).obj Y)))
  (CategoryStruct.comp (Y := ((e' e).functor ⋙ (e' e).inverse).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ ((e' e).functor ⋙ (e' e).inverse) X Y)
    (((e' e).functor ⋙ (e' e).inverse).map (Iso.hom (β_ X Y)) ≫ δ ((e' e).functor ⋙ (e' e).inverse) Y X))
Tactic: have : (β_ (((e' e).functor ⋙ (e' e).inverse).obj X)
        (((e' e).functor ⋙ (e' e).inverse).obj Y)).hom =
          Functor.LaxMonoidal.μ (((e' e).functor ⋙ (e' e).inverse)) X Y ≫
            ((e' e).functor ⋙ (e' e).inverse).map (β_ X Y).hom ≫
              Functor.OplaxMonoidal.δ ((e' e).functor ⋙ (e' e).inverse) Y X := by
      simp only [((e' e).functor ⋙ (e' e).inverse).map_braiding X Y,
        assoc, Functor.Monoidal.μ_δ, comp_id, Functor.Monoidal.μ_δ_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ Eq (α := V ⟶ tensorObj.{v, u} (𝒞 := inst) X Y) (f ≫ lift g h) (lift (f ≫ g) (f ≫ h))
have h_fst : CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (f ≫ lift g h) (fst X Y) =
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift (f ≫ g) (f ≫ h)) (fst X Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
h_fst :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (f ≫ lift g h) (fst X Y) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift (f ≫ g) (f ≫ h)) (fst X Y)
⊢ Eq (α := V ⟶ tensorObj.{v, u} (𝒞 := inst) X Y) (f ≫ lift g h) (lift (f ≫ g) (f ≫ h))
have h_snd : CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (f ≫ lift g h) (snd X Y) =
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift (f ≫ g) (f ≫ h)) (snd X Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
⊢ lift (fst X Y) (snd X Y) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)
have h_fst : CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift (fst X Y) (snd X Y)) (fst X Y) =
  𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) ≫ fst X Y
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
h_fst :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift (fst X Y) (snd X Y)) (fst X Y) =
    𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) ≫ fst X Y
⊢ lift (fst X Y) (snd X Y) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)
have h_snd : CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift (fst X Y) (snd X Y)) (snd X Y) =
  𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) ≫ snd X Y
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
V W X Y Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ Eq (α := V ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z) (lift f g ≫ (h ⊗ₘ k)) (lift (f ≫ h) (g ≫ k))
have h_fst : CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y Z) (lift f g ≫ (h ⊗ₘ k)) (fst Y Z) =
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y Z) (lift (f ≫ h) (g ≫ k)) (fst Y Z)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
V W X Y Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
h_fst :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y Z) (lift f g ≫ (h ⊗ₘ k)) (fst Y Z) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y Z) (lift (f ≫ h) (g ≫ k)) (fst Y Z)
⊢ Eq (α := V ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z) (lift f g ≫ (h ⊗ₘ k)) (lift (f ≫ h) (g ≫ k))
have h_snd : CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y Z) (lift f g ≫ (h ⊗ₘ k)) (snd Y Z) =
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y Z) (lift (f ≫ h) (g ≫ k)) (snd Y Z)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (lift (fst W Y ≫ g) (snd W Y ≫ g'))
    (g ⊗ₘ g')
have h_fst : Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ X)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Z) (lift (fst W Y ≫ g) (snd W Y ≫ g')) (fst X Z))
  ((g ⊗ₘ g') ≫ fst X Z)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
h_fst :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Z) (lift (fst W Y ≫ g) (snd W Y ≫ g')) (fst X Z))
    ((g ⊗ₘ g') ≫ fst X Z)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (lift (fst W Y ≫ g) (snd W Y ≫ g'))
    (g ⊗ₘ g')
have h_snd : Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ Z)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Z) (lift (fst W Y ≫ g) (snd W Y ≫ g')) (snd X Z))
  ((g ⊗ₘ g') ≫ snd X Z)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ X) (X ◁ toUnit Y ≫ Iso.hom (ρ_ X)) (fst X Y)
have rw : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst)))
  ((X ◁ toUnit Y ≫ Iso.hom (ρ_ X)) ≫ Iso.inv (ρ_ X)) (fst X Y ≫ Iso.inv (ρ_ X))
Tactic: rw [← cancel_mono (ρ_ X).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ Y) (toUnit X ▷ Y ≫ Iso.hom (λ_ Y)) (snd X Y)
have rw : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) Y)
  ((toUnit X ▷ Y ≫ Iso.hom (λ_ Y)) ≫ Iso.inv (λ_ Y)) (snd X Y ≫ Iso.inv (λ_ Y))
Tactic: rw [← cancel_mono (λ_ Y).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
f : X ⟶ tensorUnit.{v, u} C (𝒞 := inst)
g : X ⟶ Y
⊢ lift f g ≫ Iso.hom (λ_ Y) = g
have rw : lift f g = g ≫ Iso.inv (λ_ Y)
Tactic: rw [← Iso.eq_comp_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
g : X ⟶ tensorUnit.{v, u} C (𝒞 := inst)
⊢ lift f g ≫ Iso.hom (ρ_ Y) = f
have rw : lift f g = f ≫ Iso.inv (ρ_ Y)
Tactic: rw [← Iso.eq_comp_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
W X Y Z : C
⊢ tensorμ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z) = fst W X ⊗ₘ fst Y Z
have h_fst : (tensorμ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z)) ≫ fst W Y =
  (fst W X ⊗ₘ fst Y Z) ≫ fst W Y
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
W X Y Z : C
h_fst :
  (tensorμ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z)) ≫ fst W Y =
    (fst W X ⊗ₘ fst Y Z) ≫ fst W Y
⊢ tensorμ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z) = fst W X ⊗ₘ fst Y Z
have h_snd : (tensorμ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z)) ≫ snd W Y =
  (fst W X ⊗ₘ fst Y Z) ≫ snd W Y
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
W X Y Z : C
⊢ tensorμ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z) = snd W X ⊗ₘ snd Y Z
have h_fst : (tensorμ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z)) ≫ fst X Z =
  (snd W X ⊗ₘ snd Y Z) ≫ fst X Z
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
W X Y Z : C
h_fst :
  (tensorμ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z)) ≫ fst X Z =
    (snd W X ⊗ₘ snd Y Z) ≫ fst X Z
⊢ tensorμ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z) = snd W X ⊗ₘ snd Y Z
have h_snd : (tensorμ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z)) ≫ snd X Z =
  (snd W X ⊗ₘ snd Y Z) ≫ snd X Z
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
W X Y Z : C
⊢ tensorδ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z) = fst W Y ⊗ₘ fst X Z
have h_fst : (tensorδ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ fst W X =
  (fst W Y ⊗ₘ fst X Z) ≫ fst W X
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
W X Y Z : C
h_fst :
  (tensorδ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ fst W X =
    (fst W Y ⊗ₘ fst X Z) ≫ fst W X
⊢ tensorδ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z) = fst W Y ⊗ₘ fst X Z
have h_snd : (tensorδ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ snd W X =
  (fst W Y ⊗ₘ fst X Z) ≫ snd W X
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
W X Y Z : C
⊢ tensorδ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z) = snd W Y ⊗ₘ snd X Z
have h_fst : (tensorδ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ fst Y Z =
  (snd W Y ⊗ₘ snd X Z) ≫ fst Y Z
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
W X Y Z : C
h_fst :
  (tensorδ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ fst Y Z =
    (snd W Y ⊗ₘ snd X Z) ≫ fst Y Z
⊢ tensorδ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z) = snd W Y ⊗ₘ snd X Z
have h_snd : (tensorδ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ snd Y Z =
  (snd W Y ⊗ₘ snd X Z) ≫ snd Y Z
Tactic: ext