awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
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)))

Tactic:
natTrans_ext L W (fun X₁ ↦ ?_)

Premises used: CategoryTheory.Localization.natTrans_ext
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
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
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₁))
⊢ 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)))

Tactic:
refine natTrans_ext L W (fun X₁ ↦ ?_)

Premises used: CategoryTheory.Localization.natTrans_ext
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
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 (α :=
    ((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
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
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)))
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₁)))))
⊢ 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:
dsimp [e] at this ⊢
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
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))
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₁))))))
⊢ 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:
monoidal_simps
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
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₁)) (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:
simp [reassoc_of% this, curriedTensorPreIsoPost_hom_app_app, tensorHom_def,
      whisker_exchange_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, ← map_comp]

Premises used: CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
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
⊢ Eq (α := tensorUnit.{v_3, u_3} E (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))) (ε F)
    (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)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
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
X Y : C
⊢ Eq (α :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj X)) (F.obj (L.obj Y)) ⟶
      F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (L.obj X) (L.obj Y)))
    (μ F (L.obj X) (L.obj Y))
    (((Lifting.iso L W G F).hom.app X ⊗ₘ (Lifting.iso L W G F).hom.app Y) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) (μ G X Y)
        ((Lifting.iso L W G F).inv.app (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) ≫ F.map (δ L X Y)))

Tactic:
simp [Functor.CoreMonoidal.toLaxMonoidal_μ, curriedTensorPreIsoPost_hom_app_app]

Premises used: CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app, CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal_μ
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
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

Tactic:
⟨?_, fun _ _ ↦ ?_⟩

Premises used: CategoryTheory.NatTrans.IsMonoidal.mk
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
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)
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)
⊢ NatTrans.IsMonoidal (Lifting.iso L W G F).hom

Tactic:
refine ⟨?_, fun _ _ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
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
⊢ 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:
simp [functorMonoidalOfComp_ε]

Premises used: CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
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
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:
simp [functorMonoidalOfComp_μ]

Premises used: CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
obtain : ∀ (P : Precylinder.{v_1, u_1} X) (h : P.LeftHomotopy f₀ f₁) (hπ : W P.π), F.map f₀ = F.map f₁
⊢ F.map f₀ = F.map f₁

Tactic:
obtain ⟨P, h, hπ⟩ := hr f₀ f₁ hf
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
P : Precylinder.{v_1, u_1} X
h : P.LeftHomotopy f₀ f₁
hπ : W P.π
simp : F.map P.i₀ ≫ F.map h.h = F.map P.i₁ ≫ F.map h.h
⊢ F.map f₀ = F.map f₁

Tactic:
simp only [← h.h₀, ← h.h₁, Functor.map_comp]

Premises used: HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀, HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
P : Precylinder.{v_1, u_1} X
h : P.LeftHomotopy f₀ f₁
hπ : W P.π
e_a : F.map P.i₀ = F.map P.i₁
⊢ F.map P.i₀ ≫ F.map h.h = F.map P.i₁ ≫ F.map h.h

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
P : Precylinder.{v_1, u_1} X
h : P.LeftHomotopy f₀ f₁
hπ : W P.π
⊢ IsIso (F.map P.π)

Tactic:
have := hF _ hπ
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
P : Precylinder.{v_1, u_1} X
h : P.LeftHomotopy f₀ f₁
hπ : W P.π
this : IsIso (F.map P.π)
⊢ F.map P.i₀ = F.map P.i₁

Tactic:
simp [← cancel_mono (F.map P.π), ← Functor.map_comp]

Premises used: HomotopicalAlgebra.Precylinder.π, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} (Quotient r) E
h : functor r ⋙ F₁ = functor r ⋙ F₂
h_obj : ∀ (X : Quotient r), F₁.obj X = F₂.obj X
h_map : autoParam (∀ (X Y : Quotient r) (f : X ⟶ Y), F₁.map f = eqToHom ⋯ ≫ F₂.map f ≫ eqToHom ⋯) Functor.ext._auto_1
⊢ F₁ = F₂

Tactic:
fapply Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} (Quotient r) E
h : functor r ⋙ F₁ = functor r ⋙ F₂
X : C
⊢ F₁.obj (mk (r := r) X) = F₂.obj (mk (r := r) X)

Tactic:
Functor.congr_obj h X

Premises used: CategoryTheory.Functor.congr_obj