Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : L' ⟶ G✝.obj L
β✝ : R ⋙ G✝ ⟶ F✝ ⋙ R'
F : C ≌ A
G : D ≌ B
α : L' ⟶ G.functor.obj L
α' : L ⟶ G.inverse.obj L'
β : R ⋙ G.functor ⟶ F.functor ⋙ R'
β' : R' ⋙ G.inverse ⟶ F.inverse ⋙ R
hαα' : α ≫ G.functor.map α' = G.counitIso.inv.app L'
hα'α : α' ≫ G.inverse.map α = G.unitIso.hom.app L
hββ' :
  R.rightUnitor.hom ≫ R.leftUnitor.inv ≫ Functor.whiskerRight F.unitIso.hom R ≫ (F.functor.associator F.inverse R).hom =
    R.whiskerLeft G.unitIso.hom ≫
      (R.associator G.functor G.inverse).inv ≫
        Functor.whiskerRight β G.inverse ≫ (F.functor.associator R' G.inverse).hom ≫ F.functor.whiskerLeft β'
hβ'β :
  Functor.whiskerRight β' G.functor ≫
      (F.inverse.associator R G.functor).hom ≫
        F.inverse.whiskerLeft β ≫ (F.inverse.associator F.functor R').inv ≫ Functor.whiskerRight F.counitIso.hom R' =
    (R'.associator G.inverse G.functor).hom ≫ R'.whiskerLeft G.counitIso.hom ≫ R'.rightUnitor.hom ≫ R'.leftUnitor.inv
⊢ 𝟙 L = (α' ≫ G.inverse.map α) ≫ G.unitIso.inv.app L

pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : L' ⟶ G✝.obj L
β✝ : R ⋙ G✝ ⟶ F✝ ⋙ R'
F : C ≌ A
G : D ≌ B
α : L' ⟶ G.functor.obj L
α' : L ⟶ G.inverse.obj L'
β : R ⋙ G.functor ⟶ F.functor ⋙ R'
β' : R' ⋙ G.inverse ⟶ F.inverse ⋙ R
hαα' : α ≫ G.functor.map α' = G.counitIso.inv.app L'
hα'α : α' ≫ G.inverse.map α = G.unitIso.hom.app L
hββ' :
  R.rightUnitor.hom ≫ R.leftUnitor.inv ≫ Functor.whiskerRight F.unitIso.hom R ≫ (F.functor.associator F.inverse R).hom =
    R.whiskerLeft G.unitIso.hom ≫
      (R.associator G.functor G.inverse).inv ≫
        Functor.whiskerRight β G.inverse ≫ (F.functor.associator R' G.inverse).hom ≫ F.functor.whiskerLeft β'
hβ'β :
  Functor.whiskerRight β' G.functor ≫
      (F.inverse.associator R G.functor).hom ≫
        F.inverse.whiskerLeft β ≫ (F.inverse.associator F.functor R').inv ≫ Functor.whiskerRight F.counitIso.hom R' =
    (R'.associator G.inverse G.functor).hom ≫ R'.whiskerLeft G.counitIso.hom ≫ R'.rightUnitor.hom ≫ R'.leftUnitor.inv
⊢ (R.rightUnitor.hom ≫ R.leftUnitor.inv) ≫ Functor.whiskerRight F.unitIso.hom R =
    R.whiskerLeft G.unitIso.hom ≫
      (R.associator G.functor G.inverse).inv ≫
        Functor.whiskerRight β G.inverse ≫
          (F.functor.associator R' G.inverse).hom ≫ F.functor.whiskerLeft β' ≫ (F.functor.associator F.inverse R).inv

pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : L' ⟶ G✝.obj L
β✝ : R ⋙ G✝ ⟶ F✝ ⋙ R'
F : C ≌ A
G : D ≌ B
α : L' ⟶ G.functor.obj L
α' : L ⟶ G.inverse.obj L'
β : R ⋙ G.functor ⟶ F.functor ⋙ R'
β' : R' ⋙ G.inverse ⟶ F.inverse ⋙ R
hαα' : α ≫ G.functor.map α' = G.counitIso.inv.app L'
hα'α : α' ≫ G.inverse.map α = G.unitIso.hom.app L
hββ' :
  R.rightUnitor.hom ≫ R.leftUnitor.inv ≫ Functor.whiskerRight F.unitIso.hom R ≫ (F.functor.associator F.inverse R).hom =
    R.whiskerLeft G.unitIso.hom ≫
      (R.associator G.functor G.inverse).inv ≫
        Functor.whiskerRight β G.inverse ≫ (F.functor.associator R' G.inverse).hom ≫ F.functor.whiskerLeft β'
hβ'β :
  Functor.whiskerRight β' G.functor ≫
      (F.inverse.associator R G.functor).hom ≫
        F.inverse.whiskerLeft β ≫ (F.inverse.associator F.functor R').inv ≫ Functor.whiskerRight F.counitIso.hom R' =
    (R'.associator G.inverse G.functor).hom ≫ R'.whiskerLeft G.counitIso.hom ≫ R'.rightUnitor.hom ≫ R'.leftUnitor.inv
⊢ α ≫ G.functor.map α' = 𝟙 L' ≫ G.counitIso.inv.app L'

pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : L' ⟶ G✝.obj L
β✝ : R ⋙ G✝ ⟶ F✝ ⋙ R'
F : C ≌ A
G : D ≌ B
α : L' ⟶ G.functor.obj L
α' : L ⟶ G.inverse.obj L'
β : R ⋙ G.functor ⟶ F.functor ⋙ R'
β' : R' ⋙ G.inverse ⟶ F.inverse ⋙ R
hαα' : α ≫ G.functor.map α' = G.counitIso.inv.app L'
hα'α : α' ≫ G.inverse.map α = G.unitIso.hom.app L
hββ' :
  R.rightUnitor.hom ≫ R.leftUnitor.inv ≫ Functor.whiskerRight F.unitIso.hom R ≫ (F.functor.associator F.inverse R).hom =
    R.whiskerLeft G.unitIso.hom ≫
      (R.associator G.functor G.inverse).inv ≫
        Functor.whiskerRight β G.inverse ≫ (F.functor.associator R' G.inverse).hom ≫ F.functor.whiskerLeft β'
hβ'β :
  Functor.whiskerRight β' G.functor ≫
      (F.inverse.associator R G.functor).hom ≫
        F.inverse.whiskerLeft β ≫ (F.inverse.associator F.functor R').inv ≫ Functor.whiskerRight F.counitIso.hom R' =
    (R'.associator G.inverse G.functor).hom ≫ R'.whiskerLeft G.counitIso.hom ≫ R'.rightUnitor.hom ≫ R'.leftUnitor.inv
⊢ ((R'.associator G.inverse G.functor).inv ≫
        Functor.whiskerRight β' G.functor ≫
          (F.inverse.associator R G.functor).hom ≫ F.inverse.whiskerLeft β ≫ (F.inverse.associator F.functor R').inv) ≫
      Functor.whiskerRight F.counitIso.hom R' =
    R'.whiskerLeft G.counitIso.hom ≫ R'.rightUnitor.hom ≫ R'.leftUnitor.inv

pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : L' ⟶ G✝.obj L
β✝ : R ⋙ G✝ ⟶ F✝ ⋙ R'
F : C ≌ A
G : D ≌ B
α : L' ⟶ G.functor.obj L
α' : L ⟶ G.inverse.obj L'
β : R ⋙ G.functor ⟶ F.functor ⋙ R'
β' : R' ⋙ G.inverse ⟶ F.inverse ⋙ R
hαα' : α ≫ G.functor.map α' = G.counitIso.inv.app L'
hα'α : α' ≫ G.inverse.map α = G.unitIso.hom.app L
hββ' :
  R.rightUnitor.hom ≫ R.leftUnitor.inv ≫ Functor.whiskerRight F.unitIso.hom R ≫ (F.functor.associator F.inverse R).hom =
    R.whiskerLeft G.unitIso.hom ≫
      (R.associator G.functor G.inverse).inv ≫
        Functor.whiskerRight β G.inverse ≫ (F.functor.associator R' G.inverse).hom ≫ F.functor.whiskerLeft β'
hβ'β :
  Functor.whiskerRight β' G.functor ≫
      (F.inverse.associator R G.functor).hom ≫
        F.inverse.whiskerLeft β ≫ (F.inverse.associator F.functor R').inv ≫ Functor.whiskerRight F.counitIso.hom R' =
    (R'.associator G.inverse G.functor).hom ≫ R'.whiskerLeft G.counitIso.hom ≫ R'.rightUnitor.hom ≫ R'.leftUnitor.inv
⊢ ∀ (X : StructuredArrow L R),
    (map₂ α β).map
          (((map₂IdIso L (𝟙 L) (R.rightUnitor.hom ≫ R.leftUnitor.inv) ⋯ ⋯).symm ≪≫
                  map₂Congr (𝟙 L) (R.rightUnitor.hom ≫ R.leftUnitor.inv) F.unitIso G.unitIso (α' ≫ G.inverse.map α)
                      ((R.associator G.functor G.inverse).inv ≫
                        Functor.whiskerRight β G.inverse ≫
                          (F.functor.associator R' G.inverse).hom ≫
                            F.functor.whiskerLeft β' ≫ (F.functor.associator F.inverse R).inv)
                      ?m.563 ?m.564 ≪≫
                    (map₂CompMap₂Iso α' β' α β).symm).hom.app
            X) ≫
        (map₂CompMap₂Iso α β α' β' ≪≫
                map₂Congr (α ≫ G.functor.map α')
                    ((R'.associator G.inverse G.functor).inv ≫
                      Functor.whiskerRight β' G.functor ≫
                        (F.inverse.associator R G.functor).hom ≫
                          F.inverse.whiskerLeft β ≫ (F.inverse.associator F.functor R').inv)
                    F.counitIso G.counitIso (𝟙 L') (R'.rightUnitor.hom ≫ R'.leftUnitor.inv) ?m.659 ?m.660 ≪≫
                  map₂IdIso L' (𝟙 L') (R'.rightUnitor.hom ≫ R'.leftUnitor.inv) ⋯ ⋯).hom.app
          ((map₂ α β).obj X) =
      𝟙 ((map₂ α β).obj X)

Tactic:
finally
  · simp [reassoc_of% hα'α]
  · ext X
    simpa using congr($(hββ').app X)
  · simp [hαα']
  · ext X
    simpa using congr($(hβ'β).app X)
  · simp [map₂Congr]

Goal state after: