[GOAL]
C : Type u
X Y Z : F C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((fun x x_1 => x ≈ x_1) ⇒ (fun x x_1 => x ≈ x_1) ⇒ fun x x_1 => x ≈ x_1) Hom.comp Hom.comp
[PROOFSTEP]
intro f f' hf g g' hg
[GOAL]
C : Type u
X Y Z : F C
f✝ : X ⟶ Y
g✝ : Y ⟶ Z
f f' : X ⟶ᵐ Y
hf : f ≈ f'
g g' : Y ⟶ᵐ Z
hg : g ≈ g'
⊢ Hom.comp f g ≈ Hom.comp f' g'
[PROOFSTEP]
exact comp hf hg
[GOAL]
C : Type u
⊢ ∀ {X Y : F C} (f : X ⟶ Y), 𝟙 X ≫ f = f
[PROOFSTEP]
rintro X Y ⟨f⟩
[GOAL]
case mk
C : Type u
X Y : F C
f✝ : X ⟶ Y
f : X ⟶ᵐ Y
⊢ 𝟙 X ≫ Quot.mk Setoid.r f = Quot.mk Setoid.r f
[PROOFSTEP]
exact Quotient.sound (id_comp f)
[GOAL]
C : Type u
⊢ ∀ {X Y : F C} (f : X ⟶ Y), f ≫ 𝟙 Y = f
[PROOFSTEP]
rintro X Y ⟨f⟩
[GOAL]
case mk
C : Type u
X Y : F C
f✝ : X ⟶ Y
f : X ⟶ᵐ Y
⊢ Quot.mk Setoid.r f ≫ 𝟙 Y = Quot.mk Setoid.r f
[PROOFSTEP]
exact Quotient.sound (comp_id f)
[GOAL]
C : Type u
⊢ ∀ {W X Y Z : F C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
rintro W X Y Z ⟨f⟩ ⟨g⟩ ⟨h⟩
[GOAL]
case mk.mk.mk
C : Type u
W X Y Z : F C
f✝ : W ⟶ X
f : W ⟶ᵐ X
g✝ : X ⟶ Y
g : X ⟶ᵐ Y
h✝ : Y ⟶ Z
h : Y ⟶ᵐ Z
⊢ (Quot.mk Setoid.r f ≫ Quot.mk Setoid.r g) ≫ Quot.mk Setoid.r h =
    Quot.mk Setoid.r f ≫ Quot.mk Setoid.r g ≫ Quot.mk Setoid.r h
[PROOFSTEP]
exact Quotient.sound (assoc f g h)
[GOAL]
C : Type u
X₁ Y₁ X₂ Y₂ : F C
⊢ ((fun x x_1 => x ≈ x_1) ⇒ (fun x x_1 => x ≈ x_1) ⇒ fun x x_1 => x ≈ x_1) Hom.tensor Hom.tensor
[PROOFSTEP]
intro _ _ h _ _ h'
[GOAL]
C : Type u
X₁ Y₁ X₂ Y₂ : F C
a✝¹ b✝¹ : X₁ ⟶ᵐ Y₁
h : a✝¹ ≈ b✝¹
a✝ b✝ : X₂ ⟶ᵐ Y₂
h' : a✝ ≈ b✝
⊢ Hom.tensor a✝¹ a✝ ≈ Hom.tensor b✝¹ b✝
[PROOFSTEP]
exact HomEquiv.tensor h h'
[GOAL]
C : Type u
⊢ ∀ {X₁ Y₁ X₂ Y₂ : F C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    (fun X₁ Y₁ X₂ Y₂ =>
          Quotient.map₂ Hom.tensor
            (_ :
              ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
        X₁ Y₁ X₂ Y₂ f g =
      (fun {X₁ X₂} f Y =>
            Quotient.map (fun f' => Hom.tensor f' (Hom.id Y))
              (_ : ∀ (x x_1 : X₁ ⟶ᵐ X₂), x ≈ x_1 → HomEquiv (Hom.tensor x (Hom.id Y)) (Hom.tensor x_1 (Hom.id Y))) f)
          f X₂ ≫
        (fun X x x_1 f =>
            Quotient.map (fun f' => Hom.tensor (Hom.id X) f')
              (_ : ∀ (x_2 x_3 : x ⟶ᵐ x_1), x_2 ≈ x_3 → HomEquiv (Hom.tensor (Hom.id X) x_2) (Hom.tensor (Hom.id X) x_3))
              f)
          Y₁ X₂ Y₂ g
[PROOFSTEP]
rintro W X Y Z ⟨f⟩ ⟨g⟩
[GOAL]
case mk.mk
C : Type u
W X Y Z : F C
f✝ : W ⟶ X
f : W ⟶ᵐ X
g✝ : Y ⟶ Z
g : Y ⟶ᵐ Z
⊢ (fun X₁ Y₁ X₂ Y₂ =>
        Quotient.map₂ Hom.tensor
          (_ :
            ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
              a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
      W X Y Z (Quot.mk Setoid.r f) (Quot.mk Setoid.r g) =
    (fun {X₁ X₂} f Y =>
          Quotient.map (fun f' => Hom.tensor f' (Hom.id Y))
            (_ : ∀ (x x_1 : X₁ ⟶ᵐ X₂), x ≈ x_1 → HomEquiv (Hom.tensor x (Hom.id Y)) (Hom.tensor x_1 (Hom.id Y))) f)
        (Quot.mk Setoid.r f) Y ≫
      (fun X x x_1 f =>
          Quotient.map (fun f' => Hom.tensor (Hom.id X) f')
            (_ : ∀ (x_2 x_3 : x ⟶ᵐ x_1), x_2 ≈ x_3 → HomEquiv (Hom.tensor (Hom.id X) x_2) (Hom.tensor (Hom.id X) x_3))
            f)
        X Y Z (Quot.mk Setoid.r g)
[PROOFSTEP]
apply Quotient.sound
[GOAL]
case mk.mk.a
C : Type u
W X Y Z : F C
f✝ : W ⟶ X
f : W ⟶ᵐ X
g✝ : Y ⟶ Z
g : Y ⟶ᵐ Z
⊢ Hom.tensor f g ≈ Hom.comp ((fun f' => Hom.tensor f' (Hom.id Y)) f) ((fun f' => Hom.tensor (Hom.id X) f') g)
[PROOFSTEP]
calc
  Hom.tensor f g
  _ ≈ Hom.tensor (Hom.comp f (Hom.id X)) (Hom.comp (Hom.id Y) g) := by
    apply HomEquiv.tensor (HomEquiv.comp_id f).symm (HomEquiv.id_comp g).symm
  _ ≈ Hom.comp (Hom.tensor f (Hom.id Y)) (Hom.tensor (Hom.id X) g) := by apply HomEquiv.tensor_comp
[GOAL]
C : Type u
W X Y Z : F C
f✝ : W ⟶ X
f : W ⟶ᵐ X
g✝ : Y ⟶ Z
g : Y ⟶ᵐ Z
⊢ Hom.tensor f g ≈ Hom.tensor (Hom.comp f (Hom.id X)) (Hom.comp (Hom.id Y) g)
[PROOFSTEP]
apply HomEquiv.tensor (HomEquiv.comp_id f).symm (HomEquiv.id_comp g).symm
[GOAL]
C : Type u
W X Y Z : F C
f✝ : W ⟶ X
f : W ⟶ᵐ X
g✝ : Y ⟶ Z
g : Y ⟶ᵐ Z
⊢ Hom.tensor (Hom.comp f (Hom.id X)) (Hom.comp (Hom.id Y) g) ≈
    Hom.comp (Hom.tensor f (Hom.id Y)) (Hom.tensor (Hom.id X) g)
[PROOFSTEP]
apply HomEquiv.tensor_comp
[GOAL]
C : Type u
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : F C
⊢ ∀ (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (fun X₁ Y₁ X₂ Y₂ =>
          Quotient.map₂ Hom.tensor
            (_ :
              ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
        X₁ Z₁ X₂ Z₂ (f₁ ≫ g₁) (f₂ ≫ g₂) =
      (fun X₁ Y₁ X₂ Y₂ =>
            Quotient.map₂ Hom.tensor
              (_ :
                ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                  a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
          X₁ Y₁ X₂ Y₂ f₁ f₂ ≫
        (fun X₁ Y₁ X₂ Y₂ =>
            Quotient.map₂ Hom.tensor
              (_ :
                ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                  a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
          Y₁ Z₁ Y₂ Z₂ g₁ g₂
[PROOFSTEP]
rintro ⟨f₁⟩ ⟨f₂⟩ ⟨g₁⟩ ⟨g₂⟩
[GOAL]
case mk.mk.mk.mk
C : Type u
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : F C
f₁✝ : X₁ ⟶ Y₁
f₁ : X₁ ⟶ᵐ Y₁
f₂✝ : X₂ ⟶ Y₂
f₂ : X₂ ⟶ᵐ Y₂
g₁✝ : Y₁ ⟶ Z₁
g₁ : Y₁ ⟶ᵐ Z₁
g₂✝ : Y₂ ⟶ Z₂
g₂ : Y₂ ⟶ᵐ Z₂
⊢ (fun X₁ Y₁ X₂ Y₂ =>
        Quotient.map₂ Hom.tensor
          (_ :
            ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
              a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
      X₁ Z₁ X₂ Z₂ (Quot.mk Setoid.r f₁ ≫ Quot.mk Setoid.r g₁) (Quot.mk Setoid.r f₂ ≫ Quot.mk Setoid.r g₂) =
    (fun X₁ Y₁ X₂ Y₂ =>
          Quotient.map₂ Hom.tensor
            (_ :
              ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
        X₁ Y₁ X₂ Y₂ (Quot.mk Setoid.r f₁) (Quot.mk Setoid.r f₂) ≫
      (fun X₁ Y₁ X₂ Y₂ =>
          Quotient.map₂ Hom.tensor
            (_ :
              ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
        Y₁ Z₁ Y₂ Z₂ (Quot.mk Setoid.r g₁) (Quot.mk Setoid.r g₂)
[PROOFSTEP]
exact Quotient.sound (tensor_comp _ _ _ _)
[GOAL]
C : Type u
⊢ ∀ (X Y : F C),
    (fun X x x_1 f =>
          Quotient.map (fun f' => Hom.tensor (Hom.id X) f')
            (_ : ∀ (x_2 x_3 : x ⟶ᵐ x_1), x_2 ≈ x_3 → HomEquiv (Hom.tensor (Hom.id X) x_2) (Hom.tensor (Hom.id X) x_3))
            f)
        X Y Y (𝟙 Y) =
      𝟙 ((fun X Y => tensor X Y) X Y)
[PROOFSTEP]
rintro X Y
[GOAL]
C : Type u
X Y : F C
⊢ (fun X x x_1 f =>
        Quotient.map (fun f' => Hom.tensor (Hom.id X) f')
          (_ : ∀ (x_2 x_3 : x ⟶ᵐ x_1), x_2 ≈ x_3 → HomEquiv (Hom.tensor (Hom.id X) x_2) (Hom.tensor (Hom.id X) x_3)) f)
      X Y Y (𝟙 Y) =
    𝟙 ((fun X Y => tensor X Y) X Y)
[PROOFSTEP]
apply Quotient.sound
[GOAL]
case a
C : Type u
X Y : F C
⊢ (fun f' => Hom.tensor (Hom.id X) f') (Hom.id Y) ≈ Hom.id ((fun X Y => tensor X Y) X Y)
[PROOFSTEP]
apply HomEquiv.tensor_id
[GOAL]
C : Type u
⊢ ∀ (X Y : F C),
    (fun {X₁ X₂} f Y =>
          Quotient.map (fun f' => Hom.tensor f' (Hom.id Y))
            (_ : ∀ (x x_1 : X₁ ⟶ᵐ X₂), x ≈ x_1 → HomEquiv (Hom.tensor x (Hom.id Y)) (Hom.tensor x_1 (Hom.id Y))) f)
        (𝟙 X) Y =
      𝟙 ((fun X Y => tensor X Y) X Y)
[PROOFSTEP]
intro X Y
[GOAL]
C : Type u
X Y : F C
⊢ (fun {X₁ X₂} f Y =>
        Quotient.map (fun f' => Hom.tensor f' (Hom.id Y))
          (_ : ∀ (x x_1 : X₁ ⟶ᵐ X₂), x ≈ x_1 → HomEquiv (Hom.tensor x (Hom.id Y)) (Hom.tensor x_1 (Hom.id Y))) f)
      (𝟙 X) Y =
    𝟙 ((fun X Y => tensor X Y) X Y)
[PROOFSTEP]
apply Quotient.sound
[GOAL]
case a
C : Type u
X Y : F C
⊢ (fun f' => Hom.tensor f' (Hom.id Y)) (Hom.id X) ≈ Hom.id ((fun X Y => tensor X Y) X Y)
[PROOFSTEP]
apply HomEquiv.tensor_id
[GOAL]
C : Type u
X₁ X₂ X₃ Y₁ Y₂ Y₃ : F C
⊢ ∀ (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    (fun X₁ Y₁ X₂ Y₂ =>
            Quotient.map₂ Hom.tensor
              (_ :
                ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                  a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
          ((fun X Y => tensor X Y) X₁ X₂) ((fun X Y => tensor X Y) Y₁ Y₂) X₃ Y₃
          ((fun X₁ Y₁ X₂ Y₂ =>
              Quotient.map₂ Hom.tensor
                (_ :
                  ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                    a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
            X₁ Y₁ X₂ Y₂ f₁ f₂)
          f₃ ≫
        ((fun X Y Z =>
              Iso.mk
                (Quotient.mk
                  (setoidHom ((fun X Y => tensor X Y) ((fun X Y => tensor X Y) X Y) Z)
                    ((fun X Y => tensor X Y) X ((fun X Y => tensor X Y) Y Z)))
                  (Hom.α_hom X Y Z))
                (Quotient.mk
                  (setoidHom ((fun X Y => tensor X Y) X ((fun X Y => tensor X Y) Y Z))
                    ((fun X Y => tensor X Y) ((fun X Y => tensor X Y) X Y) Z))
                  (Hom.α_inv X Y Z)))
            Y₁ Y₂ Y₃).hom =
      ((fun X Y Z =>
              Iso.mk
                (Quotient.mk
                  (setoidHom ((fun X Y => tensor X Y) ((fun X Y => tensor X Y) X Y) Z)
                    ((fun X Y => tensor X Y) X ((fun X Y => tensor X Y) Y Z)))
                  (Hom.α_hom X Y Z))
                (Quotient.mk
                  (setoidHom ((fun X Y => tensor X Y) X ((fun X Y => tensor X Y) Y Z))
                    ((fun X Y => tensor X Y) ((fun X Y => tensor X Y) X Y) Z))
                  (Hom.α_inv X Y Z)))
            X₁ X₂ X₃).hom ≫
        (fun X₁ Y₁ X₂ Y₂ =>
            Quotient.map₂ Hom.tensor
              (_ :
                ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                  a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
          X₁ Y₁ ((fun X Y => tensor X Y) X₂ X₃) ((fun X Y => tensor X Y) Y₂ Y₃) f₁
          ((fun X₁ Y₁ X₂ Y₂ =>
              Quotient.map₂ Hom.tensor
                (_ :
                  ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                    a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
            X₂ Y₂ X₃ Y₃ f₂ f₃)
[PROOFSTEP]
rintro ⟨f₁⟩ ⟨f₂⟩ ⟨f₃⟩
[GOAL]
case mk.mk.mk
C : Type u
X₁ X₂ X₃ Y₁ Y₂ Y₃ : F C
f₁✝ : X₁ ⟶ Y₁
f₁ : X₁ ⟶ᵐ Y₁
f₂✝ : X₂ ⟶ Y₂
f₂ : X₂ ⟶ᵐ Y₂
f₃✝ : X₃ ⟶ Y₃
f₃ : X₃ ⟶ᵐ Y₃
⊢ (fun X₁ Y₁ X₂ Y₂ =>
          Quotient.map₂ Hom.tensor
            (_ :
              ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
        ((fun X Y => tensor X Y) X₁ X₂) ((fun X Y => tensor X Y) Y₁ Y₂) X₃ Y₃
        ((fun X₁ Y₁ X₂ Y₂ =>
            Quotient.map₂ Hom.tensor
              (_ :
                ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                  a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
          X₁ Y₁ X₂ Y₂ (Quot.mk Setoid.r f₁) (Quot.mk Setoid.r f₂))
        (Quot.mk Setoid.r f₃) ≫
      ((fun X Y Z =>
            Iso.mk
              (Quotient.mk
                (setoidHom ((fun X Y => tensor X Y) ((fun X Y => tensor X Y) X Y) Z)
                  ((fun X Y => tensor X Y) X ((fun X Y => tensor X Y) Y Z)))
                (Hom.α_hom X Y Z))
              (Quotient.mk
                (setoidHom ((fun X Y => tensor X Y) X ((fun X Y => tensor X Y) Y Z))
                  ((fun X Y => tensor X Y) ((fun X Y => tensor X Y) X Y) Z))
                (Hom.α_inv X Y Z)))
          Y₁ Y₂ Y₃).hom =
    ((fun X Y Z =>
            Iso.mk
              (Quotient.mk
                (setoidHom ((fun X Y => tensor X Y) ((fun X Y => tensor X Y) X Y) Z)
                  ((fun X Y => tensor X Y) X ((fun X Y => tensor X Y) Y Z)))
                (Hom.α_hom X Y Z))
              (Quotient.mk
                (setoidHom ((fun X Y => tensor X Y) X ((fun X Y => tensor X Y) Y Z))
                  ((fun X Y => tensor X Y) ((fun X Y => tensor X Y) X Y) Z))
                (Hom.α_inv X Y Z)))
          X₁ X₂ X₃).hom ≫
      (fun X₁ Y₁ X₂ Y₂ =>
          Quotient.map₂ Hom.tensor
            (_ :
              ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
        X₁ Y₁ ((fun X Y => tensor X Y) X₂ X₃) ((fun X Y => tensor X Y) Y₂ Y₃) (Quot.mk Setoid.r f₁)
        ((fun X₁ Y₁ X₂ Y₂ =>
            Quotient.map₂ Hom.tensor
              (_ :
                ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                  a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
          X₂ Y₂ X₃ Y₃ (Quot.mk Setoid.r f₂) (Quot.mk Setoid.r f₃))
[PROOFSTEP]
exact Quotient.sound (associator_naturality _ _ _)
[GOAL]
C : Type u
X Y : F C
⊢ ∀ (f : X ⟶ Y),
    (fun X₁ Y₁ X₂ Y₂ =>
            Quotient.map₂ Hom.tensor
              (_ :
                ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                  a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
          Unit Unit X Y (𝟙 Unit) f ≫
        ((fun X =>
              Iso.mk (Quotient.mk (setoidHom ((fun X Y => tensor X Y) Unit X) X) (Hom.l_hom X))
                (Quotient.mk (setoidHom X ((fun X Y => tensor X Y) Unit X)) (Hom.l_inv X)))
            Y).hom =
      ((fun X =>
              Iso.mk (Quotient.mk (setoidHom ((fun X Y => tensor X Y) Unit X) X) (Hom.l_hom X))
                (Quotient.mk (setoidHom X ((fun X Y => tensor X Y) Unit X)) (Hom.l_inv X)))
            X).hom ≫
        f
[PROOFSTEP]
rintro ⟨f⟩
[GOAL]
case mk
C : Type u
X Y : F C
f✝ : X ⟶ Y
f : X ⟶ᵐ Y
⊢ (fun X₁ Y₁ X₂ Y₂ =>
          Quotient.map₂ Hom.tensor
            (_ :
              ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
        Unit Unit X Y (𝟙 Unit) (Quot.mk Setoid.r f) ≫
      ((fun X =>
            Iso.mk (Quotient.mk (setoidHom ((fun X Y => tensor X Y) Unit X) X) (Hom.l_hom X))
              (Quotient.mk (setoidHom X ((fun X Y => tensor X Y) Unit X)) (Hom.l_inv X)))
          Y).hom =
    ((fun X =>
            Iso.mk (Quotient.mk (setoidHom ((fun X Y => tensor X Y) Unit X) X) (Hom.l_hom X))
              (Quotient.mk (setoidHom X ((fun X Y => tensor X Y) Unit X)) (Hom.l_inv X)))
          X).hom ≫
      Quot.mk Setoid.r f
[PROOFSTEP]
exact Quotient.sound (l_naturality _)
[GOAL]
C : Type u
X Y : F C
⊢ ∀ (f : X ⟶ Y),
    (fun X₁ Y₁ X₂ Y₂ =>
            Quotient.map₂ Hom.tensor
              (_ :
                ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                  a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
          X Y Unit Unit f (𝟙 Unit) ≫
        ((fun X =>
              Iso.mk (Quotient.mk (setoidHom ((fun X Y => tensor X Y) X Unit) X) (Hom.ρ_hom X))
                (Quotient.mk (setoidHom X ((fun X Y => tensor X Y) X Unit)) (Hom.ρ_inv X)))
            Y).hom =
      ((fun X =>
              Iso.mk (Quotient.mk (setoidHom ((fun X Y => tensor X Y) X Unit) X) (Hom.ρ_hom X))
                (Quotient.mk (setoidHom X ((fun X Y => tensor X Y) X Unit)) (Hom.ρ_inv X)))
            X).hom ≫
        f
[PROOFSTEP]
rintro ⟨f⟩
[GOAL]
case mk
C : Type u
X Y : F C
f✝ : X ⟶ Y
f : X ⟶ᵐ Y
⊢ (fun X₁ Y₁ X₂ Y₂ =>
          Quotient.map₂ Hom.tensor
            (_ :
              ∀ ⦃a b : X₁ ⟶ᵐ Y₁⦄,
                a ≈ b → ∀ ⦃a_1 b_1 : X₂ ⟶ᵐ Y₂⦄, a_1 ≈ b_1 → HomEquiv (Hom.tensor a a_1) (Hom.tensor b b_1)))
        X Y Unit Unit (Quot.mk Setoid.r f) (𝟙 Unit) ≫
      ((fun X =>
            Iso.mk (Quotient.mk (setoidHom ((fun X Y => tensor X Y) X Unit) X) (Hom.ρ_hom X))
              (Quotient.mk (setoidHom X ((fun X Y => tensor X Y) X Unit)) (Hom.ρ_inv X)))
          Y).hom =
    ((fun X =>
            Iso.mk (Quotient.mk (setoidHom ((fun X Y => tensor X Y) X Unit) X) (Hom.ρ_hom X))
              (Quotient.mk (setoidHom X ((fun X Y => tensor X Y) X Unit)) (Hom.ρ_inv X)))
          X).hom ≫
      Quot.mk Setoid.r f
[PROOFSTEP]
exact Quotient.sound (ρ_naturality _)
[GOAL]
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
X Y : F C
⊢ ∀ (a b : X ⟶ᵐ Y), a ≈ b → projectMapAux f a = projectMapAux f b
[PROOFSTEP]
intro f g h
[GOAL]
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
h : f ≈ g
⊢ projectMapAux f✝ f = projectMapAux f✝ g
[PROOFSTEP]
induction h with
| refl => rfl
| symm _ _ _ hfg' => exact hfg'.symm
| trans _ _ hfg hgh => exact hfg.trans hgh
| comp _ _ hf hg => dsimp only [projectMapAux]; rw [hf, hg]
| tensor _ _ hfg hfg' => dsimp only [projectMapAux]; rw [hfg, hfg']
| comp_id => dsimp only [projectMapAux]; rw [Category.comp_id]
| id_comp => dsimp only [projectMapAux]; rw [Category.id_comp]
| assoc => dsimp only [projectMapAux]; rw [Category.assoc]
| tensor_id => dsimp only [projectMapAux]; rw [MonoidalCategory.tensor_id]; rfl
| tensor_comp => dsimp only [projectMapAux]; rw [MonoidalCategory.tensor_comp]
| α_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
| α_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
| associator_naturality => dsimp only [projectMapAux]; rw [MonoidalCategory.associator_naturality]
| ρ_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
| ρ_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
| ρ_naturality => dsimp only [projectMapAux, projectObj]; rw [MonoidalCategory.rightUnitor_naturality]
| l_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
| l_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
| l_naturality =>
  dsimp only [projectMapAux, projectObj]
  exact MonoidalCategory.leftUnitor_naturality _
| pentagon =>
  dsimp only [projectMapAux]
  exact MonoidalCategory.pentagon _ _ _ _
| triangle =>
  dsimp only [projectMapAux]
  exact MonoidalCategory.triangle _ _
[GOAL]
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
h : f ≈ g
⊢ projectMapAux f✝ f = projectMapAux f✝ g
[PROOFSTEP]
induction h with
| refl => rfl
| symm _ _ _ hfg' => exact hfg'.symm
| trans _ _ hfg hgh => exact hfg.trans hgh
| comp _ _ hf hg => dsimp only [projectMapAux]; rw [hf, hg]
| tensor _ _ hfg hfg' => dsimp only [projectMapAux]; rw [hfg, hfg']
| comp_id => dsimp only [projectMapAux]; rw [Category.comp_id]
| id_comp => dsimp only [projectMapAux]; rw [Category.id_comp]
| assoc => dsimp only [projectMapAux]; rw [Category.assoc]
| tensor_id => dsimp only [projectMapAux]; rw [MonoidalCategory.tensor_id]; rfl
| tensor_comp => dsimp only [projectMapAux]; rw [MonoidalCategory.tensor_comp]
| α_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
| α_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
| associator_naturality => dsimp only [projectMapAux]; rw [MonoidalCategory.associator_naturality]
| ρ_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
| ρ_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
| ρ_naturality => dsimp only [projectMapAux, projectObj]; rw [MonoidalCategory.rightUnitor_naturality]
| l_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
| l_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
| l_naturality =>
  dsimp only [projectMapAux, projectObj]
  exact MonoidalCategory.leftUnitor_naturality _
| pentagon =>
  dsimp only [projectMapAux]
  exact MonoidalCategory.pentagon _ _ _ _
| triangle =>
  dsimp only [projectMapAux]
  exact MonoidalCategory.triangle _ _
[GOAL]
case refl
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
⊢ projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f✝
[PROOFSTEP]

| refl => rfl
[GOAL]
case refl
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
⊢ projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f✝
[PROOFSTEP]
rfl
[GOAL]
case symm
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ g✝ : X✝ ⟶ᵐ Y✝
a✝ : HomEquiv f✝ g✝
hfg' : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ g✝
⊢ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f✝
[PROOFSTEP]

| symm _ _ _ hfg' => exact hfg'.symm
[GOAL]
case symm
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ g✝ : X✝ ⟶ᵐ Y✝
a✝ : HomEquiv f✝ g✝
hfg' : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ g✝
⊢ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f✝
[PROOFSTEP]
exact hfg'.symm
[GOAL]
case trans
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ g✝ h✝ : X✝ ⟶ᵐ Y✝
a✝¹ : HomEquiv f✝ g✝
a✝ : HomEquiv g✝ h✝
hfg : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ g✝
hgh : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ h✝
⊢ projectMapAux f✝¹ f✝ = projectMapAux f✝¹ h✝
[PROOFSTEP]

| trans _ _ hfg hgh => exact hfg.trans hgh
[GOAL]
case trans
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ g✝ h✝ : X✝ ⟶ᵐ Y✝
a✝¹ : HomEquiv f✝ g✝
a✝ : HomEquiv g✝ h✝
hfg : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ g✝
hgh : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ h✝
⊢ projectMapAux f✝¹ f✝ = projectMapAux f✝¹ h✝
[PROOFSTEP]
exact hfg.trans hgh
[GOAL]
case comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ Z✝ : F C
f✝ f'✝ : X✝ ⟶ᵐ Y✝
g✝ g'✝ : Y✝ ⟶ᵐ Z✝
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hg : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ (Hom.comp f✝ g✝) = projectMapAux f✝¹ (Hom.comp f'✝ g'✝)
[PROOFSTEP]

| comp _ _ hf hg => dsimp only [projectMapAux]; rw [hf, hg]
[GOAL]
case comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ Z✝ : F C
f✝ f'✝ : X✝ ⟶ᵐ Y✝
g✝ g'✝ : Y✝ ⟶ᵐ Z✝
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hg : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ (Hom.comp f✝ g✝) = projectMapAux f✝¹ (Hom.comp f'✝ g'✝)
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ Z✝ : F C
f✝ f'✝ : X✝ ⟶ᵐ Y✝
g✝ g'✝ : Y✝ ⟶ᵐ Z✝
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hg : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ f✝ ≫ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f'✝ ≫ projectMapAux f✝¹ g'✝
[PROOFSTEP]
rw [hf, hg]
[GOAL]
case tensor
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
W✝ X✝ Y✝ Z✝ : F C
f✝ f'✝ : W✝ ⟶ᵐ X✝
g✝ g'✝ : Y✝ ⟶ᵐ Z✝
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hfg : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hfg' : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ (Hom.tensor f✝ g✝) = projectMapAux f✝¹ (Hom.tensor f'✝ g'✝)
[PROOFSTEP]

| tensor _ _ hfg hfg' => dsimp only [projectMapAux]; rw [hfg, hfg']
[GOAL]
case tensor
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
W✝ X✝ Y✝ Z✝ : F C
f✝ f'✝ : W✝ ⟶ᵐ X✝
g✝ g'✝ : Y✝ ⟶ᵐ Z✝
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hfg : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hfg' : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ (Hom.tensor f✝ g✝) = projectMapAux f✝¹ (Hom.tensor f'✝ g'✝)
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case tensor
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
W✝ X✝ Y✝ Z✝ : F C
f✝ f'✝ : W✝ ⟶ᵐ X✝
g✝ g'✝ : Y✝ ⟶ᵐ Z✝
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hfg : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hfg' : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ f✝ ⊗ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f'✝ ⊗ projectMapAux f✝¹ g'✝
[PROOFSTEP]
rw [hfg, hfg']
[GOAL]
case comp_id
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
⊢ projectMapAux f✝¹ (Hom.comp f✝ (Hom.id Y✝)) = projectMapAux f✝¹ f✝
[PROOFSTEP]

| comp_id => dsimp only [projectMapAux]; rw [Category.comp_id]
[GOAL]
case comp_id
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
⊢ projectMapAux f✝¹ (Hom.comp f✝ (Hom.id Y✝)) = projectMapAux f✝¹ f✝
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case comp_id
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
⊢ projectMapAux f✝¹ f✝ ≫ 𝟙 (projectObj f✝¹ Y✝) = projectMapAux f✝¹ f✝
[PROOFSTEP]
rw [Category.comp_id]
[GOAL]
case id_comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
⊢ projectMapAux f✝¹ (Hom.comp (Hom.id X✝) f✝) = projectMapAux f✝¹ f✝
[PROOFSTEP]

| id_comp => dsimp only [projectMapAux]; rw [Category.id_comp]
[GOAL]
case id_comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
⊢ projectMapAux f✝¹ (Hom.comp (Hom.id X✝) f✝) = projectMapAux f✝¹ f✝
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case id_comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
⊢ 𝟙 (projectObj f✝¹ X✝) ≫ projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f✝
[PROOFSTEP]
rw [Category.id_comp]
[GOAL]
case assoc
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ U✝ V✝ : F C
f✝ : X✝ ⟶ᵐ U✝
g✝ : U✝ ⟶ᵐ V✝
h✝ : V✝ ⟶ᵐ Y✝
⊢ projectMapAux f✝¹ (Hom.comp (Hom.comp f✝ g✝) h✝) = projectMapAux f✝¹ (Hom.comp f✝ (Hom.comp g✝ h✝))
[PROOFSTEP]

| assoc => dsimp only [projectMapAux]; rw [Category.assoc]
[GOAL]
case assoc
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ U✝ V✝ : F C
f✝ : X✝ ⟶ᵐ U✝
g✝ : U✝ ⟶ᵐ V✝
h✝ : V✝ ⟶ᵐ Y✝
⊢ projectMapAux f✝¹ (Hom.comp (Hom.comp f✝ g✝) h✝) = projectMapAux f✝¹ (Hom.comp f✝ (Hom.comp g✝ h✝))
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case assoc
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ U✝ V✝ : F C
f✝ : X✝ ⟶ᵐ U✝
g✝ : U✝ ⟶ᵐ V✝
h✝ : V✝ ⟶ᵐ Y✝
⊢ (projectMapAux f✝¹ f✝ ≫ projectMapAux f✝¹ g✝) ≫ projectMapAux f✝¹ h✝ =
    projectMapAux f✝¹ f✝ ≫ projectMapAux f✝¹ g✝ ≫ projectMapAux f✝¹ h✝
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
case tensor_id
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
⊢ projectMapAux f✝ (Hom.tensor (Hom.id X✝) (Hom.id Y✝)) = projectMapAux f✝ (Hom.id (tensor X✝ Y✝))
[PROOFSTEP]

| tensor_id => dsimp only [projectMapAux]; rw [MonoidalCategory.tensor_id]; rfl
[GOAL]
case tensor_id
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
⊢ projectMapAux f✝ (Hom.tensor (Hom.id X✝) (Hom.id Y✝)) = projectMapAux f✝ (Hom.id (tensor X✝ Y✝))
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case tensor_id
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
⊢ 𝟙 (projectObj f✝ X✝) ⊗ 𝟙 (projectObj f✝ Y✝) = 𝟙 (projectObj f✝ (tensor X✝ Y✝))
[PROOFSTEP]
rw [MonoidalCategory.tensor_id]
[GOAL]
case tensor_id
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
⊢ 𝟙 (projectObj f✝ X✝ ⊗ projectObj f✝ Y✝) = 𝟙 (projectObj f✝ (tensor X✝ Y✝))
[PROOFSTEP]
rfl
[GOAL]
case tensor_comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : F C
f₁✝ : X₁✝ ⟶ᵐ Y₁✝
f₂✝ : X₂✝ ⟶ᵐ Y₂✝
g₁✝ : Y₁✝ ⟶ᵐ Z₁✝
g₂✝ : Y₂✝ ⟶ᵐ Z₂✝
⊢ projectMapAux f✝ (Hom.tensor (Hom.comp f₁✝ g₁✝) (Hom.comp f₂✝ g₂✝)) =
    projectMapAux f✝ (Hom.comp (Hom.tensor f₁✝ f₂✝) (Hom.tensor g₁✝ g₂✝))
[PROOFSTEP]

| tensor_comp => dsimp only [projectMapAux]; rw [MonoidalCategory.tensor_comp]
[GOAL]
case tensor_comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : F C
f₁✝ : X₁✝ ⟶ᵐ Y₁✝
f₂✝ : X₂✝ ⟶ᵐ Y₂✝
g₁✝ : Y₁✝ ⟶ᵐ Z₁✝
g₂✝ : Y₂✝ ⟶ᵐ Z₂✝
⊢ projectMapAux f✝ (Hom.tensor (Hom.comp f₁✝ g₁✝) (Hom.comp f₂✝ g₂✝)) =
    projectMapAux f✝ (Hom.comp (Hom.tensor f₁✝ f₂✝) (Hom.tensor g₁✝ g₂✝))
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case tensor_comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : F C
f₁✝ : X₁✝ ⟶ᵐ Y₁✝
f₂✝ : X₂✝ ⟶ᵐ Y₂✝
g₁✝ : Y₁✝ ⟶ᵐ Z₁✝
g₂✝ : Y₂✝ ⟶ᵐ Z₂✝
⊢ projectMapAux f✝ f₁✝ ≫ projectMapAux f✝ g₁✝ ⊗ projectMapAux f✝ f₂✝ ≫ projectMapAux f✝ g₂✝ =
    (projectMapAux f✝ f₁✝ ⊗ projectMapAux f✝ f₂✝) ≫ (projectMapAux f✝ g₁✝ ⊗ projectMapAux f✝ g₂✝)
[PROOFSTEP]
rw [MonoidalCategory.tensor_comp]
[GOAL]
case α_hom_inv
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ Z✝ : F C
⊢ projectMapAux f✝ (Hom.comp (α_hom X✝ Y✝ Z✝) (α_inv X✝ Y✝ Z✝)) = projectMapAux f✝ (Hom.id (tensor (tensor X✝ Y✝) Z✝))
[PROOFSTEP]

| α_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
[GOAL]
case α_hom_inv
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ Z✝ : F C
⊢ projectMapAux f✝ (Hom.comp (α_hom X✝ Y✝ Z✝) (α_inv X✝ Y✝ Z✝)) = projectMapAux f✝ (Hom.id (tensor (tensor X✝ Y✝) Z✝))
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case α_hom_inv
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ Z✝ : F C
⊢ (α_ (projectObj f✝ X✝) (projectObj f✝ Y✝) (projectObj f✝ Z✝)).hom ≫
      (α_ (projectObj f✝ X✝) (projectObj f✝ Y✝) (projectObj f✝ Z✝)).inv =
    𝟙 (projectObj f✝ (tensor (tensor X✝ Y✝) Z✝))
[PROOFSTEP]
rw [Iso.hom_inv_id]
[GOAL]
case α_inv_hom
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ Z✝ : F C
⊢ projectMapAux f✝ (Hom.comp (α_inv X✝ Y✝ Z✝) (α_hom X✝ Y✝ Z✝)) = projectMapAux f✝ (Hom.id (tensor X✝ (tensor Y✝ Z✝)))
[PROOFSTEP]

| α_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
[GOAL]
case α_inv_hom
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ Z✝ : F C
⊢ projectMapAux f✝ (Hom.comp (α_inv X✝ Y✝ Z✝) (α_hom X✝ Y✝ Z✝)) = projectMapAux f✝ (Hom.id (tensor X✝ (tensor Y✝ Z✝)))
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case α_inv_hom
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ Z✝ : F C
⊢ (α_ (projectObj f✝ X✝) (projectObj f✝ Y✝) (projectObj f✝ Z✝)).inv ≫
      (α_ (projectObj f✝ X✝) (projectObj f✝ Y✝) (projectObj f✝ Z✝)).hom =
    𝟙 (projectObj f✝ (tensor X✝ (tensor Y✝ Z✝)))
[PROOFSTEP]
rw [Iso.inv_hom_id]
[GOAL]
case associator_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : F C
f₁✝ : X₁✝ ⟶ᵐ Y₁✝
f₂✝ : X₂✝ ⟶ᵐ Y₂✝
f₃✝ : X₃✝ ⟶ᵐ Y₃✝
⊢ projectMapAux f✝ (Hom.comp (Hom.tensor (Hom.tensor f₁✝ f₂✝) f₃✝) (α_hom Y₁✝ Y₂✝ Y₃✝)) =
    projectMapAux f✝ (Hom.comp (α_hom X₁✝ X₂✝ X₃✝) (Hom.tensor f₁✝ (Hom.tensor f₂✝ f₃✝)))
[PROOFSTEP]

| associator_naturality => dsimp only [projectMapAux]; rw [MonoidalCategory.associator_naturality]
[GOAL]
case associator_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : F C
f₁✝ : X₁✝ ⟶ᵐ Y₁✝
f₂✝ : X₂✝ ⟶ᵐ Y₂✝
f₃✝ : X₃✝ ⟶ᵐ Y₃✝
⊢ projectMapAux f✝ (Hom.comp (Hom.tensor (Hom.tensor f₁✝ f₂✝) f₃✝) (α_hom Y₁✝ Y₂✝ Y₃✝)) =
    projectMapAux f✝ (Hom.comp (α_hom X₁✝ X₂✝ X₃✝) (Hom.tensor f₁✝ (Hom.tensor f₂✝ f₃✝)))
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case associator_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : F C
f₁✝ : X₁✝ ⟶ᵐ Y₁✝
f₂✝ : X₂✝ ⟶ᵐ Y₂✝
f₃✝ : X₃✝ ⟶ᵐ Y₃✝
⊢ ((projectMapAux f✝ f₁✝ ⊗ projectMapAux f✝ f₂✝) ⊗ projectMapAux f✝ f₃✝) ≫
      (α_ (projectObj f✝ Y₁✝) (projectObj f✝ Y₂✝) (projectObj f✝ Y₃✝)).hom =
    (α_ (projectObj f✝ X₁✝) (projectObj f✝ X₂✝) (projectObj f✝ X₃✝)).hom ≫
      (projectMapAux f✝ f₁✝ ⊗ projectMapAux f✝ f₂✝ ⊗ projectMapAux f✝ f₃✝)
[PROOFSTEP]
rw [MonoidalCategory.associator_naturality]
[GOAL]
case ρ_hom_inv
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ : F C
⊢ projectMapAux f✝ (Hom.comp (ρ_hom X✝) (ρ_inv X✝)) = projectMapAux f✝ (Hom.id (tensor X✝ Unit))
[PROOFSTEP]

| ρ_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
[GOAL]
case ρ_hom_inv
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ : F C
⊢ projectMapAux f✝ (Hom.comp (ρ_hom X✝) (ρ_inv X✝)) = projectMapAux f✝ (Hom.id (tensor X✝ Unit))
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case ρ_hom_inv
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ : F C
⊢ (ρ_ (projectObj f✝ X✝)).hom ≫ (ρ_ (projectObj f✝ X✝)).inv = 𝟙 (projectObj f✝ (tensor X✝ Unit))
[PROOFSTEP]
rw [Iso.hom_inv_id]
[GOAL]
case ρ_inv_hom
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ : F C
⊢ projectMapAux f✝ (Hom.comp (ρ_inv X✝) (ρ_hom X✝)) = projectMapAux f✝ (Hom.id X✝)
[PROOFSTEP]

| ρ_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
[GOAL]
case ρ_inv_hom
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ : F C
⊢ projectMapAux f✝ (Hom.comp (ρ_inv X✝) (ρ_hom X✝)) = projectMapAux f✝ (Hom.id X✝)
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case ρ_inv_hom
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ : F C
⊢ (ρ_ (projectObj f✝ X✝)).inv ≫ (ρ_ (projectObj f✝ X✝)).hom = 𝟙 (projectObj f✝ X✝)
[PROOFSTEP]
rw [Iso.inv_hom_id]
[GOAL]
case ρ_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
⊢ projectMapAux f✝¹ (Hom.comp (Hom.tensor f✝ (Hom.id Unit)) (ρ_hom Y✝)) = projectMapAux f✝¹ (Hom.comp (ρ_hom X✝) f✝)
[PROOFSTEP]

| ρ_naturality => dsimp only [projectMapAux, projectObj]; rw [MonoidalCategory.rightUnitor_naturality]
[GOAL]
case ρ_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
⊢ projectMapAux f✝¹ (Hom.comp (Hom.tensor f✝ (Hom.id Unit)) (ρ_hom Y✝)) = projectMapAux f✝¹ (Hom.comp (ρ_hom X✝) f✝)
[PROOFSTEP]
dsimp only [projectMapAux, projectObj]
[GOAL]
case ρ_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
⊢ (projectMapAux f✝¹ f✝ ⊗ 𝟙 (𝟙_ D)) ≫ (ρ_ (projectObj f✝¹ Y✝)).hom = (ρ_ (projectObj f✝¹ X✝)).hom ≫ projectMapAux f✝¹ f✝
[PROOFSTEP]
rw [MonoidalCategory.rightUnitor_naturality]
[GOAL]
case l_hom_inv
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ : F C
⊢ projectMapAux f✝ (Hom.comp (l_hom X✝) (l_inv X✝)) = projectMapAux f✝ (Hom.id (tensor Unit X✝))
[PROOFSTEP]

| l_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
[GOAL]
case l_hom_inv
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ : F C
⊢ projectMapAux f✝ (Hom.comp (l_hom X✝) (l_inv X✝)) = projectMapAux f✝ (Hom.id (tensor Unit X✝))
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case l_hom_inv
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ : F C
⊢ (λ_ (projectObj f✝ X✝)).hom ≫ (λ_ (projectObj f✝ X✝)).inv = 𝟙 (projectObj f✝ (tensor Unit X✝))
[PROOFSTEP]
rw [Iso.hom_inv_id]
[GOAL]
case l_inv_hom
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ : F C
⊢ projectMapAux f✝ (Hom.comp (l_inv X✝) (l_hom X✝)) = projectMapAux f✝ (Hom.id X✝)
[PROOFSTEP]

| l_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
[GOAL]
case l_inv_hom
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ : F C
⊢ projectMapAux f✝ (Hom.comp (l_inv X✝) (l_hom X✝)) = projectMapAux f✝ (Hom.id X✝)
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case l_inv_hom
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ : F C
⊢ (λ_ (projectObj f✝ X✝)).inv ≫ (λ_ (projectObj f✝ X✝)).hom = 𝟙 (projectObj f✝ X✝)
[PROOFSTEP]
rw [Iso.inv_hom_id]
[GOAL]
case l_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
⊢ projectMapAux f✝¹ (Hom.comp (Hom.tensor (Hom.id Unit) f✝) (l_hom Y✝)) = projectMapAux f✝¹ (Hom.comp (l_hom X✝) f✝)
[PROOFSTEP]

| l_naturality =>
  dsimp only [projectMapAux, projectObj]
  exact MonoidalCategory.leftUnitor_naturality _
[GOAL]
case l_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
⊢ projectMapAux f✝¹ (Hom.comp (Hom.tensor (Hom.id Unit) f✝) (l_hom Y✝)) = projectMapAux f✝¹ (Hom.comp (l_hom X✝) f✝)
[PROOFSTEP]
dsimp only [projectMapAux, projectObj]
[GOAL]
case l_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
⊢ (𝟙 (𝟙_ D) ⊗ projectMapAux f✝¹ f✝) ≫ (λ_ (projectObj f✝¹ Y✝)).hom = (λ_ (projectObj f✝¹ X✝)).hom ≫ projectMapAux f✝¹ f✝
[PROOFSTEP]
exact MonoidalCategory.leftUnitor_naturality _
[GOAL]
case pentagon
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
W✝ X✝ Y✝ Z✝ : F C
⊢ projectMapAux f✝
      (Hom.comp (Hom.tensor (α_hom W✝ X✝ Y✝) (Hom.id Z✝))
        (Hom.comp (α_hom W✝ (tensor X✝ Y✝) Z✝) (Hom.tensor (Hom.id W✝) (α_hom X✝ Y✝ Z✝)))) =
    projectMapAux f✝ (Hom.comp (α_hom (tensor W✝ X✝) Y✝ Z✝) (α_hom W✝ X✝ (tensor Y✝ Z✝)))
[PROOFSTEP]

| pentagon =>
  dsimp only [projectMapAux]
  exact MonoidalCategory.pentagon _ _ _ _
[GOAL]
case pentagon
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
W✝ X✝ Y✝ Z✝ : F C
⊢ projectMapAux f✝
      (Hom.comp (Hom.tensor (α_hom W✝ X✝ Y✝) (Hom.id Z✝))
        (Hom.comp (α_hom W✝ (tensor X✝ Y✝) Z✝) (Hom.tensor (Hom.id W✝) (α_hom X✝ Y✝ Z✝)))) =
    projectMapAux f✝ (Hom.comp (α_hom (tensor W✝ X✝) Y✝ Z✝) (α_hom W✝ X✝ (tensor Y✝ Z✝)))
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case pentagon
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
W✝ X✝ Y✝ Z✝ : F C
⊢ ((α_ (projectObj f✝ W✝) (projectObj f✝ X✝) (projectObj f✝ Y✝)).hom ⊗ 𝟙 (projectObj f✝ Z✝)) ≫
      (α_ (projectObj f✝ W✝) (projectObj f✝ (tensor X✝ Y✝)) (projectObj f✝ Z✝)).hom ≫
        (𝟙 (projectObj f✝ W✝) ⊗ (α_ (projectObj f✝ X✝) (projectObj f✝ Y✝) (projectObj f✝ Z✝)).hom) =
    (α_ (projectObj f✝ (tensor W✝ X✝)) (projectObj f✝ Y✝) (projectObj f✝ Z✝)).hom ≫
      (α_ (projectObj f✝ W✝) (projectObj f✝ X✝) (projectObj f✝ (tensor Y✝ Z✝))).hom
[PROOFSTEP]
exact MonoidalCategory.pentagon _ _ _ _
[GOAL]
case triangle
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
⊢ projectMapAux f✝ (Hom.comp (α_hom X✝ Unit Y✝) (Hom.tensor (Hom.id X✝) (l_hom Y✝))) =
    projectMapAux f✝ (Hom.tensor (ρ_hom X✝) (Hom.id Y✝))
[PROOFSTEP]

| triangle =>
  dsimp only [projectMapAux]
  exact MonoidalCategory.triangle _ _
[GOAL]
case triangle
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
⊢ projectMapAux f✝ (Hom.comp (α_hom X✝ Unit Y✝) (Hom.tensor (Hom.id X✝) (l_hom Y✝))) =
    projectMapAux f✝ (Hom.tensor (ρ_hom X✝) (Hom.id Y✝))
[PROOFSTEP]
dsimp only [projectMapAux]
[GOAL]
case triangle
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : F C
f g : X ⟶ᵐ Y
X✝ Y✝ : F C
⊢ (α_ (projectObj f✝ X✝) (projectObj f✝ Unit) (projectObj f✝ Y✝)).hom ≫
      (𝟙 (projectObj f✝ X✝) ⊗ (λ_ (projectObj f✝ Y✝)).hom) =
    (ρ_ (projectObj f✝ X✝)).hom ⊗ 𝟙 (projectObj f✝ Y✝)
[PROOFSTEP]
exact MonoidalCategory.triangle _ _
[GOAL]
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
⊢ ∀ {X Y Z : F C} (f_1 : X ⟶ Y) (g : Y ⟶ Z),
    { obj := projectObj f, map := fun {X Y} => projectMap f X Y }.map (f_1 ≫ g) =
      { obj := projectObj f, map := fun {X Y} => projectMap f X Y }.map f_1 ≫
        { obj := projectObj f, map := fun {X Y} => projectMap f X Y }.map g
[PROOFSTEP]
rintro _ _ _ ⟨_⟩ ⟨_⟩
[GOAL]
case mk.mk
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
X✝ Y✝ Z✝ : F C
f✝ : X✝ ⟶ Y✝
a✝¹ : X✝ ⟶ᵐ Y✝
g✝ : Y✝ ⟶ Z✝
a✝ : Y✝ ⟶ᵐ Z✝
⊢ { obj := projectObj f, map := fun {X Y} => projectMap f X Y }.map (Quot.mk Setoid.r a✝¹ ≫ Quot.mk Setoid.r a✝) =
    { obj := projectObj f, map := fun {X Y} => projectMap f X Y }.map (Quot.mk Setoid.r a✝¹) ≫
      { obj := projectObj f, map := fun {X Y} => projectMap f X Y }.map (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
x✝³ x✝² x✝¹ x✝ : F C
f : x✝³ ⟶ x✝²
g : x✝¹ ⟶ x✝
⊢ ((Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).map f ⊗
        (Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).map g) ≫
      (fun X Y =>
          𝟙
            ((Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).obj X ⊗
              (Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).obj Y))
        x✝² x✝ =
    (fun X Y =>
          𝟙
            ((Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).obj X ⊗
              (Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).obj Y))
        x✝³ x✝¹ ≫
      (Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).map (f ⊗ g)
[PROOFSTEP]
induction' f using Quotient.recOn
[GOAL]
case f
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
x✝³ x✝² x✝¹ x✝ : F C
g : x✝¹ ⟶ x✝
a✝ : x✝³ ⟶ᵐ x✝²
⊢ ((Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).map (Quotient.mk (setoidHom x✝³ x✝²) a✝) ⊗
        (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).map g) ≫
      (fun X Y =>
          𝟙
            ((Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj X ⊗
              (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj Y))
        x✝² x✝ =
    (fun X Y =>
          𝟙
            ((Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj X ⊗
              (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj Y))
        x✝³ x✝¹ ≫
      (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).map
        (Quotient.mk (setoidHom x✝³ x✝²) a✝ ⊗ g)
[PROOFSTEP]
induction' g using Quotient.recOn
[GOAL]
case f.f
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
x✝³ x✝² x✝¹ x✝ : F C
a✝¹ : x✝³ ⟶ᵐ x✝²
a✝ : x✝¹ ⟶ᵐ x✝
⊢ ((Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).map
          (Quotient.mk (setoidHom x✝³ x✝²) a✝¹) ⊗
        (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).map
          (Quotient.mk (setoidHom x✝¹ x✝) a✝)) ≫
      (fun X Y =>
          𝟙
            ((Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj X ⊗
              (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj Y))
        x✝² x✝ =
    (fun X Y =>
          𝟙
            ((Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj X ⊗
              (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj Y))
        x✝³ x✝¹ ≫
      (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).map
        (Quotient.mk (setoidHom x✝³ x✝²) a✝¹ ⊗ Quotient.mk (setoidHom x✝¹ x✝) a✝)
[PROOFSTEP]
dsimp
[GOAL]
case f.f
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
x✝³ x✝² x✝¹ x✝ : F C
a✝¹ : x✝³ ⟶ᵐ x✝²
a✝ : x✝¹ ⟶ᵐ x✝
⊢ (projectMap f x✝³ x✝² (Quotient.mk (setoidHom x✝³ x✝²) a✝¹) ⊗
        projectMap f x✝¹ x✝ (Quotient.mk (setoidHom x✝¹ x✝) a✝)) ≫
      𝟙 (projectObj f x✝² ⊗ projectObj f x✝) =
    𝟙 (projectObj f x✝³ ⊗ projectObj f x✝¹) ≫
      projectMap f (x✝³ ⊗ x✝¹) (x✝² ⊗ x✝) (Quotient.mk (setoidHom x✝³ x✝²) a✝¹ ⊗ Quotient.mk (setoidHom x✝¹ x✝) a✝)
[PROOFSTEP]
simp
[GOAL]
case f.f
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
x✝³ x✝² x✝¹ x✝ : F C
a✝¹ : x✝³ ⟶ᵐ x✝²
a✝ : x✝¹ ⟶ᵐ x✝
⊢ projectMap f x✝³ x✝² (Quotient.mk (setoidHom x✝³ x✝²) a✝¹) ⊗ projectMap f x✝¹ x✝ (Quotient.mk (setoidHom x✝¹ x✝) a✝) =
    projectMap f (x✝³ ⊗ x✝¹) (x✝² ⊗ x✝) (Quotient.mk (setoidHom x✝³ x✝²) a✝¹ ⊗ Quotient.mk (setoidHom x✝¹ x✝) a✝)
[PROOFSTEP]
rfl
[GOAL]
case f.h
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
x✝³ x✝² x✝¹ x✝ : F C
g : x✝¹ ⟶ x✝
a✝¹ : x✝³ ⟶ᵐ x✝²
a✝ b✝ : x✝¹ ⟶ᵐ x✝
p✝ : a✝ ≈ b✝
⊢ (_ :
      ((Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).map
              (Quotient.mk (setoidHom x✝³ x✝²) a✝¹) ⊗
            (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).map
              (Quotient.mk (setoidHom x✝¹ x✝) b✝)) ≫
          (fun X Y =>
              𝟙
                ((Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj X ⊗
                  (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj Y))
            x✝² x✝ =
        (fun X Y =>
              𝟙
                ((Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj X ⊗
                  (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj Y))
            x✝³ x✝¹ ≫
          (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).map
            (Quotient.mk (setoidHom x✝³ x✝²) a✝¹ ⊗ Quotient.mk (setoidHom x✝¹ x✝) b✝)) =
    (_ :
      ((Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).map
              (Quotient.mk (setoidHom x✝³ x✝²) a✝¹) ⊗
            (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).map
              (Quotient.mk (setoidHom x✝¹ x✝) b✝)) ≫
          (fun X Y =>
              𝟙
                ((Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj X ⊗
                  (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj Y))
            x✝² x✝ =
        (fun X Y =>
              𝟙
                ((Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj X ⊗
                  (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).obj Y))
            x✝³ x✝¹ ≫
          (Functor.mk { obj := projectObj f, map := fun {X Y} => projectMap f X Y }).map
            (Quotient.mk (setoidHom x✝³ x✝²) a✝¹ ⊗ Quotient.mk (setoidHom x✝¹ x✝) b✝))
[PROOFSTEP]
rfl
[GOAL]
case h
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
x✝³ x✝² x✝¹ x✝ : F C
f : x✝³ ⟶ x✝²
g : x✝¹ ⟶ x✝
a✝ b✝ : x✝³ ⟶ᵐ x✝²
p✝ : a✝ ≈ b✝
⊢ (_ :
      ((Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).map
              (Quotient.mk (setoidHom x✝³ x✝²) b✝) ⊗
            (Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).map g) ≫
          (fun X Y =>
              𝟙
                ((Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).obj X ⊗
                  (Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).obj Y))
            x✝² x✝ =
        (fun X Y =>
              𝟙
                ((Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).obj X ⊗
                  (Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).obj Y))
            x✝³ x✝¹ ≫
          (Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).map
            (Quotient.mk (setoidHom x✝³ x✝²) b✝ ⊗ g)) =
    (_ :
      ((Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).map
              (Quotient.mk (setoidHom x✝³ x✝²) b✝) ⊗
            (Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).map g) ≫
          (fun X Y =>
              𝟙
                ((Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).obj X ⊗
                  (Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).obj Y))
            x✝² x✝ =
        (fun X Y =>
              𝟙
                ((Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).obj X ⊗
                  (Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).obj Y))
            x✝³ x✝¹ ≫
          (Functor.mk { obj := projectObj f✝, map := fun {X Y} => projectMap f✝ X Y }).map
            (Quotient.mk (setoidHom x✝³ x✝²) b✝ ⊗ g))
[PROOFSTEP]
rfl
