awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst_3 : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst_4 : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
⊢ CategoryStruct.comp (Y := mapBifunctorMapObj F p X₁ Y₁) (mapBifunctorMapMap F p e.inv e'.inv)
      (mapBifunctorMapMap F p e.hom e'.hom) =
    𝟙 (mapBifunctorMapObj F p X₂ Y₂)
have h : ∀ (x : K) (i : I) (j : J) (hij : p (i, j) = x),
  Eq (α := (F.obj (X₂ i)).obj (Y₂ j) ⟶ mapBifunctorMapObj F p X₂ Y₂ x)
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₂ Y₂ x) (ιMapBifunctorMapObj F p X₂ Y₂ i j x hij)
      (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₁ Y₁) (mapBifunctorMapMap F p e.inv e'.inv)
        (mapBifunctorMapMap F p e.hom e'.hom) x))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₂ Y₂ x) (ιMapBifunctorMapObj F p X₂ Y₂ i j x hij)
      (𝟙 (mapBifunctorMapObj F p X₂ Y₂) x))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
inst_3 : ∀ (X : GradedObject I C₁) (Y : GradedObject J C₂), (((mapBifunctor F I J).obj X).obj Y).HasMap p
X₁ X₂ : GradedObject I C₁
φ : X₁ ⟶ X₂
Y₁ Y₂ : GradedObject J C₂
ψ : Y₁ ⟶ Y₂
⊢ Eq (α :=
    Quiver.Hom (V := GradedObject K C₃)
      (Functor.obj
        { obj := fun (Y : GradedObject J C₂) ↦ mapBifunctorMapObj F p X₁ Y,
          map := fun {X Y : GradedObject J C₂} (ψ : X ⟶ Y) ↦ mapBifunctorMapMap F p (𝟙 X₁) ψ, map_id := ⋯,
          map_comp := ⋯ }
        Y₁)
      (Functor.obj
        { obj := fun (Y : GradedObject J C₂) ↦ mapBifunctorMapObj F p X₂ Y,
          map := fun {X Y : GradedObject J C₂} (ψ : X ⟶ Y) ↦ mapBifunctorMapMap F p (𝟙 X₂) ψ, map_id := ⋯,
          map_comp := ⋯ }
        Y₂))
    (Functor.map
        { obj := fun (Y : GradedObject J C₂) ↦ mapBifunctorMapObj F p X₁ Y,
          map := fun {X Y : GradedObject J C₂} (ψ : X ⟶ Y) ↦ mapBifunctorMapMap F p (𝟙 X₁) ψ, map_id := ⋯,
          map_comp := ⋯ : GradedObject J C₂ ⥤ GradedObject K C₃ }
        ψ ≫
      mapBifunctorMapMap F p φ (𝟙 Y₂))
    (CategoryStruct.comp (Y :=
      Functor.obj
        { obj := fun (Y : GradedObject J C₂) ↦ mapBifunctorMapObj F p X₂ Y,
          map := fun {X Y : GradedObject J C₂} (ψ : X ⟶ Y) ↦ mapBifunctorMapMap F p (𝟙 X₂) ψ, map_id := ⋯,
          map_comp := ⋯ }
        Y₁)
      (mapBifunctorMapMap F p φ (𝟙 Y₁))
      (Functor.map
        { obj := fun (Y : GradedObject J C₂) ↦ mapBifunctorMapObj F p X₂ Y,
          map := fun {X Y : GradedObject J C₂} (ψ : X ⟶ Y) ↦ mapBifunctorMapMap F p (𝟙 X₂) ψ, map_id := ⋯,
          map_comp := ⋯ }
        ψ))
have dsimp : Eq (α := mapBifunctorMapObj F p X₁ Y₁ ⟶ mapBifunctorMapObj F p X₂ Y₂)
  (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₁ Y₂)
    (mapMap (((mapBifunctor F I J).map (𝟙 X₁)).app Y₁ ≫ ((mapBifunctor F I J).obj X₁).map ψ) p)
    (mapMap (((mapBifunctor F I J).map φ).app Y₂ ≫ ((mapBifunctor F I J).obj X₂).map (𝟙 Y₂)) p))
  (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₂ Y₁)
    (mapMap (((mapBifunctor F I J).map φ).app Y₁ ≫ ((mapBifunctor F I J).obj X₂).map (𝟙 Y₁)) p)
    (mapMap (((mapBifunctor F I J).map (𝟙 X₂)).app Y₁ ≫ ((mapBifunctor F I J).obj X₂).map ψ) p))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
A : C
j : I
f g : tensorObj.{u, v_1, u_1} X₁ X₂ j ⟶ A
h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ f = ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ g
⊢ f = g
have hfg : ∀ (i : I × I)
  (hij :
    (match (motive := I × I → I) i with
      | (i, j) => i + j) =
      j),
  (Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂).ιMapObj
        (fun (x : I × I) ↦
          match (motive := I × I → I) x with
          | (i, j) => i + j)
        i j hij ≫
      f =
    (Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X₁) X₂).ιMapObj
        (fun (x : I × I) ↦
          match (motive := I × I → I) x with
          | (i, j) => i + j)
        i j hij ≫
      g
Tactic: apply mapObj_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst_3 : HasTensor.{u, v_1, u_1} X₁ Y₁
inst_4 : HasTensor.{u, v_1, u_1} X₂ Y₂
i₁ i₂ i₁₂ : I
h : i₁ + i₂ = i₁₂
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (Y₁ i₂) ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂ i₁₂)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ Y₁ i₁₂) (ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h) (tensorHom f g i₁₂))
    ((f i₁ ⊗ₘ g i₂) ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h)
have rw : Eq (α := MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (Y₁ i₂) ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂ i₁₂)
  (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ Y₁ i₁₂) (ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h) (tensorHom f g i₁₂))
  (f i₁ ▷ Y₁ i₂ ≫ X₂ i₁ ◁ g i₂ ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h)
Tactic: rw [tensorHom_def, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X Y : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X Y
⊢ (mapMap
      (NatTrans.app (Functor.map (mapBifunctor (curriedTensor C) I I) (𝟙 X)) Y ≫
        Functor.map (Functor.obj (mapBifunctor (curriedTensor C) I I) X) (𝟙 Y))
      fun (x : I × I) ↦ x.1 + x.2) =
    𝟙 (tensorObj.{u, v_1, u_1} X Y)
have simp : Eq (α := tensorObj.{u, v_1, u_1} X Y ⟶ tensorObj.{u, v_1, u_1} X Y)
  (𝟙
    (mapObj.{u, u, v_1, u_1} (Functor.obj (Functor.obj (mapBifunctor (curriedTensor C) I I) X) Y) fun (x : I × I) ↦
      x.1 + x.2))
  (𝟙 (tensorObj.{u, v_1, u_1} X Y))
Tactic: simp only [Functor.map_id, NatTrans.id_app, comp_id, mapMap_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
inst_3 : HasTensor.{u, v_1, u_1} X₁ Y₁
inst_4 : HasTensor.{u, v_1, u_1} X₂ Y₂
inst_5 : HasTensor.{u, v_1, u_1} X₃ Y₃
⊢ Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₃ Y₃)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f₁ g₁) (tensorHom f₂ g₂))
    (tensorHom (f₁ ≫ f₂) (g₁ ≫ g₂))
have h : ∀ (x i₁ i₂ : I) (hi : i₁ + i₂ = x),
  Eq (α := MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (Y₁ i₂) ⟶ tensorObj.{u, v_1, u_1} X₃ Y₃ x)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ Y₁ x) (ιTensorObj X₁ Y₁ i₁ i₂ x hi)
      (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f₁ g₁) (tensorHom f₂ g₂) x))
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₁ Y₁ x) (ιTensorObj X₁ Y₁ i₁ i₂ x hi)
      (tensorHom (f₁ ≫ f₂) (g₁ ≫ g₂) x))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst_3 : HasTensor.{u, v_1, u_1} X₁ Y₁
inst_4 : HasTensor.{u, v_1, u_1} X₂ Y₂
inst_5 : HasTensor.{u, v_1, u_1} X₂ Y₁
⊢ Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f g)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₂ Y₁) (whiskerRight f Y₁) (whiskerLeft X₂ g))
have rw : Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f g)
  (tensorHom (f ≫ 𝟙 X₂) (𝟙 Y₁ ≫ g))
Tactic: rw [tensorHom_comp_tensorHom, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst_3 : HasTensor.{u, v_1, u_1} X₁ Y₁
inst_4 : HasTensor.{u, v_1, u_1} X₂ Y₂
inst_5 : HasTensor.{u, v_1, u_1} X₂ Y₁
rw :
  Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f g)
    (tensorHom (f ≫ 𝟙 X₂) (𝟙 Y₁ ≫ g))
⊢ Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f g)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₂ Y₁) (whiskerRight f Y₁) (whiskerLeft X₂ g))
have rw₁ : Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f g) (tensorHom (f ≫ 𝟙 X₂) g)
Tactic: rw [tensorHom_comp_tensorHom, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst_3 : HasTensor.{u, v_1, u_1} X₁ Y₁
inst_4 : HasTensor.{u, v_1, u_1} X₂ Y₂
inst_5 : HasTensor.{u, v_1, u_1} X₂ Y₁
rw :
  Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f g)
    (tensorHom (f ≫ 𝟙 X₂) (𝟙 Y₁ ≫ g))
rw₁ : Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f g) (tensorHom (f ≫ 𝟙 X₂) g)
⊢ Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f g)
    (CategoryStruct.comp (Y := tensorObj.{u, v_1, u_1} X₂ Y₁) (whiskerRight f Y₁) (whiskerLeft X₂ g))
have rw₂ : Eq (α := tensorObj.{u, v_1, u_1} X₁ Y₁ ⟶ tensorObj.{u, v_1, u_1} X₂ Y₂) (tensorHom f g) (tensorHom f g)
Tactic: rw [tensorHom_comp_tensorHom, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₂ X₃
inst_4 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)
inst_5 : HasTensor.{u, v_1, u_1} Y₂ Y₃
inst_6 : HasTensor.{u, v_1, u_1} Y₁ (tensorObj.{u, v_1, u_1} Y₂ Y₃)
i₁ i₂ i₃ j : I
h rw : i₁ + i₂ + i₃ = j
⊢ i₁ + (i₂ + i₃) = j
have rw₁ : j = j
Tactic: rw [← add_assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₂ X₃
inst_4 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)
inst_5 : HasTensor.{u, v_1, u_1} Y₂ Y₃
inst_6 : HasTensor.{u, v_1, u_1} Y₁ (tensorObj.{u, v_1, u_1} Y₂ Y₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₂₃ : I
h' : i₂ + i₃ = i₂₃
⊢ i₁ + i₂₃ = j
have rw : i₁ + (i₂ + i₃) = j
Tactic: rw [← h', ← add_assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₂ X₃
inst_4 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)
inst_5 : HasTensor.{u, v_1, u_1} Y₂ Y₃
inst_6 : HasTensor.{u, v_1, u_1} Y₁ (tensorObj.{u, v_1, u_1} Y₂ Y₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₂₃ : I
h' : i₂ + i₃ = i₂₃
rw : i₁ + (i₂ + i₃) = j
rw₁ : i₁ + i₂ + i₃ = j
⊢ i₁ + i₂₃ = j
have rw₂ : j = j
Tactic: rw [← h', ← add_assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ X₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₂ X₃
inst_4 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₂₃ : I
h' : i₂ + i₃ = i₂₃
⊢ Eq.{v_1 + 1} (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁)
        (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₂ i₂) (X₃ i₃)) ⟶
      tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) j)
    (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
    (X₁ i₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ i₂₃ h' ≫ ιTensorObj X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) i₁ i₂₃ j ⋯)
have subst : Eq.{v_1 + 1} (α :=
  MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁)
      (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₂ i₂) (X₃ i₃)) ⟶
    tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) j)
  (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
  (X₁ i₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ (i₂ + i₃) sorry ≫ ιTensorObj X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) i₁ (i₂ + i₃) j sorry)
Tactic: subst h'
Cleared hypotheses: i₂₃, h'
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ X₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₂ X₃
inst_4 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)
j : I
A : C
f g : tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) j ⟶ A
H : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ X₂ X₃
h :
  ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j),
    ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f = ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ g
⊢ f = g
have apply : ∀ (i₁ i₂ i₃ : I) (h : r₁₂₃ (i₁, i₂, i₃) = j),
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X₁ i₁))
        (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X₂ i₂)) (X₃ i₃)) ⟶
      A)
    (ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f)
    (ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g)
Tactic: apply mapBifunctorBifunctor₂₃MapObj_ext (H := H)
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
inst_4 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃
inst_5 : HasTensor.{u, v_1, u_1} Y₁ Y₂
inst_6 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} Y₁ Y₂) Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₁₂ : I
h' : i₁ + i₂ = i₁₂
rw : i₁ + i₂ + i₃ = j
⊢ i₁₂ + i₃ = j
have rw₁ : j = j
Tactic: rw [← h', h]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ X₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
inst_4 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₁₂ : I
h' : i₁ + i₂ = i₁₂
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1)
        (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (X₂ i₂)) (X₃ i₃) ⟶
      tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ j)
    (ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h)
    (ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h' ▷ X₃ i₃ ≫ ιTensorObj (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ i₁₂ i₃ j ⋯)
have subst : Eq (α :=
  MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1)
      (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) (X₁ i₁) (X₂ i₂)) (X₃ i₃) ⟶
    tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ j)
  (ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h)
  (ιTensorObj X₁ X₂ i₁ i₂ (i₁ + i₂) sorry ▷ X₃ i₃ ≫ ιTensorObj (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ (i₁ + i₂) i₃ j sorry)
Tactic: subst h'
Cleared hypotheses: i₁₂, h'
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ X₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₁ X₂
inst_4 : HasTensor.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃
j : I
A : C
f g : tensorObj.{u, v_1, u_1} (tensorObj.{u, v_1, u_1} X₁ X₂) X₃ j ⟶ A
H : HasGoodTensor₁₂Tensor.{u, v_1, u_1} X₁ X₂ X₃
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
⊢ f = g
have apply : ∀ (i₁ i₂ i₃ : I) (h : r₁₂₃ (i₁, i₂, i₃) = j),
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (curriedTensor C)
          (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X₁ i₁)) (X₂ i₂)))
        (X₃ i₃) ⟶
      A)
    (ιMapBifunctor₁₂BifunctorMapObj (curriedTensor C) (curriedTensor C) ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f)
    (ιMapBifunctor₁₂BifunctorMapObj (curriedTensor C) (curriedTensor C) ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g)
Tactic: apply mapBifunctor₁₂BifunctorMapObj_ext (H := H)
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ X₃ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₂ X₃
inst_4 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃)
j : I
A Z : C
f g :
  MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst_1) Z
      (tensorObj.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ X₃) j) ⟶
    A
H : HasGoodTensorTensor₂₃.{u, v_1, u_1} X₁ X₂ X₃
hZ : HasLeftTensor₃ObjExt.{u, v_1, u_1} Z X₁ X₂ X₃ j
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
⊢ f = g
have refine : ∀ (j_1 : Discrete (↑(r₁₂₃ ⁻¹' {j}) : Type u)),
  Eq.{v_1 + 1} (α :=
    Functor.obj.{u, v_1, u, u_1}
        (Discrete.functor
            ((Functor.obj
                  (Functor.obj
                    (Functor.obj (mapTrifunctor (bifunctorComp₂₃ (curriedTensor C) (curriedTensor C)) I I I) X₁) X₂)
                  X₃).mapObjFun
              r₁₂₃ j) ⋙
          Functor.obj (curriedTensor C) Z)
        j_1 ⟶
      A)
    (NatTrans.app
        (Cocone.ι
          (Functor.mapCocone (Functor.obj (curriedTensor C) Z)
            (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)))
        j_1 ≫
      f)
    (NatTrans.app
        (Cocone.ι
          (Functor.mapCocone (Functor.obj (curriedTensor C) Z)
            (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)))
        j_1 ≫
      g)
Tactic: refine (@isColimitOfPreserves C _ C _ _ _ _ ((curriedTensor C).obj Z) _
      (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj (H := H) (j := j)) hZ).hom_ext ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ X₃ X₄ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₃ X₄
inst_4 : HasTensor.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_5 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
⊢ i₁ + (i₂ + i₃ + i₄) = j
have rw : i₁ + (i₂ + i₃ + i₄) = i₁ + i₂ + i₃ + i₄
Tactic: rw [← h, ← add_assoc, ← add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ X₃ X₄ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₃ X₄
inst_4 : HasTensor.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_5 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
rw : i₁ + (i₂ + i₃ + i₄) = i₁ + i₂ + i₃ + i₄
⊢ i₁ + (i₂ + i₃ + i₄) = j
have rw₁ : i₁ + (i₂ + i₃) + i₄ = i₁ + i₂ + i₃ + i₄
Tactic: rw [← h, ← add_assoc, ← add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ X₃ X₄ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₃ X₄
inst_4 : HasTensor.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_5 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
rw : i₁ + (i₂ + i₃ + i₄) = i₁ + i₂ + i₃ + i₄
rw₁ : i₁ + (i₂ + i₃) + i₄ = i₁ + i₂ + i₃ + i₄
⊢ i₁ + (i₂ + i₃ + i₄) = j
have rw₂ : i₁ + i₂ + i₃ + i₄ = i₁ + i₂ + i₃ + i₄
Tactic: rw [← h, ← add_assoc, ← add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ X₃ X₄ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₃ X₄
inst_4 : HasTensor.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_5 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
i₂₃₄ : I
hi : i₂ + i₃ + i₄ = i₂₃₄
⊢ i₁ + i₂₃₄ = j
have rw : i₁ + (i₂ + i₃ + i₄) = j
Tactic: rw [← hi, ← add_assoc, ← add_assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ X₃ X₄ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₃ X₄
inst_4 : HasTensor.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_5 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
i₂₃₄ : I
hi : i₂ + i₃ + i₄ = i₂₃₄
rw : i₁ + (i₂ + i₃ + i₄) = j
⊢ i₁ + i₂₃₄ = j
have rw₁ : i₁ + (i₂ + i₃) + i₄ = j
Tactic: rw [← hi, ← add_assoc, ← add_assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Monoidal (goal)
Goal:
I : Type u
inst : AddMonoid I
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
X₁ X₂ X₃ X₄ : GradedObject I C
inst_3 : HasTensor.{u, v_1, u_1} X₃ X₄
inst_4 : HasTensor.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄)
inst_5 : HasTensor.{u, v_1, u_1} X₁ (tensorObj.{u, v_1, u_1} X₂ (tensorObj.{u, v_1, u_1} X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
i₂₃₄ : I
hi : i₂ + i₃ + i₄ = i₂₃₄
rw : i₁ + (i₂ + i₃ + i₄) = j
rw₁ : i₁ + (i₂ + i₃) + i₄ = j
rw₂ : i₁ + i₂ + i₃ + i₄ = j
⊢ i₁ + i₂₃₄ = j
have rw₃ : j = j
Tactic: rw [← hi, ← add_assoc, ← add_assoc, h]