awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
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))
have 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))
Tactic: simp [i]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (hypothesis)
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)
⊢ 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)))
have 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))
Tactic: have : c.π.app ⟨0⟩ = i.hom ≫ (limitCone F).π.app ⟨0⟩ := by simp [i]; rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
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) (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)))
have 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))
Tactic: rw [this, types_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
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) (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))
have 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)))
Tactic: apply Function.Surjective.comp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
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)))
⊢ 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))
have 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)
Tactic: apply Function.Surjective.comp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
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) (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)
have hf : Epi i.hom
Tactic: rw [← epi_iff_surjective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
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
⊢ 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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
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
have 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
Tactic: refine ⟨fun ⟨t⟩ s hs ↦ ?_, fun h ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun ⟨t⟩ s hs ↦ ?_, fun h ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
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
⊢ (↾fun (x_1 : cs.pt) ↦ x) ≫ c.π.app j = cs.π.app j
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (hypothesis)
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
⊢ IsLimit c
have this : ∀ (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
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
this :
  ∀ (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
⊢ IsLimit c
have refine_2 : (x : (c_1 : Cone F) → (y : c_1.pt) → c.pt) →
  (hx :
      ∀ (c_1 : Cone F) (y : c_1.pt),
        (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 =
                  (↑(sectionOfCone c_1 y) : (j : J) → F.obj j) j)
            (x c_1 y) ∧
          ∀ (y_1 : c.pt),
            (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 =
                      (↑(sectionOfCone c_1 y) : (j : J) → F.obj j) j)
                y_1 →
              y_1 = x c_1 y) →
    IsLimit c
Tactic: choose x hx using fun c y ↦ h _ (sectionOfCone c y).2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c_1 : Cone F
h :
  ∀ s ∈ F.sections,
    ∃! x : c_1.pt,
      ∀ (j : J),
        (hom (FC := TypeCat.Fun) (c_1.π.app j) :
              (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c_1.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
            x =
          s j
this :
  ∀ (c : Cone F) (y : c.pt),
    ∃! x : c_1.pt,
      ∀ (j : J),
        (hom (FC := TypeCat.Fun) (c_1.π.app j) :
              (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c_1.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
            x =
          (↑(sectionOfCone c y) : (j : J) → F.obj j) j
x : (c : Cone F) → (y : c.pt) → c_1.pt
hx :
  ∀ (c : Cone F) (y : c.pt),
    (fun (x : c_1.pt) ↦
          ∀ (j : J),
            (hom (FC := TypeCat.Fun) (c_1.π.app j) :
                  (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c_1.pt).obj j)) →
                    (fun (X : Type u) ↦ X) (F.obj j))
                x =
              (↑(sectionOfCone c y) : (j : J) → F.obj j) j)
        (x c y) ∧
      ∀ (y_1 : c_1.pt),
        (fun (x : c_1.pt) ↦
              ∀ (j : J),
                (hom (FC := TypeCat.Fun) (c_1.π.app j) :
                      (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c_1.pt).obj j)) →
                        (fun (X : Type u) ↦ X) (F.obj j))
                    x =
                  (↑(sectionOfCone c y) : (j : J) → F.obj j) j)
            y_1 →
          y_1 = x c y
c : Cone F
j : J
⊢ (fun (d : Cone F) ↦ ↾x d) c ≫ c_1.π.app j = c.π.app j
have h₁ : ∀ (y : c.pt),
  TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) ((fun (d : Cone F) ↦ ↾x d) c ≫ c_1.π.app j)) y =
    (hom (FC := TypeCat.Fun) (c.π.app j)).toFun y
Tactic: ext y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c_1 : Cone F
h :
  ∀ s ∈ F.sections,
    ∃! x : c_1.pt,
      ∀ (j : J),
        (hom (FC := TypeCat.Fun) (c_1.π.app j) :
              (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c_1.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
            x =
          s j
this :
  ∀ (c : Cone F) (y : c.pt),
    ∃! x : c_1.pt,
      ∀ (j : J),
        (hom (FC := TypeCat.Fun) (c_1.π.app j) :
              (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c_1.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
            x =
          (↑(sectionOfCone c y) : (j : J) → F.obj j) j
x : (c : Cone F) → (y : c.pt) → c_1.pt
hx :
  ∀ (c : Cone F) (y : c.pt),
    (fun (x : c_1.pt) ↦
          ∀ (j : J),
            (hom (FC := TypeCat.Fun) (c_1.π.app j) :
                  (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c_1.pt).obj j)) →
                    (fun (X : Type u) ↦ X) (F.obj j))
                x =
              (↑(sectionOfCone c y) : (j : J) → F.obj j) j)
        (x c y) ∧
      ∀ (y_1 : c_1.pt),
        (fun (x : c_1.pt) ↦
              ∀ (j : J),
                (hom (FC := TypeCat.Fun) (c_1.π.app j) :
                      (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c_1.pt).obj j)) →
                        (fun (X : Type u) ↦ X) (F.obj j))
                    x =
                  (↑(sectionOfCone c y) : (j : J) → F.obj j) j)
            y_1 →
          y_1 = x c y
c : Cone F
f : c.pt ⟶ c_1.pt
hf : ∀ (j : J), f ≫ c_1.π.app j = c.π.app j
⊢ f = (fun (d : Cone F) ↦ ↾x d) c
have h₁ : ∀ (y : c.pt),
  (hom (FC := TypeCat.Fun) f).toFun y =
    TypeCat.Fun.toFun (@hom _ types TypeCat.Fun _ _ _ _ _ ((fun (d : Cone F) ↦ ↾x d) c)) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
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) ↔ Function.Bijective (sectionOfCone c)
have simp_rw : (∀ s ∈ F.sections,
    ∃! x : c.pt,
      ∀ (j : J), (hom (FC := TypeCat.Fun) (c.π.app j) : (a : ((Functor.const J).obj c.pt).obj j) → F.obj j) x = s j) ↔
  Function.Bijective (sectionOfCone c)
Tactic: simp_rw [isLimit_iff, Function.bijective_iff_existsUnique, Subtype.forall, F.sections_ext_iff,
    sectionOfCone]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : Cone F
simp_rw :
  (∀ s ∈ F.sections,
      ∃! x : c.pt,
        ∀ (j : J), (hom (FC := TypeCat.Fun) (c.π.app j) : (a : ((Functor.const J).obj c.pt).obj j) → F.obj j) x = s j) ↔
    Function.Bijective (sectionOfCone c)
⊢ Nonempty (IsLimit c) ↔ Function.Bijective (sectionOfCone c)
have simp_rw₁ : (∀ s ∈ F.sections,
    ∃! x : c.pt,
      ∀ (j : J), (hom (FC := TypeCat.Fun) (c.π.app j) : (a : ((Functor.const J).obj c.pt).obj j) → F.obj j) x = s j) ↔
  ∀ (b : (↑F.sections : Type (max u v))), ∃! a : c.pt, sectionOfCone c a = b
Tactic: simp_rw [isLimit_iff, Function.bijective_iff_existsUnique, Subtype.forall, F.sections_ext_iff,
    sectionOfCone]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : Cone F
simp_rw :
  (∀ s ∈ F.sections,
      ∃! x : c.pt,
        ∀ (j : J), (hom (FC := TypeCat.Fun) (c.π.app j) : (a : ((Functor.const J).obj c.pt).obj j) → F.obj j) x = s j) ↔
    Function.Bijective (sectionOfCone c)
simp_rw₁ :
  (∀ s ∈ F.sections,
      ∃! x : c.pt,
        ∀ (j : J), (hom (FC := TypeCat.Fun) (c.π.app j) : (a : ((Functor.const J).obj c.pt).obj j) → F.obj j) x = s j) ↔
    ∀ (b : (↑F.sections : Type (max u v))), ∃! a : c.pt, sectionOfCone c a = b
⊢ Nonempty (IsLimit c) ↔ Function.Bijective (sectionOfCone c)
have simp_rw₂ : (∀ s ∈ F.sections,
    ∃! x : c.pt,
      ∀ (j : J), (hom (FC := TypeCat.Fun) (c.π.app j) : (a : ((Functor.const J).obj c.pt).obj j) → F.obj j) x = s j) ↔
  ∀ (a : (j : J) → F.obj j) (b : a ∈ F.sections),
    ∃! a_1 : c.pt, sectionOfCone c a_1 = Subtype.mk (p := fun (a : (j : J) → F.obj j) ↦ a ∈ F.sections) a b
Tactic: simp_rw [isLimit_iff, Function.bijective_iff_existsUnique, Subtype.forall, F.sections_ext_iff,
    sectionOfCone]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : Cone F
simp_rw :
  (∀ s ∈ F.sections,
      ∃! x : c.pt,
        ∀ (j : J), (hom (FC := TypeCat.Fun) (c.π.app j) : (a : ((Functor.const J).obj c.pt).obj j) → F.obj j) x = s j) ↔
    Function.Bijective (sectionOfCone c)
simp_rw₁ :
  (∀ s ∈ F.sections,
      ∃! x : c.pt,
        ∀ (j : J), (hom (FC := TypeCat.Fun) (c.π.app j) : (a : ((Functor.const J).obj c.pt).obj j) → F.obj j) x = s j) ↔
    ∀ (b : (↑F.sections : Type (max u v))), ∃! a : c.pt, sectionOfCone c a = b
simp_rw₂ :
  (∀ s ∈ F.sections,
      ∃! x : c.pt,
        ∀ (j : J), (hom (FC := TypeCat.Fun) (c.π.app j) : (a : ((Functor.const J).obj c.pt).obj j) → F.obj j) x = s j) ↔
    ∀ (a : (j : J) → F.obj j) (b : a ∈ F.sections),
      ∃! a_1 : c.pt, sectionOfCone c a_1 = Subtype.mk (p := fun (a : (j : J) → F.obj j) ↦ a ∈ F.sections) a b
⊢ Nonempty (IsLimit c) ↔ Function.Bijective (sectionOfCone c)
have simp_rw₃ : (∀ s ∈ F.sections,
    ∃! x : c.pt,
      ∀ (j : J), (hom (FC := TypeCat.Fun) (c.π.app j) : (a : ((Functor.const J).obj c.pt).obj j) → F.obj j) x = s j) ↔
  ∀ (a : (j : J) → F.obj j) (b : a ∈ F.sections),
    ∃! a_1 : c.pt, ∀ (j : J), (↑(sectionOfCone c a_1) : (j : J) → F.obj j) j = a j
Tactic: simp_rw [isLimit_iff, Function.bijective_iff_existsUnique, Subtype.forall, F.sections_ext_iff,
    sectionOfCone]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : Cone F
t : IsLimit c
x : (↑F.sections : Type (max u v))
j : J
| (↑x : (j : J) → F.obj j) j
have rw : (↑((isLimitEquivSections t).toFun ((isLimitEquivSections t).invFun x)) : (j : J) → F.obj j) j
Tactic: rw [← (isLimitEquivSections t).right_inv x]