awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) unit) (Functor.obj L' X))
    (Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
        NatTrans.app
          (liftNatTrans L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') L'
            (Functor.obj (Functor.flip (tensorBifunctor L W ε)) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
            (𝟭 (LocalizedMonoidal L W ε)) (Functor.whiskerRight (Iso.hom (rightUnitorNatIso C)) L' ≫ L.leftUnitor.hom))
          (Functor.obj L' X) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) unit) (Functor.obj L' X))
    (Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
        Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X)) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) unit) (Functor.obj L' X))
have rw : Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
    CategoryStruct.comp (Y := Functor.obj (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') X)
      (NatTrans.app
        (Iso.hom
          (Lifting.iso L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
            (Functor.obj (Functor.flip (tensorBifunctor L W ε))
              (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
        X)
      (NatTrans.app (Functor.whiskerRight (Iso.hom (rightUnitorNatIso C)) L' ≫ L.leftUnitor.hom) X ≫
        NatTrans.app (Iso.inv (Lifting.iso L' W L' (𝟭 (LocalizedMonoidal L W ε)))) X) =
  Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
    Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))
Tactic: rw [liftNatTrans_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X : C
⊢ Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
      CategoryStruct.comp (Y := Functor.obj (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') X)
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (Functor.flip (tensorBifunctor L W ε))
                (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          X)
        (NatTrans.app (Functor.whiskerRight (Iso.hom (rightUnitorNatIso C)) L' ≫ L.leftUnitor.hom) X ≫
          NatTrans.app (Iso.inv (Lifting.iso L' W L' (𝟭 (LocalizedMonoidal L W ε)))) X) =
    Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
      Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))
have dsimp : Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
    CategoryStruct.comp (Y := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
      (NatTrans.app
        (Iso.hom
          (Lifting.iso L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
            (Functor.obj (Functor.flip (tensorBifunctor L W ε))
              (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
        X)
      ((Functor.map L' (Iso.hom (ρ_ X)) ≫ 𝟙 (L.obj X)) ≫ 𝟙 (Functor.obj L' X)) =
  Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
    Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X : C
⊢ Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
      CategoryStruct.comp (Y :=
        Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (Functor.flip (tensorBifunctor L W ε))
                (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          X)
        ((Functor.map L' (Iso.hom (ρ_ X)) ≫ 𝟙 (L.obj X)) ≫ 𝟙 (Functor.obj L' X)) =
    Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
      Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))
have rw : Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
    CategoryStruct.comp (Y := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
      (NatTrans.app
        (Iso.hom
          (Lifting.iso L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
            (Functor.obj (Functor.flip (tensorBifunctor L W ε))
              (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
        X)
      (Functor.map L' (Iso.hom (ρ_ X)) ≫ 𝟙 (L.obj X) ≫ 𝟙 (Functor.obj L' X)) =
  Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
    Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))
Tactic: rw [assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X : C
⊢ Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
      CategoryStruct.comp (Y :=
        Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (Functor.flip (tensorBifunctor L W ε))
                (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          X)
        (Functor.map L' (Iso.hom (ρ_ X)) ≫ 𝟙 (L.obj X) ≫ 𝟙 (Functor.obj L' X)) =
    Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
      Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))
have change : Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
    Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
      Functor.map L' (Iso.hom (ρ_ X)) ≫ 𝟙 (Functor.obj L' X) ≫ 𝟙 (Functor.obj L' X) =
  Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
    Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))
Tactic: change _ ≫ (μ L W ε _ _).hom ≫ _ ≫ 𝟙 _ ≫ 𝟙 _ = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₁ X₂) X₃ ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₂ Y₃))
    (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)) (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))
have h₁ : ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃ ≫
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app Y₃ =
  ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app X₃ ≫
    ((Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃
Tactic: have h₁ := (((associator L W ε).hom.app Y₁).app Y₂).naturality f₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
h₁ :
  ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃ ≫
      ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app Y₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app X₃ ≫
      ((Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₁ X₂) X₃ ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₂ Y₃))
    (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)) (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))
have h₂ : ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).map f₂ ≫
        (NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app
    X₃ =
  ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app X₂ ≫
        (Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).map f₂).app
    X₃
Tactic: have h₂ := NatTrans.congr_app (((associator L W ε).hom.app Y₁).naturality f₂) X₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
h₁ :
  ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃ ≫
      ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app Y₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app X₃ ≫
      ((Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃
h₂ :
  ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).map f₂ ≫
          (NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app
      X₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app X₂ ≫
          (Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).map f₂).app
      X₃
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₁ X₂) X₃ ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₂ Y₃))
    (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)) (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))
have h₃ : ((Functor.map (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) f₁ ≫
            NatTrans.app (Iso.hom (associator L W ε)) Y₁).app
        X₂).app
    X₃ =
  ((NatTrans.app (Iso.hom (associator L W ε)) X₁ ≫
            Functor.map (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) f₁).app
        X₂).app
    X₃
Tactic: have h₃ := NatTrans.congr_app (NatTrans.congr_app ((associator L W ε).hom.naturality f₁) X₂) X₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
h₁ :
  ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃ ≫
      ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app Y₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app X₃ ≫
      ((Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃
h₂ :
  ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).map f₂ ≫
          (NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app
      X₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app X₂ ≫
          (Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).map f₂).app
      X₃
h₃ :
  ((Functor.map (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) f₁ ≫
              NatTrans.app (Iso.hom (associator L W ε)) Y₁).app
          X₂).app
      X₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) X₁ ≫
              Functor.map (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) f₁).app
          X₂).app
      X₃
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₁ X₂) X₃ ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₂ Y₃))
    (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)) (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))
have simp : NatTrans.app
      (Functor.map (tensorBifunctor L W ε) (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) X₂) ≫
        Functor.map (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) Y₁).map f₂))
      X₃ ≫
    (Functor.obj (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) Y₁).obj Y₂)).map f₃ ≫
      (((Iso.app (associator L W ε) Y₁).app Y₂).app Y₃).hom =
  (((Iso.app (associator L W ε) X₁).app X₂).app X₃).hom ≫
    NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) ((Functor.obj (tensorBifunctor L W ε) X₂).obj X₃) ≫
      (Functor.obj (tensorBifunctor L W ε) Y₁).map (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₂) X₃) ≫
        (Functor.obj (tensorBifunctor L W ε) Y₁).map ((Functor.obj (tensorBifunctor L W ε) Y₂).map f₃)
Tactic: simp +instances only [monoidalCategoryStruct, Functor.map_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
h₁ :
  ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃ ≫
      ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app Y₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app X₃ ≫
      ((Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃
h₂ :
  ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).map f₂ ≫
          (NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app
      X₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app X₂ ≫
          (Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).map f₂).app
      X₃
h₃ :
  ((Functor.map (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) f₁ ≫
              NatTrans.app (Iso.hom (associator L W ε)) Y₁).app
          X₂).app
      X₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) X₁ ≫
              Functor.map (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) f₁).app
          X₂).app
      X₃
⊢ NatTrans.app
        (Functor.map (tensorBifunctor L W ε) (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) X₂) ≫
          Functor.map (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) Y₁).map f₂))
        X₃ ≫
      (Functor.obj (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) Y₁).obj Y₂)).map f₃ ≫
        (((Iso.app (associator L W ε) Y₁).app Y₂).app Y₃).hom =
    (((Iso.app (associator L W ε) X₁).app X₂).app X₃).hom ≫
      NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) ((Functor.obj (tensorBifunctor L W ε) X₂).obj X₃) ≫
        (Functor.obj (tensorBifunctor L W ε) Y₁).map (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₂) X₃) ≫
          (Functor.obj (tensorBifunctor L W ε) Y₁).map ((Functor.obj (tensorBifunctor L W ε) Y₂).map f₃)
have dsimp : (NatTrans.app (Functor.map (tensorBifunctor L W ε) (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) X₂)) X₃ ≫
      NatTrans.app (Functor.map (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) Y₁).map f₂)) X₃) ≫
    (Functor.obj (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) Y₁).obj Y₂)).map f₃ ≫
      ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app Y₃ =
  ((NatTrans.app (Iso.hom (associator L W ε)) X₁).app X₂).app X₃ ≫
    NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) ((Functor.obj (tensorBifunctor L W ε) X₂).obj X₃) ≫
      (Functor.obj (tensorBifunctor L W ε) Y₁).map (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₂) X₃) ≫
        (Functor.obj (tensorBifunctor L W ε) Y₁).map ((Functor.obj (tensorBifunctor L W ε) Y₂).map f₃)
Tactic: dsimp at h₁ h₂ h₃ ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
⊢ Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄
have obtain : ∀ (X₁ : C) (e₁ : Functor.obj L' X₁ ≅ Y₁), Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄
Tactic: obtain ⟨X₁, ⟨e₁⟩⟩ : ∃ X₁, Nonempty ((L').obj X₁ ≅ Y₁) := ⟨_, ⟨(L').objObjPreimageIso Y₁⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
⊢ Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄
have obtain : ∀ (X₂ : C) (e₂ : Functor.obj L' X₂ ≅ Y₂), Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄
Tactic: obtain ⟨X₂, ⟨e₂⟩⟩ : ∃ X₂, Nonempty ((L').obj X₂ ≅ Y₂) := ⟨_, ⟨(L').objObjPreimageIso Y₂⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
⊢ Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄
have obtain : ∀ (X₃ : C) (e₃ : Functor.obj L' X₃ ≅ Y₃), Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄
Tactic: obtain ⟨X₃, ⟨e₃⟩⟩ : ∃ X₃, Nonempty ((L').obj X₃ ≅ Y₃) := ⟨_, ⟨(L').objObjPreimageIso Y₃⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
X₃ : C
e₃ : Functor.obj L' X₃ ≅ Y₃
⊢ Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄
have obtain : ∀ (X₄ : C) (e₄ : Functor.obj L' X₄ ≅ Y₄), Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄
Tactic: obtain ⟨X₄, ⟨e₄⟩⟩ : ∃ X₄, Nonempty ((L').obj X₄ ≅ Y₄) := ⟨_, ⟨(L').objObjPreimageIso Y₄⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
X₃ : C
e₃ : Functor.obj L' X₃ ≅ Y₃
X₄ : C
e₄ : Functor.obj L' X₄ ≅ Y₄
this :
  Pentagon.{v_2, u_2} (C := LocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂) (Functor.obj L' X₃)
    (Functor.obj L' X₄)
⊢ Iso.hom (α_ Y₁ Y₂ Y₃) ▷ Y₄ ≫
      Iso.hom (α_ Y₁ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₂ Y₃) Y₄) ≫
        Y₁ ◁ Iso.hom (α_ Y₂ Y₃ Y₄) =
    Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
have refine_1 : Eq (α :=
  tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃)
      Y₄ ⟶
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₂
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄)))
  (Iso.hom (α_ Y₁ Y₂ Y₃) ▷ Y₄ ≫
    Iso.hom (α_ Y₁ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₂ Y₃) Y₄) ≫
      Y₁ ◁ Iso.hom (α_ Y₂ Y₃ Y₄))
  ((((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
    (Iso.hom (α_ (Functor.obj L' X₁) (Functor.obj L' X₂) (Functor.obj L' X₃)) ▷ Functor.obj L' X₄ ≫
        Iso.hom
            (α_ (Functor.obj L' X₁)
              (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₂) (Functor.obj L' X₃))
              (Functor.obj L' X₄)) ≫
          Functor.obj L' X₁ ◁ Iso.hom (α_ (Functor.obj L' X₂) (Functor.obj L' X₃) (Functor.obj L' X₄))) ≫
      (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom))
Tactic: refine Eq.trans ?_ (((((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫= this =≫
      (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)).trans ?_)