awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (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 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ X₂ X₃ : C
⊢ Eq (α :=
    (((curriedTensorPrePre F).obj (L.obj X₁)).obj (L.obj X₂)).obj (L.obj X₃) ⟶
      (((curriedTensorPostPost' F).obj (L.obj X₁)).obj (L.obj X₂)).obj (L.obj X₃))
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app (LaxMonoidal.ofBifunctor.firstMap (Iso.hom (curriedTensorPreIsoPost L W F G))) (L.obj X₁))
        (L.obj X₂))
      (L.obj X₃))
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app (LaxMonoidal.ofBifunctor.secondMap (Iso.hom (curriedTensorPreIsoPost L W F G))) (L.obj X₁))
        (L.obj X₂))
      (L.obj X₃))
have refine_1 : Eq (α :=
  tensorObj.{v_3, u_3} (𝒞 := inst_2) (tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj X₁)) (F.obj (L.obj X₂)))
      (F.obj (L.obj X₃)) ⟶
    F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (L.obj X₁) (tensorObj.{v_2, u_2} (𝒞 := inst_1) (L.obj X₂) (L.obj X₃))))
  (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁)) (L.obj X₂) ▷ F.obj (L.obj X₃) ≫
    NatTrans.app
        (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G))
          (tensorObj.{v_2, u_2} (𝒞 := inst_1) (L.obj X₁) (L.obj X₂)))
        (L.obj X₃) ≫
      F.map (Iso.hom (α_ (L.obj X₁) (L.obj X₂) (L.obj X₃))))
  (Iso.hom (α_ (F.obj (L.obj X₁)) (F.obj (L.obj X₂)) (F.obj (L.obj X₃))) ≫
    F.obj (L.obj X₁) ◁ NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₂)) (L.obj X₃) ≫
      NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁))
        (tensorObj.{v_2, u_2} (𝒞 := inst_1) (L.obj X₂) (L.obj X₃)))
Tactic: dsimp [e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (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 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ Eq (α := F ⋙ tensorUnitLeft E ⟶ F) (LaxMonoidal.ofBifunctor.leftMapₗ F)
    (CategoryStruct.comp (Y := (curriedTensorPre F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
      (LaxMonoidal.ofBifunctor.topMapₗ
        (Iso.hom
          (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
            (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
      (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) ≫
        LaxMonoidal.ofBifunctor.bottomMapₗ F))
have refine_2 : ∀ (X₂ : C),
  Eq (α := (F ⋙ tensorUnitLeft E).obj (L.obj X₂) ⟶ F.obj (L.obj X₂))
    (NatTrans.app (LaxMonoidal.ofBifunctor.leftMapₗ F) (L.obj X₂))
    (NatTrans.app
      (CategoryStruct.comp (Y := (curriedTensorPre F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (LaxMonoidal.ofBifunctor.topMapₗ
          (Iso.hom
            (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
              (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
        (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) ≫
          LaxMonoidal.ofBifunctor.bottomMapₗ F))
      (L.obj X₂))
Tactic: refine natTrans_ext L W (fun X₂ ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (hypothesis)
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 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₂ : C
⊢ Eq (α := (F ⋙ tensorUnitLeft E).obj (L.obj X₂) ⟶ F.obj (L.obj X₂))
    (NatTrans.app (LaxMonoidal.ofBifunctor.leftMapₗ F) (L.obj X₂))
    (NatTrans.app
      (CategoryStruct.comp (Y := (curriedTensorPre F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (LaxMonoidal.ofBifunctor.topMapₗ
          (Iso.hom
            (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
              (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
        (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) ≫
          LaxMonoidal.ofBifunctor.bottomMapₗ F))
      (L.obj X₂))
have this : Eq (α :=
  ((curriedTensorPre F).obj (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))).obj (L.obj X₂) ⟶
    ((curriedTensorPost F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))).obj (L.obj X₂))
  (NatTrans.app
    ((curriedTensorPre F).map (Iso.inv (εIso L)) ≫
      NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
    (L.obj X₂))
  (NatTrans.app
    (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
      (curriedTensorPost F).map (Iso.inv (εIso L)))
    (L.obj X₂))
Tactic: have := NatTrans.congr_app ((curriedTensorPreIsoPost L W F G).hom.naturality (εIso L).inv)
      (L.obj X₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (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 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₂ : C
this :
  Eq (α :=
    ((curriedTensorPre F).obj (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))).obj (L.obj X₂) ⟶
      ((curriedTensorPost F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))).obj (L.obj X₂))
    (NatTrans.app
      ((curriedTensorPre F).map (Iso.inv (εIso L)) ≫
        NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
      (L.obj X₂))
    (NatTrans.app
      (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
        (curriedTensorPost F).map (Iso.inv (εIso L)))
      (L.obj X₂))
⊢ Eq (α := (F ⋙ tensorUnitLeft E).obj (L.obj X₂) ⟶ F.obj (L.obj X₂))
    (NatTrans.app (LaxMonoidal.ofBifunctor.leftMapₗ F) (L.obj X₂))
    (NatTrans.app
      (CategoryStruct.comp (Y := (curriedTensorPre F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (LaxMonoidal.ofBifunctor.topMapₗ
          (Iso.hom
            (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
              (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
        (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) ≫
          LaxMonoidal.ofBifunctor.bottomMapₗ F))
      (L.obj X₂))
have refine_2 : Eq (α :=
  tensorObj.{v_3, u_3} (𝒞 := inst_2) (tensorUnit.{v_3, u_3} E (𝒞 := inst_2)) (F.obj (L.obj X₂)) ⟶ F.obj (L.obj X₂))
  (Iso.hom (λ_ (F.obj (L.obj X₂))))
  (CategoryStruct.comp (Y :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))) (F.obj (L.obj X₂)))
    (CategoryStruct.comp (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (ε G)
        ((Lifting.iso L W G F).inv.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≫ F.map (η L)) ▷
      F.obj (L.obj X₂))
    (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (L.obj X₂) ≫
      F.map (Iso.hom (λ_ (L.obj X₂)))))
Tactic: dsimp [e] at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (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 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₂ : C
this :
  Eq (α :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) (F.obj (L.obj X₂)) ⟶
      F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) (L.obj X₂)))
    (F.map (η L) ▷ F.obj (L.obj X₂) ≫
      NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (L.obj X₂))
    (NatTrans.app
        (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (L.obj X₂) ≫
      F.map (η L ▷ L.obj X₂))
⊢ Eq (α :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (tensorUnit.{v_3, u_3} E (𝒞 := inst_2)) (F.obj (L.obj X₂)) ⟶ F.obj (L.obj X₂))
    (Iso.hom (λ_ (F.obj (L.obj X₂))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))) (F.obj (L.obj X₂)))
      (CategoryStruct.comp (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (ε G)
          ((Lifting.iso L W G F).inv.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≫ F.map (η L)) ▷
        F.obj (L.obj X₂))
      (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
          (L.obj X₂) ≫
        F.map (Iso.hom (λ_ (L.obj X₂)))))
have refine_2 : Eq (α :=
  tensorObj.{v_3, u_3} (𝒞 := inst_2) (tensorUnit.{v_3, u_3} E (𝒞 := inst_2)) (F.obj (L.obj X₂)) ⟶ F.obj (L.obj X₂))
  (Iso.hom (λ_ (F.obj (L.obj X₂))))
  (CategoryStruct.comp (Y :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (F.obj (L.obj X₂)))
    (ε G ▷ F.obj (L.obj X₂))
    ((Lifting.iso L W G F).inv.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ▷ F.obj (L.obj X₂) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))) (F.obj (L.obj X₂)))
        (F.map (η L) ▷ F.obj (L.obj X₂))
        (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
            (L.obj X₂) ≫
          F.map (Iso.hom (λ_ (L.obj X₂))))))
Tactic: monoidal_simps
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (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 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ Eq (α := F ⋙ tensorUnitRight E ⟶ F) (LaxMonoidal.ofBifunctor.leftMapᵣ F)
    (CategoryStruct.comp (Y := (curriedTensorPre F).flip.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
      (LaxMonoidal.ofBifunctor.topMapᵣ
        (Iso.hom
          (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
            (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
      (CategoryStruct.comp (Y :=
        (obj (flipFunctor D D E) (curriedTensorPost F)).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (NatTrans.app (map (flipFunctor D D E) (Iso.hom (curriedTensorPreIsoPost L W F G)))
          (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (LaxMonoidal.ofBifunctor.bottomMapᵣ F)))
have refine_3 : ∀ (X₁ : C),
  Eq (α := (F ⋙ tensorUnitRight E).obj (L.obj X₁) ⟶ F.obj (L.obj X₁))
    (NatTrans.app (LaxMonoidal.ofBifunctor.leftMapᵣ F) (L.obj X₁))
    (NatTrans.app
      (CategoryStruct.comp (Y := (curriedTensorPre F).flip.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (LaxMonoidal.ofBifunctor.topMapᵣ
          (Iso.hom
            (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
              (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
        (CategoryStruct.comp (Y :=
          (obj (flipFunctor D D E) (curriedTensorPost F)).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
          (NatTrans.app (map (flipFunctor D D E) (Iso.hom (curriedTensorPreIsoPost L W F G)))
            (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
          (LaxMonoidal.ofBifunctor.bottomMapᵣ F)))
      (L.obj X₁))
Tactic: refine natTrans_ext L W (fun X₁ ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (hypothesis)
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 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ : C
⊢ Eq (α := (F ⋙ tensorUnitRight E).obj (L.obj X₁) ⟶ F.obj (L.obj X₁))
    (NatTrans.app (LaxMonoidal.ofBifunctor.leftMapᵣ F) (L.obj X₁))
    (NatTrans.app
      (CategoryStruct.comp (Y := (curriedTensorPre F).flip.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (LaxMonoidal.ofBifunctor.topMapᵣ
          (Iso.hom
            (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
              (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
        (CategoryStruct.comp (Y :=
          (obj (flipFunctor D D E) (curriedTensorPost F)).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
          (NatTrans.app (map (flipFunctor D D E) (Iso.hom (curriedTensorPreIsoPost L W F G)))
            (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
          (LaxMonoidal.ofBifunctor.bottomMapᵣ F)))
      (L.obj X₁))
have this : Eq (α :=
  ((curriedTensorPre F).obj (L.obj X₁)).obj (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⟶
    ((curriedTensorPost F).obj (L.obj X₁)).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
  (((curriedTensorPre F).obj (L.obj X₁)).map (Iso.inv (εIso L)) ≫
    NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁))
      (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
  (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁))
      (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
    ((curriedTensorPost F).obj (L.obj X₁)).map (Iso.inv (εIso L)))
Tactic: have := ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).naturality (εIso L).inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (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 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ : C
this :
  Eq (α :=
    ((curriedTensorPre F).obj (L.obj X₁)).obj (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⟶
      ((curriedTensorPost F).obj (L.obj X₁)).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
    (((curriedTensorPre F).obj (L.obj X₁)).map (Iso.inv (εIso L)) ≫
      NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁))
        (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
    (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁))
        (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
      ((curriedTensorPost F).obj (L.obj X₁)).map (Iso.inv (εIso L)))
⊢ Eq (α := (F ⋙ tensorUnitRight E).obj (L.obj X₁) ⟶ F.obj (L.obj X₁))
    (NatTrans.app (LaxMonoidal.ofBifunctor.leftMapᵣ F) (L.obj X₁))
    (NatTrans.app
      (CategoryStruct.comp (Y := (curriedTensorPre F).flip.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (LaxMonoidal.ofBifunctor.topMapᵣ
          (Iso.hom
            (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
              (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
        (CategoryStruct.comp (Y :=
          (obj (flipFunctor D D E) (curriedTensorPost F)).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
          (NatTrans.app (map (flipFunctor D D E) (Iso.hom (curriedTensorPreIsoPost L W F G)))
            (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
          (LaxMonoidal.ofBifunctor.bottomMapᵣ F)))
      (L.obj X₁))
have refine_3 : Eq (α :=
  tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj X₁)) (tensorUnit.{v_3, u_3} E (𝒞 := inst_2)) ⟶ F.obj (L.obj X₁))
  (Iso.hom (ρ_ (F.obj (L.obj X₁))))
  (CategoryStruct.comp (Y :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj X₁)) (F.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))))
    (F.obj (L.obj X₁) ◁
      CategoryStruct.comp (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (ε G)
        ((Lifting.iso L W G F).inv.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≫ F.map (η L)))
    (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁))
        (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) ≫
      F.map (Iso.hom (ρ_ (L.obj X₁)))))
Tactic: dsimp [e] at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (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 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ : C
this :
  Eq (α :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj X₁)) (F.obj (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) ⟶
      F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (L.obj X₁) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))))
    (F.obj (L.obj X₁) ◁ F.map (η L) ≫
      NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁))
        (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
    (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁))
        (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
      F.map (L.obj X₁ ◁ η L))
⊢ Eq (α :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj X₁)) (tensorUnit.{v_3, u_3} E (𝒞 := inst_2)) ⟶ F.obj (L.obj X₁))
    (Iso.hom (ρ_ (F.obj (L.obj X₁))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj X₁)) (F.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))))
      (F.obj (L.obj X₁) ◁
        CategoryStruct.comp (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (ε G)
          ((Lifting.iso L W G F).inv.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≫ F.map (η L)))
      (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁))
          (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) ≫
        F.map (Iso.hom (ρ_ (L.obj X₁)))))
have refine_3 : Eq (α :=
  tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj X₁)) (tensorUnit.{v_3, u_3} E (𝒞 := inst_2)) ⟶ F.obj (L.obj X₁))
  (Iso.hom (ρ_ (F.obj (L.obj X₁))))
  (CategoryStruct.comp (Y :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj X₁)) (G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
    (F.obj (L.obj X₁) ◁ ε G)
    (F.obj (L.obj X₁) ◁ (Lifting.iso L W G F).inv.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj X₁)) (F.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))))
        (F.obj (L.obj X₁) ◁ F.map (η L))
        (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁))
            (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) ≫
          F.map (Iso.hom (ρ_ (L.obj X₁))))))
Tactic: monoidal_simps
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (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 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
this : F.Monoidal := functorMonoidalOfComp L W F G
⊢ NatTrans.IsMonoidal (Lifting.iso L W G F).hom
have refine_1 : Eq (α := tensorUnit.{v_3, u_3} E (𝒞 := inst_2) ⟶ G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
  (ε (L ⋙ F) ≫ (Lifting.iso L W G F).hom.app (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (ε G)
Tactic: refine ⟨?_, fun _ _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (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 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
this : F.Monoidal := functorMonoidalOfComp L W F G
refine_1 :
  Eq (α := tensorUnit.{v_3, u_3} E (𝒞 := inst_2) ⟶ G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (ε (L ⋙ F) ≫ (Lifting.iso L W G F).hom.app (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (ε G)
⊢ NatTrans.IsMonoidal (Lifting.iso L W G F).hom
have refine_2 : ∀ (x x_1 : C),
  Eq (α :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) ((L ⋙ F).obj x) ((L ⋙ F).obj x_1) ⟶
      G.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x x_1))
    (μ (L ⋙ F) x x_1 ≫ (Lifting.iso L W G F).hom.app (tensorObj.{v_1, u_1} (𝒞 := inst) x x_1))
    (((Lifting.iso L W G F).hom.app x ⊗ₘ (Lifting.iso L W G F).hom.app x_1) ≫ μ G x x_1)
Tactic: refine ⟨?_, fun _ _ ↦ ?_⟩