awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F : Functor.{v₁, v₄, u₁, u₄} A A'
G : Functor.{v₂, v₅, u₂, u₅} B B'
H : Functor.{v₃, v₆, u₃, u₆} T T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst_6 : IsFiltered.{v₂, u₂} B
inst_7 : R.Final
inst_8 : R'.Final
inst_9 : F.Final
inst_10 : G.Final
x : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
e_α :
  u₂ =
    CategoryStruct.comp (Y := obj.{v₆, v₆, u₆, u₆} (𝟭 T' ⋙ 𝟭 T') (R'.obj j₂)) (𝟙 (L'.obj i₂) ≫ Functor.map (𝟭 T') u₂)
      (Functor.map (𝟭 T' ⋙ 𝟭 T') (𝟙 (R'.obj j₂)))
e_β :
  iR.hom =
    (G.associator R' (𝟭 T' ⋙ 𝟭 T')).inv ≫
      whiskerRight (𝟙 (G ⋙ R')) (𝟭 T' ⋙ 𝟭 T') ≫
        Iso.hom (associator (𝟭 B) (G ⋙ R') (𝟭 T' ⋙ 𝟭 T')) ≫
          whiskerLeft (𝟭 B)
              (((G ⋙ R').associator (𝟭 T') (𝟭 T')).inv ≫
                whiskerRight iR.hom (𝟭 T') ≫
                  Iso.hom (associator (𝟭 B) (R ⋙ H) (𝟭 T')) ≫
                    whiskerLeft (𝟭 B) (𝟙 (R ⋙ H)) ≫ Iso.inv (associator (𝟭 B) R H)) ≫
            Iso.inv (associator (𝟭 B) (𝟭 B ⋙ R) H)
⊢ StructuredArrow.map₂ u₂ iR.hom =
    StructuredArrow.map₂ (F := 𝟭 B ⋙ 𝟭 B ⋙ R)
      (CategoryStruct.comp (Y := obj.{v₆, v₆, u₆, u₆} (𝟭 T' ⋙ 𝟭 T') (R'.obj j₂)) (𝟙 (L'.obj i₂) ≫ Functor.map (𝟭 T') u₂)
        (Functor.map (𝟭 T' ⋙ 𝟭 T') (𝟙 (R'.obj j₂))))
      ((G.associator R' (𝟭 T' ⋙ 𝟭 T')).inv ≫
        whiskerRight (𝟙 (G ⋙ R')) (𝟭 T' ⋙ 𝟭 T') ≫
          Iso.hom (associator (𝟭 B) (G ⋙ R') (𝟭 T' ⋙ 𝟭 T')) ≫
            whiskerLeft (𝟭 B)
                (((G ⋙ R').associator (𝟭 T') (𝟭 T')).inv ≫
                  whiskerRight iR.hom (𝟭 T') ≫
                    Iso.hom (associator (𝟭 B) (R ⋙ H) (𝟭 T')) ≫
                      whiskerLeft (𝟭 B) (𝟙 (R ⋙ H)) ≫ Iso.inv (associator (𝟭 B) R H)) ≫
              Iso.inv (associator (𝟭 B) (𝟭 B ⋙ R) H))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F : Functor.{v₁, v₄, u₁, u₄} A A'
G : Functor.{v₂, v₅, u₂, u₅} B B'
H : Functor.{v₃, v₆, u₃, u₆} T T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst_6 : IsFiltered.{v₂, u₂} B
inst_7 : R.Final
inst_8 : R'.Final
inst_9 : F.Final
inst_10 : G.Final
x : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
⊢ u₂ =
    CategoryStruct.comp (Y := obj.{v₆, v₆, u₆, u₆} (𝟭 T' ⋙ 𝟭 T') (R'.obj j₂)) (𝟙 (L'.obj i₂) ≫ Functor.map (𝟭 T') u₂)
      (Functor.map (𝟭 T' ⋙ 𝟭 T') (𝟙 (R'.obj j₂)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F : Functor.{v₁, v₄, u₁, u₄} A A'
G : Functor.{v₂, v₅, u₂, u₅} B B'
H : Functor.{v₃, v₆, u₃, u₆} T T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst_6 : IsFiltered.{v₂, u₂} B
inst_7 : R.Final
inst_8 : R'.Final
inst_9 : F.Final
inst_10 : G.Final
x : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
e_β :
  ∀ (x : B),
    iR.hom.app x =
      NatTrans.app
        ((G.associator R' (𝟭 T' ⋙ 𝟭 T')).inv ≫
          whiskerRight (𝟙 (G ⋙ R')) (𝟭 T' ⋙ 𝟭 T') ≫
            Iso.hom (associator (𝟭 B) (G ⋙ R') (𝟭 T' ⋙ 𝟭 T')) ≫
              whiskerLeft (𝟭 B)
                  (((G ⋙ R').associator (𝟭 T') (𝟭 T')).inv ≫
                    whiskerRight iR.hom (𝟭 T') ≫
                      Iso.hom (associator (𝟭 B) (R ⋙ H) (𝟭 T')) ≫
                        whiskerLeft (𝟭 B) (𝟙 (R ⋙ H)) ≫ Iso.inv (associator (𝟭 B) R H)) ≫
                Iso.inv (associator (𝟭 B) (𝟭 B ⋙ R) H))
        x
⊢ iR.hom =
    (G.associator R' (𝟭 T' ⋙ 𝟭 T')).inv ≫
      whiskerRight (𝟙 (G ⋙ R')) (𝟭 T' ⋙ 𝟭 T') ≫
        Iso.hom (associator (𝟭 B) (G ⋙ R') (𝟭 T' ⋙ 𝟭 T')) ≫
          whiskerLeft (𝟭 B)
              (((G ⋙ R').associator (𝟭 T') (𝟭 T')).inv ≫
                whiskerRight iR.hom (𝟭 T') ≫
                  Iso.hom (associator (𝟭 B) (R ⋙ H) (𝟭 T')) ≫
                    whiskerLeft (𝟭 B) (𝟙 (R ⋙ H)) ≫ Iso.inv (associator (𝟭 B) R H)) ≫
            Iso.inv (associator (𝟭 B) (𝟭 B ⋙ R) H)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F : Functor.{v₁, v₄, u₁, u₄} A A'
G : Functor.{v₂, v₅, u₂, u₅} B B'
H : Functor.{v₃, v₆, u₃, u₆} T T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst_6 : IsFiltered.{v₂, u₂} B
inst_7 : R.Final
inst_8 : R'.Final
inst_9 : F.Final
inst_10 : G.Final
x : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
x_1 : B
⊢ iR.hom.app x_1 =
    NatTrans.app
      ((G.associator R' (𝟭 T' ⋙ 𝟭 T')).inv ≫
        whiskerRight (𝟙 (G ⋙ R')) (𝟭 T' ⋙ 𝟭 T') ≫
          Iso.hom (associator (𝟭 B) (G ⋙ R') (𝟭 T' ⋙ 𝟭 T')) ≫
            whiskerLeft (𝟭 B)
                (((G ⋙ R').associator (𝟭 T') (𝟭 T')).inv ≫
                  whiskerRight iR.hom (𝟭 T') ≫
                    Iso.hom (associator (𝟭 B) (R ⋙ H) (𝟭 T')) ≫
                      whiskerLeft (𝟭 B) (𝟙 (R ⋙ H)) ≫ Iso.inv (associator (𝟭 B) R H)) ≫
              Iso.inv (associator (𝟭 B) (𝟭 B ⋙ R) H))
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F : Functor.{v₁, v₄, u₁, u₄} A A'
G : Functor.{v₂, v₅, u₂, u₅} B B'
H : Functor.{v₃, v₆, u₃, u₆} T T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst_6 : IsFiltered.{v₂, u₂} B
inst_7 : R.Final
inst_8 : R'.Final
inst_9 : F.Final
inst_10 : G.Final
x : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
have :
  ∀
    (this :
      StructuredArrow.map₂ u₂ iR.hom ≅
        StructuredArrow.post j₂ G R' ⋙
          StructuredArrow.map₂ (F := 𝟭 B) (G := 𝟭 T') u₂ iR.hom ⋙ StructuredArrow.pre (L'.obj i₂) R H),
    IsConnected
      (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ : Comma L' R' }.left)) iL.hom)
        (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ : Comma L' R' }.hom (inv iR.inv)))
⊢ IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ : Comma L' R' }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ : Comma L' R' }.hom (inv iR.inv)))

Tactic:
have : StructuredArrow.map₂ u₂ iR.hom ≅ StructuredArrow.post j₂ G R' ⋙
      StructuredArrow.map₂ (G := 𝟭 _) (F := 𝟭 _) (R' := R ⋙ H) u₂ iR.hom ⋙
      StructuredArrow.pre _ R H :=
    eqToIso (by
      congr
      · simp
      · ext; simp) ≪≫
    (StructuredArrow.map₂CompMap₂Iso _ _ _ _).symm ≪≫
    isoWhiskerLeft _ ((StructuredArrow.map₂CompMap₂Iso _ _ _ _).symm ≪≫
      isoWhiskerLeft _ (StructuredArrow.preIsoMap₂ _ _ _).symm) ≪≫
    isoWhiskerRight (StructuredArrow.postIsoMap₂ j₂ G R').symm _
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F : Functor.{v₁, v₄, u₁, u₄} A A'
G : Functor.{v₂, v₅, u₂, u₅} B B'
H : Functor.{v₃, v₆, u₃, u₆} T T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst_6 : IsFiltered.{v₂, u₂} B
inst_7 : R.Final
inst_8 : R'.Final
inst_9 : F.Final
inst_10 : G.Final
x : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this_1 : (R ⋙ H).Final
this :
  StructuredArrow.map₂ u₂ iR.hom ≅
    StructuredArrow.post j₂ G R' ⋙
      StructuredArrow.map₂ (F := 𝟭 B) (G := 𝟭 T') u₂ iR.hom ⋙ StructuredArrow.pre (L'.obj i₂) R H
⊢ (StructuredArrow.map₂ u₂ iR.hom).Final

Tactic:
haveI := final_of_natIso this.symm
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F : Functor.{v₁, v₄, u₁, u₄} A A'
G : Functor.{v₂, v₅, u₂, u₅} B B'
H : Functor.{v₃, v₆, u₃, u₆} T T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst_6 : IsFiltered.{v₂, u₂} B
inst_7 : R.Final
inst_8 : R'.Final
inst_9 : F.Final
inst_10 : G.Final
x : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this_1 : (R ⋙ H).Final
this_2 :
  StructuredArrow.map₂ u₂ iR.hom ≅
    StructuredArrow.post j₂ G R' ⋙
      StructuredArrow.map₂ (F := 𝟭 B) (G := 𝟭 T') u₂ iR.hom ⋙ StructuredArrow.pre (L'.obj i₂) R H
this : (StructuredArrow.map₂ u₂ iR.hom).Final
rw :
  IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ : Comma L' R' }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ : Comma L' R' }.hom iR.hom))
⊢ IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ : Comma L' R' }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ : Comma L' R' }.hom (inv iR.inv)))

Tactic:
rw [IsIso.Iso.inv_inv]

Premises used: CategoryTheory.IsIso.Iso.inv_inv
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F : Functor.{v₁, v₄, u₁, u₄} A A'
G : Functor.{v₂, v₅, u₂, u₅} B B'
H : Functor.{v₃, v₆, u₃, u₆} T T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst_6 : IsFiltered.{v₂, u₂} B
inst_7 : R.Final
inst_8 : R'.Final
inst_9 : F.Final
inst_10 : G.Final
x : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this_1 : (R ⋙ H).Final
this_2 :
  StructuredArrow.map₂ u₂ iR.hom ≅
    StructuredArrow.post j₂ G R' ⋙
      StructuredArrow.map₂ (F := 𝟭 B) (G := 𝟭 T') u₂ iR.hom ⋙ StructuredArrow.pre (L'.obj i₂) R H
this : (StructuredArrow.map₂ u₂ iR.hom).Final
⊢ IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ : Comma L' R' }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ : Comma L' R' }.hom iR.hom))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsFiltered.{v₁, u₁} A
inst_4 : IsFiltered.{v₂, u₂} B
inst_5 : R.Final
⊢ ∀ (a : A), IsFiltered (Comma (fromPUnit (L.obj a)) R)

Tactic:
haveI (a : A) : IsFiltered (Comma (fromPUnit (L.obj a)) R) :=
    R.final_iff_isFiltered_structuredArrow.mp inferInstance (L.obj a)
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsFiltered.{v₁, u₁} A
inst_4 : IsFiltered.{v₂, u₂} B
inst_5 : R.Final
this : ∀ (a : A), IsFiltered (Comma (fromPUnit (L.obj a)) R)
⊢ ∀ (a : A), Final (D := Over.{v₁, u₁} a) (fromPUnit (Over.mk (𝟙 a)))

Tactic:
have (a : A) : (fromPUnit (Over.mk (𝟙 a))).Final := final_const_of_isTerminal Over.mkIdTerminal
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsFiltered.{v₁, u₁} A
inst_4 : IsFiltered.{v₂, u₂} B
inst_5 : R.Final
this_1 : ∀ (a : A), IsFiltered (Comma (fromPUnit (L.obj a)) R)
this : ∀ (a : A), Final (D := Over.{v₁, u₁} a) (fromPUnit (Over.mk (𝟙 a)))
η : (a : A) → fromPUnit (Over.mk (𝟙 a)) ⋙ Over.forget a ⋙ L ≅ fromPUnit (L.obj a) :=
  fun (a : A) ↦
    NatIso.ofComponents
      (fun (x : Discrete PUnit.{1}) ↦ Iso.refl ((fromPUnit (Over.mk (𝟙 a)) ⋙ Over.forget a ⋙ L).obj x)) ⋯
⊢ ∀ (a : A), IsFiltered (Comma (Over.forget a ⋙ L) R)

Tactic:
have (a : A) := IsFiltered.of_final (map (L := fromPUnit (L.obj a)) (F := 𝟭 T) (η a).hom
    ((Iso.refl (𝟭 B ⋙ R)).inv))
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsFiltered.{v₁, u₁} A
inst_4 : IsFiltered.{v₂, u₂} B
inst_5 : R.Final
this_1 : ∀ (a : A), IsFiltered (Comma (fromPUnit (L.obj a)) R)
this_2 : ∀ (a : A), Final (D := Over.{v₁, u₁} a) (fromPUnit (Over.mk (𝟙 a)))
η : (a : A) → fromPUnit (Over.mk (𝟙 a)) ⋙ Over.forget a ⋙ L ≅ fromPUnit (L.obj a) :=
  fun (a : A) ↦
    NatIso.ofComponents
      (fun (x : Discrete PUnit.{1}) ↦ Iso.refl ((fromPUnit (Over.mk (𝟙 a)) ⋙ Over.forget a ⋙ L).obj x)) ⋯
this : ∀ (a : A), IsFiltered (Comma (Over.forget a ⋙ L) R)
⊢ RepresentablyCoflat (fst L R)

Tactic:
have : RepresentablyCoflat (fst L R) :=
    ⟨fun a => IsFiltered.of_equivalence (CostructuredArrow.ofCommaFstEquivalence L R a).symm⟩
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsFiltered.{v₁, u₁} A
inst_4 : IsFiltered.{v₂, u₂} B
inst_5 : R.Final
this_1 : ∀ (a : A), IsFiltered (Comma (fromPUnit (L.obj a)) R)
this_2 : ∀ (a : A), Final (D := Over.{v₁, u₁} a) (fromPUnit (Over.mk (𝟙 a)))
η : (a : A) → fromPUnit (Over.mk (𝟙 a)) ⋙ Over.forget a ⋙ L ≅ fromPUnit (L.obj a) :=
  fun (a : A) ↦
    NatIso.ofComponents
      (fun (x : Discrete PUnit.{1}) ↦ Iso.refl ((fromPUnit (Over.mk (𝟙 a)) ⋙ Over.forget a ⋙ L).obj x)) ⋯
this_3 : ∀ (a : A), IsFiltered (Comma (Over.forget a ⋙ L) R)
this : RepresentablyCoflat (fst L R)
⊢ IsFiltered (Comma L R)

Tactic:
apply isFiltered_of_representablyCoflat (fst L R)

Premises used: CategoryTheory.Comma.fst, CategoryTheory.isFiltered_of_representablyCoflat
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsCofiltered.{v₁, u₁} A
inst_4 : IsCofiltered.{v₂, u₂} B
inst_5 : L.Initial
⊢ IsCofiltered (Comma L R)

Tactic:
IsCofiltered.of_equivalence (Comma.opEquiv _ _).symm

Premises used: CategoryTheory.Comma.opEquiv, CategoryTheory.Equivalence.symm, CategoryTheory.IsCofiltered.of_equivalence
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsFiltered.{v₁, u₁} A
inst_4 : IsFiltered.{v₂, u₂} B
inst_5 : R.Final
iL : Functor.star A ⋙ 𝟭 (Discrete PUnit.{2}) ≅ L ⋙ Functor.star T := Iso.refl (Functor.star A ⋙ 𝟭 (Discrete PUnit.{2}))
iR : 𝟭 B ⋙ Functor.star B ≅ R ⋙ Functor.star T := Iso.refl (𝟭 B ⋙ Functor.star B)
⊢ (map iL.hom iR.inv).Final

Tactic:
have := map_final iL iR
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsFiltered.{v₁, u₁} A
inst_4 : IsFiltered.{v₂, u₂} B
inst_5 : R.Final
iL : Functor.star A ⋙ 𝟭 (Discrete PUnit.{2}) ≅ L ⋙ Functor.star T := Iso.refl (Functor.star A ⋙ 𝟭 (Discrete PUnit.{2}))
iR : 𝟭 B ⋙ Functor.star B ≅ R ⋙ Functor.star T := Iso.refl (𝟭 B ⋙ Functor.star B)
this : (map iL.hom iR.inv).Final
s : Equivalence.{max v₂ 1, v₂, max u₂ 1, u₂} (Comma.{1, v₂, 1, 1, u₂, 1} (𝟭 (Discrete PUnit.{2})) (Functor.star B)) B :=
  Equivalence.trans (equivProd (𝟭 (Discrete PUnit.{2})) (Functor.star B)) (prod.leftUnitorEquivalence B)
X Y : Comma L R
f : X ⟶ Y
⊢ (map iL.hom iR.inv ⋙ s.functor).map f ≫
      Iso.hom
        ((fun (x : Comma L R) ↦
            (Iso.refl ((map iL.hom iR.inv ⋙ s.functor).obj x) :
              (map iL.hom iR.inv ⋙ s.functor).obj x ≅ (map iL.hom iR.inv ⋙ s.functor).obj x))
          Y) =
    Iso.hom
        ((fun (x : Comma L R) ↦
            (Iso.refl ((map iL.hom iR.inv ⋙ s.functor).obj x) :
              (map iL.hom iR.inv ⋙ s.functor).obj x ≅ (map iL.hom iR.inv ⋙ s.functor).obj x))
          X) ≫
      (snd L R).map f

Tactic:
simp [iL, iR, s]
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsFiltered.{v₁, u₁} A
inst_4 : IsFiltered.{v₂, u₂} B
inst_5 : R.Final
iL : Functor.star A ⋙ 𝟭 (Discrete PUnit.{2}) ≅ L ⋙ Functor.star T := Iso.refl (Functor.star A ⋙ 𝟭 (Discrete PUnit.{2}))
iR : 𝟭 B ⋙ Functor.star B ≅ R ⋙ Functor.star T := Iso.refl (𝟭 B ⋙ Functor.star B)
this : (map iL.hom iR.inv).Final
s : Equivalence.{max v₂ 1, v₂, max u₂ 1, u₂} (Comma.{1, v₂, 1, 1, u₂, 1} (𝟭 (Discrete PUnit.{2})) (Functor.star B)) B :=
  Equivalence.trans (equivProd (𝟭 (Discrete PUnit.{2})) (Functor.star B)) (prod.leftUnitorEquivalence B)
iS : map iL.hom iR.inv ⋙ s.functor ≅ snd L R :=
  NatIso.ofComponents (fun (x : Comma L R) ↦ Iso.refl ((map iL.hom iR.inv ⋙ s.functor).obj x)) ⋯
⊢ (snd L R).Final

Tactic:
apply final_of_natIso iS

Premises used: CategoryTheory.Functor.final_of_natIso
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsCofiltered.{v₁, u₁} A
inst_4 : IsCofiltered.{v₂, u₂} B
inst_5 : L.Initial
⊢ ((opFunctor L R).leftOp ⋙ snd R.op L.op).Final

Tactic:
have : ((opFunctor L R).leftOp ⋙ snd R.op L.op).Final :=
    final_equivalence_comp (opEquiv L R).functor.leftOp _
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsCofiltered.{v₁, u₁} A
inst_4 : IsCofiltered.{v₂, u₂} B
inst_5 : L.Initial
this : ((opFunctor L R).leftOp ⋙ snd R.op L.op).Final
⊢ (fst L R).op.Final

Tactic:
have : (fst L R).op.Final := final_of_natIso <| opFunctorCompSnd _ _
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsCofiltered.{v₁, u₁} A
inst_4 : IsCofiltered.{v₂, u₂} B
inst_5 : L.Initial
this_1 : ((opFunctor L R).leftOp ⋙ snd R.op L.op).Final
this : (fst L R).op.Final
⊢ (fst L R).Initial

Tactic:
apply initial_of_final_op

Premises used: CategoryTheory.Functor.initial_of_final_op
-- Module: Mathlib.CategoryTheory.Comma.LocallySmall
Goal:
A : Type u₁
B : Type u₂
T : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : LocallySmall.{w, v₁, u₁} A
inst_4 : LocallySmall.{w, v₂, u₂} B
X Y : Comma L R
x x_1 : X ⟶ Y
h :
  Eq (α := Prod.{v₁, v₂} (X.left ⟶ Y.left) (X.right ⟶ Y.right)) ((fun (g : X ⟶ Y) ↦ (g.left, g.right)) x)
    ((fun (g : X ⟶ Y) ↦ (g.left, g.right)) x_1)
⊢ x = x_1

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Comma.LocallySmall
Goal:
A : Type u₁
B : Type u₂
T_1 : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} T_1
S : T_1
T : Functor.{v₂, v₃, u₂, u₃} B T_1
inst_3 : LocallySmall.{w, v₂, u₂} B
⊢ LocallySmall.{w, v₂, max u₂ v₃} (StructuredArrow S T)

Tactic:
Comma.locallySmall _ _

Premises used: CategoryTheory.StructuredArrow.Hom, CategoryTheory.Comma.locallySmall, CategoryTheory.StructuredArrow
-- Module: Mathlib.CategoryTheory.Comma.LocallySmall
Goal:
A : Type u₁
B : Type u₂
T : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} T
S : Functor.{v₁, v₃, u₁, u₃} A T
X : T
inst_3 : LocallySmall.{w, v₁, u₁} A
⊢ LocallySmall.{w, v₁, max u₁ v₃} (CostructuredArrow S X)

Tactic:
Comma.locallySmall _ _

Premises used: CategoryTheory.CostructuredArrow, CategoryTheory.Comma.locallySmall
-- Module: Mathlib.CategoryTheory.Comma.LocallySmall
Goal:
A : Type u₁
B : Type u₂
T : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} T
X : T
inst_3 : LocallySmall.{w, v₃, u₃} T
⊢ LocallySmall.{w, v₃, max u₃ v₃} (Over.{v₃, u₃} X)

Tactic:
CostructuredArrow.locallySmall _ _

Premises used: CategoryTheory.Over, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.locallySmall
-- Module: Mathlib.CategoryTheory.Comma.LocallySmall
Goal:
A : Type u₁
B : Type u₂
T : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} T
X : T
inst_3 : LocallySmall.{w, v₃, u₃} T
⊢ LocallySmall.{w, v₃, max u₃ v₃} (Under.{v₃, u₃} X)

Tactic:
StructuredArrow.locallySmall _ _

Premises used: CategoryTheory.StructuredArrow.Hom, CategoryTheory.Under, CategoryTheory.Under.Hom, CategoryTheory.StructuredArrow.locallySmall
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
f g : Over.{v₁, u₁} X
φ : f ⟶ g
⊢ Hom.left φ ≫ g.hom = f.hom

Tactic:
simpa using (CommaMorphism.w φ)

Premises used: CategoryTheory.CommaMorphism.w
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
f g : Over.{v₁, u₁} X
φ : f ⟶ g
⊢ left φ ≫ g.hom = f.hom

Tactic:
Over.w φ

Premises used: CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V : Over.{v₁, u₁} X
f g : U ⟶ V
h : Hom.left f = Hom.left g
let :
  ∀ (left : U.left ⟶ V.left) (b : U.right ⟶ V.right)
    (w : Functor.map (𝟭 T) left ≫ V.hom = U.hom ≫ Functor.map (Functor.fromPUnit X) b)
    (h : Hom.left { left := left, right := b, w := w : CommaMorphism U V } = Hom.left g),
    { left := left, right := b, w := w : CommaMorphism U V } = g
⊢ f = g

Tactic:
let ⟨_,b,_⟩ := f