[GOAL]
J : Type v
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
⊢ SolutionSetCondition G
[PROOFSTEP]
intro A
[GOAL]
J : Type v
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
⊢ ∃ ι B f, ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
[PROOFSTEP]
refine' ⟨PUnit, fun _ => (leftAdjoint G).obj A, fun _ => (Adjunction.ofRightAdjoint G).unit.app A, _⟩
[GOAL]
J : Type v
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
⊢ ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, (fun x => NatTrans.app (Adjunction.ofRightAdjoint G).unit A) i ≫ G.map g = h
[PROOFSTEP]
intro B h
[GOAL]
J : Type v
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
B : D
h : A ⟶ G.obj B
⊢ ∃ i g, (fun x => NatTrans.app (Adjunction.ofRightAdjoint G).unit A) i ≫ G.map g = h
[PROOFSTEP]
refine' ⟨PUnit.unit, ((Adjunction.ofRightAdjoint G).homEquiv _ _).symm h, _⟩
[GOAL]
J : Type v
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : C
B : D
h : A ⟶ G.obj B
⊢ (fun x => NatTrans.app (Adjunction.ofRightAdjoint G).unit A) PUnit.unit ≫
      G.map (↑(Adjunction.homEquiv (Adjunction.ofRightAdjoint G) A B).symm h) =
    h
[PROOFSTEP]
rw [← Adjunction.homEquiv_unit, Equiv.apply_symm_apply]
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
hG : SolutionSetCondition G
⊢ IsRightAdjoint G
[PROOFSTEP]
refine' @isRightAdjointOfStructuredArrowInitials _ _ _ _ G ?_
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
hG : SolutionSetCondition G
⊢ ∀ (A : C), HasInitial (StructuredArrow A G)
[PROOFSTEP]
intro A
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
hG : SolutionSetCondition G
A : C
⊢ HasInitial (StructuredArrow A G)
[PROOFSTEP]
specialize hG A
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
hG : ∃ ι B f, ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
⊢ HasInitial (StructuredArrow A G)
[PROOFSTEP]
choose ι B f g using hG
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
⊢ HasInitial (StructuredArrow A G)
[PROOFSTEP]
let B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
⊢ HasInitial (StructuredArrow A G)
[PROOFSTEP]
have hB' : ∀ A' : StructuredArrow A G, ∃ i, Nonempty (B' i ⟶ A') :=
  by
  intro A'
  obtain ⟨i, _, t⟩ := g _ A'.hom
  exact ⟨i, ⟨StructuredArrow.homMk _ t⟩⟩
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
⊢ ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')
[PROOFSTEP]
intro A'
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
A' : StructuredArrow A G
⊢ ∃ i, Nonempty (B' i ⟶ A')
[PROOFSTEP]
obtain ⟨i, _, t⟩ := g _ A'.hom
[GOAL]
case intro.intro
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
A' : StructuredArrow A G
i : ι
w✝ : B i ⟶ A'.right
t : f i ≫ G.map w✝ = A'.hom
⊢ ∃ i, Nonempty (B' i ⟶ A')
[PROOFSTEP]
exact ⟨i, ⟨StructuredArrow.homMk _ t⟩⟩
[GOAL]
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
hB' : ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')
⊢ HasInitial (StructuredArrow A G)
[PROOFSTEP]
obtain ⟨T, hT⟩ := has_weakly_initial_of_weakly_initial_set_and_hasProducts hB'
[GOAL]
case intro
J : Type v
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
hB' : ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')
T : StructuredArrow A G
hT : ∀ (X : StructuredArrow A G), Nonempty (T ⟶ X)
⊢ HasInitial (StructuredArrow A G)
[PROOFSTEP]
apply hasInitial_of_weakly_initial_and_hasWideEqualizers hT


[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


[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ ∀ ⦃X Y : C ⥤ D⦄ (f : X ⟶ Y),
    (𝟭 (C ⥤ D)).map f ≫
        (fun X =>
            (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
          Y =
      (fun X => (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
          X ≫
        ((whiskeringRight C D E).obj F ⋙ (whiskeringRight C E D).obj G).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ D
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (C ⥤ D)).map f✝ ≫
      (fun X => (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
        Y✝ =
    (fun X => (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
        X✝ ≫
      ((whiskeringRight C D E).obj F ⋙ (whiskeringRight C E D).obj G).map f✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ D
f✝ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app
      ((𝟭 (C ⥤ D)).map f✝ ≫
        (fun X =>
            (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
          Y✝)
      x✝ =
    NatTrans.app
      ((fun X =>
            (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
          X✝ ≫
        ((whiskeringRight C D E).obj F ⋙ (whiskeringRight C E D).obj G).map f✝)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ D
f✝ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app f✝ x✝ ≫ 𝟙 (Y✝.obj x✝) ≫ NatTrans.app adj.unit (Y✝.obj x✝) ≫ 𝟙 (G.obj (F.obj (Y✝.obj x✝))) =
    (𝟙 (X✝.obj x✝) ≫ NatTrans.app adj.unit (X✝.obj x✝) ≫ 𝟙 (G.obj (F.obj (X✝.obj x✝)))) ≫
      G.map (F.map (NatTrans.app f✝ x✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ ∀ ⦃X Y : C ⥤ E⦄ (f : X ⟶ Y),
    ((whiskeringRight C E D).obj G ⋙ (whiskeringRight C D E).obj F).map f ≫
        (fun X => (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom) Y =
      (fun X => (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom) X ≫
        (𝟭 (C ⥤ E)).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ E
f✝ : X✝ ⟶ Y✝
⊢ ((whiskeringRight C E D).obj G ⋙ (whiskeringRight C D E).obj F).map f✝ ≫
      (fun X => (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom) Y✝ =
    (fun X => (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom) X✝ ≫
      (𝟭 (C ⥤ E)).map f✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ E
f✝ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app
      (((whiskeringRight C E D).obj G ⋙ (whiskeringRight C D E).obj F).map f✝ ≫
        (fun X => (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom) Y✝)
      x✝ =
    NatTrans.app
      ((fun X => (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom) X✝ ≫
        (𝟭 (C ⥤ E)).map f✝)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ E
f✝ : X✝ ⟶ Y✝
x✝ : C
⊢ F.map (G.map (NatTrans.app f✝ x✝)) ≫
      𝟙 (F.obj (G.obj (Y✝.obj x✝))) ≫ NatTrans.app adj.counit (Y✝.obj x✝) ≫ 𝟙 (Y✝.obj x✝) =
    (𝟙 (F.obj (G.obj (X✝.obj x✝))) ≫ NatTrans.app adj.counit (X✝.obj x✝) ≫ 𝟙 (X✝.obj x✝)) ≫ NatTrans.app f✝ x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ whiskerRight
        (NatTrans.mk fun X =>
          (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
        ((whiskeringRight C D E).obj F) ≫
      (Functor.associator ((whiskeringRight C D E).obj F) ((whiskeringRight C E D).obj G)
            ((whiskeringRight C D E).obj F)).hom ≫
        whiskerLeft ((whiskeringRight C D E).obj F)
          (NatTrans.mk fun X =>
            (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom) =
    NatTrans.id (𝟭 (C ⥤ D) ⋙ (whiskeringRight C D E).obj F)
[PROOFSTEP]
ext
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x✝¹ : C ⥤ D
x✝ : C
⊢ NatTrans.app
      (NatTrans.app
        (whiskerRight
            (NatTrans.mk fun X =>
              (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
            ((whiskeringRight C D E).obj F) ≫
          (Functor.associator ((whiskeringRight C D E).obj F) ((whiskeringRight C E D).obj G)
                ((whiskeringRight C D E).obj F)).hom ≫
            whiskerLeft ((whiskeringRight C D E).obj F)
              (NatTrans.mk fun X =>
                (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom))
        x✝¹)
      x✝ =
    NatTrans.app (NatTrans.app (NatTrans.id (𝟭 (C ⥤ D) ⋙ (whiskeringRight C D E).obj F)) x✝¹) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x✝¹ : C ⥤ D
x✝ : C
⊢ F.map (𝟙 (x✝¹.obj x✝) ≫ NatTrans.app adj.unit (x✝¹.obj x✝) ≫ 𝟙 (G.obj (F.obj (x✝¹.obj x✝)))) ≫
      𝟙 (F.obj (G.obj (F.obj (x✝¹.obj x✝)))) ≫
        𝟙 (F.obj (G.obj (F.obj (x✝¹.obj x✝)))) ≫ NatTrans.app adj.counit (F.obj (x✝¹.obj x✝)) ≫ 𝟙 (F.obj (x✝¹.obj x✝)) =
    𝟙 (F.obj (x✝¹.obj x✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ whiskerLeft ((whiskeringRight C E D).obj G)
        (NatTrans.mk fun X =>
          (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv) ≫
      (Functor.associator ((whiskeringRight C E D).obj G) ((whiskeringRight C D E).obj F)
            ((whiskeringRight C E D).obj G)).inv ≫
        whiskerRight
          (NatTrans.mk fun X => (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom)
          ((whiskeringRight C E D).obj G) =
    NatTrans.id ((whiskeringRight C E D).obj G ⋙ 𝟭 (C ⥤ D))
[PROOFSTEP]
ext
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x✝¹ : C ⥤ E
x✝ : C
⊢ NatTrans.app
      (NatTrans.app
        (whiskerLeft ((whiskeringRight C E D).obj G)
            (NatTrans.mk fun X =>
              (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv) ≫
          (Functor.associator ((whiskeringRight C E D).obj G) ((whiskeringRight C D E).obj F)
                ((whiskeringRight C E D).obj G)).inv ≫
            whiskerRight
              (NatTrans.mk fun X =>
                (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom)
              ((whiskeringRight C E D).obj G))
        x✝¹)
      x✝ =
    NatTrans.app (NatTrans.app (NatTrans.id ((whiskeringRight C E D).obj G ⋙ 𝟭 (C ⥤ D))) x✝¹) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x✝¹ : C ⥤ E
x✝ : C
⊢ (𝟙 (G.obj (x✝¹.obj x✝)) ≫ NatTrans.app adj.unit (G.obj (x✝¹.obj x✝)) ≫ 𝟙 (G.obj (F.obj (G.obj (x✝¹.obj x✝))))) ≫
      𝟙 (G.obj (F.obj (G.obj (x✝¹.obj x✝)))) ≫
        G.map (𝟙 (F.obj (G.obj (x✝¹.obj x✝))) ≫ NatTrans.app adj.counit (x✝¹.obj x✝) ≫ 𝟙 (x✝¹.obj x✝)) =
    𝟙 (G.obj (x✝¹.obj x✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ ∀ ⦃X Y : D ⥤ C⦄ (f : X ⟶ Y),
    (𝟭 (D ⥤ C)).map f ≫
        (fun X =>
            (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
          Y =
      (fun X => (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
          X ≫
        ((whiskeringLeft E D C).obj G ⋙ (whiskeringLeft D E C).obj F).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : D ⥤ C
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (D ⥤ C)).map f✝ ≫
      (fun X => (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
        Y✝ =
    (fun X => (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
        X✝ ≫
      ((whiskeringLeft E D C).obj G ⋙ (whiskeringLeft D E C).obj F).map f✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : D ⥤ C
f✝ : X✝ ⟶ Y✝
x✝ : D
⊢ NatTrans.app
      ((𝟭 (D ⥤ C)).map f✝ ≫
        (fun X =>
            (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
          Y✝)
      x✝ =
    NatTrans.app
      ((fun X =>
            (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
          X✝ ≫
        ((whiskeringLeft E D C).obj G ⋙ (whiskeringLeft D E C).obj F).map f✝)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : D ⥤ C
f✝ : X✝ ⟶ Y✝
x✝ : D
⊢ NatTrans.app f✝ x✝ ≫ 𝟙 (Y✝.obj x✝) ≫ Y✝.map (NatTrans.app adj.unit x✝) ≫ 𝟙 (Y✝.obj (G.obj (F.obj x✝))) =
    (𝟙 (X✝.obj x✝) ≫ X✝.map (NatTrans.app adj.unit x✝) ≫ 𝟙 (X✝.obj (G.obj (F.obj x✝)))) ≫
      NatTrans.app f✝ (G.obj (F.obj x✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ ∀ ⦃X Y : E ⥤ C⦄ (f : X ⟶ Y),
    ((whiskeringLeft D E C).obj F ⋙ (whiskeringLeft E D C).obj G).map f ≫
        (fun X => (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom) Y =
      (fun X => (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom) X ≫
        (𝟭 (E ⥤ C)).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : E ⥤ C
f✝ : X✝ ⟶ Y✝
⊢ ((whiskeringLeft D E C).obj F ⋙ (whiskeringLeft E D C).obj G).map f✝ ≫
      (fun X => (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom) Y✝ =
    (fun X => (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom) X✝ ≫
      (𝟭 (E ⥤ C)).map f✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : E ⥤ C
f✝ : X✝ ⟶ Y✝
x✝ : E
⊢ NatTrans.app
      (((whiskeringLeft D E C).obj F ⋙ (whiskeringLeft E D C).obj G).map f✝ ≫
        (fun X => (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom) Y✝)
      x✝ =
    NatTrans.app
      ((fun X => (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom) X✝ ≫
        (𝟭 (E ⥤ C)).map f✝)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : E ⥤ C
f✝ : X✝ ⟶ Y✝
x✝ : E
⊢ NatTrans.app f✝ (F.obj (G.obj x✝)) ≫
      𝟙 (Y✝.obj (F.obj (G.obj x✝))) ≫ Y✝.map (NatTrans.app adj.counit x✝) ≫ 𝟙 (Y✝.obj x✝) =
    (𝟙 (X✝.obj (F.obj (G.obj x✝))) ≫ X✝.map (NatTrans.app adj.counit x✝) ≫ 𝟙 (X✝.obj x✝)) ≫ NatTrans.app f✝ x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ whiskerRight
        (NatTrans.mk fun X =>
          (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
        ((whiskeringLeft E D C).obj G) ≫
      (Functor.associator ((whiskeringLeft E D C).obj G) ((whiskeringLeft D E C).obj F)
            ((whiskeringLeft E D C).obj G)).hom ≫
        whiskerLeft ((whiskeringLeft E D C).obj G)
          (NatTrans.mk fun X =>
            (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom) =
    NatTrans.id (𝟭 (D ⥤ C) ⋙ (whiskeringLeft E D C).obj G)
[PROOFSTEP]
ext x
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x : D ⥤ C
x✝ : E
⊢ NatTrans.app
      (NatTrans.app
        (whiskerRight
            (NatTrans.mk fun X =>
              (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
            ((whiskeringLeft E D C).obj G) ≫
          (Functor.associator ((whiskeringLeft E D C).obj G) ((whiskeringLeft D E C).obj F)
                ((whiskeringLeft E D C).obj G)).hom ≫
            whiskerLeft ((whiskeringLeft E D C).obj G)
              (NatTrans.mk fun X =>
                (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom))
        x)
      x✝ =
    NatTrans.app (NatTrans.app (NatTrans.id (𝟭 (D ⥤ C) ⋙ (whiskeringLeft E D C).obj G)) x) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x : D ⥤ C
x✝ : E
⊢ (𝟙 (x.obj (G.obj x✝)) ≫ x.map (NatTrans.app adj.unit (G.obj x✝)) ≫ 𝟙 (x.obj (G.obj (F.obj (G.obj x✝))))) ≫
      𝟙 (x.obj (G.obj (F.obj (G.obj x✝)))) ≫
        𝟙 (x.obj (G.obj (F.obj (G.obj x✝)))) ≫ x.map (G.map (NatTrans.app adj.counit x✝)) ≫ 𝟙 (x.obj (G.obj x✝)) =
    𝟙 (x.obj (G.obj x✝))
[PROOFSTEP]
simp [Category.id_comp, Category.comp_id, ← x.map_comp]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ whiskerLeft ((whiskeringLeft D E C).obj F)
        (NatTrans.mk fun X =>
          (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom) ≫
      (Functor.associator ((whiskeringLeft D E C).obj F) ((whiskeringLeft E D C).obj G)
            ((whiskeringLeft D E C).obj F)).inv ≫
        whiskerRight
          (NatTrans.mk fun X => (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom)
          ((whiskeringLeft D E C).obj F) =
    NatTrans.id ((whiskeringLeft D E C).obj F ⋙ 𝟭 (D ⥤ C))
[PROOFSTEP]
ext x
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x : E ⥤ C
x✝ : D
⊢ NatTrans.app
      (NatTrans.app
        (whiskerLeft ((whiskeringLeft D E C).obj F)
            (NatTrans.mk fun X =>
              (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom) ≫
          (Functor.associator ((whiskeringLeft D E C).obj F) ((whiskeringLeft E D C).obj G)
                ((whiskeringLeft D E C).obj F)).inv ≫
            whiskerRight
              (NatTrans.mk fun X =>
                (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom)
              ((whiskeringLeft D E C).obj F))
        x)
      x✝ =
    NatTrans.app (NatTrans.app (NatTrans.id ((whiskeringLeft D E C).obj F ⋙ 𝟭 (D ⥤ C))) x) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x : E ⥤ C
x✝ : D
⊢ (𝟙 (x.obj (F.obj x✝)) ≫ x.map (F.map (NatTrans.app adj.unit x✝)) ≫ 𝟙 (x.obj (F.obj (G.obj (F.obj x✝))))) ≫
      𝟙 (x.obj (F.obj (G.obj (F.obj x✝)))) ≫
        𝟙 (x.obj (F.obj (G.obj (F.obj x✝)))) ≫ x.map (NatTrans.app adj.counit (F.obj x✝)) ≫ 𝟙 (x.obj (F.obj x✝)) =
    𝟙 (x.obj (F.obj x✝))
[PROOFSTEP]
simp [Category.id_comp, Category.comp_id, ← x.map_comp]


[GOAL]
A : Mon_ (Type u)
x y z : A.X
⊢ x * y * z = x * (y * z)
[PROOFSTEP]
convert congr_fun A.mul_assoc ((x, y), z)
[GOAL]
A : Mon_ (Type u)
x : A.X
⊢ 1 * x = x
[PROOFSTEP]
convert congr_fun A.one_mul (PUnit.unit, x)
[GOAL]
A : Mon_ (Type u)
x : A.X
⊢ x * 1 = x
[PROOFSTEP]
convert congr_fun A.mul_one (x, PUnit.unit)
[GOAL]
A : MonCat
⊢ (MonoidalCategory.tensorHom (fun x => 1) (𝟙 ↑A) ≫ fun p => p.fst * p.snd) = (MonoidalCategory.leftUnitor ↑A).hom
[PROOFSTEP]
ext ⟨_, _⟩
[GOAL]
case h.mk
A : MonCat
fst✝ : MonoidalCategory.tensorUnit (Type u)
snd✝ : ↑A
⊢ (MonoidalCategory.tensorHom (fun x => 1) (𝟙 ↑A) ≫ fun p => p.fst * p.snd) (fst✝, snd✝) =
    (MonoidalCategory.leftUnitor ↑A).hom (fst✝, snd✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.mk
A : MonCat
fst✝ : MonoidalCategory.tensorUnit (Type u)
snd✝ : ↑A
⊢ 1 * snd✝ = snd✝
[PROOFSTEP]
simp
[GOAL]
A : MonCat
⊢ ((MonoidalCategory.tensorHom (𝟙 ↑A) fun x => 1) ≫ fun p => p.fst * p.snd) = (MonoidalCategory.rightUnitor ↑A).hom
[PROOFSTEP]
ext ⟨_, _⟩
[GOAL]
case h.mk
A : MonCat
fst✝ : ↑A
snd✝ : MonoidalCategory.tensorUnit (Type u)
⊢ ((MonoidalCategory.tensorHom (𝟙 ↑A) fun x => 1) ≫ fun p => p.fst * p.snd) (fst✝, snd✝) =
    (MonoidalCategory.rightUnitor ↑A).hom (fst✝, snd✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.mk
A : MonCat
fst✝ : ↑A
snd✝ : MonoidalCategory.tensorUnit (Type u)
⊢ fst✝ * 1 = fst✝
[PROOFSTEP]
simp
[GOAL]
A : MonCat
⊢ (MonoidalCategory.tensorHom (fun p => p.fst * p.snd) (𝟙 ↑A) ≫ fun p => p.fst * p.snd) =
    (MonoidalCategory.associator ↑A ↑A ↑A).hom ≫
      (MonoidalCategory.tensorHom (𝟙 ↑A) fun p => p.fst * p.snd) ≫ fun p => p.fst * p.snd
[PROOFSTEP]
ext ⟨⟨x, y⟩, z⟩
[GOAL]
case h.mk.mk
A : MonCat
z x y : ↑A
⊢ (MonoidalCategory.tensorHom (fun p => p.fst * p.snd) (𝟙 ↑A) ≫ fun p => p.fst * p.snd) ((x, y), z) =
    ((MonoidalCategory.associator ↑A ↑A ↑A).hom ≫
        (MonoidalCategory.tensorHom (𝟙 ↑A) fun p => p.fst * p.snd) ≫ fun p => p.fst * p.snd)
      ((x, y), z)
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
⊢ ∀ {X Y : Mon_ (Type u)} (f : X ⟶ Y),
    (𝟭 (Mon_ (Type u))).map f ≫
        ((fun A =>
              Iso.mk (Mon_.Hom.mk (𝟙 ((𝟭 (Mon_ (Type u))).obj A).X)) (Mon_.Hom.mk (𝟙 ((functor ⋙ inverse).obj A).X)))
            Y).hom =
      ((fun A => Iso.mk (Mon_.Hom.mk (𝟙 ((𝟭 (Mon_ (Type u))).obj A).X)) (Mon_.Hom.mk (𝟙 ((functor ⋙ inverse).obj A).X)))
            X).hom ≫
        (functor ⋙ inverse).map f
[PROOFSTEP]
aesop_cat
[GOAL]
⊢ ∀ {X Y : MonCat} (f : X ⟶ Y),
    (inverse ⋙ functor).map f ≫
        ((fun A =>
              Iso.mk
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : ↑((inverse ⋙ functor).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) }
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : ↑((𝟭 MonCat).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
            Y).hom =
      ((fun A =>
              Iso.mk
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : ↑((inverse ⋙ functor).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) }
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : ↑((𝟭 MonCat).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
            X).hom ≫
        (𝟭 MonCat).map f
[PROOFSTEP]
aesop_cat
[GOAL]
⊢ ∀ {X Y : Mon_ (Type u)} (f : X ⟶ Y),
    (functor ⋙ forget MonCat).map f ≫ ((fun A => Iso.refl ((functor ⋙ forget MonCat).obj A)) Y).hom =
      ((fun A => Iso.refl ((functor ⋙ forget MonCat).obj A)) X).hom ≫ (Mon_.forget (Type u)).map f
[PROOFSTEP]
aesop_cat
[GOAL]
A : CommMon_ (Type u)
src✝ : Monoid A.X := monMonoid A.toMon_
x y : A.X
⊢ x * y = y * x
[PROOFSTEP]
convert congr_fun A.mul_comm (y, x)
[GOAL]
A : CommMonCat
src✝ : Mon_ (Type u) := MonTypeEquivalenceMon.inverse.obj ((forget₂ CommMonCat MonCat).obj A)
⊢ (β_ (Mon_.mk src✝.X src✝.one src✝.mul).X (Mon_.mk src✝.X src✝.one src✝.mul).X).hom ≫
      (Mon_.mk src✝.X src✝.one src✝.mul).mul =
    (Mon_.mk src✝.X src✝.one src✝.mul).mul
[PROOFSTEP]
ext ⟨x : A, y : A⟩
[GOAL]
case h.mk
A : CommMonCat
src✝ : Mon_ (Type u) := MonTypeEquivalenceMon.inverse.obj ((forget₂ CommMonCat MonCat).obj A)
x y : ↑A
⊢ ((β_ (Mon_.mk src✝.X src✝.one src✝.mul).X (Mon_.mk src✝.X src✝.one src✝.mul).X).hom ≫
        (Mon_.mk src✝.X src✝.one src✝.mul).mul)
      (x, y) =
    Mon_.mul (Mon_.mk src✝.X src✝.one src✝.mul) (x, y)
[PROOFSTEP]
exact CommMonoid.mul_comm y x
[GOAL]
⊢ ∀ {X Y : CommMon_ (Type u)} (f : X ⟶ Y),
    (𝟭 (CommMon_ (Type u))).map f ≫
        ((fun A =>
              Iso.mk (Mon_.Hom.mk (𝟙 ((𝟭 (CommMon_ (Type u))).obj A).X))
                (Mon_.Hom.mk
                  (𝟙 ((CommMonTypeEquivalenceCommMon.functor ⋙ CommMonTypeEquivalenceCommMon.inverse).obj A).X)))
            Y).hom =
      ((fun A =>
              Iso.mk (Mon_.Hom.mk (𝟙 ((𝟭 (CommMon_ (Type u))).obj A).X))
                (Mon_.Hom.mk
                  (𝟙 ((CommMonTypeEquivalenceCommMon.functor ⋙ CommMonTypeEquivalenceCommMon.inverse).obj A).X)))
            X).hom ≫
        (CommMonTypeEquivalenceCommMon.functor ⋙ CommMonTypeEquivalenceCommMon.inverse).map f
[PROOFSTEP]
aesop_cat
[GOAL]
⊢ ∀ {X Y : CommMonCat} (f : X ⟶ Y),
    (CommMonTypeEquivalenceCommMon.inverse ⋙ CommMonTypeEquivalenceCommMon.functor).map f ≫
        ((fun A =>
              Iso.mk
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀
                        (x y :
                          ↑((CommMonTypeEquivalenceCommMon.inverse ⋙ CommMonTypeEquivalenceCommMon.functor).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) }
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : ↑((𝟭 CommMonCat).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
            Y).hom =
      ((fun A =>
              Iso.mk
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀
                        (x y :
                          ↑((CommMonTypeEquivalenceCommMon.inverse ⋙ CommMonTypeEquivalenceCommMon.functor).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) }
                { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : ↑((𝟭 CommMonCat).obj A)),
                        OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
            X).hom ≫
        (𝟭 CommMonCat).map f
[PROOFSTEP]
aesop_cat
[GOAL]
⊢ ∀ {X Y : CommMon_ (Type u)} (f : X ⟶ Y),
    (CommMonTypeEquivalenceCommMon.functor ⋙ forget₂ CommMonCat MonCat).map f ≫
        ((fun A => Iso.refl ((CommMonTypeEquivalenceCommMon.functor ⋙ forget₂ CommMonCat MonCat).obj A)) Y).hom =
      ((fun A => Iso.refl ((CommMonTypeEquivalenceCommMon.functor ⋙ forget₂ CommMonCat MonCat).obj A)) X).hom ≫
        (CommMon_.forget₂Mon_ (Type u) ⋙ MonTypeEquivalenceMon.functor).map f
[PROOFSTEP]
aesop_cat


[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
⊢ (fun f => (initial.to (StructuredArrow.mk f)).right) ((fun g => (⊥_ StructuredArrow A G).hom ≫ G.map g) g) = g
[PROOFSTEP]
let B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
⊢ (fun f => (initial.to (StructuredArrow.mk f)).right) ((fun g => (⊥_ StructuredArrow A G).hom ≫ G.map g) g) = g
[PROOFSTEP]
let g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g rfl
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g
⊢ (fun f => (initial.to (StructuredArrow.mk f)).right) ((fun g => (⊥_ StructuredArrow A G).hom ≫ G.map g) g) = g
[PROOFSTEP]
have : initial.to _ = g' := by aesop_cat
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g
⊢ initial.to B' = g'
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g
this : initial.to B' = g'
⊢ (fun f => (initial.to (StructuredArrow.mk f)).right) ((fun g => (⊥_ StructuredArrow A G).hom ≫ G.map g) g) = g
[PROOFSTEP]
change CommaMorphism.right (initial.to B') = _
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g
this : initial.to B' = g'
⊢ (initial.to B').right = g
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g
this : initial.to B' = g'
⊢ g'.right = g
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
f : A ⟶ G.obj B
⊢ (fun g => (⊥_ StructuredArrow A G).hom ≫ G.map g) ((fun f => (initial.to (StructuredArrow.mk f)).right) f) = f
[PROOFSTEP]
let B' : StructuredArrow A G := StructuredArrow.mk f
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
f : A ⟶ G.obj B
B' : StructuredArrow A G := StructuredArrow.mk f
⊢ (fun g => (⊥_ StructuredArrow A G).hom ≫ G.map g) ((fun f => (initial.to (StructuredArrow.mk f)).right) f) = f
[PROOFSTEP]
apply (CommaMorphism.w (initial.to B')).symm.trans (Category.id_comp _)
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
x✝¹ : C
x✝ : D
⊢ ∀ (Y' : D) (g : x✝ ⟶ Y') (h : (⊥_ StructuredArrow x✝¹ G).right ⟶ x✝),
    ↑(leftAdjointOfStructuredArrowInitialsAux G x✝¹ Y') (h ≫ g) =
      ↑(leftAdjointOfStructuredArrowInitialsAux G x✝¹ x✝) h ≫ G.map g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
⊢ Function.LeftInverse (fun g => G.map g ≫ (⊤_ CostructuredArrow G A).hom) fun g =>
    (terminal.from (CostructuredArrow.mk g)).left
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
⊢ (fun g => (terminal.from (CostructuredArrow.mk g)).left) ((fun g => G.map g ≫ (⊤_ CostructuredArrow G A).hom) g) = g
[PROOFSTEP]
let B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
⊢ (fun g => (terminal.from (CostructuredArrow.mk g)).left) ((fun g => G.map g ≫ (⊤_ CostructuredArrow G A).hom) g) = g
[PROOFSTEP]
let g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g rfl
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g
⊢ (fun g => (terminal.from (CostructuredArrow.mk g)).left) ((fun g => G.map g ≫ (⊤_ CostructuredArrow G A).hom) g) = g
[PROOFSTEP]
have : terminal.from _ = g' := by aesop_cat
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g
⊢ terminal.from B' = g'
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g
this : terminal.from B' = g'
⊢ (fun g => (terminal.from (CostructuredArrow.mk g)).left) ((fun g => G.map g ≫ (⊤_ CostructuredArrow G A).hom) g) = g
[PROOFSTEP]
change CommaMorphism.left (terminal.from B') = _
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g
this : terminal.from B' = g'
⊢ (terminal.from B').left = g
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g
this : terminal.from B' = g'
⊢ g'.left = g
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B₁ B₂ : D
A : C
f : B₁ ⟶ B₂
g : G.obj B₂ ⟶ A
⊢ ↑(rightAdjointOfCostructuredArrowTerminalsAux G B₁ A) (G.map f ≫ g) =
    f ≫ ↑(rightAdjointOfCostructuredArrowTerminalsAux G B₂ A) g
[PROOFSTEP]
rw [← Equiv.eq_symm_apply]
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B₁ B₂ : D
A : C
f : B₁ ⟶ B₂
g : G.obj B₂ ⟶ A
⊢ G.map f ≫ g =
    ↑(rightAdjointOfCostructuredArrowTerminalsAux G B₁ A).symm
      (f ≫ ↑(rightAdjointOfCostructuredArrowTerminalsAux G B₂ A) g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : C
s : Cocone (Functor.empty (StructuredArrow A G))
m : (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).pt ⟶ s.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    NatTrans.app (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).ι j ≫ m = NatTrans.app s.ι j
⊢ m =
    (fun B =>
        StructuredArrow.homMk (↑(Adjunction.homEquiv h ((Functor.fromPUnit A).obj B.pt.left) B.pt.right).symm B.pt.hom))
      s
[PROOFSTEP]
apply StructuredArrow.ext
[GOAL]
case a
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : C
s : Cocone (Functor.empty (StructuredArrow A G))
m : (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).pt ⟶ s.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    NatTrans.app (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).ι j ≫ m = NatTrans.app s.ι j
⊢ m.right =
    ((fun B =>
          StructuredArrow.homMk
            (↑(Adjunction.homEquiv h ((Functor.fromPUnit A).obj B.pt.left) B.pt.right).symm B.pt.hom))
        s).right
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : C
s : Cocone (Functor.empty (StructuredArrow A G))
m : (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).pt ⟶ s.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    NatTrans.app (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).ι j ≫ m = NatTrans.app s.ι j
⊢ m.right = ↑(Adjunction.homEquiv h A s.pt.right).symm s.pt.hom
[PROOFSTEP]
rw [Equiv.eq_symm_apply, Adjunction.homEquiv_unit]
[GOAL]
case a
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : C
s : Cocone (Functor.empty (StructuredArrow A G))
m : (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).pt ⟶ s.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    NatTrans.app (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).ι j ≫ m = NatTrans.app s.ι j
⊢ NatTrans.app h.unit A ≫ G.map m.right = s.pt.hom
[PROOFSTEP]
apply StructuredArrow.w m
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : D
s : Cone (Functor.empty (CostructuredArrow F A))
m : s.pt ⟶ (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).π j = NatTrans.app s.π j
⊢ m =
    (fun B =>
        CostructuredArrow.homMk (↑(Adjunction.homEquiv h B.pt.left ((Functor.fromPUnit A).obj B.pt.right)) B.pt.hom))
      s
[PROOFSTEP]
apply CostructuredArrow.ext
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : D
s : Cone (Functor.empty (CostructuredArrow F A))
m : s.pt ⟶ (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).π j = NatTrans.app s.π j
⊢ m.left =
    ((fun B =>
          CostructuredArrow.homMk (↑(Adjunction.homEquiv h B.pt.left ((Functor.fromPUnit A).obj B.pt.right)) B.pt.hom))
        s).left
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : D
s : Cone (Functor.empty (CostructuredArrow F A))
m : s.pt ⟶ (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).π j = NatTrans.app s.π j
⊢ m.left = ↑(Adjunction.homEquiv h s.pt.left A) s.pt.hom
[PROOFSTEP]
rw [h.eq_homEquiv_apply, Adjunction.homEquiv_counit]
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : D
s : Cone (Functor.empty (CostructuredArrow F A))
m : s.pt ⟶ (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).π j = NatTrans.app s.π j
⊢ F.map m.left ≫ NatTrans.app h.counit A = s.pt.hom
[PROOFSTEP]
exact CostructuredArrow.w m