awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : J ⥤ Comma L R
inst_4 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
m : (coconeOfPreserves F t₁ c₂).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfPreserves F t₁ c₂).ι.app j ≫ m = s.ι.app j
j : J
⊢ c₂.ι.app j ≫ m.right = ((snd L R).mapCocone s).ι.app j

Tactic:
simp [← w]
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : J ⥤ Comma L R
inst_4 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
m : (coconeOfPreserves F t₁ c₂).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfPreserves F t₁ c₂).ι.app j ≫ m = s.ι.app j
⊢ m.right =
    CommaMorphism.right { left := t₁.desc ((fst L R).mapCocone s), right := t₂.desc ((snd L R).mapCocone s), w := ⋯ }

Tactic:
exact t₂.uniq ((snd L R).mapCocone s) _ (fun j => by simp [← w])

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Comma.snd
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F_1 F : J ⥤ Comma L R
inst_4 : HasLimit (F ⋙ fst L R)
inst_5 : HasLimit (F ⋙ snd L R)
inst_6 : PreservesLimit (F ⋙ snd L R) R
⊢ HasLimit F

Tactic:
HasLimit.mk ⟨_, coneOfPreservesIsLimit _ (limit.isLimit _) (limit.isLimit _)⟩

Premises used: CategoryTheory.Comma.coneOfPreservesIsLimit, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : J ⥤ Comma L R
inst_4 : HasLimitsOfSize.{w, w', v₁, u₁} A
inst_5 : HasLimitsOfSize.{w, w', v₂, u₂} B
inst_6 : PreservesLimitsOfSize.{w, w', v₂, v₃, u₂, u₃} R
⊢ HasLimitsOfSize.{w, w', max v₁ v₂, max (max u₂ u₁) v₃} (Comma L R)

Tactic:
⟨fun _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasLimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F_1 F : J ⥤ Comma L R
inst_4 : HasColimit (F ⋙ fst L R)
inst_5 : HasColimit (F ⋙ snd L R)
inst_6 : PreservesColimit (F ⋙ fst L R) L
⊢ HasColimit F

Tactic:
HasColimit.mk ⟨_, coconeOfPreservesIsColimit _ (colimit.isColimit _) (colimit.isColimit _)⟩

Premises used: CategoryTheory.Comma.coconeOfPreservesIsColimit, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : J ⥤ Comma L R
inst_4 : HasColimitsOfSize.{w, w', v₁, u₁} A
inst_5 : HasColimitsOfSize.{w, w', v₂, u₂} B
inst_6 : PreservesColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} L
⊢ HasColimitsOfSize.{w, w', max v₁ v₂, max (max u₂ u₁) v₃} (Comma L R)

Tactic:
⟨fun _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasColimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
F : J ⥤ Arrow.{v₃, u₃} T
i₁ : HasLimit (F ⋙ leftFunc)
i₂ : HasLimit (F ⋙ rightFunc)
⊢ HasLimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))

Tactic:
haveI : HasLimit (F ⋙ Comma.fst _ _) := i₁
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
F : J ⥤ Arrow.{v₃, u₃} T
i₁ : HasLimit (F ⋙ leftFunc)
i₂ : HasLimit (F ⋙ rightFunc)
this : HasLimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
⊢ HasLimit (F ⋙ Comma.snd (𝟭 T) (𝟭 T))

Tactic:
haveI : HasLimit (F ⋙ Comma.snd _ _) := i₂
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
F : J ⥤ Arrow.{v₃, u₃} T
i₁ : HasLimit (F ⋙ leftFunc)
i₂ : HasLimit (F ⋙ rightFunc)
this_1 : HasLimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
this : HasLimit (F ⋙ Comma.snd (𝟭 T) (𝟭 T))
⊢ HasLimit F

Tactic:
apply Comma.hasLimit

Premises used: CategoryTheory.Comma.hasLimit
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
inst_4 : HasLimits.{v₃, u₃} T
⊢ HasLimits (Arrow.{v₃, u₃} T)

Tactic:
⟨fun _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasLimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
F : J ⥤ Arrow.{v₃, u₃} T
i₁ : HasColimit (F ⋙ leftFunc)
i₂ : HasColimit (F ⋙ rightFunc)
⊢ HasColimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))

Tactic:
haveI : HasColimit (F ⋙ Comma.fst _ _) := i₁
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
F : J ⥤ Arrow.{v₃, u₃} T
i₁ : HasColimit (F ⋙ leftFunc)
i₂ : HasColimit (F ⋙ rightFunc)
this : HasColimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
⊢ HasColimit (F ⋙ Comma.snd (𝟭 T) (𝟭 T))

Tactic:
haveI : HasColimit (F ⋙ Comma.snd _ _) := i₂
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
F : J ⥤ Arrow.{v₃, u₃} T
i₁ : HasColimit (F ⋙ leftFunc)
i₂ : HasColimit (F ⋙ rightFunc)
this_1 : HasColimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
this : HasColimit (F ⋙ Comma.snd (𝟭 T) (𝟭 T))
⊢ HasColimit F

Tactic:
apply Comma.hasColimit

Premises used: CategoryTheory.Comma.hasColimit
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
inst_4 : HasColimits.{v₃, u₃} T
⊢ HasColimits (Arrow.{v₃, u₃} T)

Tactic:
⟨fun _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasColimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
inst_4 : HasColimitsOfShape.{w', w, v₃, u₃} J T
⊢ PreservesColimitsOfShape (C := Arrow.{v₃, u₃} T) J leftFunc

Tactic:
apply Comma.preservesColimitsOfShape_fst

Premises used: CategoryTheory.Comma.preservesColimitsOfShape_fst
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
inst_4 : HasColimitsOfShape.{w', w, v₃, u₃} J T
⊢ PreservesColimitsOfShape (C := Arrow.{v₃, u₃} T) J rightFunc

Tactic:
apply Comma.preservesColimitsOfShape_snd

Premises used: CategoryTheory.Comma.preservesColimitsOfShape_snd
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
X : T
G : Functor.{v₁, v₃, u₁, u₃} A T
F : J ⥤ StructuredArrow X G
inst_4 : G.Faithful
inst_5 : G.Full
Y : A
⊢ HasInitial (StructuredArrow (G.obj Y) G)

Tactic:
StructuredArrow.mkIdInitial.hasInitial

Premises used: CategoryTheory.StructuredArrow.mkIdInitial, CategoryTheory.Limits.IsInitial.hasInitial
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
X : T
G : Functor.{v₁, v₃, u₁, u₃} A T
F : J ⥤ StructuredArrow X G
i₁ : HasLimit (F ⋙ proj X G)
i₂ : PreservesLimit (F ⋙ proj X G) G
⊢ HasLimit (F ⋙ Comma.snd (fromPUnit X) G)

Tactic:
haveI : HasLimit (F ⋙ Comma.snd (Functor.fromPUnit X) G) := i₁
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
X : T
G : Functor.{v₁, v₃, u₁, u₃} A T
F : J ⥤ StructuredArrow X G
i₁ : HasLimit (F ⋙ proj X G)
i₂ : PreservesLimit (F ⋙ proj X G) G
this : HasLimit (F ⋙ Comma.snd (fromPUnit X) G)
⊢ PreservesLimit (F ⋙ Comma.snd (fromPUnit X) G) G

Tactic:
haveI : PreservesLimit (F ⋙ Comma.snd (Functor.fromPUnit X) G) _ := i₂
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
X : T
G : Functor.{v₁, v₃, u₁, u₃} A T
F : J ⥤ StructuredArrow X G
i₁ : HasLimit (F ⋙ proj X G)
i₂ : PreservesLimit (F ⋙ proj X G) G
this_1 : HasLimit (F ⋙ Comma.snd (fromPUnit X) G)
this : PreservesLimit (F ⋙ Comma.snd (fromPUnit X) G) G
⊢ HasLimit F

Tactic:
apply Comma.hasLimit

Premises used: CategoryTheory.Comma.hasLimit
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J_1 : Type w
inst : Category.{w', w} J_1
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
X : T
G : Functor.{v₁, v₃, u₁, u₃} A T
F : J_1 ⥤ StructuredArrow X G
inst_4 : HasLimitsOfSize.{w, w', v₁, u₁} A
inst_5 : PreservesLimitsOfSize.{w, w', v₁, v₃, u₁, u₃} G
J : Type w'
hJ : Category.{w, w'} J
⊢ HasLimitsOfShape J (StructuredArrow X G)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
X : T
G : Functor.{v₁, v₃, u₁, u₃} A T
F : J ⥤ StructuredArrow X G
inst_4 : HasPullbacks.{v₁, u₁} A
inst_5 : PreservesLimitsOfShape WalkingCospan G
Y Z : StructuredArrow X G
f : Y ⟶ Z
inst_6 : Mono f
⊢ Mono (Hom.right f)

Tactic:
show Mono ((proj X G).map f) from inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
T : Type u₃
inst_1 : Category.{v₃, u₃} T
X : T
G : Functor.{v₁, v₃, u₁, u₃} A T
inst_2 : HasPullbacks.{v₁, u₁} A
inst_3 : PreservesLimitsOfShape WalkingCospan G
Y Z : StructuredArrow X G
f : Y ⟶ Z
⊢ Mono f ↔ Mono (Hom.right f)

Tactic:
⟨fun _ => inferInstance, fun _ => mono_of_mono_right f⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.StructuredArrow.mono_of_mono_right
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
G : Functor.{v₁, v₃, u₁, u₃} A T
X : T
F : J ⥤ CostructuredArrow G X
inst_4 : G.Faithful
inst_5 : G.Full
Y : A
⊢ HasTerminal (CostructuredArrow G (G.obj Y))

Tactic:
CostructuredArrow.mkIdTerminal.hasTerminal

Premises used: CategoryTheory.Limits.IsTerminal.hasTerminal, CategoryTheory.CostructuredArrow.mkIdTerminal
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
G : Functor.{v₁, v₃, u₁, u₃} A T
X : T
F : J ⥤ CostructuredArrow G X
i₁ : HasColimit (F ⋙ proj G X)
i₂ : PreservesColimit (F ⋙ proj G X) G
⊢ HasColimit (F ⋙ Comma.fst G (fromPUnit X))

Tactic:
haveI : HasColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) := i₁
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
G : Functor.{v₁, v₃, u₁, u₃} A T
X : T
F : J ⥤ CostructuredArrow G X
i₁ : HasColimit (F ⋙ proj G X)
i₂ : PreservesColimit (F ⋙ proj G X) G
this : HasColimit (F ⋙ Comma.fst G (fromPUnit X))
⊢ PreservesColimit (F ⋙ Comma.fst G (fromPUnit X)) G

Tactic:
haveI : PreservesColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) _ := i₂
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
G : Functor.{v₁, v₃, u₁, u₃} A T
X : T
F : J ⥤ CostructuredArrow G X
i₁ : HasColimit (F ⋙ proj G X)
i₂ : PreservesColimit (F ⋙ proj G X) G
this_1 : HasColimit (F ⋙ Comma.fst G (fromPUnit X))
this : PreservesColimit (F ⋙ Comma.fst G (fromPUnit X)) G
⊢ HasColimit F

Tactic:
apply Comma.hasColimit

Premises used: CategoryTheory.Comma.hasColimit
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
G : Functor.{v₁, v₃, u₁, u₃} A T
X : T
F : J ⥤ CostructuredArrow G X
inst_4 : HasColimitsOfSize.{w, w', v₁, u₁} A
inst_5 : PreservesColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} G
⊢ HasColimitsOfSize.{w, w', v₁, max u₁ v₃} (CostructuredArrow G X)

Tactic:
⟨fun _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasColimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
G : Functor.{v₁, v₃, u₁, u₃} A T
X : T
F : J ⥤ CostructuredArrow G X
inst_4 : HasPushouts.{v₁, u₁} A
inst_5 : PreservesColimitsOfShape WalkingSpan G
Y Z : CostructuredArrow G X
f : Y ⟶ Z
inst_6 : Epi f
⊢ Epi f.left

Tactic:
show Epi ((proj G X).map f) from inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
T : Type u₃
inst_1 : Category.{v₃, u₃} T
G : Functor.{v₁, v₃, u₁, u₃} A T
X : T
inst_2 : HasPushouts.{v₁, u₁} A
inst_3 : PreservesColimitsOfShape WalkingSpan G
Y Z : CostructuredArrow G X
f : Y ⟶ Z
⊢ Epi f ↔ Epi f.left

Tactic:
⟨fun _ => inferInstance, fun _ => epi_of_epi_left f⟩

Premises used: inferInstance, CategoryTheory.CostructuredArrow.epi_of_epi_left, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Comma
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
X : T
⊢ HasTerminal (Over.{v₃, u₃} X)

Tactic:
CostructuredArrow.hasTerminal

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

Tactic:
Under.mkIdInitial.hasInitial

Premises used: CategoryTheory.Under.mkIdInitial, CategoryTheory.Limits.IsInitial.hasInitial
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
⊢ Functor.Full (forget (Type u) (FC := TypeCat.Fun))

Tactic:
Functor.Full.id

Premises used: CategoryTheory.Functor.Full.id, CategoryTheory.Functor.id
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
⊢ PreservesLimitsOfSize.{u_1, u_2, u, u, u + 1, u + 1} (forget (Type u) (FC := TypeCat.Fun))

Tactic:
id_preservesLimitsOfSize

Premises used: CategoryTheory.Functor.id, CategoryTheory.Limits.id_preservesLimitsOfSize
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
⊢ PreservesColimitsOfSize.{u_1, u_2, u, u, u + 1, u + 1} (forget (Type u) (FC := TypeCat.Fun))

Tactic:
id_preservesColimitsOfSize

Premises used: CategoryTheory.Functor.id, CategoryTheory.Limits.id_preservesColimitsOfSize
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
⊢ ReflectsLimitsOfSize.{u_1, u_2, u, u, u + 1, u + 1} (forget (Type u) (FC := TypeCat.Fun))

Tactic:
id_reflectsLimits

Premises used: CategoryTheory.Limits.id_reflectsLimits, CategoryTheory.Functor.id
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
⊢ ReflectsColimitsOfSize.{u_1, u_2, u, u, u + 1, u + 1} (forget (Type u) (FC := TypeCat.Fun))

Tactic:
id_reflectsColimits

Premises used: CategoryTheory.Functor.id, CategoryTheory.Limits.id_reflectsColimits
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
⊢ Functor.IsEquivalence (forget (Type u) (FC := TypeCat.Fun))

Tactic:
Functor.isEquivalence_refl

Premises used: CategoryTheory.Functor.id, CategoryTheory.Functor.isEquivalence_refl
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
⊢ Functor.IsCorepresentable (forget (Type u) (FC := TypeCat.Fun))

Tactic:
inferInstanceAs (𝟭 <| Type u).IsCorepresentable

Premises used: _private.0.CategoryTheory.Types.instIsCorepresentableForgetTypeFun._proof_1
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Functor.IsCorepresentable (forget C (FC := FC) (CC := CC))
J : Type w
inst_4 : Category.{t, w} J
G : Functor.{t, v, w, u} J C
inst_5 : HasLimit G
rw : HasLimit (G ⋙ forget C (FC := FC) (CC := CC))
⊢ Small.{v, max v w} (↑(G ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max v w))

Tactic:
rw [← Types.hasLimit_iff_small_sections]

Premises used: CategoryTheory.Limits.Types.hasLimit_iff_small_sections
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Functor.IsCorepresentable (forget C (FC := FC) (CC := CC))
J : Type w
inst_4 : Category.{t, w} J
G : Functor.{t, v, w, u} J C
inst_5 : HasLimit G
⊢ HasLimit (G ⋙ forget C (FC := FC) (CC := CC))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst_1 : (X Y : C) → FunLike.{u_1 + 1, r + 1, r + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{r, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
inst_4 : PreservesLimit F (forget C (FC := FC) (CC := CC))
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCone (forget C (FC := FC) (CC := CC)) D
x : E.pt
y : ToType.{r, v, u, u_1} (FC := FC) (CC := CC) D.pt
H :
  Eq (α := (j : J) → CC (F.obj j))
    ((fun (x : ToType.{r, v, u, u_1} (FC := FC) (CC := CC) D.pt) (j : J) ↦
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.π.app j) :
              (a : CC (((Functor.const J).obj D.pt).obj j)) → CC (F.obj j))
            x :
          CC (F.obj j)))
      x)
    ((fun (x : ToType.{r, v, u, u_1} (FC := FC) (CC := CC) D.pt) (j : J) ↦
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.π.app j) :
              (a : CC (((Functor.const J).obj D.pt).obj j)) → CC (F.obj j))
            x :
          CC (F.obj j)))
      y)
a :
  Eq (α := (↑(F ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max r w)))
    ((Types.isLimitEquivSections (isLimitOfPreserves (forget C (FC := FC) (CC := CC)) hD) :
          (a : ((forget C).mapCone D).pt) → (↑(F ⋙ forget C).sections : Type (max r w)))
        x :
      (↑(F ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max r w)))
    ((Types.isLimitEquivSections (isLimitOfPreserves (forget C (FC := FC) (CC := CC)) hD) :
          (a : ((forget C).mapCone D).pt) → (↑(F ⋙ forget C).sections : Type (max r w)))
        y :
      (↑(F ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max r w)))
⊢ x = y

Tactic:
apply (Types.isLimitEquivSections (isLimitOfPreserves _ hD)).injective

Premises used: CategoryTheory.Limits.Types.isLimitEquivSections, Equiv.injective, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst_1 : (X Y : C) → FunLike.{u_1 + 1, r + 1, r + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{r, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
inst_4 : PreservesLimit F (forget C (FC := FC) (CC := CC))
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCone (forget C (FC := FC) (CC := CC)) D
x : E.pt
y : ToType.{r, v, u, u_1} (FC := FC) (CC := CC) D.pt
H :
  Eq (α := (j : J) → CC (F.obj j))
    ((fun (x : ToType.{r, v, u, u_1} (FC := FC) (CC := CC) D.pt) (j : J) ↦
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.π.app j) :
              (a : CC (((Functor.const J).obj D.pt).obj j)) → CC (F.obj j))
            x :
          CC (F.obj j)))
      x)
    ((fun (x : ToType.{r, v, u, u_1} (FC := FC) (CC := CC) D.pt) (j : J) ↦
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.π.app j) :
              (a : CC (((Functor.const J).obj D.pt).obj j)) → CC (F.obj j))
            x :
          CC (F.obj j)))
      y)
a :
  ∀ (j : J),
    Eq.{r + 1} (α := (F ⋙ forget C (FC := FC) (CC := CC)).obj j)
      ((↑((Types.isLimitEquivSections (isLimitOfPreserves (forget C (FC := FC) (CC := CC)) hD) :
                (a : ((forget C).mapCone D).pt) → (↑(F ⋙ forget C).sections : Type (max r w)))
              x) :
          (j : J) → (F ⋙ forget C).obj j)
        j)
      ((↑((Types.isLimitEquivSections (isLimitOfPreserves (forget C (FC := FC) (CC := CC)) hD) :
                (a : ((forget C).mapCone D).pt) → (↑(F ⋙ forget C).sections : Type (max r w)))
              y) :
          (j : J) → (F ⋙ forget C).obj j)
        j)
⊢ Eq (α := (↑(F ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max r w)))
    ((Types.isLimitEquivSections (isLimitOfPreserves (forget C (FC := FC) (CC := CC)) hD) :
          (a : ((forget C).mapCone D).pt) → (↑(F ⋙ forget C).sections : Type (max r w)))
        x :
      (↑(F ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max r w)))
    ((Types.isLimitEquivSections (isLimitOfPreserves (forget C (FC := FC) (CC := CC)) hD) :
          (a : ((forget C).mapCone D).pt) → (↑(F ⋙ forget C).sections : Type (max r w)))
        y :
      (↑(F ⋙ forget C (FC := FC) (CC := CC)).sections : Type (max r w)))

Tactic:
ext j