[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ RepresentablyFlat (𝟭 C)
[PROOFSTEP]
constructor
[GOAL]
case cofiltered
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ ∀ (X : C), IsCofiltered (StructuredArrow X (𝟭 C))
[PROOFSTEP]
intro X
[GOAL]
case cofiltered
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
⊢ IsCofiltered (StructuredArrow X (𝟭 C))
[PROOFSTEP]
haveI : Nonempty (StructuredArrow X (𝟭 C)) := ⟨StructuredArrow.mk (𝟙 _)⟩
[GOAL]
case cofiltered
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
⊢ IsCofiltered (StructuredArrow X (𝟭 C))
[PROOFSTEP]
suffices : IsCofilteredOrEmpty (StructuredArrow X (𝟭 C))
[GOAL]
case cofiltered
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this✝ : Nonempty (StructuredArrow X (𝟭 C))
this : IsCofilteredOrEmpty (StructuredArrow X (𝟭 C))
⊢ IsCofiltered (StructuredArrow X (𝟭 C))
[PROOFSTEP]
constructor
[GOAL]
case this
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
⊢ IsCofilteredOrEmpty (StructuredArrow X (𝟭 C))
[PROOFSTEP]
constructor
[GOAL]
case this.cone_objs
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
⊢ ∀ (X_1 Y : StructuredArrow X (𝟭 C)), ∃ W x x, True
[PROOFSTEP]
intro Y Z
[GOAL]
case this.cone_objs
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
Y Z : StructuredArrow X (𝟭 C)
⊢ ∃ W x x, True
[PROOFSTEP]
use StructuredArrow.mk (𝟙 _)
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
Y Z : StructuredArrow X (𝟭 C)
⊢ ∃ x x, True
[PROOFSTEP]
use StructuredArrow.homMk Y.hom (by erw [Functor.id_map, Category.id_comp])
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
Y Z : StructuredArrow X (𝟭 C)
⊢ (StructuredArrow.mk (𝟙 X)).hom ≫ (𝟭 C).map Y.hom = Y.hom
[PROOFSTEP]
erw [Functor.id_map, Category.id_comp]
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
Y Z : StructuredArrow X (𝟭 C)
⊢ ∃ x, True
[PROOFSTEP]
use StructuredArrow.homMk Z.hom (by erw [Functor.id_map, Category.id_comp])
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
Y Z : StructuredArrow X (𝟭 C)
⊢ (StructuredArrow.mk (𝟙 X)).hom ≫ (𝟭 C).map Z.hom = Z.hom
[PROOFSTEP]
erw [Functor.id_map, Category.id_comp]
[GOAL]
case this.cone_maps
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
⊢ ∀ ⦃X_1 Y : StructuredArrow X (𝟭 C)⦄ (f g : X_1 ⟶ Y), ∃ W h, h ≫ f = h ≫ g
[PROOFSTEP]
intro Y Z f g
[GOAL]
case this.cone_maps
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
Y Z : StructuredArrow X (𝟭 C)
f g : Y ⟶ Z
⊢ ∃ W h, h ≫ f = h ≫ g
[PROOFSTEP]
use StructuredArrow.mk (𝟙 _)
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
Y Z : StructuredArrow X (𝟭 C)
f g : Y ⟶ Z
⊢ ∃ h, h ≫ f = h ≫ g
[PROOFSTEP]
use StructuredArrow.homMk Y.hom (by erw [Functor.id_map, Category.id_comp])
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
Y Z : StructuredArrow X (𝟭 C)
f g : Y ⟶ Z
⊢ (StructuredArrow.mk (𝟙 X)).hom ≫ (𝟭 C).map Y.hom = Y.hom
[PROOFSTEP]
erw [Functor.id_map, Category.id_comp]
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
Y Z : StructuredArrow X (𝟭 C)
f g : Y ⟶ Z
⊢ StructuredArrow.homMk Y.hom ≫ f = StructuredArrow.homMk Y.hom ≫ g
[PROOFSTEP]
ext
[GOAL]
case h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
Y Z : StructuredArrow X (𝟭 C)
f g : Y ⟶ Z
⊢ (StructuredArrow.homMk Y.hom ≫ f).right = (StructuredArrow.homMk Y.hom ≫ g).right
[PROOFSTEP]
trans Z.hom
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
Y Z : StructuredArrow X (𝟭 C)
f g : Y ⟶ Z
⊢ (StructuredArrow.homMk Y.hom ≫ f).right = Z.hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X : C
this : Nonempty (StructuredArrow X (𝟭 C))
Y Z : StructuredArrow X (𝟭 C)
f g : Y ⟶ Z
⊢ Z.hom = (StructuredArrow.homMk Y.hom ≫ g).right
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
⊢ RepresentablyFlat (F ⋙ G)
[PROOFSTEP]
constructor
[GOAL]
case cofiltered
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
⊢ ∀ (X : E), IsCofiltered (StructuredArrow X (F ⋙ G))
[PROOFSTEP]
intro X
[GOAL]
case cofiltered
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))
[PROOFSTEP]
have : Nonempty (StructuredArrow X (F ⋙ G)) :=
  by
  have f₁ : StructuredArrow X G := Nonempty.some inferInstance
  have f₂ : StructuredArrow f₁.right F := Nonempty.some inferInstance
  exact ⟨StructuredArrow.mk (f₁.hom ≫ G.map f₂.hom)⟩
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
⊢ Nonempty (StructuredArrow X (F ⋙ G))
[PROOFSTEP]
have f₁ : StructuredArrow X G := Nonempty.some inferInstance
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
f₁ : StructuredArrow X G
⊢ Nonempty (StructuredArrow X (F ⋙ G))
[PROOFSTEP]
have f₂ : StructuredArrow f₁.right F := Nonempty.some inferInstance
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
f₁ : StructuredArrow X G
f₂ : StructuredArrow f₁.right F
⊢ Nonempty (StructuredArrow X (F ⋙ G))
[PROOFSTEP]
exact ⟨StructuredArrow.mk (f₁.hom ≫ G.map f₂.hom)⟩
[GOAL]
case cofiltered
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))
[PROOFSTEP]
suffices : IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G))
[GOAL]
case cofiltered
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this✝ : Nonempty (StructuredArrow X (F ⋙ G))
this : IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G))
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))
[PROOFSTEP]
constructor
[GOAL]
case this
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
⊢ IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G))
[PROOFSTEP]
constructor
[GOAL]
case this.cone_objs
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
⊢ ∀ (X_1 Y : StructuredArrow X (F ⋙ G)), ∃ W x x, True
[PROOFSTEP]
intro Y Z
[GOAL]
case this.cone_objs
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
⊢ ∃ W x x, True
[PROOFSTEP]
let W := @IsCofiltered.min (StructuredArrow X G) _ _ (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
[GOAL]
case this.cone_objs
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
W : StructuredArrow X G := IsCofiltered.min (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
⊢ ∃ W x x, True
[PROOFSTEP]
let Y' : W ⟶ _ := IsCofiltered.minToLeft _ _
[GOAL]
case this.cone_objs
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
W : StructuredArrow X G := IsCofiltered.min (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Y' : W ⟶ StructuredArrow.mk Y.hom := IsCofiltered.minToLeft (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
⊢ ∃ W x x, True
[PROOFSTEP]
let Z' : W ⟶ _ := IsCofiltered.minToRight _ _
[GOAL]
case this.cone_objs
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
W : StructuredArrow X G := IsCofiltered.min (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Y' : W ⟶ StructuredArrow.mk Y.hom := IsCofiltered.minToLeft (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Z' : W ⟶ StructuredArrow.mk Z.hom := IsCofiltered.minToRight (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
⊢ ∃ W x x, True
[PROOFSTEP]
let W' := @IsCofiltered.min (StructuredArrow W.right F) _ _ (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
[GOAL]
case this.cone_objs
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
W : StructuredArrow X G := IsCofiltered.min (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Y' : W ⟶ StructuredArrow.mk Y.hom := IsCofiltered.minToLeft (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Z' : W ⟶ StructuredArrow.mk Z.hom := IsCofiltered.minToRight (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
W' : StructuredArrow W.right F := IsCofiltered.min (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
⊢ ∃ W x x, True
[PROOFSTEP]
let Y'' : W' ⟶ _ := IsCofiltered.minToLeft _ _
[GOAL]
case this.cone_objs
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
W : StructuredArrow X G := IsCofiltered.min (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Y' : W ⟶ StructuredArrow.mk Y.hom := IsCofiltered.minToLeft (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Z' : W ⟶ StructuredArrow.mk Z.hom := IsCofiltered.minToRight (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
W' : StructuredArrow W.right F := IsCofiltered.min (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
Y'' : W' ⟶ StructuredArrow.mk Y'.right :=
  IsCofiltered.minToLeft (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
⊢ ∃ W x x, True
[PROOFSTEP]
let Z'' : W' ⟶ _ := IsCofiltered.minToRight _ _
[GOAL]
case this.cone_objs
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
W : StructuredArrow X G := IsCofiltered.min (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Y' : W ⟶ StructuredArrow.mk Y.hom := IsCofiltered.minToLeft (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Z' : W ⟶ StructuredArrow.mk Z.hom := IsCofiltered.minToRight (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
W' : StructuredArrow W.right F := IsCofiltered.min (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
Y'' : W' ⟶ StructuredArrow.mk Y'.right :=
  IsCofiltered.minToLeft (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
Z'' : W' ⟶ StructuredArrow.mk Z'.right :=
  IsCofiltered.minToRight (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
⊢ ∃ W x x, True
[PROOFSTEP]
use StructuredArrow.mk (W.hom ≫ G.map W'.hom)
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
W : StructuredArrow X G := IsCofiltered.min (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Y' : W ⟶ StructuredArrow.mk Y.hom := IsCofiltered.minToLeft (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Z' : W ⟶ StructuredArrow.mk Z.hom := IsCofiltered.minToRight (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
W' : StructuredArrow W.right F := IsCofiltered.min (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
Y'' : W' ⟶ StructuredArrow.mk Y'.right :=
  IsCofiltered.minToLeft (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
Z'' : W' ⟶ StructuredArrow.mk Z'.right :=
  IsCofiltered.minToRight (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
⊢ ∃ x x, True
[PROOFSTEP]
use StructuredArrow.homMk Y''.right (by simp [← G.map_comp])
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
W : StructuredArrow X G := IsCofiltered.min (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Y' : W ⟶ StructuredArrow.mk Y.hom := IsCofiltered.minToLeft (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Z' : W ⟶ StructuredArrow.mk Z.hom := IsCofiltered.minToRight (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
W' : StructuredArrow W.right F := IsCofiltered.min (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
Y'' : W' ⟶ StructuredArrow.mk Y'.right :=
  IsCofiltered.minToLeft (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
Z'' : W' ⟶ StructuredArrow.mk Z'.right :=
  IsCofiltered.minToRight (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
⊢ (StructuredArrow.mk (W.hom ≫ G.map W'.hom)).hom ≫ (F ⋙ G).map Y''.right = Y.hom
[PROOFSTEP]
simp [← G.map_comp]
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
W : StructuredArrow X G := IsCofiltered.min (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Y' : W ⟶ StructuredArrow.mk Y.hom := IsCofiltered.minToLeft (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Z' : W ⟶ StructuredArrow.mk Z.hom := IsCofiltered.minToRight (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
W' : StructuredArrow W.right F := IsCofiltered.min (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
Y'' : W' ⟶ StructuredArrow.mk Y'.right :=
  IsCofiltered.minToLeft (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
Z'' : W' ⟶ StructuredArrow.mk Z'.right :=
  IsCofiltered.minToRight (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
⊢ ∃ x, True
[PROOFSTEP]
use StructuredArrow.homMk Z''.right (by simp [← G.map_comp])
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
W : StructuredArrow X G := IsCofiltered.min (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Y' : W ⟶ StructuredArrow.mk Y.hom := IsCofiltered.minToLeft (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
Z' : W ⟶ StructuredArrow.mk Z.hom := IsCofiltered.minToRight (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
W' : StructuredArrow W.right F := IsCofiltered.min (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
Y'' : W' ⟶ StructuredArrow.mk Y'.right :=
  IsCofiltered.minToLeft (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
Z'' : W' ⟶ StructuredArrow.mk Z'.right :=
  IsCofiltered.minToRight (StructuredArrow.mk Y'.right) (StructuredArrow.mk Z'.right)
⊢ (StructuredArrow.mk (W.hom ≫ G.map W'.hom)).hom ≫ (F ⋙ G).map Z''.right = Z.hom
[PROOFSTEP]
simp [← G.map_comp]
[GOAL]
case this.cone_maps
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
⊢ ∀ ⦃X_1 Y : StructuredArrow X (F ⋙ G)⦄ (f g : X_1 ⟶ Y), ∃ W h, h ≫ f = h ≫ g
[PROOFSTEP]
intro Y Z f g
[GOAL]
case this.cone_maps
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
f g : Y ⟶ Z
⊢ ∃ W h, h ≫ f = h ≫ g
[PROOFSTEP]
let W :=
  @IsCofiltered.eq (StructuredArrow X G) _ _ (StructuredArrow.mk Y.hom) (StructuredArrow.mk Z.hom)
    (StructuredArrow.homMk (F.map f.right) (StructuredArrow.w f))
    (StructuredArrow.homMk (F.map g.right) (StructuredArrow.w g))
[GOAL]
case this.cone_maps
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
f g : Y ⟶ Z
W : StructuredArrow X G :=
  IsCofiltered.eq (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
⊢ ∃ W h, h ≫ f = h ≫ g
[PROOFSTEP]
let h : W ⟶ _ := IsCofiltered.eqHom _ _
[GOAL]
case this.cone_maps
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
f g : Y ⟶ Z
W : StructuredArrow X G :=
  IsCofiltered.eq (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h : W ⟶ StructuredArrow.mk Y.hom :=
  IsCofiltered.eqHom (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
⊢ ∃ W h, h ≫ f = h ≫ g
[PROOFSTEP]
let h_cond : h ≫ _ = h ≫ _ := IsCofiltered.eq_condition _ _
[GOAL]
case this.cone_maps
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
f g : Y ⟶ Z
W : StructuredArrow X G :=
  IsCofiltered.eq (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h : W ⟶ StructuredArrow.mk Y.hom :=
  IsCofiltered.eqHom (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h_cond : h ≫ StructuredArrow.homMk (F.map f.right) = h ≫ StructuredArrow.homMk (F.map g.right) :=
  IsCofiltered.eq_condition (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
⊢ ∃ W h, h ≫ f = h ≫ g
[PROOFSTEP]
let W' :=
  @IsCofiltered.eq (StructuredArrow W.right F) _ _ (StructuredArrow.mk h.right)
    (StructuredArrow.mk (h.right ≫ F.map f.right)) (StructuredArrow.homMk f.right rfl)
    (StructuredArrow.homMk g.right (congr_arg CommaMorphism.right h_cond).symm)
[GOAL]
case this.cone_maps
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
f g : Y ⟶ Z
W : StructuredArrow X G :=
  IsCofiltered.eq (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h : W ⟶ StructuredArrow.mk Y.hom :=
  IsCofiltered.eqHom (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h_cond : h ≫ StructuredArrow.homMk (F.map f.right) = h ≫ StructuredArrow.homMk (F.map g.right) :=
  IsCofiltered.eq_condition (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
W' : StructuredArrow W.right F := IsCofiltered.eq (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
⊢ ∃ W h, h ≫ f = h ≫ g
[PROOFSTEP]
let h' : W' ⟶ _ := IsCofiltered.eqHom _ _
[GOAL]
case this.cone_maps
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
f g : Y ⟶ Z
W : StructuredArrow X G :=
  IsCofiltered.eq (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h : W ⟶ StructuredArrow.mk Y.hom :=
  IsCofiltered.eqHom (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h_cond : h ≫ StructuredArrow.homMk (F.map f.right) = h ≫ StructuredArrow.homMk (F.map g.right) :=
  IsCofiltered.eq_condition (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
W' : StructuredArrow W.right F := IsCofiltered.eq (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
h' : W' ⟶ StructuredArrow.mk h.right :=
  IsCofiltered.eqHom (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
⊢ ∃ W h, h ≫ f = h ≫ g
[PROOFSTEP]
let h'_cond : h' ≫ _ = h' ≫ _ := IsCofiltered.eq_condition _ _
[GOAL]
case this.cone_maps
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
f g : Y ⟶ Z
W : StructuredArrow X G :=
  IsCofiltered.eq (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h : W ⟶ StructuredArrow.mk Y.hom :=
  IsCofiltered.eqHom (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h_cond : h ≫ StructuredArrow.homMk (F.map f.right) = h ≫ StructuredArrow.homMk (F.map g.right) :=
  IsCofiltered.eq_condition (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
W' : StructuredArrow W.right F := IsCofiltered.eq (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
h' : W' ⟶ StructuredArrow.mk h.right :=
  IsCofiltered.eqHom (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
h'_cond : h' ≫ StructuredArrow.homMk f.right = h' ≫ StructuredArrow.homMk g.right :=
  IsCofiltered.eq_condition (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
⊢ ∃ W h, h ≫ f = h ≫ g
[PROOFSTEP]
use StructuredArrow.mk (W.hom ≫ G.map W'.hom)
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
f g : Y ⟶ Z
W : StructuredArrow X G :=
  IsCofiltered.eq (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h : W ⟶ StructuredArrow.mk Y.hom :=
  IsCofiltered.eqHom (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h_cond : h ≫ StructuredArrow.homMk (F.map f.right) = h ≫ StructuredArrow.homMk (F.map g.right) :=
  IsCofiltered.eq_condition (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
W' : StructuredArrow W.right F := IsCofiltered.eq (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
h' : W' ⟶ StructuredArrow.mk h.right :=
  IsCofiltered.eqHom (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
h'_cond : h' ≫ StructuredArrow.homMk f.right = h' ≫ StructuredArrow.homMk g.right :=
  IsCofiltered.eq_condition (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
⊢ ∃ h, h ≫ f = h ≫ g
[PROOFSTEP]
use StructuredArrow.homMk h'.right (by simp [← G.map_comp])
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
f g : Y ⟶ Z
W : StructuredArrow X G :=
  IsCofiltered.eq (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h : W ⟶ StructuredArrow.mk Y.hom :=
  IsCofiltered.eqHom (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h_cond : h ≫ StructuredArrow.homMk (F.map f.right) = h ≫ StructuredArrow.homMk (F.map g.right) :=
  IsCofiltered.eq_condition (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
W' : StructuredArrow W.right F := IsCofiltered.eq (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
h' : W' ⟶ StructuredArrow.mk h.right :=
  IsCofiltered.eqHom (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
h'_cond : h' ≫ StructuredArrow.homMk f.right = h' ≫ StructuredArrow.homMk g.right :=
  IsCofiltered.eq_condition (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
⊢ (StructuredArrow.mk (W.hom ≫ G.map W'.hom)).hom ≫ (F ⋙ G).map h'.right = Y.hom
[PROOFSTEP]
simp [← G.map_comp]
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
f g : Y ⟶ Z
W : StructuredArrow X G :=
  IsCofiltered.eq (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h : W ⟶ StructuredArrow.mk Y.hom :=
  IsCofiltered.eqHom (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h_cond : h ≫ StructuredArrow.homMk (F.map f.right) = h ≫ StructuredArrow.homMk (F.map g.right) :=
  IsCofiltered.eq_condition (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
W' : StructuredArrow W.right F := IsCofiltered.eq (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
h' : W' ⟶ StructuredArrow.mk h.right :=
  IsCofiltered.eqHom (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
h'_cond : h' ≫ StructuredArrow.homMk f.right = h' ≫ StructuredArrow.homMk g.right :=
  IsCofiltered.eq_condition (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
⊢ StructuredArrow.homMk h'.right ≫ f = StructuredArrow.homMk h'.right ≫ g
[PROOFSTEP]
ext
[GOAL]
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
this : Nonempty (StructuredArrow X (F ⋙ G))
Y Z : StructuredArrow X (F ⋙ G)
f g : Y ⟶ Z
W : StructuredArrow X G :=
  IsCofiltered.eq (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h : W ⟶ StructuredArrow.mk Y.hom :=
  IsCofiltered.eqHom (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
h_cond : h ≫ StructuredArrow.homMk (F.map f.right) = h ≫ StructuredArrow.homMk (F.map g.right) :=
  IsCofiltered.eq_condition (StructuredArrow.homMk (F.map f.right)) (StructuredArrow.homMk (F.map g.right))
W' : StructuredArrow W.right F := IsCofiltered.eq (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
h' : W' ⟶ StructuredArrow.mk h.right :=
  IsCofiltered.eqHom (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
h'_cond : h' ≫ StructuredArrow.homMk f.right = h' ≫ StructuredArrow.homMk g.right :=
  IsCofiltered.eq_condition (StructuredArrow.homMk f.right) (StructuredArrow.homMk g.right)
⊢ (StructuredArrow.homMk h'.right ≫ f).right = (StructuredArrow.homMk h'.right ≫ g).right
[PROOFSTEP]
exact (congr_arg CommaMorphism.right h'_cond : _)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
⊢ HasFiniteLimits (StructuredArrow X F)
[PROOFSTEP]
apply hasFiniteLimits_of_hasFiniteLimits_of_size.{v₁} (StructuredArrow X F)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
⊢ ∀ (J : Type v₁) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J (StructuredArrow X F)
[PROOFSTEP]
intro J sJ fJ
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
J : Type v₁
sJ : SmallCategory J
fJ : FinCategory J
⊢ HasLimitsOfShape J (StructuredArrow X F)
[PROOFSTEP]
constructor
  -- porting note: instance was inferred automatically in Lean 3
[GOAL]
case has_limit
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
J : Type v₁
sJ : SmallCategory J
fJ : FinCategory J
⊢ autoParam (∀ (F_1 : J ⥤ StructuredArrow X F), HasLimit F_1) _auto✝
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
x : J
⊢ lift F hc s ≫ NatTrans.app (F.mapCone c).π x = NatTrans.app s.π x
[PROOFSTEP]
simp [lift, ← Functor.map_comp]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
⊢ f₁ = f₂
[PROOFSTEP]
let α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun X => eqToHom (by simp [← h₁])
    naturality := fun j₁ j₂ φ =>
      by
      ext
        -- porting note: Lean 3 proof was `simp` but `Comma.eqToHom_right`
                -- isn't firing for some reason
                -- Asked here https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20not.20using.20a.20simp.20lemma/near/353943416
                -- I'm now doing `simp, rw [Comma.eqToHom_right, Comma.eqToHom_right], simp` but
                -- I squeezed the first `simp`.
      simp only [Functor.mapCone_pt, Functor.comp_obj, Cone.toStructuredArrow_obj, Functor.mapCone_π_app, map_mk,
        mk_right, Functor.comp_map, Cone.toStructuredArrow_map, comp_right, map_map_right, homMk_right]
      rw [Comma.eqToHom_right, Comma.eqToHom_right]
        -- this is a `simp` lemma
      simp }
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
X : J
⊢ (Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁).obj X = (Cone.toStructuredArrow s).obj X
[PROOFSTEP]
simp [← h₁]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
j₁ j₂ : J
φ : j₁ ⟶ j₂
⊢ (Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁).map φ ≫
      (fun X =>
          eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X)))
        j₂ =
    (fun X =>
          eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X)))
        j₁ ≫
      (Cone.toStructuredArrow s).map φ
[PROOFSTEP]
ext
  -- porting note: Lean 3 proof was `simp` but `Comma.eqToHom_right`
          -- isn't firing for some reason
          -- Asked here https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20not.20using.20a.20simp.20lemma/near/353943416
          -- I'm now doing `simp, rw [Comma.eqToHom_right, Comma.eqToHom_right], simp` but
          -- I squeezed the first `simp`.
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
j₁ j₂ : J
φ : j₁ ⟶ j₂
⊢ ((Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁).map φ ≫
        (fun X =>
            eqToHom
              (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X)))
          j₂).right =
    ((fun X =>
            eqToHom
              (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X)))
          j₁ ≫
        (Cone.toStructuredArrow s).map φ).right
[PROOFSTEP]
simp only [Functor.mapCone_pt, Functor.comp_obj, Cone.toStructuredArrow_obj, Functor.mapCone_π_app, map_mk, mk_right,
  Functor.comp_map, Cone.toStructuredArrow_map, comp_right, map_map_right, homMk_right]
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
j₁ j₂ : J
φ : j₁ ⟶ j₂
⊢ φ ≫
      (eqToHom
          (_ :
            StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π j₂)) = StructuredArrow.mk (NatTrans.app s.π j₂))).right =
    (eqToHom
          (_ :
            StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π j₁)) = StructuredArrow.mk (NatTrans.app s.π j₁))).right ≫
      φ
[PROOFSTEP]
rw [Comma.eqToHom_right, Comma.eqToHom_right]
  -- this is a `simp` lemma
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
j₁ j₂ : J
φ : j₁ ⟶ j₂
⊢ φ ≫
      eqToHom
        (_ :
          (StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π j₂))).right =
            (StructuredArrow.mk (NatTrans.app s.π j₂)).right) =
    eqToHom
        (_ :
          (StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π j₁))).right =
            (StructuredArrow.mk (NatTrans.app s.π j₁)).right) ≫
      φ
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
⊢ f₁ = f₂
[PROOFSTEP]
let α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun X => eqToHom (by simp [← h₂])
    naturality := fun _ _ _ =>
      by
      ext
        -- porting note: see comments above. `simp` should close this goal (and did in Lean 3)
      simp only [Functor.mapCone_pt, Functor.comp_obj, Cone.toStructuredArrow_obj, Functor.mapCone_π_app, map_mk,
        mk_right, Functor.comp_map, Cone.toStructuredArrow_map, comp_right, map_map_right, homMk_right]
      rw [Comma.eqToHom_right, Comma.eqToHom_right]
        -- this is a `simp` lemma
      simp }
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
X : J
⊢ (Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂).obj X = (Cone.toStructuredArrow s).obj X
[PROOFSTEP]
simp [← h₂]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ (Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂).map x✝ ≫
      (fun X =>
          eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X)))
        x✝¹ =
    (fun X =>
          eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X)))
        x✝² ≫
      (Cone.toStructuredArrow s).map x✝
[PROOFSTEP]
ext
  -- porting note: see comments above. `simp` should close this goal (and did in Lean 3)
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ ((Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂).map x✝ ≫
        (fun X =>
            eqToHom
              (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X)))
          x✝¹).right =
    ((fun X =>
            eqToHom
              (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X)))
          x✝² ≫
        (Cone.toStructuredArrow s).map x✝).right
[PROOFSTEP]
simp only [Functor.mapCone_pt, Functor.comp_obj, Cone.toStructuredArrow_obj, Functor.mapCone_π_app, map_mk, mk_right,
  Functor.comp_map, Cone.toStructuredArrow_map, comp_right, map_map_right, homMk_right]
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ x✝ ≫
      (eqToHom
          (_ :
            StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π x✝¹)) = StructuredArrow.mk (NatTrans.app s.π x✝¹))).right =
    (eqToHom
          (_ :
            StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π x✝²)) = StructuredArrow.mk (NatTrans.app s.π x✝²))).right ≫
      x✝
[PROOFSTEP]
rw [Comma.eqToHom_right, Comma.eqToHom_right]
  -- this is a `simp` lemma
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ x✝ ≫
      eqToHom
        (_ :
          (StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π x✝¹))).right =
            (StructuredArrow.mk (NatTrans.app s.π x✝¹)).right) =
    eqToHom
        (_ :
          (StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π x✝²))).right =
            (StructuredArrow.mk (NatTrans.app s.π x✝²)).right) ≫
      x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
⊢ f₁ = f₂
[PROOFSTEP]
let c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F) : _)).obj (c.toStructuredArrowCone F f₁)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
⊢ f₁ = f₂
[PROOFSTEP]
let c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F) : _)).obj
    (c.toStructuredArrowCone F f₂)
      -- The two cones can then be combined and we may obtain a cone over the two cones since
        -- `StructuredArrow s.pt F` is cofiltered.
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
⊢ f₁ = f₂
[PROOFSTEP]
let c₀ := IsCofiltered.cone (biconeMk _ c₁ c₂)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
⊢ f₁ = f₂
[PROOFSTEP]
let g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
⊢ f₁ = f₂
[PROOFSTEP]
let g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
⊢ f₁ = f₂
[PROOFSTEP]
have : ∀ j : J, g₁.right ≫ c.π.app j = g₂.right ≫ c.π.app j :=
  by
  intro j
  injection c₀.π.naturality (BiconeHom.left j) with _ e₁
  injection c₀.π.naturality (BiconeHom.right j) with _ e₂
  have e₃ := e₁.symm.trans e₂
  simp (config := { zeta := false }) at e₃ 
  rw [Comma.eqToHom_right, Comma.eqToHom_right] at e₃ 
  simpa (config := { zeta := false }) using e₃
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
⊢ ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
[PROOFSTEP]
intro j
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
j : J
⊢ g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
[PROOFSTEP]
injection c₀.π.naturality (BiconeHom.left j) with _ e₁
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
j : J
left_eq✝ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.left j)).left ≫ (NatTrans.app c₀.π (Bicone.diagram j)).left =
    (NatTrans.app c₀.π Bicone.left).left ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).left
e₁ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.left j)).right ≫ (NatTrans.app c₀.π (Bicone.diagram j)).right =
    (NatTrans.app c₀.π Bicone.left).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right
⊢ g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
[PROOFSTEP]
injection c₀.π.naturality (BiconeHom.right j) with _ e₂
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
j : J
left_eq✝¹ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.left j)).left ≫ (NatTrans.app c₀.π (Bicone.diagram j)).left =
    (NatTrans.app c₀.π Bicone.left).left ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).left
e₁ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.left j)).right ≫ (NatTrans.app c₀.π (Bicone.diagram j)).right =
    (NatTrans.app c₀.π Bicone.left).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right
left_eq✝ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.right j)).left ≫ (NatTrans.app c₀.π (Bicone.diagram j)).left =
    (NatTrans.app c₀.π Bicone.right).left ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).left
e₂ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.right j)).right ≫
      (NatTrans.app c₀.π (Bicone.diagram j)).right =
    (NatTrans.app c₀.π Bicone.right).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).right
⊢ g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
[PROOFSTEP]
have e₃ := e₁.symm.trans e₂
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
j : J
left_eq✝¹ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.left j)).left ≫ (NatTrans.app c₀.π (Bicone.diagram j)).left =
    (NatTrans.app c₀.π Bicone.left).left ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).left
e₁ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.left j)).right ≫ (NatTrans.app c₀.π (Bicone.diagram j)).right =
    (NatTrans.app c₀.π Bicone.left).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right
left_eq✝ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.right j)).left ≫ (NatTrans.app c₀.π (Bicone.diagram j)).left =
    (NatTrans.app c₀.π Bicone.right).left ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).left
e₂ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.right j)).right ≫
      (NatTrans.app c₀.π (Bicone.diagram j)).right =
    (NatTrans.app c₀.π Bicone.right).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).right
e₃ :
  (NatTrans.app c₀.π Bicone.left).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right =
    (NatTrans.app c₀.π Bicone.right).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).right
⊢ g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
[PROOFSTEP]
simp (config := { zeta := false }) at e₃ 
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
j : J
left_eq✝¹ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.left j)).left ≫ (NatTrans.app c₀.π (Bicone.diagram j)).left =
    (NatTrans.app c₀.π Bicone.left).left ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).left
e₁ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.left j)).right ≫ (NatTrans.app c₀.π (Bicone.diagram j)).right =
    (NatTrans.app c₀.π Bicone.left).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right
left_eq✝ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.right j)).left ≫ (NatTrans.app c₀.π (Bicone.diagram j)).left =
    (NatTrans.app c₀.π Bicone.right).left ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).left
e₂ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.right j)).right ≫
      (NatTrans.app c₀.π (Bicone.diagram j)).right =
    (NatTrans.app c₀.π Bicone.right).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).right
e₃ :
  (NatTrans.app c₀.π Bicone.left).right ≫
      NatTrans.app c.π j ≫
        (eqToHom
            (_ :
              (pre s.pt K F).obj (StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π j))) =
                (pre s.pt K F).obj (StructuredArrow.mk (NatTrans.app s.π j)))).right =
    (NatTrans.app c₀.π Bicone.right).right ≫
      NatTrans.app c.π j ≫
        (eqToHom
            (_ :
              (pre s.pt K F).obj (StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π j))) =
                (pre s.pt K F).obj (StructuredArrow.mk (NatTrans.app s.π j)))).right
⊢ g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
[PROOFSTEP]
rw [Comma.eqToHom_right, Comma.eqToHom_right] at e₃ 
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
j : J
left_eq✝¹ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.left j)).left ≫ (NatTrans.app c₀.π (Bicone.diagram j)).left =
    (NatTrans.app c₀.π Bicone.left).left ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).left
e₁ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.left j)).right ≫ (NatTrans.app c₀.π (Bicone.diagram j)).right =
    (NatTrans.app c₀.π Bicone.left).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right
left_eq✝ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.right j)).left ≫ (NatTrans.app c₀.π (Bicone.diagram j)).left =
    (NatTrans.app c₀.π Bicone.right).left ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).left
e₂ :
  (((Functor.const (Bicone J)).obj c₀.pt).map (BiconeHom.right j)).right ≫
      (NatTrans.app c₀.π (Bicone.diagram j)).right =
    (NatTrans.app c₀.π Bicone.right).right ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).right
e₃ :
  (NatTrans.app c₀.π Bicone.left).right ≫
      NatTrans.app c.π j ≫
        eqToHom
          (_ :
            ((pre s.pt K F).obj (StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π j)))).right =
              ((pre s.pt K F).obj (StructuredArrow.mk (NatTrans.app s.π j))).right) =
    (NatTrans.app c₀.π Bicone.right).right ≫
      NatTrans.app c.π j ≫
        eqToHom
          (_ :
            ((pre s.pt K F).obj (StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π j)))).right =
              ((pre s.pt K F).obj (StructuredArrow.mk (NatTrans.app s.π j))).right)
⊢ g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
[PROOFSTEP]
simpa (config := { zeta := false }) using e₃
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
⊢ f₁ = f₂
[PROOFSTEP]
have : c.extend g₁.right = c.extend g₂.right := by
  unfold Cone.extend
  congr 1
  ext x
  apply this
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
⊢ Cone.extend c g₁.right = Cone.extend c g₂.right
[PROOFSTEP]
unfold Cone.extend
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
⊢ { pt := c₀.pt.right, π := NatTrans.app (Cone.extensions c) (op c₀.pt.right) { down := g₁.right } } =
    { pt := c₀.pt.right, π := NatTrans.app (Cone.extensions c) (op c₀.pt.right) { down := g₂.right } }
[PROOFSTEP]
congr 1
[GOAL]
case e_π
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
⊢ NatTrans.app (Cone.extensions c) (op c₀.pt.right) { down := g₁.right } =
    NatTrans.app (Cone.extensions c) (op c₀.pt.right) { down := g₂.right }
[PROOFSTEP]
ext x
[GOAL]
case e_π.w.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
x : J
⊢ NatTrans.app (NatTrans.app (Cone.extensions c) (op c₀.pt.right) { down := g₁.right }) x =
    NatTrans.app (NatTrans.app (Cone.extensions c) (op c₀.pt.right) { down := g₂.right }) x
[PROOFSTEP]
apply this
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this : Cone.extend c g₁.right = Cone.extend c g₂.right
⊢ f₁ = f₂
[PROOFSTEP]
have : g₁.right = g₂.right
[GOAL]
case this
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this : Cone.extend c g₁.right = Cone.extend c g₂.right
⊢ g₁.right = g₂.right
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝¹ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this✝ : Cone.extend c g₁.right = Cone.extend c g₂.right
this : g₁.right = g₂.right
⊢ f₁ = f₂
[PROOFSTEP]
calc
  g₁.right = hc.lift (c.extend g₁.right) :=
    by
    apply
      hc.uniq
        (c.extend _)
          -- Porting note: was `by tidy`, but `aesop` only works if max heartbeats
                -- is increased, so we replace it by the output of `tidy?`
    intro j; rfl
  _ = hc.lift (c.extend g₂.right) := by congr
  _ = g₂.right := by
    symm
    apply
      hc.uniq
        (c.extend _)
          -- Porting note: was `by tidy`, but `aesop` only works if max heartbeats
                -- is increased, so we replace it by the output of `tidy?`
    intro _;
    rfl
      -- Finally, since `fᵢ` factors through `F(gᵢ)`, the result follows.
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this : Cone.extend c g₁.right = Cone.extend c g₂.right
⊢ g₁.right = IsLimit.lift hc (Cone.extend c g₁.right)
[PROOFSTEP]
apply
  hc.uniq
    (c.extend _)
      -- Porting note: was `by tidy`, but `aesop` only works if max heartbeats
            -- is increased, so we replace it by the output of `tidy?`
[GOAL]
case x
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this : Cone.extend c g₁.right = Cone.extend c g₂.right
⊢ ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = NatTrans.app (Cone.extend c g₁.right).π j
[PROOFSTEP]
intro j
[GOAL]
case x
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this : Cone.extend c g₁.right = Cone.extend c g₂.right
j : J
⊢ g₁.right ≫ NatTrans.app c.π j = NatTrans.app (Cone.extend c g₁.right).π j
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this : Cone.extend c g₁.right = Cone.extend c g₂.right
⊢ IsLimit.lift hc (Cone.extend c g₁.right) = IsLimit.lift hc (Cone.extend c g₂.right)
[PROOFSTEP]
congr
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this : Cone.extend c g₁.right = Cone.extend c g₂.right
⊢ IsLimit.lift hc (Cone.extend c g₂.right) = g₂.right
[PROOFSTEP]
symm
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this : Cone.extend c g₁.right = Cone.extend c g₂.right
⊢ g₂.right = IsLimit.lift hc (Cone.extend c g₂.right)
[PROOFSTEP]
apply
  hc.uniq
    (c.extend _)
      -- Porting note: was `by tidy`, but `aesop` only works if max heartbeats
            -- is increased, so we replace it by the output of `tidy?`
[GOAL]
case x
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this : Cone.extend c g₁.right = Cone.extend c g₂.right
⊢ ∀ (j : J), g₂.right ≫ NatTrans.app c.π j = NatTrans.app (Cone.extend c g₂.right).π j
[PROOFSTEP]
intro _
[GOAL]
case x
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this : Cone.extend c g₁.right = Cone.extend c g₂.right
j✝ : J
⊢ g₂.right ≫ NatTrans.app c.π j✝ = NatTrans.app (Cone.extend c g₂.right).π j✝
[PROOFSTEP]
rfl
  -- Finally, since `fᵢ` factors through `F(gᵢ)`, the result follows.
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝¹ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this✝ : Cone.extend c g₁.right = Cone.extend c g₂.right
this : g₁.right = g₂.right
⊢ f₁ = f₂
[PROOFSTEP]
calc
  f₁ = 𝟙 _ ≫ f₁ := by simp
  _ = c₀.pt.hom ≫ F.map g₁.right := g₁.w
  _ = c₀.pt.hom ≫ F.map g₂.right := by rw [this]
  _ = 𝟙 _ ≫ f₂ := g₂.w.symm
  _ = f₂ := by simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝¹ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this✝ : Cone.extend c g₁.right = Cone.extend c g₂.right
this : g₁.right = g₂.right
⊢ f₁ = 𝟙 s.pt ≫ f₁
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝¹ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this✝ : Cone.extend c g₁.right = Cone.extend c g₂.right
this : g₁.right = g₂.right
⊢ c₀.pt.hom ≫ F.map g₁.right = c₀.pt.hom ≫ F.map g₂.right
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K✝ : J ⥤ C
F : C ⥤ D
inst✝ : RepresentablyFlat F
c✝ : Cone K✝
hc✝ : IsLimit c✝
s✝ : Cone (K✝ ⋙ F)
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
h₂ : ∀ (j : J), f₂ ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
α₁ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₁ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₁ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
α₂ : Cone.toStructuredArrow (F.mapCone c) ⋙ map f₂ ⟶ Cone.toStructuredArrow s :=
  NatTrans.mk fun X =>
    eqToHom (_ : StructuredArrow.mk (f₂ ≫ F.map (NatTrans.app c.π X)) = StructuredArrow.mk (NatTrans.app s.π X))
c₁ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₁)
c₂ : Cone (Cone.toStructuredArrow s ⋙ pre s.pt K F) :=
  (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (Cone.toStructuredArrowCone c F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := NatTrans.app c₀.π Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := NatTrans.app c₀.π Bicone.right
this✝¹ : ∀ (j : J), g₁.right ≫ NatTrans.app c.π j = g₂.right ≫ NatTrans.app c.π j
this✝ : Cone.extend c g₁.right = Cone.extend c g₂.right
this : g₁.right = g₂.right
⊢ 𝟙 s.pt ≫ f₂ = f₂
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
⊢ PreservesFiniteLimits F
[PROOFSTEP]
apply preservesFiniteLimitsOfPreservesFiniteLimitsOfSize
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
⊢ (J : Type ?u.100310) → {𝒥 : SmallCategory J} → FinCategory J → PreservesLimitsOfShape J F
[PROOFSTEP]
intro J _ _
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.100310
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
constructor
[GOAL]
case h.preservesLimit
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.100310
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ autoParam ({K : J ⥤ C} → PreservesLimit K F) _auto✝
[PROOFSTEP]
intro K
[GOAL]
case h.preservesLimit
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.100310
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
⊢ PreservesLimit K F
[PROOFSTEP]
constructor
[GOAL]
case h.preservesLimit.preserves
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.100310
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
⊢ {c : Cone K} → IsLimit c → IsLimit (F.mapCone c)
[PROOFSTEP]
intro c hc
[GOAL]
case h.preservesLimit.preserves
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.100310
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ IsLimit (F.mapCone c)
[PROOFSTEP]
exact
  { lift := PreservesFiniteLimitsOfFlat.lift F hc
    fac := PreservesFiniteLimitsOfFlat.fac F hc
    uniq := fun s m h => by
      apply PreservesFiniteLimitsOfFlat.uniq F hc
      exact h
      exact PreservesFiniteLimitsOfFlat.fac F hc s }
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
⊢ m = PreservesFiniteLimitsOfFlat.lift F hc s
[PROOFSTEP]
apply PreservesFiniteLimitsOfFlat.uniq F hc
[GOAL]
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
⊢ ∀ (j : J), m ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
⊢ ∀ (j : J), PreservesFiniteLimitsOfFlat.lift F hc s ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
[PROOFSTEP]
exact h
[GOAL]
case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
⊢ ∀ (j : J), PreservesFiniteLimitsOfFlat.lift F hc s ≫ NatTrans.app (F.mapCone c).π j = NatTrans.app s.π j
[PROOFSTEP]
exact PreservesFiniteLimitsOfFlat.fac F hc s
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
inst✝ : HasFiniteLimits C
F : C ⥤ D
x : PreservesFiniteLimits F
⊢ (fun x => preservesFiniteLimitsOfFlat F) (_ : RepresentablyFlat F) = x
[PROOFSTEP]
cases x
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
inst✝ : HasFiniteLimits C
F : C ⥤ D
preservesFiniteLimits✝ : (J : Type) → [inst : SmallCategory J] → [inst_1 : FinCategory J] → PreservesLimitsOfShape J F
⊢ (fun x => preservesFiniteLimitsOfFlat F) (_ : RepresentablyFlat F) = PreservesFiniteLimits.mk
[PROOFSTEP]
unfold preservesFiniteLimitsOfFlat
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
inst✝ : HasFiniteLimits C
F : C ⥤ D
preservesFiniteLimits✝ : (J : Type) → [inst : SmallCategory J] → [inst_1 : FinCategory J] → PreservesLimitsOfShape J F
⊢ (fun x => preservesFiniteLimitsOfPreservesFiniteLimitsOfSize F fun J {𝒥} x_1 => PreservesLimitsOfShape.mk)
      (_ : RepresentablyFlat F) =
    PreservesFiniteLimits.mk
[PROOFSTEP]
dsimp only [preservesFiniteLimitsOfPreservesFiniteLimitsOfSize]
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
inst✝ : HasFiniteLimits C
F : C ⥤ D
preservesFiniteLimits✝ : (J : Type) → [inst : SmallCategory J] → [inst_1 : FinCategory J] → PreservesLimitsOfShape J F
⊢ PreservesFiniteLimits.mk = PreservesFiniteLimits.mk
[PROOFSTEP]
congr
  -- porting note: this next line wasn't needed in lean 3
[GOAL]
case mk.e_preservesFiniteLimits
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
inst✝ : HasFiniteLimits C
F : C ⥤ D
preservesFiniteLimits✝ : (J : Type) → [inst : SmallCategory J] → [inst_1 : FinCategory J] → PreservesLimitsOfShape J F
⊢ (fun J x x_1 => preservesLimitsOfShapeOfEquiv (Equivalence.symm (ULiftHomULiftCategory.equiv J)) F) =
    preservesFiniteLimits✝
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
⊢ ∀ {X_1 Y : C ⥤ E} (f : X_1 ⟶ Y),
    (lan F ⋙ (evaluation D E).obj X).map f ≫ ((fun G => colim.mapIso (Iso.refl (Lan.diagram F G X))) Y).hom =
      ((fun G => colim.mapIso (Iso.refl (Lan.diagram F G X))) X_1).hom ≫
        ((whiskeringLeft (CostructuredArrow F X) C E).obj (CostructuredArrow.proj F X) ⋙ colim).map f
[PROOFSTEP]
intro G H i
[GOAL]
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G H : C ⥤ E
i : G ⟶ H
⊢ (lan F ⋙ (evaluation D E).obj X).map i ≫ ((fun G => colim.mapIso (Iso.refl (Lan.diagram F G X))) H).hom =
    ((fun G => colim.mapIso (Iso.refl (Lan.diagram F G X))) G).hom ≫
      ((whiskeringLeft (CostructuredArrow F X) C E).obj (CostructuredArrow.proj F X) ⋙ colim).map i
[PROOFSTEP]
apply colimit.hom_ext
[GOAL]
case w
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G H : C ⥤ E
i : G ⟶ H
⊢ ∀ (j : CostructuredArrow F X),
    colimit.ι (Lan.diagram F G X) j ≫
        (lan F ⋙ (evaluation D E).obj X).map i ≫ ((fun G => colim.mapIso (Iso.refl (Lan.diagram F G X))) H).hom =
      colimit.ι (Lan.diagram F G X) j ≫
        ((fun G => colim.mapIso (Iso.refl (Lan.diagram F G X))) G).hom ≫
          ((whiskeringLeft (CostructuredArrow F X) C E).obj (CostructuredArrow.proj F X) ⋙ colim).map i
[PROOFSTEP]
intro j
[GOAL]
case w
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G H : C ⥤ E
i : G ⟶ H
j : CostructuredArrow F X
⊢ colimit.ι (Lan.diagram F G X) j ≫
      (lan F ⋙ (evaluation D E).obj X).map i ≫ ((fun G => colim.mapIso (Iso.refl (Lan.diagram F G X))) H).hom =
    colimit.ι (Lan.diagram F G X) j ≫
      ((fun G => colim.mapIso (Iso.refl (Lan.diagram F G X))) G).hom ≫
        ((whiskeringLeft (CostructuredArrow F X) C E).obj (CostructuredArrow.proj F X) ⋙ colim).map i
[PROOFSTEP]
simp only [Functor.comp_map, Functor.mapIso_refl, evaluation_obj_map, whiskeringLeft_obj_map, lan_map_app,
  colimit.ι_desc_assoc, Category.comp_id, Category.assoc]
  -- porting note: this deals with the fact that the type of `lan_map_app` has changed
        -- See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/change.20in.20behaviour.20with.20.60simps.60/near/354350606
[GOAL]
case w
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G H : C ⥤ E
i : G ⟶ H
j : CostructuredArrow F X
⊢ NatTrans.app i j.left ≫
      NatTrans.app (↑(Lan.equiv F H (Lan.loc F H)) (𝟙 (Lan.loc F H))) j.left ≫
        colimit.pre (Lan.diagram F H X) (CostructuredArrow.map j.hom) ≫ (Iso.refl (colim.obj (Lan.diagram F H X))).hom =
    colimit.ι (Lan.diagram F G X) j ≫
      (Iso.refl (colim.obj (Lan.diagram F G X))).hom ≫ colim.map (whiskerLeft (CostructuredArrow.proj F X) i)
[PROOFSTEP]
erw [show
    ((Lan.equiv F H (Lan.loc F H)) (𝟙 (Lan.loc F H))).app j.left =
      colimit.ι (Lan.diagram F H (F.obj j.left)) (CostructuredArrow.mk (𝟙 (F.obj j.left)))
    by apply Category.comp_id]
[GOAL]
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G H : C ⥤ E
i : G ⟶ H
j : CostructuredArrow F X
⊢ NatTrans.app (↑(Lan.equiv F H (Lan.loc F H)) (𝟙 (Lan.loc F H))) j.left =
    colimit.ι (Lan.diagram F H (F.obj j.left)) (CostructuredArrow.mk (𝟙 (F.obj j.left)))
[PROOFSTEP]
apply Category.comp_id
[GOAL]
case w
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G H : C ⥤ E
i : G ⟶ H
j : CostructuredArrow F X
⊢ NatTrans.app i j.left ≫
      colimit.ι (Lan.diagram F H (F.obj j.left)) (CostructuredArrow.mk (𝟙 (F.obj j.left))) ≫
        colimit.pre (Lan.diagram F H X) (CostructuredArrow.map j.hom) ≫ (Iso.refl (colim.obj (Lan.diagram F H X))).hom =
    colimit.ι (Lan.diagram F G X) j ≫
      (Iso.refl (colim.obj (Lan.diagram F G X))).hom ≫ colim.map (whiskerLeft (CostructuredArrow.proj F X) i)
[PROOFSTEP]
erw [colimit.ι_pre_assoc (Lan.diagram F H X) (CostructuredArrow.map j.hom), Category.id_comp, Category.comp_id,
  colimit.ι_map]
[GOAL]
case w
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G H : C ⥤ E
i : G ⟶ H
j : CostructuredArrow F X
⊢ NatTrans.app i j.left ≫
      colimit.ι (Lan.diagram F H X) ((CostructuredArrow.map j.hom).obj (CostructuredArrow.mk (𝟙 (F.obj j.left)))) =
    NatTrans.app (whiskerLeft (CostructuredArrow.proj F X) i) j ≫
      colimit.ι (((whiskeringLeft (CostructuredArrow F X) C E).obj (CostructuredArrow.proj F X)).obj H) j
[PROOFSTEP]
rcases j with ⟨j_left, ⟨⟨⟩⟩, j_hom⟩
[GOAL]
case w.mk.mk.unit
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G H : C ⥤ E
i : G ⟶ H
j_left : C
j_hom : F.obj j_left ⟶ (Functor.fromPUnit X).obj { as := PUnit.unit }
⊢ NatTrans.app i { left := j_left, right := { as := PUnit.unit }, hom := j_hom }.left ≫
      colimit.ι (Lan.diagram F H X)
        ((CostructuredArrow.map { left := j_left, right := { as := PUnit.unit }, hom := j_hom }.hom).obj
          (CostructuredArrow.mk (𝟙 (F.obj { left := j_left, right := { as := PUnit.unit }, hom := j_hom }.left)))) =
    NatTrans.app (whiskerLeft (CostructuredArrow.proj F X) i)
        { left := j_left, right := { as := PUnit.unit }, hom := j_hom } ≫
      colimit.ι (((whiskeringLeft (CostructuredArrow F X) C E).obj (CostructuredArrow.proj F X)).obj H)
        { left := j_left, right := { as := PUnit.unit }, hom := j_hom }
[PROOFSTEP]
congr
[GOAL]
case w.mk.mk.unit.e_a.h.e_7.h
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G H : C ⥤ E
i : G ⟶ H
j_left : C
j_hom : F.obj j_left ⟶ (Functor.fromPUnit X).obj { as := PUnit.unit }
⊢ (CostructuredArrow.map { left := j_left, right := { as := PUnit.unit }, hom := j_hom }.hom).obj
      (CostructuredArrow.mk (𝟙 (F.obj { left := j_left, right := { as := PUnit.unit }, hom := j_hom }.left))) =
    { left := j_left, right := { as := PUnit.unit }, hom := j_hom }
[PROOFSTEP]
rw [CostructuredArrow.map_mk, Category.id_comp, CostructuredArrow.mk]
[GOAL]
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
F : C ⥤ D
inst✝ : RepresentablyFlat F
⊢ PreservesFiniteLimits (lan F.op)
[PROOFSTEP]
apply preservesFiniteLimitsOfPreservesFiniteLimitsOfSize.{u₁}
[GOAL]
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
F : C ⥤ D
inst✝ : RepresentablyFlat F
⊢ (J : Type u₁) → {𝒥 : SmallCategory J} → FinCategory J → PreservesLimitsOfShape J (lan F.op)
[PROOFSTEP]
intro J _ _
[GOAL]
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type u₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J (lan F.op)
[PROOFSTEP]
skip
[GOAL]
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type u₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J (lan F.op)
[PROOFSTEP]
apply preservesLimitsOfShapeOfEvaluation (lan F.op : (Cᵒᵖ ⥤ E) ⥤ Dᵒᵖ ⥤ E) J
[GOAL]
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type u₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ (k : Dᵒᵖ) → PreservesLimitsOfShape J (lan F.op ⋙ (evaluation Dᵒᵖ E).obj k)
[PROOFSTEP]
intro K
[GOAL]
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type u₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : Dᵒᵖ
⊢ PreservesLimitsOfShape J (lan F.op ⋙ (evaluation Dᵒᵖ E).obj K)
[PROOFSTEP]
haveI : IsFiltered (CostructuredArrow F.op K) := IsFiltered.of_equivalence (structuredArrowOpEquivalence F (unop K))
[GOAL]
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type u₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : Dᵒᵖ
this : IsFiltered (CostructuredArrow F.op K)
⊢ PreservesLimitsOfShape J (lan F.op ⋙ (evaluation Dᵒᵖ E).obj K)
[PROOFSTEP]
exact preservesLimitsOfShapeOfNatIso (lanEvaluationIsoColim _ _ _).symm
[GOAL]
C D : Type u₁
inst✝¹⁰ : SmallCategory C
inst✝⁹ : SmallCategory D
E : Type u₂
inst✝⁸ : Category.{u₁, u₂} E
inst✝⁷ : ConcreteCategory E
inst✝⁶ : HasLimits E
inst✝⁵ : HasColimits E
inst✝⁴ : ReflectsLimits (forget E)
inst✝³ : PreservesFilteredColimits (forget E)
inst✝² : PreservesLimits (forget E)
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
⊢ PreservesFiniteLimits (lan F.op)
[PROOFSTEP]
haveI := flat_of_preservesFiniteLimits F
[GOAL]
C D : Type u₁
inst✝¹⁰ : SmallCategory C
inst✝⁹ : SmallCategory D
E : Type u₂
inst✝⁸ : Category.{u₁, u₂} E
inst✝⁷ : ConcreteCategory E
inst✝⁶ : HasLimits E
inst✝⁵ : HasColimits E
inst✝⁴ : ReflectsLimits (forget E)
inst✝³ : PreservesFilteredColimits (forget E)
inst✝² : PreservesLimits (forget E)
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
this : RepresentablyFlat F
⊢ PreservesFiniteLimits (lan F.op)
[PROOFSTEP]
infer_instance
[GOAL]
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan F.op)
⊢ RepresentablyFlat F
[PROOFSTEP]
skip
[GOAL]
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan F.op)
⊢ RepresentablyFlat F
[PROOFSTEP]
haveI := preservesFiniteLimitsOfFlat (lan F.op : _ ⥤ Dᵒᵖ ⥤ Type u₁)
[GOAL]
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan F.op)
this : PreservesFiniteLimits (lan F.op)
⊢ RepresentablyFlat F
[PROOFSTEP]
haveI : PreservesFiniteLimits F :=
  by
  apply preservesFiniteLimitsOfPreservesFiniteLimitsOfSize.{u₁}
  intros; skip; apply preservesLimitOfLanPreservesLimit
[GOAL]
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan F.op)
this : PreservesFiniteLimits (lan F.op)
⊢ PreservesFiniteLimits F
[PROOFSTEP]
apply preservesFiniteLimitsOfPreservesFiniteLimitsOfSize.{u₁}
[GOAL]
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan F.op)
this : PreservesFiniteLimits (lan F.op)
⊢ (J : Type u₁) → {𝒥 : SmallCategory J} → FinCategory J → PreservesLimitsOfShape J F
[PROOFSTEP]
intros
[GOAL]
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan F.op)
this : PreservesFiniteLimits (lan F.op)
J✝ : Type u₁
𝒥✝ : SmallCategory J✝
x✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ F
[PROOFSTEP]
skip
[GOAL]
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan F.op)
this : PreservesFiniteLimits (lan F.op)
J✝ : Type u₁
𝒥✝ : SmallCategory J✝
x✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ F
[PROOFSTEP]
apply preservesLimitOfLanPreservesLimit
[GOAL]
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan F.op)
this✝ : PreservesFiniteLimits (lan F.op)
this : PreservesFiniteLimits F
⊢ RepresentablyFlat F
[PROOFSTEP]
apply flat_of_preservesFiniteLimits
[GOAL]
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
x✝ : PreservesFiniteLimits (lan F.op)
⊢ PreservesFiniteLimits F
[PROOFSTEP]
apply preservesFiniteLimitsOfPreservesFiniteLimitsOfSize.{u₁}
[GOAL]
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
x✝ : PreservesFiniteLimits (lan F.op)
⊢ (J : Type u₁) → {𝒥 : SmallCategory J} → FinCategory J → PreservesLimitsOfShape J F
[PROOFSTEP]
intros
[GOAL]
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
x✝¹ : PreservesFiniteLimits (lan F.op)
J✝ : Type u₁
𝒥✝ : SmallCategory J✝
x✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ F
[PROOFSTEP]
apply preservesLimitOfLanPreservesLimit
[GOAL]
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
x : PreservesFiniteLimits F
⊢ (fun x => preservesFiniteLimitsOfPreservesFiniteLimitsOfSize F fun J {𝒥} x_1 => preservesLimitOfLanPreservesLimit F J)
      ((fun x => inferInstance) x) =
    x
[PROOFSTEP]
dsimp only [preservesFiniteLimitsOfPreservesFiniteLimitsOfSize]
[GOAL]
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
x : PreservesFiniteLimits F
⊢ PreservesFiniteLimits.mk = x
[PROOFSTEP]
congr
  -- porting note: next line wasn't necessary in lean 3
[GOAL]
case e_preservesFiniteLimits
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
x : PreservesFiniteLimits F
⊢ (fun J x_1 x_2 => preservesLimitsOfShapeOfEquiv (Equivalence.symm (ULiftHomULiftCategory.equiv J)) F) =
    PreservesFiniteLimits.preservesFiniteLimits
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
x : PreservesFiniteLimits (lan F.op)
⊢ (fun x => inferInstance)
      ((fun x =>
          preservesFiniteLimitsOfPreservesFiniteLimitsOfSize F fun J {𝒥} x_1 => preservesLimitOfLanPreservesLimit F J)
        x) =
    x
[PROOFSTEP]
dsimp only [lanPreservesFiniteLimitsOfPreservesFiniteLimits, lanPreservesFiniteLimitsOfFlat,
  preservesFiniteLimitsOfPreservesFiniteLimitsOfSize]
[GOAL]
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
x : PreservesFiniteLimits (lan F.op)
⊢ inferInstance = x
[PROOFSTEP]
congr
  -- porting note: next line wasn't necessary in lean 3
[GOAL]
case h.e_2.h.h.e_2.h.e_preservesFiniteLimits
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category.{u₁, u₂} E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
x : PreservesFiniteLimits (lan F.op)
⊢ (fun J x_1 x_2 => preservesLimitsOfShapeOfEquiv (Equivalence.symm (ULiftHomULiftCategory.equiv J)) (lan F.op)) =
    PreservesFiniteLimits.preservesFiniteLimits
[PROOFSTEP]
apply Subsingleton.elim
