awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
s :
  Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
    (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0
b : β
hb : b ∈ Set.range f
pos :
  ∀ (a : α),
    CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
        (Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (f a))
        (CategoryStruct.comp (Y :=
          Cocone.pt.{0, v, 0, u} (F :=
            parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
              (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
            (sigmaConstCokernelCofork R f))
          (Cofork.π (sigmaConstCokernelCofork R f))
          ((fun
                (s :
                  Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y :=
                    sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0) ↦
              (Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦
                  match (motive := (↑(Set.range f)ᶜ : Type u_2) → (R ⟶ s.pt)) x with
                  | ⟨b, property⟩ => Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b ≫ s.π :
                (sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R) ⟶ s.pt))
            s)) =
      Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (f a) ≫ s.π
⊢ CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b)
      (CategoryStruct.comp (Y :=
        Cocone.pt.{0, v, 0, u} (F :=
          parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
            (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
          (sigmaConstCokernelCofork R f))
        (Cofork.π (sigmaConstCokernelCofork R f))
        ((fun
              (s :
                Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y :=
                  sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0) ↦
            (Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦
                match (motive := (↑(Set.range f)ᶜ : Type u_2) → (R ⟶ s.pt)) x with
                | ⟨b, property⟩ => Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b ≫ s.π :
              (sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R) ⟶ s.pt))
          s)) =
    Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b ≫ s.π

Tactic:
obtain ⟨a, rfl⟩ := hb

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
s :
  Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
    (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0
a : α
⊢ CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (f a))
      (CategoryStruct.comp (Y :=
        Cocone.pt.{0, v, 0, u} (F :=
          parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
            (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
          (sigmaConstCokernelCofork R f))
        (Cofork.π (sigmaConstCokernelCofork R f))
        ((fun
              (s :
                Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y :=
                  sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0) ↦
            (Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦
                match (motive := (↑(Set.range f)ᶜ : Type u_2) → (R ⟶ s.pt)) x with
                | ⟨b, property⟩ => Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b ≫ s.π :
              (sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R) ⟶ s.pt))
          s)) =
    Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (f a) ≫ s.π

Tactic:
simpa [-CokernelCofork.condition] using Sigma.ι (fun _ ↦ R) a ≫= s.condition.symm

Premises used: CategoryTheory.Limits.CokernelCofork.condition, CategoryTheory.Limits.Sigma.ι, CategoryTheory.Limits.Cofork.condition, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
s :
  Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
    (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0
b : β
hb : b ∉ Set.range f
⊢ CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b)
      (CategoryStruct.comp (Y :=
        Cocone.pt.{0, v, 0, u} (F :=
          parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
            (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
          (sigmaConstCokernelCofork R f))
        (Cofork.π (sigmaConstCokernelCofork R f))
        ((fun
              (s :
                Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y :=
                  sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0) ↦
            (Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦
                match (motive := (↑(Set.range f)ᶜ : Type u_2) → (R ⟶ s.pt)) x with
                | ⟨b, property⟩ => Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b ≫ s.π :
              (sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R) ⟶ s.pt))
          s)) =
    Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b ≫ s.π

Tactic:
simp [ι_sigmaConstCokernelCofork_π_assoc _ _ _ hb]

Premises used: CategoryTheory.Limits.ι_sigmaConstCokernelCofork_π_assoc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
s :
  Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
    (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0
m :
  Cocone.pt.{0, v, 0, u} (F :=
      parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
        (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
      (sigmaConstCokernelCofork R f) ⟶
    s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
dsimp :
  m = Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑x : β) ≫ s.π
⊢ m =
    (fun
          (s :
            Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y :=
              sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0) ↦
        (Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦
            match (motive := (↑(Set.range f)ᶜ : Type u_2) → (R ⟶ s.pt)) x with
            | ⟨b, property⟩ => Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b ≫ s.π :
          (sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R) ⟶ s.pt))
      s

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
s :
  Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
    (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0
m :
  Cocone.pt.{0, v, 0, u} (F :=
      parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
        (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
      (sigmaConstCokernelCofork R f) ⟶
    s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
h :
  ∀ (b : β) (hb : b ∈ (Set.range f)ᶜ),
    Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
          (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
        m =
      CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
          (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb))
        (Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦
          Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑x : β) ≫ s.π)
⊢ m = Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑x : β) ≫ s.π

Tactic:
ext ⟨b, hb⟩
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
s :
  Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
    (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0
m :
  Cocone.pt.{0, v, 0, u} (F :=
      parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
        (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
      (sigmaConstCokernelCofork R f) ⟶
    s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
b : β
hb : b ∈ (Set.range f)ᶜ
h :
  Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) ≫
      s.π
h₁ :
  Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) ≫
      Cofork.π (sigmaConstCokernelCofork R f) ≫ m
h₂ :
  Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ)
          (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) hb) ≫
      m
h₃ : (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) ∉ Set.range f
h₄ :
  Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ)
          (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) hb) ≫
      m
h₅ : (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) ∉ Set.range f
⊢ Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
      (Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb))
      (Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦
        Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑x : β) ≫ s.π)

Tactic:
rw [Sigma.ι_desc, ← hm, ι_sigmaConstCokernelCofork_π_assoc]

Premises used: CategoryTheory.Limits.ι_sigmaConstCokernelCofork_π_assoc, CategoryTheory.Limits.Sigma.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
⊢ HasCokernel.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
    (Sigma.map' f fun (x : α) ↦ 𝟙 R)

Tactic:
⟨_, isColimitSigmaConstCokernelCofork R f⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.isColimitSigmaConstCokernelCofork
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
inst_2 : HasCoproducts.{w, v, u} C
α β : Type w
f : α ⟶ β
dsimp :
  HasCokernel.{v, u} (C := C) (X := sigmaObj.{w, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{w, v, u} fun (x : β) ↦ R)
    (Sigma.map' (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : α) → β) fun (x : α) ↦ 𝟙 R)
⊢ HasCokernel.{v, u} (X := Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) α)
    (Functor.map (Functor.obj sigmaConst R) f)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
inst_2 : HasCoproducts.{w, v, u} C
α β : Type w
f : α ⟶ β
⊢ HasCokernel.{v, u} (C := C) (X := sigmaObj.{w, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{w, v, u} fun (x : β) ↦ R)
    (Sigma.map' (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : α) → β) fun (x : α) ↦ 𝟙 R)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Ulift
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
K : Functor.{v_1, u, u_1, u + 1} J (Type u)
x : (↑K.sections : Type (max u u_1))
u : (j : J) → K.obj j
hu : u ∈ K.sections
j j' : J
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type (max u v)) ↦ X) ((K ⋙ uliftFunctor.{v, u}).obj j'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((K ⋙ uliftFunctor.{v, u}).map f) :
        (a : (fun (X : Type (max u v)) ↦ X) ((K ⋙ uliftFunctor.{v, u}).obj j)) →
          (fun (X : Type (max u v)) ↦ X) ((K ⋙ uliftFunctor.{v, u}).obj j'))
      ((fun (j : J) ↦ { down := u j : ULift.{v, u} (K.obj j) }) j))
    ((fun (j : J) ↦ { down := u j : ULift.{v, u} (K.obj j) }) j')

Tactic:
simp [hu f]
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Ulift
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
K : Functor.{v_1, u, u_1, u + 1} J (Type u)
x : (↑(K ⋙ uliftFunctor.{v, u}).sections : Type (max (max u u_1) v))
u : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j
hu : u ∈ (K ⋙ uliftFunctor.{v, u}).sections
j j' : J
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type u) ↦ X) (K.obj j'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map f) :
          (a : (fun (X : Type u) ↦ X) (K.obj j)) → (fun (X : Type u) ↦ X) (K.obj j'))
        ((fun (j : J) ↦ (u j).down) j) :
      (fun (X : Type u) ↦ X) (K.obj j'))
    ((fun (j : J) ↦ (u j).down) j' : K.obj j')

Tactic:
simp [← hu f]
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Ulift
Goal:
J : Type w
inst : Category.{w', w} J
K : Functor.{w', u, w, u + 1} J (Type u)
c : Cone K
hc : IsLimit c
rw :
  ∀ s ∈ (K ⋙ uliftFunctor.{v, u}).sections,
    ∃! x : (uliftFunctor.{v, u}.mapCone c).pt,
      ∀ (j : J),
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((uliftFunctor.{v, u}.mapCone c).π.app j) :
              (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj (uliftFunctor.{v, u}.mapCone c).pt).obj j)) →
                (fun (X : Type (max u v)) ↦ X) ((K ⋙ uliftFunctor.{v, u}).obj j))
            x =
          s j
⊢ Nonempty (IsLimit (uliftFunctor.{v, u}.mapCone c))

Tactic:
rw [Types.isLimit_iff ((uliftFunctor.{v, u}).mapCone c)]
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Ulift
Goal:
J : Type w
inst : Category.{w', w} J
K : Functor.{w', u, w, u + 1} J (Type u)
c : Cone K
hc : IsLimit c
s : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j
hs : s ∈ (K ⋙ uliftFunctor.{v, u}).sections
obtain :
  ∀ (x : c.pt)
    (hx₁ :
      ∀ (j : J),
        Eq (α := (fun (X : Type u) ↦ X) (K.obj j))
          ((ConcreteCategory.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) (K.obj j))
              x :
            (fun (X : Type u) ↦ X) (K.obj j))
          ((↑(((sectionsEquiv K).symm :
                      (a : (↑(K ⋙ uliftFunctor.{v, u}).sections : Type (max (max u w) v))) →
                        (↑K.sections : Type (max u w)))
                    (Subtype.mk (p := fun (x : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j) ↦
                      x ∈ (K ⋙ uliftFunctor.{v, u}).sections) s ⋯)) :
                (j : J) → K.obj j)
              j :
            K.obj j))
    (hx₂ :
      ∀ (y : c.pt),
        (fun (x : c.pt) ↦
              ∀ (j : J),
                Eq (α := (fun (X : Type u) ↦ X) (K.obj j))
                  ((ConcreteCategory.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) (K.obj j))
                      x :
                    (fun (X : Type u) ↦ X) (K.obj j))
                  ((↑(((sectionsEquiv K).symm :
                              (a : (↑(K ⋙ uliftFunctor.{v, u}).sections : Type (max (max u w) v))) →
                                (↑K.sections : Type (max u w)))
                            (Subtype.mk (p := fun (x : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j) ↦
                              x ∈ (K ⋙ uliftFunctor.{v, u}).sections) s ⋯)) :
                        (j : J) → K.obj j)
                      j :
                    K.obj j))
            y →
          y = x),
    ∃! x : (uliftFunctor.{v, u}.mapCone c).pt,
      ∀ (j : J),
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((uliftFunctor.{v, u}.mapCone c).π.app j) :
              (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj (uliftFunctor.{v, u}.mapCone c).pt).obj j)) →
                (fun (X : Type (max u v)) ↦ X) ((K ⋙ uliftFunctor.{v, u}).obj j))
            x =
          s j
⊢ ∃! x : (uliftFunctor.{v, u}.mapCone c).pt,
    ∀ (j : J),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((uliftFunctor.{v, u}.mapCone c).π.app j) :
            (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj (uliftFunctor.{v, u}.mapCone c).pt).obj j)) →
              (fun (X : Type (max u v)) ↦ X) ((K ⋙ uliftFunctor.{v, u}).obj j))
          x =
        s j

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := (Types.isLimit_iff c).mp ⟨hc⟩ _ ((sectionsEquiv K).symm ⟨s, hs⟩).2

Premises used: CategoryTheory.Limits.Types.sectionsEquiv, Nonempty.intro, Subtype.mk, Iff.mp, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.Types.isLimit_iff, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Ulift
Goal:
J : Type w
inst : Category.{w', w} J
K : Functor.{w', u, w, u + 1} J (Type u)
c : Cone K
hc : IsLimit c
s : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j
hs : s ∈ (K ⋙ uliftFunctor.{v, u}).sections
x : c.pt
hx₁ :
  ∀ (j : J),
    Eq (α := (fun (X : Type u) ↦ X) (K.obj j))
      ((ConcreteCategory.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) (K.obj j))
          x :
        (fun (X : Type u) ↦ X) (K.obj j))
      ((↑(((sectionsEquiv K).symm :
                  (a : (↑(K ⋙ uliftFunctor.{v, u}).sections : Type (max (max u w) v))) → (↑K.sections : Type (max u w)))
                (Subtype.mk (p := fun (x : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j) ↦
                  x ∈ (K ⋙ uliftFunctor.{v, u}).sections) s ⋯)) :
            (j : J) → K.obj j)
          j :
        K.obj j)
hx₂ :
  ∀ (y : c.pt),
    (fun (x : c.pt) ↦
          ∀ (j : J),
            Eq (α := (fun (X : Type u) ↦ X) (K.obj j))
              ((ConcreteCategory.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) (K.obj j))
                  x :
                (fun (X : Type u) ↦ X) (K.obj j))
              ((↑(((sectionsEquiv K).symm :
                          (a : (↑(K ⋙ uliftFunctor.{v, u}).sections : Type (max (max u w) v))) →
                            (↑K.sections : Type (max u w)))
                        (Subtype.mk (p := fun (x : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j) ↦
                          x ∈ (K ⋙ uliftFunctor.{v, u}).sections) s ⋯)) :
                    (j : J) → K.obj j)
                  j :
                K.obj j))
        y →
      y = x
⊢ ∃! x : (uliftFunctor.{v, u}.mapCone c).pt,
    ∀ (j : J),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((uliftFunctor.{v, u}.mapCone c).π.app j) :
            (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj (uliftFunctor.{v, u}.mapCone c).pt).obj j)) →
              (fun (X : Type (max u v)) ↦ X) ((K ⋙ uliftFunctor.{v, u}).obj j))
          x =
        s j

Tactic:
⟨⟨x⟩, fun i => ULift.ext _ _ (hx₁ i),
          fun y hy => ULift.ext _ _ (hx₂ y.down fun i ↦ ULift.ext_iff.mp (hy i))⟩

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ConcreteCategory.hom, ULift.ext, CategoryTheory.uliftFunctor, ExistsUnique, And.intro, Exists.intro, Iff.mp, CategoryTheory.Functor.mapCone, ULift.up, DFunLike.coe, ULift.down, ULift.ext_iff, CategoryTheory.NatTrans.app