awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (Opposite.op
                { down := { down := h : PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p)) } :
                  ULift.{0, 0} (PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p))) })) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op p))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
        ((fun (x : ℕᵒᵖ) ↦
            (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
              | Opposite.op n => preimage hF a n :
              F.obj x))
          (Opposite.op p)) :
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
    ((fun (x : ℕᵒᵖ) ↦
          (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
            | Opposite.op n => preimage hF a n :
            F.obj x))
        (Opposite.op m) :
      F.obj (Opposite.op m))
⊢ m ≤ p

Tactic:
have h' : m ≤ p := h
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (Opposite.op
                { down := { down := h : PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p)) } :
                  ULift.{0, 0} (PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p))) })) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op p))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
        ((fun (x : ℕᵒᵖ) ↦
            (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
              | Opposite.op n => preimage hF a n :
              F.obj x))
          (Opposite.op p)) :
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
    ((fun (x : ℕᵒᵖ) ↦
          (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
            | Opposite.op n => preimage hF a n :
            F.obj x))
        (Opposite.op m) :
      F.obj (Opposite.op m))
h' : m ≤ p
⊢ Eq (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE h').op) :
          (a : F.obj (Opposite.op p)) → F.obj (Opposite.op m))
        (preimage hF a p) :
      F.obj (Opposite.op m))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (Opposite.op
                { down := { down := h : PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p)) } :
                  ULift.{0, 0} (PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p))) })) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op p))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
        ((fun (x : ℕᵒᵖ) ↦
            (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
              | Opposite.op n => preimage hF a n :
              F.obj x))
          (Opposite.op p)) :
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
simp :
  Eq (α := c.pt ⟶ F.obj (Opposite.op 0)) (c.π.app (Opposite.op 0))
    ((hc.conePointUniqueUpToIso (limitConeIsLimit F)).hom ≫
      ↾fun (u : (↑F.sections : Type u)) ↦ (↑u : (j : ℕᵒᵖ) → F.obj j) (Opposite.op 0))
⊢ Eq (α := Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0) ⟶ F.obj (Opposite.op 0))
    (c.π.app (Opposite.op 0)) (i.hom ≫ (limitCone F).π.app (Opposite.op 0))

Tactic:
simp [i]
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
⊢ Eq (α := c.pt ⟶ F.obj (Opposite.op 0)) (c.π.app (Opposite.op 0))
    ((hc.conePointUniqueUpToIso (limitConeIsLimit F)).hom ≫
      ↾fun (u : (↑F.sections : Type u)) ↦ (↑u : (j : ℕᵒᵖ) → F.obj j) (Opposite.op 0))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
⊢ Eq (α := Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0) ⟶ F.obj (Opposite.op 0))
    (c.π.app (Opposite.op 0)) (i.hom ≫ (limitCone F).π.app (Opposite.op 0))

Tactic:
have : c.π.app ⟨0⟩ = i.hom ≫ (limitCone F).π.app ⟨0⟩ := by simp [i]; rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this :
  Eq (α := Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0) ⟶ F.obj (Opposite.op 0))
    (c.π.app (Opposite.op 0)) (i.hom ≫ (limitCone F).π.app (Opposite.op 0))
rw :
  Function.Surjective (α :=
    (fun (X : Type u) ↦ X) (Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0))) (β :=
    (fun (X : Type u) ↦ X) (F.obj (Opposite.op 0)))
    (Function.comp (β := (fun (X : Type u) ↦ X) (limitCone F).pt)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((limitCone F).π.app (Opposite.op 0))) :
        (a : (fun (X : Type u) ↦ X) (limitCone F).pt) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op 0)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) i.hom) :
        (a : (fun (X : Type u) ↦ X) ((fun (X : Type u) ↦ X) (((Functor.const ℕᵒᵖ).obj c.pt).obj (Opposite.op 0)))) →
          (fun (X : Type u) ↦ X) (limitCone F).pt))
⊢ Function.Surjective (α :=
    (fun (X : Type u) ↦ X) (Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0))) (β :=
    (fun (X : Type u) ↦ X) (F.obj (Opposite.op 0)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.π.app (Opposite.op 0))) :
      (a : (fun (X : Type u) ↦ X) (((Functor.const ℕᵒᵖ).obj c.pt).obj (Opposite.op 0))) →
        (fun (X : Type u) ↦ X) (F.obj (Opposite.op 0)))

Tactic:
rw [this, types_comp]

Premises used: CategoryTheory.types_comp
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this :
  Eq (α := Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0) ⟶ F.obj (Opposite.op 0))
    (c.π.app (Opposite.op 0)) (i.hom ≫ (limitCone F).π.app (Opposite.op 0))
hg :
  Function.Surjective (α := (fun (X : Type u) ↦ X) (limitCone F).pt) (β :=
    (fun (X : Type u) ↦ X) (F.obj (Opposite.op 0)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((limitCone F).π.app (Opposite.op 0))) :
      (a : (fun (X : Type u) ↦ X) (limitCone F).pt) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op 0)))
hf :
  Function.Surjective (α :=
    (fun (X : Type u) ↦ X) (Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0))) (β :=
    (fun (X : Type u) ↦ X) (limitCone F).pt)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) i.hom) :
      (a : (fun (X : Type u) ↦ X) ((fun (X : Type u) ↦ X) (((Functor.const ℕᵒᵖ).obj c.pt).obj (Opposite.op 0)))) →
        (fun (X : Type u) ↦ X) (limitCone F).pt)
⊢ Function.Surjective (α :=
    (fun (X : Type u) ↦ X) (Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0))) (β :=
    (fun (X : Type u) ↦ X) (F.obj (Opposite.op 0)))
    (Function.comp (β := (fun (X : Type u) ↦ X) (limitCone F).pt)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((limitCone F).π.app (Opposite.op 0))) :
        (a : (fun (X : Type u) ↦ X) (limitCone F).pt) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op 0)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) i.hom) :
        (a : (fun (X : Type u) ↦ X) ((fun (X : Type u) ↦ X) (((Functor.const ℕᵒᵖ).obj c.pt).obj (Opposite.op 0)))) →
          (fun (X : Type u) ↦ X) (limitCone F).pt))

Tactic:
apply Function.Surjective.comp

Premises used: Function.Surjective.comp
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this :
  Eq (α := Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0) ⟶ F.obj (Opposite.op 0))
    (c.π.app (Opposite.op 0)) (i.hom ≫ (limitCone F).π.app (Opposite.op 0))
⊢ Function.Surjective (α := (fun (X : Type u) ↦ X) (limitCone F).pt) (β :=
    (fun (X : Type u) ↦ X) (F.obj (Opposite.op 0)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((limitCone F).π.app (Opposite.op 0))) :
      (a : (fun (X : Type u) ↦ X) (limitCone F).pt) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op 0)))

Tactic:
surjective_π_app_zero_of_surjective_map_aux hF

Premises used: CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map_aux
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this :
  Eq (α := Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0) ⟶ F.obj (Opposite.op 0))
    (c.π.app (Opposite.op 0)) (i.hom ≫ (limitCone F).π.app (Opposite.op 0))
⊢ Function.Surjective (α := (fun (X : Type u) ↦ X) (limitCone F).pt) (β :=
    (fun (X : Type u) ↦ X) (F.obj (Opposite.op 0)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((limitCone F).π.app (Opposite.op 0))) :
      (a : (fun (X : Type u) ↦ X) (limitCone F).pt) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op 0)))

Tactic:
exact surjective_π_app_zero_of_surjective_map_aux hF

Premises used: CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map_aux
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this :
  Eq (α := Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0) ⟶ F.obj (Opposite.op 0))
    (c.π.app (Opposite.op 0)) (i.hom ≫ (limitCone F).π.app (Opposite.op 0))
hf : Epi i.hom
⊢ Function.Surjective (α :=
    (fun (X : Type u) ↦ X) (Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0))) (β :=
    (fun (X : Type u) ↦ X) (limitCone F).pt)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) i.hom) :
      (a : (fun (X : Type u) ↦ X) ((fun (X : Type u) ↦ X) (((Functor.const ℕᵒᵖ).obj c.pt).obj (Opposite.op 0)))) →
        (fun (X : Type u) ↦ X) (limitCone F).pt)

Tactic:
rw [← epi_iff_surjective]

Premises used: CategoryTheory.epi_iff_surjective
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this :
  Eq (α := Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0) ⟶ F.obj (Opposite.op 0))
    (c.π.app (Opposite.op 0)) (i.hom ≫ (limitCone F).π.app (Opposite.op 0))
⊢ Epi i.hom

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
s : (j : J) → F.obj j
hs : s ∈ F.sections
x x_1 : J
f : x ⟶ x_1
h :
  ∀ (x_2 : Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) PUnit.{u + 1}) x),
    TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (Functor.map (Functor.obj (Functor.const J) PUnit.{u + 1}) f ≫
            ↾fun (x : Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) PUnit.{u + 1}) x_1) ↦ s x_1))
        x_2 =
      TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          ((↾fun (x_3 : Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) PUnit.{u + 1}) x) ↦ s x) ≫ F.map f))
        x_2
⊢ Eq (α := Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) PUnit.{u + 1}) x ⟶ F.obj x_1)
    (Functor.map (Functor.obj (Functor.const J) PUnit.{u + 1}) f ≫
      ↾fun (x : Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) PUnit.{u + 1}) x_1) ↦ s x_1)
    ((↾fun (x_2 : Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) PUnit.{u + 1}) x) ↦ s x) ≫ F.map f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
s : (j : J) → F.obj j
hs : s ∈ F.sections
x x_1 : J
f : x ⟶ x_1
x_2 : Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) PUnit.{u + 1}) x
⊢ TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj (Functor.const J) PUnit.{u + 1}) f ≫
          ↾fun (x : Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) PUnit.{u + 1}) x_1) ↦ s x_1))
      x_2 =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        ((↾fun (x_3 : Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) PUnit.{u + 1}) x) ↦ s x) ≫ F.map f))
      x_2

Tactic:
(hs f).symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
s : (j : J) → F.obj j
hs : s ∈ F.sections
x x_1 : J
f : x ⟶ x_1
x_2 : Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) PUnit.{u + 1}) x
⊢ TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj (Functor.const J) PUnit.{u + 1}) f ≫
          ↾fun (x : Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) PUnit.{u + 1}) x_1) ↦ s x_1))
      x_2 =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        ((↾fun (x_3 : Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) PUnit.{u + 1}) x) ↦ s x) ≫ F.map f))
      x_2

Tactic:
exact (hs f).symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : Cone F
⊢ Nonempty (IsLimit c) ↔
    ∀ s ∈ F.sections,
      ∃! x : c.pt,
        ∀ (j : J),
          (hom (FC := TypeCat.Fun) (c.π.app j) :
                (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
              x =
            s j

Tactic:
⟨fun ⟨t⟩ s hs ↦ ?_, fun h ↦ ⟨?_⟩⟩

Premises used: _private.0.CategoryTheory.Limits.Types.isLimit_iff.match_1, Nonempty.intro, ExistsUnique, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : Cone F
refine_1 :
  Nonempty (IsLimit c) →
    ∀ (s : (j : J) → F.obj j) (hs : s ∈ F.sections) (t : IsLimit c),
      ∃! x : c.pt,
        ∀ (j : J),
          (hom (FC := TypeCat.Fun) (c.π.app j) :
                (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
              x =
            s j
refine_2 :
  (h :
      ∀ s ∈ F.sections,
        ∃! x : c.pt,
          ∀ (j : J),
            (hom (FC := TypeCat.Fun) (c.π.app j) :
                  (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
                x =
              s j) →
    IsLimit c
⊢ Nonempty (IsLimit c) ↔
    ∀ s ∈ F.sections,
      ∃! x : c.pt,
        ∀ (j : J),
          (hom (FC := TypeCat.Fun) (c.π.app j) :
                (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
              x =
            s j

Tactic:
refine ⟨fun ⟨t⟩ s hs ↦ ?_, fun h ↦ ⟨?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : Cone F
h_1 : Nonempty (IsLimit c)
s : (j : J) → F.obj j
hs : s ∈ F.sections
t : IsLimit c
cs : Cone F := coneOfSection (s := s) ⋯
x : c.pt
hx :
  (fun (x : c.pt) ↦
      ∀ (j : J),
        (hom (FC := TypeCat.Fun) (c.π.app j) :
              (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
            x =
          s j)
    x
j : J
h :
  ∀ (x_1 : cs.pt),
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) ((↾fun (x_2 : cs.pt) ↦ x) ≫ c.π.app j)) x_1 =
      (hom (FC := TypeCat.Fun) (cs.π.app j)).toFun x_1
⊢ (↾fun (x_1 : cs.pt) ↦ x) ≫ c.π.app j = cs.π.app j

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : Cone F
h : Nonempty (IsLimit c)
s : (j : J) → F.obj j
hs : s ∈ F.sections
t : IsLimit c
cs : Cone F := coneOfSection (s := s) ⋯
x : c.pt
hx :
  (fun (x : c.pt) ↦
      ∀ (j : J),
        (hom (FC := TypeCat.Fun) (c.π.app j) :
              (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
            x =
          s j)
    x
j : J
x_1 : cs.pt
⊢ TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) ((↾fun (x_2 : cs.pt) ↦ x) ≫ c.π.app j)) x_1 =
    (hom (FC := TypeCat.Fun) (cs.π.app j)).toFun x_1

Tactic:
hx j
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : Cone F
h : Nonempty (IsLimit c)
s : (j : J) → F.obj j
hs : s ∈ F.sections
t : IsLimit c
cs : Cone F := coneOfSection (s := s) ⋯
x : c.pt
hx :
  (fun (x : c.pt) ↦
      ∀ (j : J),
        (hom (FC := TypeCat.Fun) (c.π.app j) :
              (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
            x =
          s j)
    x
j : J
x_1 : cs.pt
⊢ TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) ((↾fun (x_2 : cs.pt) ↦ x) ≫ c.π.app j)) x_1 =
    (hom (FC := TypeCat.Fun) (cs.π.app j)).toFun x_1

Tactic:
exact hx j
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : Cone F
h : Nonempty (IsLimit c)
s : (j : J) → F.obj j
hs : s ∈ F.sections
t : IsLimit c
cs : Cone F := coneOfSection (s := s) ⋯
⊢ ∃! x : c.pt,
    ∀ (j : J),
      (hom (FC := TypeCat.Fun) (c.π.app j) :
            (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
          x =
        s j

Tactic:
exact ⟨t.lift cs ⟨⟩, fun j ↦ congr_hom (t.fac cs j) ⟨⟩,
      fun x hx ↦ congr_hom (CC := fun X ↦ X)
        (t.uniq cs (↾fun _ ↦ x) fun j ↦ by ext; exact hx j) ⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : Cone F
h :
  ∀ s ∈ F.sections,
    ∃! x : c.pt,
      ∀ (j : J),
        (hom (FC := TypeCat.Fun) (c.π.app j) :
              (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
            x =
          s j
⊢ ∀ (c_1 : Cone F) (y : c_1.pt),
    ∃! x : c.pt,
      ∀ (j : J),
        (hom (FC := TypeCat.Fun) (c.π.app j) :
              (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
            x =
          (↑(sectionOfCone c_1 y) : (j : J) → F.obj j) j

Tactic:
have := fun c y ↦ h _ (sectionOfCone c y).2