awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
⊢ Functor.Faithful (C := CommRingObjCat.{v, u} C) (forget₂RingObjCat C)

Tactic:
(fullyFaithfulForget₂RingObjCat C).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.CommRingObjCat.fullyFaithfulForget₂RingObjCat
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
⊢ Functor.Full (C := CommRingObjCat.{v, u} C) (forget₂RingObjCat C)

Tactic:
(fullyFaithfulForget₂RingObjCat C).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.CommRingObjCat.fullyFaithfulForget₂RingObjCat
-- Module: Mathlib.CategoryTheory.Monoidal.Skeleton
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : Skeleton.{v, u} C
⊢ X * Y = toSkeleton (tensorObj.{v, u} (𝒞 := inst) (Quotient.out X) (Quotient.out Y))

Tactic:
rfl

Premises used: Quot.out, Quotient.out, Classical.choose, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Skeleton
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
⊢ Eq (α := Skeleton.{v, u} C) 1 (toSkeleton (tensorUnit.{v, u} C (𝒞 := inst)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Skeleton
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
⊢ toSkeleton (tensorObj.{v, u} (𝒞 := inst) X Y) = HMul.hMul (α := Skeleton.{v, u} C) (toSkeleton X) (toSkeleton Y)

Tactic:
let φ := (skeletonEquivalence C).symm.unitIso.app; Quotient.sound ⟨φ X ⊗ᵢ φ Y⟩

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.MonoidalCategory.tensorIso, Nonempty.intro, CategoryTheory.InducedCategory, Quotient.sound, CategoryTheory.Iso.app, CategoryTheory.skeletonEquivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Skeleton
-- Module: Mathlib.CategoryTheory.Monoidal.Skeleton
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : MonoidalCategory.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
e : Equivalence.{v, v_1, u, u_1} C D
inst_4 : F.Monoidal
hC : Skeletal.{v, u} C
hD : Skeletal.{v_1, u_1} D
x : Monoid C := monoidOfSkeletalMonoidal hC
x_1 : Monoid D := monoidOfSkeletalMonoidal hD
⊢ C →* D

Tactic:
exact
  { toFun := F.obj
    map_one' := hD ⟨(Monoidal.εIso F).symm⟩
    map_mul' X Y := hD ⟨(Monoidal.μIso F X Y).symm⟩ }
-- Module: Mathlib.CategoryTheory.Monoidal.Skeleton
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : MonoidalCategory.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
e : Equivalence.{v, v_1, u, u_1} C D
inst_4 : e.functor.Monoidal
hC : Skeletal.{v, u} C
hD : Skeletal.{v_1, u_1} D
x : Monoid C := monoidOfSkeletalMonoidal hC
x_1 : Monoid D := monoidOfSkeletalMonoidal hD
⊢ C ≃* D

Tactic:
exact
  { toFun := e.functor.obj
    invFun := e.inverse.obj
    left_inv X := hC ⟨(e.unitIso.app X).symm⟩
    right_inv X := hD ⟨e.counitIso.app X⟩
    map_mul' X Y := hD ⟨(Monoidal.μIso e.functor X Y).symm⟩ }
-- Module: Mathlib.CategoryTheory.Monoidal.Subcategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P₁ P₂ Q : ObjectProperty.{v, u} C
inst_2 : P₁.TensorLE P₂ Q
X₁ X₂ : C
h₁ : P₁ X₁
h₂ : P₂ X₂
⊢ Q (tensorObj.{v, u} (𝒞 := inst) X₁ X₂)

Tactic:
TensorLE.prop_tensor _ _ h₁ h₂

Premises used: CategoryTheory.ObjectProperty.TensorLE.prop_tensor
-- Module: Mathlib.CategoryTheory.Monoidal.Subcategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.ContainsUnit
⊢ P (tensorUnit.{v, u} C (𝒞 := inst))

Tactic:
ContainsUnit.prop_unit

Premises used: CategoryTheory.ObjectProperty.ContainsUnit.prop_unit
-- Module: Mathlib.CategoryTheory.Monoidal.Subcategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
inst_3 : P.IsMonoidalClosed
X Y : C
hX : P X
hY : P Y
⊢ P (Functor.obj.{v, v, u, u} (ihom X) Y)

Tactic:
IsMonoidalClosed.prop_ihom _ _ hX hY

Premises used: CategoryTheory.ObjectProperty.IsMonoidalClosed.prop_ihom
-- Module: Mathlib.CategoryTheory.Monoidal.Subcategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsMonoidal
⊢ Eq (α :=
    tensorUnit.{v, u} C (𝒞 := inst) ⟶ P.ι.obj (tensorUnit.{v, u} P.FullSubcategory (𝒞 := FullSubcategory.category P)))
    (ε P.ι) (𝟙 (tensorUnit.{v, u} C (𝒞 := inst)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Subcategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsMonoidal
X Y : P.FullSubcategory
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (P.ι.obj X) (P.ι.obj Y) ⟶
      P.ι.obj (tensorObj.{v, u} (𝒞 := FullSubcategory.category P) X Y))
    (μ P.ι X Y) (𝟙 (tensorObj.{v, u} (𝒞 := inst) (P.ι.obj X) (P.ι.obj Y)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Subcategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsMonoidal
X Y : P.FullSubcategory
⊢ δ P.ι X Y = 𝟙 (P.ι.obj (tensorObj.{v, u} (𝒞 := FullSubcategory.category P) X Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Subcategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsMonoidal
inst_3 : Preadditive.{v, u} C
inst_4 : MonoidalPreadditive.{v, u} C
⊢ MonoidalPreadditive.{v, u} P.FullSubcategory

Tactic:
monoidalPreadditive_of_faithful P.ι

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.monoidalPreadditive_of_faithful
-- Module: Mathlib.CategoryTheory.Monoidal.Subcategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsMonoidal
inst_3 : Preadditive.{v, u} C
R : Type u_1
inst_4 : Ring R
inst_5 : Linear.{u_1, v, u} R C
inst_6 : MonoidalPreadditive.{v, u} C
inst_7 : MonoidalLinear.{u_1, v, u} R C
⊢ MonoidalLinear.{u_1, v, u} R P.FullSubcategory

Tactic:
.ofFaithful R P.ι

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.MonoidalLinear.ofFaithful
-- Module: Mathlib.CategoryTheory.Monoidal.Subcategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsMonoidal
P' : ObjectProperty.{v, u} C
inst_3 : P'.IsMonoidal
h : P ≤ P'
⊢ Eq (α :=
    tensorUnit.{v, u} P'.FullSubcategory (𝒞 := FullSubcategory.category P') ⟶
      (ιOfLE (P := P) (P' := P') h).obj (tensorUnit.{v, u} P.FullSubcategory (𝒞 := FullSubcategory.category P)))
    (ε (ιOfLE (P := P) (P' := P') h)) (𝟙 (tensorUnit.{v, u} P'.FullSubcategory (𝒞 := FullSubcategory.category P')))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Subcategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsMonoidal
P' : ObjectProperty.{v, u} C
inst_3 : P'.IsMonoidal
h : P ≤ P'
⊢ Eq (α :=
    (ιOfLE (P := P) (P' := P') h).obj (tensorUnit.{v, u} P.FullSubcategory (𝒞 := FullSubcategory.category P)) ⟶
      tensorUnit.{v, u} P'.FullSubcategory (𝒞 := FullSubcategory.category P'))
    (η (ιOfLE (P := P) (P' := P') h))
    (𝟙 ((ιOfLE (P := P) (P' := P') h).obj (tensorUnit.{v, u} P.FullSubcategory (𝒞 := FullSubcategory.category P))))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Subcategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsMonoidal
P' : ObjectProperty.{v, u} C
inst_3 : P'.IsMonoidal
h : P ≤ P'
X Y : P.FullSubcategory
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := FullSubcategory.category P') ((ιOfLE (P := P) (P' := P') h).obj X)
        ((ιOfLE (P := P) (P' := P') h).obj Y) ⟶
      (ιOfLE (P := P) (P' := P') h).obj (tensorObj.{v, u} (𝒞 := FullSubcategory.category P) X Y))
    (μ (ιOfLE (P := P) (P' := P') h) X Y)
    (𝟙
      (tensorObj.{v, u} (𝒞 := FullSubcategory.category P') ((ιOfLE (P := P) (P' := P') h).obj X)
        ((ιOfLE (P := P) (P' := P') h).obj Y)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Subcategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsMonoidal
P' : ObjectProperty.{v, u} C
inst_3 : P'.IsMonoidal
h : P ≤ P'
X Y : P.FullSubcategory
⊢ Eq (α :=
    (ιOfLE (P := P) (P' := P') h).obj (tensorObj.{v, u} (𝒞 := FullSubcategory.category P) X Y) ⟶
      tensorObj.{v, u} (𝒞 := FullSubcategory.category P') ((ιOfLE (P := P) (P' := P') h).obj X)
        ((ιOfLE (P := P) (P' := P') h).obj Y))
    (δ (ιOfLE (P := P) (P' := P') h) X Y)
    (𝟙 ((ιOfLE (P := P) (P' := P') h).obj (tensorObj.{v, u} (𝒞 := FullSubcategory.category P) X Y)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Subcategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsMonoidal
inst_3 : MonoidalClosed.{v, u} C
inst_4 : P.IsMonoidalClosed
X Y : P.FullSubcategory
⊢ (Functor.obj.{v, v, u, u} (ihom X) Y).obj (P := P) = Functor.obj.{v, v, u, u} (ihom (X.obj (P := P))) (Y.obj (P := P))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Subcategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsMonoidal
inst_3 : MonoidalClosed.{v, u} C
inst_4 : P.IsMonoidalClosed
X Y Z : P.FullSubcategory
f : Y ⟶ Z
⊢ Eq (α := (Functor.obj.{v, v, u, u} (ihom X) Y).obj (P := P) ⟶ (Functor.obj.{v, v, u, u} (ihom X) Z).obj (P := P))
    (InducedCategory.Hom.hom (Functor.map (ihom X) f)) (Functor.map (ihom (X.obj (P := P))) f.hom)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Tor
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Abelian.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasProjectiveResolutions.{v_1, u_1} C
X Y : C
inst_5 : Projective.{v_1, u_1} Y
n : ℕ
⊢ IsZero.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (Tor C (n + 1)) X) Y)

Tactic:
apply Functor.isZero_leftDerived_obj_projective_succ

Premises used: CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ
-- Module: Mathlib.CategoryTheory.Monoidal.Tor
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Abelian.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasProjectiveResolutions.{v_1, u_1} C
X Y : C
inst_5 : Projective.{v_1, u_1} X
n : ℕ
⊢ IsZero.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (Tor' C (n + 1)) X) Y)

Tactic:
apply Functor.isZero_leftDerived_obj_projective_succ

Premises used: CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
X₁ Y₁ X₂ Y₂ : D
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
rw :
  (fData.μIso X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (fData.μIso Y₁ Y₂).hom =
    ((fData.μIso X₁ X₂).inv ≫ F.map f ▷ F.obj X₂ ≫ (fData.μIso Y₁ X₂).hom) ≫
      (fData.μIso Y₁ X₂).inv ≫ F.obj Y₁ ◁ F.map g ≫ (fData.μIso Y₁ Y₂).hom
⊢ Eq (α := F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X₁ X₂) ⟶ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y₁ Y₂))
    (F.map (f ⊗ₘ g)) (F.map (f ▷ X₂ ≫ Y₁ ◁ g))

Tactic:
rw [fData.tensorHom_eq, Functor.map_comp, fData.whiskerRight_eq, fData.whiskerLeft_eq]

Premises used: CategoryTheory.Monoidal.InducingFunctorData.tensorHom_eq, CategoryTheory.Monoidal.InducingFunctorData.whiskerRight_eq, CategoryTheory.Monoidal.InducingFunctorData.whiskerLeft_eq, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
X₁ Y₁ X₂ Y₂ : D
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (fData.μIso X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (fData.μIso Y₁ Y₂).hom =
    ((fData.μIso X₁ X₂).inv ≫ F.map f ▷ F.obj X₂ ≫ (fData.μIso Y₁ X₂).hom) ≫
      (fData.μIso Y₁ X₂).inv ≫ F.obj Y₁ ◁ F.map g ≫ (fData.μIso Y₁ Y₂).hom

Tactic:
simp only [tensorHom_def, assoc, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
X₁ X₂ : D
mk :
  ∀
    (μIso :
      (X Y : D) → tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y) ≅ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)),
    (∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso X Y₂).hom) →
      (∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso X₂ Y).hom) →
        (∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
            F.map (f ⊗ₘ g) = (μIso X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso Y₁ Y₂).hom) →
          ∀ (εIso : tensorUnit.{v₁, u₁} C (𝒞 := inst) ≅ F.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))),
            (∀ (X Y Z : D),
                F.map (Iso.hom (α_ X Y Z)) =
                  ((Iso.symm (μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) Z) ≪≫
                        ((μIso X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
                      α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫
                        (Iso.refl (F.obj X) ⊗ᵢ μIso Y Z) ≪≫ μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)).hom) →
              (∀ (X : D),
                  F.map (Iso.hom (λ_ X)) =
                    ((Iso.symm (μIso (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) X) ≪≫ (εIso.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫
                        λ_ (F.obj X)).hom) →
                (∀ (X : D),
                    F.map (Iso.hom (ρ_ X)) =
                      ((Iso.symm (μIso X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso.symm)) ≪≫
                          ρ_ (F.obj X)).hom) →
                  F.map (𝟙 X₁ ⊗ₘ 𝟙 X₂) = F.map (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X₁ X₂))
⊢ F.map (𝟙 X₁ ⊗ₘ 𝟙 X₂) = F.map (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X₁ X₂))

Tactic:
cases fData
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : D
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
mk :
  ∀
    (μIso :
      (X Y : D) → tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y) ≅ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)),
    (∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso X Y₂).hom) →
      (∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso X₂ Y).hom) →
        (∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
            F.map (f ⊗ₘ g) = (μIso X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso Y₁ Y₂).hom) →
          ∀ (εIso : tensorUnit.{v₁, u₁} C (𝒞 := inst) ≅ F.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))),
            (∀ (X Y Z : D),
                F.map (Iso.hom (α_ X Y Z)) =
                  ((Iso.symm (μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) Z) ≪≫
                        ((μIso X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
                      α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫
                        (Iso.refl (F.obj X) ⊗ᵢ μIso Y Z) ≪≫ μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)).hom) →
              (∀ (X : D),
                  F.map (Iso.hom (λ_ X)) =
                    ((Iso.symm (μIso (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) X) ≪≫ (εIso.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫
                        λ_ (F.obj X)).hom) →
                (∀ (X : D),
                    F.map (Iso.hom (ρ_ X)) =
                      ((Iso.symm (μIso X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso.symm)) ≪≫
                          ρ_ (F.obj X)).hom) →
                  Eq (α :=
                    F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X₁ X₂) ⟶ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Z₁ Z₂))
                    (F.map ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))) (F.map (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂))
⊢ Eq (α := F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X₁ X₂) ⟶ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Z₁ Z₂))
    (F.map ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))) (F.map (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂))

Tactic:
cases fData
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
X Y : D
⊢ F.map (X ◁ 𝟙 Y) = F.map (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))

Tactic:
simp [fData.whiskerLeft_eq]

Premises used: CategoryTheory.Monoidal.InducingFunctorData.whiskerLeft_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
X Y : D
⊢ F.map (𝟙 X ▷ Y) = F.map (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))

Tactic:
simp [fData.whiskerRight_eq]

Premises used: CategoryTheory.Monoidal.InducingFunctorData.whiskerRight_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
X₁ X₂ X₃ Y₁ Y₂ Y₃ : D
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Eq (α :=
    F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X₁ X₂) X₃) ⟶
      F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y₁ (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y₂ Y₃)))
    (F.map (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃))) (F.map (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)))

Tactic:
simp [fData.tensorHom_eq, fData.associator_eq, tensorHom_def, whisker_exchange_assoc]

Premises used: CategoryTheory.Monoidal.InducingFunctorData.associator_eq, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.Monoidal.InducingFunctorData.tensorHom_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
X Y : D
f : X ⟶ Y
⊢ F.map (tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ◁ f ≫ Iso.hom (λ_ Y)) = F.map (Iso.hom (λ_ X) ≫ f)

Tactic:
simp [fData.leftUnitor_eq, fData.whiskerLeft_eq, whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.Monoidal.InducingFunctorData.whiskerLeft_eq, CategoryTheory.Monoidal.InducingFunctorData.leftUnitor_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
X Y : D
f : X ⟶ Y
⊢ Eq (α := F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) ⟶ F.obj Y)
    (F.map (f ▷ tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ≫ Iso.hom (ρ_ Y))) (F.map (Iso.hom (ρ_ X) ≫ f))

Tactic:
simp [fData.rightUnitor_eq, fData.whiskerRight_eq, ← whisker_exchange_assoc]

Premises used: CategoryTheory.Monoidal.InducingFunctorData.rightUnitor_eq, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.Monoidal.InducingFunctorData.whiskerRight_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
a : F.obj W ◁ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y)) (F.obj Z))
| F.obj W ◁ (fData.μIso X Y).hom ▷ F.obj Z ≫ F.obj W ◁ (fData.μIso X Y).inv ▷ F.obj Z

Tactic:
rw [← whiskerLeft_comp, hom_inv_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.hom_inv_whiskerRight, CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
⊢ Iso.inv (fData.μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) Y) ▷ F.obj Z ≫
      (fData.μIso W X).inv ▷ F.obj Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj W) (F.obj X) (F.obj Y)) ▷ F.obj Z ≫
          Iso.hom (α_ (F.obj W) (tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y)) (F.obj Z)) ≫
            (((F.obj W ◁
                      𝟙
                        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y))
                          (F.obj Z)) ≫
                    F.obj W ◁ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z))) ≫
                  F.obj W ◁ F.obj X ◁ (fData.μIso Y Z).hom) ≫
                F.obj W ◁ Iso.hom (fData.μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) ≫
              Iso.hom (fData.μIso W (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) =
    Iso.inv (fData.μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X) Y) ▷ F.obj Z ≫
      Iso.hom (α_ (F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) W X)) (F.obj Y) (F.obj Z)) ≫
        (fData.μIso W X).inv ▷ tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj Y) (F.obj Z) ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj W) (F.obj X) ◁ (fData.μIso Y Z).hom ≫
            Iso.hom (α_ (F.obj W) (F.obj X) (F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) ≫
              F.obj W ◁ Iso.hom (fData.μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
                Iso.hom (fData.μIso W (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))

Tactic:
simp