awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Monoidal (goal)
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → BraidedCategory.{v₁, u₁} (C i)
X Y Z : (i : I) → C i
⊢ Eq (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X))
    (Iso.hom (α_ X Y Z) ≫
      Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z i)) ≫ Iso.hom (α_ Y Z X))
    (Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Y i)) ▷ Z ≫
      Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Z i)))
have w : ∀ (i : I),
  Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z i ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) i)
    ((Iso.hom (α_ X Y Z) ≫
          Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z i)) ≫
            Iso.hom (α_ Y Z X))
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) i)
    ((Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Y i)) ▷ Z ≫
          Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Z i)))
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Monoidal (goal)
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → BraidedCategory.{v₁, u₁} (C i)
X Y Z : (i : I) → C i
⊢ Eq (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) Y)
    (Iso.inv (α_ X Y Z) ≫
      Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y i) (Z i)) ≫ Iso.inv (α_ Z X Y))
    (X ◁ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (Y i) (Z i)) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Z i)) ▷ Y)
have w : ∀ (i : I),
  Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) i ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) Y i)
    ((Iso.inv (α_ X Y Z) ≫
          Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y i) (Z i)) ≫
            Iso.inv (α_ Z X Y))
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) Y i)
    ((X ◁ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (Y i) (Z i)) ≫
          Iso.inv (α_ X Z Y) ≫ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Z i)) ▷ Y)
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) Y i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Monoidal (goal)
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → SymmetricCategory.{v₁, u₁} (C i)
X Y : (i : I) → C i
⊢ Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X) = 𝟙 (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y)
have w : ∀ (i : I), Eq.{v₁ + 1} ((Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X)) i) (𝟙 (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Monoidal (goal)
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : MonoidalCategory.{v_1, u_1} D
F : (i : I) → Functor.{v_1, v₁, u_1, u₁} D (C i)
inst_4 : (i : I) → (F i).OplaxMonoidal
X : D
⊢ Eq (α :=
    (Functor.pi' (C := C) F).obj X ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
        ((Functor.pi' (C := C) F).obj X))
    (Iso.inv (λ_ ((Functor.pi' (C := C) F).obj X)))
    (CategoryStruct.comp (Y :=
      (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) X))
      ((Functor.pi' (C := C) F).map (Iso.inv (λ_ X)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)))
          ((Functor.pi' (C := C) F).obj X))
        (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) X)
        ((fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi' (C := C) F).obj X)))
have w : ∀ (i : I),
  Eq.{v₁ + 1} (α :=
    (Functor.pi' (C := C) F).obj X i ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
        ((Functor.pi' (C := C) F).obj X) i)
    (Iso.inv (λ_ ((Functor.pi' (C := C) F).obj X)) i :
      (Functor.pi' (C := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
          ((Functor.pi' (C := C) F).obj X) i)
    (CategoryStruct.comp (Y :=
        (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) X))
        ((Functor.pi' (C := C) F).map (Iso.inv (λ_ X)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)))
            ((Functor.pi' (C := C) F).obj X))
          (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) X)
          ((fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi' (C := C) F).obj X))
        i :
      (Functor.pi' (C := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
          ((Functor.pi' (C := C) F).obj X) i)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Monoidal (goal)
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : MonoidalCategory.{v_1, u_1} D
F : (i : I) → Functor.{v_1, v₁, u_1, u₁} D (C i)
inst_4 : (i : I) → (F i).OplaxMonoidal
X : D
⊢ Eq (α :=
    (Functor.pi' (C := C) F).obj X ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
        ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)))
    (Iso.inv (ρ_ ((Functor.pi' (C := C) F).obj X)))
    (CategoryStruct.comp (Y :=
      (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X (tensorUnit.{v_1, u_1} D (𝒞 := inst_2))))
      ((Functor.pi' (C := C) F).map (Iso.inv (ρ_ X)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
          ((Functor.pi' (C := C) F).obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2))))
        (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) X (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)))
        ((Functor.pi' (C := C) F).obj X ◁ fun (i : I) ↦ Functor.OplaxMonoidal.η (F i))))
have w : ∀ (i : I),
  Eq.{v₁ + 1} (α :=
    (Functor.pi' (C := C) F).obj X i ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
        ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
    (Iso.inv (ρ_ ((Functor.pi' (C := C) F).obj X)) i :
      (Functor.pi' (C := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
          ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
    (CategoryStruct.comp (Y :=
        (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X (tensorUnit.{v_1, u_1} D (𝒞 := inst_2))))
        ((Functor.pi' (C := C) F).map (Iso.inv (ρ_ X)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
            ((Functor.pi' (C := C) F).obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2))))
          (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) X (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)))
          ((Functor.pi' (C := C) F).obj X ◁ fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)))
        i :
      (Functor.pi' (C := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
          ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Monoidal (goal)
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → BraidedCategory.{v₁, u₁} (C i)
D : Type u_1
inst_3 : Category.{v_1, u_1} D
inst_4 : MonoidalCategory.{v_1, u_1} D
inst_5 : BraidedCategory.{v_1, u_1} D
F : (i : I) → Functor.{v_1, v₁, u_1, u₁} D (C i)
inst_6 : (i : I) → (F i).LaxBraided
X Y : D
⊢ Eq (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y) ⟶
      (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_3) Y X))
    (Functor.LaxMonoidal.μ (Functor.pi' (C := C) F) X Y ≫ (Functor.pi' (C := C) F).map (Iso.hom (β_ X Y)))
    (Iso.hom (β_ ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y)) ≫
      Functor.LaxMonoidal.μ (Functor.pi' (C := C) F) Y X)
have w : ∀ (i : I),
  Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y) i ⟶
      (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_3) Y X) i)
    ((Functor.LaxMonoidal.μ (Functor.pi' (C := C) F) X Y ≫ (Functor.pi' (C := C) F).map (Iso.hom (β_ X Y))) i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y) i ⟶
        (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_3) Y X) i)
    ((Iso.hom (β_ ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y)) ≫
          Functor.LaxMonoidal.μ (Functor.pi' (C := C) F) Y X)
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y) i ⟶
        (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_3) Y X) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Monoidal (goal)
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
D : I → Type u₂
inst_2 : (i : I) → Category.{v₂, u₂} (D i)
inst_3 : (i : I) → MonoidalCategory.{v₂, u₂} (D i)
F : (i : I) → Functor.{v₂, v₁, u₂, u₁} (D i) (C i)
inst_4 : (i : I) → (F i).OplaxMonoidal
X : (i : I) → D i
⊢ Eq (α :=
    (Functor.pi (C := D) (D := C) F).obj X ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
        ((Functor.pi (C := D) (D := C) F).obj X))
    (Iso.inv (λ_ ((Functor.pi (C := D) (D := C) F).obj X)))
    (CategoryStruct.comp (Y :=
      (Functor.pi (C := D) (D := C) F).obj
        (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D)) X))
      ((Functor.pi (C := D) (D := C) F).map (Iso.inv (λ_ X)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C)
          ((Functor.pi (C := D) (D := C) F).obj ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D)))
          ((Functor.pi (C := D) (D := C) F).obj X))
        (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D) i) (X i))
        ((fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi (C := D) (D := C) F).obj X)))
have w : ∀ (i : I),
  Eq.{v₁ + 1} (α :=
    (Functor.pi (C := D) (D := C) F).obj X i ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
        ((Functor.pi (C := D) (D := C) F).obj X) i)
    (Iso.inv (λ_ ((Functor.pi (C := D) (D := C) F).obj X)) i :
      (Functor.pi (C := D) (D := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
          ((Functor.pi (C := D) (D := C) F).obj X) i)
    (CategoryStruct.comp (Y :=
        (Functor.pi (C := D) (D := C) F).obj
          (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D)) X))
        ((Functor.pi (C := D) (D := C) F).map (Iso.inv (λ_ X)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C)
            ((Functor.pi (C := D) (D := C) F).obj ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D)))
            ((Functor.pi (C := D) (D := C) F).obj X))
          (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D) i) (X i))
          ((fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi (C := D) (D := C) F).obj X))
        i :
      (Functor.pi (C := D) (D := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
          ((Functor.pi (C := D) (D := C) F).obj X) i)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Monoidal (goal)
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
D : I → Type u₂
inst_2 : (i : I) → Category.{v₂, u₂} (D i)
inst_3 : (i : I) → MonoidalCategory.{v₂, u₂} (D i)
F : (i : I) → Functor.{v₂, v₁, u₂, u₁} (D i) (C i)
inst_4 : (i : I) → (F i).OplaxMonoidal
X : (i : I) → D i
⊢ Eq (α :=
    (Functor.pi (C := D) (D := C) F).obj X ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
        ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)))
    (Iso.inv (ρ_ ((Functor.pi (C := D) (D := C) F).obj X)))
    (CategoryStruct.comp (Y :=
      (Functor.pi (C := D) (D := C) F).obj
        (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) X ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D))))
      ((Functor.pi (C := D) (D := C) F).map (Iso.inv (ρ_ X)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
          ((Functor.pi (C := D) (D := C) F).obj ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D))))
        (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) (X i) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D) i))
        ((Functor.pi (C := D) (D := C) F).obj X ◁ fun (i : I) ↦ Functor.OplaxMonoidal.η (F i))))
have w : ∀ (i : I),
  Eq.{v₁ + 1} (α :=
    (Functor.pi (C := D) (D := C) F).obj X i ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
        ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
    (Iso.inv (ρ_ ((Functor.pi (C := D) (D := C) F).obj X)) i :
      (Functor.pi (C := D) (D := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
          ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
    (CategoryStruct.comp (Y :=
        (Functor.pi (C := D) (D := C) F).obj
          (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) X ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D))))
        ((Functor.pi (C := D) (D := C) F).map (Iso.inv (ρ_ X)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
            ((Functor.pi (C := D) (D := C) F).obj ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D))))
          (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) (X i) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D) i))
          ((Functor.pi (C := D) (D := C) F).obj X ◁ fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)))
        i :
      (Functor.pi (C := D) (D := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
          ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Monoidal (goal)
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → BraidedCategory.{v₁, u₁} (C i)
D : I → Type u₂
inst_3 : (i : I) → Category.{v₂, u₂} (D i)
inst_4 : (i : I) → MonoidalCategory.{v₂, u₂} (D i)
inst_5 : (i : I) → BraidedCategory.{v₂, u₂} (D i)
F : (i : I) → Functor.{v₂, v₁, u₂, u₁} (D i) (C i)
inst_6 : (i : I) → (F i).LaxBraided
X Y : (i : I) → D i
⊢ Eq (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
        ((Functor.pi (C := D) (D := C) F).obj Y) ⟶
      (Functor.pi (C := D) (D := C) F).obj (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) Y X))
    (Functor.LaxMonoidal.μ (Functor.pi (C := D) (D := C) F) X Y ≫
      (Functor.pi (C := D) (D := C) F).map (Iso.hom (β_ X Y)))
    (Iso.hom (β_ ((Functor.pi (C := D) (D := C) F).obj X) ((Functor.pi (C := D) (D := C) F).obj Y)) ≫
      Functor.LaxMonoidal.μ (Functor.pi (C := D) (D := C) F) Y X)
have w : ∀ (i : I),
  Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X) ((Functor.pi (C := D) (D := C) F).obj Y)
        i ⟶
      (Functor.pi (C := D) (D := C) F).obj (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) Y X) i)
    ((Functor.LaxMonoidal.μ (Functor.pi (C := D) (D := C) F) X Y ≫
          (Functor.pi (C := D) (D := C) F).map (Iso.hom (β_ X Y)))
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
          ((Functor.pi (C := D) (D := C) F).obj Y) i ⟶
        (Functor.pi (C := D) (D := C) F).obj (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) Y X) i)
    ((Iso.hom (β_ ((Functor.pi (C := D) (D := C) F).obj X) ((Functor.pi (C := D) (D := C) F).obj Y)) ≫
          Functor.LaxMonoidal.μ (Functor.pi (C := D) (D := C) F) Y X)
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
          ((Functor.pi (C := D) (D := C) F).obj Y) i ⟶
        (Functor.pi (C := D) (D := C) F).obj (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) Y X) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Monoidal (goal)
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : MonoidalCategory.{v_1, u_1} D
F G : D ⥤ ((i : I) → C i)
inst_4 : F.LaxMonoidal
inst_5 : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst_6 : ∀ (i : I), NatTrans.IsMonoidal (τ i)
⊢ Eq (α := (𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C) ⟶ G.obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)))
    (Functor.LaxMonoidal.ε F ≫ (NatTrans.pi' (C := C) τ).app (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)))
    (Functor.LaxMonoidal.ε G)
have w : ∀ (i : I),
  Eq.{v₁ + 1} (α := (𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C) i ⟶ G.obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) i)
    ((Functor.LaxMonoidal.ε F ≫ (NatTrans.pi' (C := C) τ).app (tensorUnit.{v_1, u_1} D (𝒞 := inst_2))) i :
      (𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C) i ⟶ G.obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) i)
    (Functor.LaxMonoidal.ε G i :
      (𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C) i ⟶ G.obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Monoidal (goal)
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : MonoidalCategory.{v_1, u_1} D
F G : D ⥤ ((i : I) → C i)
inst_4 : F.LaxMonoidal
inst_5 : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst_6 : ∀ (i : I), NatTrans.IsMonoidal (τ i)
X Y : D
⊢ Eq (α := tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y))
    (Functor.LaxMonoidal.μ F X Y ≫ (NatTrans.pi' (C := C) τ).app (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y))
    (((NatTrans.pi' (C := C) τ).app X ⊗ₘ (NatTrans.pi' (C := C) τ).app Y) ≫ Functor.LaxMonoidal.μ G X Y)
have w : ∀ (i : I),
  Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (F.obj X) (F.obj Y) i ⟶ G.obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y) i)
    ((Functor.LaxMonoidal.μ F X Y ≫ (NatTrans.pi' (C := C) τ).app (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y)) i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (F.obj X) (F.obj Y) i ⟶ G.obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y) i)
    ((((NatTrans.pi' (C := C) τ).app X ⊗ₘ (NatTrans.pi' (C := C) τ).app Y) ≫ Functor.LaxMonoidal.μ G X Y) i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (F.obj X) (F.obj Y) i ⟶ G.obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (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 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
⊢ G.Additive
have map_add : autoParam (∀ {X Y : C} {f g : X ⟶ Y}, G.map (f + g) = G.map f + G.map g) Additive.map_add._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : Preadditive.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.Additive
inst_7 : F.Full
inst_8 : F.EssSurj
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_9 : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
⊢ G.map (f + g) = G.map f + G.map g
have obtain : ∀ (f' : F.objPreimage X ⟶ F.objPreimage Y)
  (hf' : F.map f' = Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)),
  G.map (f + g) = G.map f + G.map g
Tactic: obtain ⟨f', hf'⟩ := F.map_surjective ((F.objObjPreimageIso X).hom ≫ f ≫
      (F.objObjPreimageIso Y).inv)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : Preadditive.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.Additive
inst_7 : F.Full
inst_8 : F.EssSurj
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_9 : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)
⊢ G.map (f + g) = G.map f + G.map g
have obtain : ∀ (g' : F.objPreimage X ⟶ F.objPreimage Y)
  (hg' : F.map g' = Iso.hom (F.objObjPreimageIso X) ≫ g ≫ Iso.inv (F.objObjPreimageIso Y)),
  G.map (f + g) = G.map f + G.map g
Tactic: obtain ⟨g', hg'⟩ := F.map_surjective ((F.objObjPreimageIso X).hom ≫ g ≫
      (F.objObjPreimageIso Y).inv)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : Preadditive.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.Additive
inst_7 : F.Full
inst_8 : F.EssSurj
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_9 : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = Iso.hom (F.objObjPreimageIso X) ≫ g ≫ Iso.inv (F.objObjPreimageIso Y)
⊢ G.map (f + g) = G.map f + G.map g
have simp : G.map
    (HAdd.hAdd (α := F.obj (F.objPreimage X) ⟶ F.obj (F.objPreimage Y))
      (Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y))
      (Iso.hom (F.objObjPreimageIso X) ≫ g ≫ Iso.inv (F.objObjPreimageIso Y))) =
  HAdd.hAdd (α := G.obj (F.obj (F.objPreimage X)) ⟶ G.obj (F.obj (F.objPreimage Y)))
    (G.map (Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)))
    (G.map (Iso.hom (F.objObjPreimageIso X) ≫ g ≫ Iso.inv (F.objObjPreimageIso Y)))
Tactic: simp only [← cancel_mono (G.map (F.objObjPreimageIso Y).inv),
      ← cancel_epi (G.map (F.objObjPreimageIso X).hom),
      Preadditive.add_comp, Preadditive.comp_add, ← Functor.map_comp]