awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (goal)
Goal:
A : Type v₁
inst : Category.{v₁, v₁} A
B : Type v₁
inst_1 : Category.{v₁, v₁} B
T : Type v₁
inst_2 : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst_3 : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  Iso.trans (Y := colimit (grothendieckProj L ⋙ G))
    (L.colimitIsoColimitGrothendieck G : colimit G ≅ colimit (grothendieckProj L ⋙ G))
    (Iso.trans (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.symm (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)) :
          colimit (grothendieckProj L ⋙ G) ≅ colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.trans (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) :
              colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ≅
                colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G) :
              colimit ((grothendieckPrecompFunctorEquivalence L R).functor ⋙ fst L R ⋙ G) ≅ colimit (fst L R ⋙ G)) :
          colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ≅ colimit (fst L R ⋙ G)) :
      colimit (grothendieckProj L ⋙ G) ≅ colimit (fst L R ⋙ G))
⊢ IsIso (X := colimit (fst L R ⋙ G)) (Y := colimit G) (colimit.pre G (fst L R))
have h : colimit.pre G (fst L R) = i.inv
Tactic: convert! i.isIso_inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (goal)
Goal:
A : Type v₁
inst : Category.{v₁, v₁} A
B : Type v₁
inst_1 : Category.{v₁, v₁} B
T : Type v₁
inst_2 : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst_3 : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  Iso.trans (Y := colimit (grothendieckProj L ⋙ G))
    (L.colimitIsoColimitGrothendieck G : colimit G ≅ colimit (grothendieckProj L ⋙ G))
    (Iso.trans (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.symm (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)) :
          colimit (grothendieckProj L ⋙ G) ≅ colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.trans (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) :
              colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ≅
                colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G) :
              colimit ((grothendieckPrecompFunctorEquivalence L R).functor ⋙ fst L R ⋙ G) ≅ colimit (fst L R ⋙ G)) :
          colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ≅ colimit (fst L R ⋙ G)) :
      colimit (grothendieckProj L ⋙ G) ≅ colimit (fst L R ⋙ G))
⊢ colimit.pre G (fst L R) = i.inv
have h : ∀ (j : Comma L R),
  CategoryStruct.comp (Y := colimit (fst L R ⋙ G)) (colimit.ι (fst L R ⋙ G) j) (colimit.pre G (fst L R)) =
    colimit.ι (fst L R ⋙ G) j ≫ i.inv
Tactic: apply colimit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (hypothesis)
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 : R.Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
fC : Comma L R ⥤ Comma L' R' :=
  map (F₁ := sA.functor) (F₂ := sB.functor) (F := sT.functor) (isoWhiskerRight sA.unitIso (L ⋙ sT.functor)).hom
    (isoWhiskerRight sB.unitIso (R ⋙ sT.functor)).hom
⊢ (fst L R).Final
have this : (fst L' R').Final
Tactic: have : Final (fst L' R') := final_fst_small _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (goal)
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 : R.Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
fC : Comma L R ⥤ Comma L' R' :=
  map (F₁ := sA.functor) (F₂ := sB.functor) (F := sT.functor) (isoWhiskerRight sA.unitIso (L ⋙ sT.functor)).hom
    (isoWhiskerRight sB.unitIso (R ⋙ sT.functor)).hom
this : (fst L' R').Final
⊢ (fst L R).Final
have apply : fC ⋙ fst L' R' ⋙ sA.inverse ≅ fst L R
Tactic: apply final_of_natIso (F := (fC ⋙ fst L' R' ⋙ sA.inverse))
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (hypothesis)
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 : L.Initial
⊢ (snd L R).Initial
have this : ((opFunctor L R).leftOp ⋙ fst R.op L.op).Final
Tactic: have : ((opFunctor L R).leftOp ⋙ fst R.op L.op).Final :=
    final_equivalence_comp (opEquiv L R).functor.leftOp (fst R.op L.op)
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (hypothesis)
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 : L.Initial
this : ((opFunctor L R).leftOp ⋙ fst R.op L.op).Final
⊢ (snd L R).Initial
have this₁ : (snd L R).op.Final
Tactic: have : (snd L R).op.Final := final_of_natIso (opFunctorCompFst _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (hypothesis)
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₂
⊢ IsConnected (StructuredArrow { left := i₂, right := j₂, hom := u₂ : Comma L' R' } (map iL.hom iR.inv))
have this : (R ⋙ H).Final
Tactic: haveI := final_of_natIso iR
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (goal)
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
⊢ IsConnected (StructuredArrow { left := i₂, right := j₂, hom := u₂ : Comma L' R' } (map iL.hom iR.inv))
have 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 (inv iR.inv)))
Tactic: rw [isConnected_iff_of_equivalence (StructuredArrow.commaMapEquivalence iL.hom iR.inv _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (goal)
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
⊢ 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))
have 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₂)))
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (goal)
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₂)))
⊢ 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))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (goal)
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
⊢ 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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (goal)
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
⊢ 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)))
have 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)))
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 _
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (hypothesis)
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
⊢ 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)))
have this₁ : (StructuredArrow.map₂ u₂ iR.hom).Final
Tactic: haveI := final_of_natIso this.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (goal)
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 (inv iR.inv)))
have 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))
Tactic: rw [IsIso.Iso.inv_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (hypothesis)
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
⊢ IsFiltered (Comma L R)
have this : ∀ (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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (hypothesis)
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)
⊢ IsFiltered (Comma L R)
have this₁ : ∀ (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (hypothesis)
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)) ⋯
⊢ IsFiltered (Comma L R)
have this₁ : ∀ (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))
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (hypothesis)
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)
⊢ IsFiltered (Comma L R)
have this₁ : RepresentablyCoflat (fst L R)
Tactic: have : RepresentablyCoflat (fst L R) :=
    ⟨fun a => IsFiltered.of_equivalence (CostructuredArrow.ofCommaFstEquivalence L R a).symm⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (hypothesis)
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)
⊢ (snd L R).Final
have this : (map iL.hom iR.inv).Final
Tactic: have := map_final iL iR
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (hypothesis)
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
⊢ (fst L R).Initial
have this : ((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 _
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Final (hypothesis)
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).Initial
have this₁ : (fst L R).op.Final
Tactic: have : (fst L R).op.Final := final_of_natIso <| opFunctorCompSnd _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
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
⊢ f = g
have 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
Tactic: let ⟨_,b,_⟩ := f
Cleared hypotheses: h