awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
Y : C
⊢ Function.LeftInverse
    (fun (u : (X : C) → Unique (X ⟶ Y)) ↦ { lift := fun (s : Cone F) ↦ default, fac := ⋯, uniq := ⋯ })
    fun
      (t :
        IsLimit
          { pt := Y,
            π :=
              {
                app := fun (X : Discrete PEmpty.{1}) ↦
                  id
                    (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ Y ⟶ F.obj x) X fun (as : PEmpty.{1}) ↦
                      ⋯.elim),
                naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) Y) F } :
            Cone F })
      (X : C) ↦
    {
      default :=
        t.lift
          { pt := X,
            π :=
              {
                app := fun (X_1 : Discrete PEmpty.{1}) ↦
                  id
                    (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ X ⟶ F.obj x) X_1
                      fun (as : PEmpty.{1}) ↦ ⋯.elim),
                naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) F } },
      uniq := ⋯ }
have dsimp : ∀
  (x :
    IsLimit
      { pt := Y,
        π :=
          { app := fun (X : Discrete PEmpty.{1}) ↦ sorry.elim, naturality := sorry :
            NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) Y) F } :
        Cone F }),
  { lift := fun (s : Cone F) ↦ default, fac := sorry, uniq := sorry } = x
Tactic: dsimp [Function.LeftInverse]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
Y : C
⊢ Function.RightInverse
    (fun (u : (X : C) → Unique (X ⟶ Y)) ↦ { lift := fun (s : Cone F) ↦ default, fac := ⋯, uniq := ⋯ })
    fun
      (t :
        IsLimit
          { pt := Y,
            π :=
              {
                app := fun (X : Discrete PEmpty.{1}) ↦
                  id
                    (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ Y ⟶ F.obj x) X fun (as : PEmpty.{1}) ↦
                      ⋯.elim),
                naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) Y) F } :
            Cone F })
      (X : C) ↦
    {
      default :=
        t.lift
          { pt := X,
            π :=
              {
                app := fun (X_1 : Discrete PEmpty.{1}) ↦
                  id
                    (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ X ⟶ F.obj x) X_1
                      fun (as : PEmpty.{1}) ↦ ⋯.elim),
                naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) F } },
      uniq := ⋯ }
have dsimp : ∀ (x : (X : C) → Unique (X ⟶ Y)), (fun (X : C) ↦ { default := default, uniq := sorry }) = x
Tactic: dsimp [Function.RightInverse, Function.LeftInverse]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
X : C
⊢ Function.LeftInverse
    (fun (u : (Y : C) → Unique (X ⟶ Y)) ↦ { desc := fun (s : Cocone F) ↦ default, fac := ⋯, uniq := ⋯ })
    fun
      (t :
        IsColimit
          { pt := X,
            ι :=
              {
                app := fun (X_1 : Discrete PEmpty.{1}) ↦
                  id
                    (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X) X_1
                      fun (as : PEmpty.{1}) ↦ ⋯.elim),
                naturality := ⋯ : NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) } :
            Cocone F })
      (X_1 : C) ↦
    {
      default :=
        t.desc
          { pt := X_1,
            ι :=
              {
                app := fun (X_2 : Discrete PEmpty.{1}) ↦
                  id
                    (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X_1) X_2
                      fun (as : PEmpty.{1}) ↦ ⋯.elim),
                naturality := ⋯ : NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X_1) } },
      uniq := ⋯ }
have dsimp : ∀
  (x :
    IsColimit
      { pt := X,
        ι :=
          { app := fun (X_1 : Discrete PEmpty.{1}) ↦ sorry.elim, naturality := sorry :
            NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) } :
        Cocone F }),
  { desc := fun (s : Cocone F) ↦ default, fac := sorry, uniq := sorry :
      IsColimit
        { pt := X,
          ι :=
            { app := fun (X_1 : Discrete PEmpty.{1}) ↦ sorry.elim, naturality := sorry :
              NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) } :
          Cocone F } } =
    x
Tactic: dsimp [Function.LeftInverse]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
t : IsTerminal.{v₁, u₁} X
f : X ⟶ Y
⊢ Mono f
have this : IsSplitMono f
Tactic: haveI := t.isSplitMono_from f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
t : IsInitial.{v₁, u₁} X
f : Y ⟶ X
⊢ Epi f
have this : IsSplitEpi f
Tactic: haveI := t.isSplitEpi_to f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
h : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ f =
    hl.lift
        { pt := c.pt,
          π :=
            {
              app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦
                id
                  (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{w + 1}) ↦ c.pt ⟶ F₁.obj x) X_1
                    fun (as : PEmpty.{w + 1}) ↦ ⋯.elim),
              naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) F₁ } } ≫
      hi.hom
have dsimp : f =
  hl.lift
      { pt := c.pt,
        π :=
          { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ sorry.elim, naturality := sorry :
            NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) F₁ } } ≫
    hi.hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
h : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ f =
    hl.lift
        { pt := c.pt,
          π :=
            { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ ⋯.elim, naturality := ⋯ :
              NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) F₁ } } ≫
      hi.hom
have rw : f = (f ≫ hi.inv) ≫ hi.hom
Tactic: rw [← hl.uniq _ (f ≫ hi.inv) _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
h : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
rw : f = (f ≫ hi.inv) ≫ hi.hom
⊢ f =
    hl.lift
        { pt := c.pt,
          π :=
            { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ ⋯.elim, naturality := ⋯ :
              NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) F₁ } } ≫
      hi.hom
have rw₁ : ∀ (j : Discrete PEmpty.{w + 1}),
  (f ≫ hi.inv) ≫ c₁.π.app j =
    NatTrans.app
      (Cone.π
        { pt := c.pt,
          π :=
            { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ sorry.elim, naturality := sorry :
              NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) F₁ } })
      j
Tactic: rw [← hl.uniq _ (f ≫ hi.inv) _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
h : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ f =
    hi.inv ≫
      hl.desc
        { pt := c.pt,
          ι :=
            {
              app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦
                id
                  (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{w + 1}) ↦ F₁.obj x ⟶ c.pt) X_1
                    fun (as : PEmpty.{w + 1}) ↦ ⋯.elim),
              naturality := ⋯ : NatTrans F₁ (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) } }
have dsimp : f =
  hi.inv ≫
    hl.desc
      { pt := c.pt,
        ι :=
          { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ sorry.elim, naturality := sorry :
            NatTrans F₁ (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) } }
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
h : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ f =
    hi.inv ≫
      hl.desc
        { pt := c.pt,
          ι :=
            { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ ⋯.elim, naturality := ⋯ :
              NatTrans F₁ (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) } }
have rw : f = hi.inv ≫ hi.hom ≫ f
Tactic: rw [← hl.uniq _ (hi.hom ≫ f) _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
h : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
rw : f = hi.inv ≫ hi.hom ≫ f
⊢ f =
    hi.inv ≫
      hl.desc
        { pt := c.pt,
          ι :=
            { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ ⋯.elim, naturality := ⋯ :
              NatTrans F₁ (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) } }
have rw₁ : ∀ (j : Discrete PEmpty.{w + 1}),
  c₁.ι.app j ≫ hi.hom ≫ f =
    NatTrans.app
      (Cocone.ι
        { pt := c.pt,
          ι :=
            { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ sorry.elim, naturality := sorry :
              NatTrans F₁ (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) } })
      j
Tactic: rw [← hl.uniq _ (hi.hom ≫ f) _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : InitialMonoClass.{v₁, u₁} C
I X : C
hI : IsInitial.{v₁, u₁} I
f : I ⟶ X
⊢ Mono f
have rw : Mono (hI.to X)
Tactic: rw [hI.hom_ext f (hI.to X)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : C
hI : IsInitial.{v₁, u₁} I
h : ∀ (X : C), Mono (hI.to X)
I' X : C
hI' : IsInitial.{v₁, u₁} I'
⊢ Mono (hI'.to X)
have rw : Mono ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)
Tactic: rw [hI'.hom_ext (hI'.to X) ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsInitial.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
j j' : J
k : j ⟶ j'
⊢ Functor.map (Functor.obj (Functor.const J) (F.obj X)) k ≫ F.map (tX.to j') = F.map (tX.to j) ≫ F.map k
have dsimp : 𝟙 (F.obj X) ≫ F.map (tX.to j') = F.map (tX.to j) ≫ F.map k
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsInitial.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
j j' : J
k : j ⟶ j'
⊢ 𝟙 (F.obj X) ≫ F.map (tX.to j') = F.map (tX.to j) ≫ F.map k
have rw : 𝟙 (F.obj X) ≫ F.map (tX.to j') = F.map (tX.to j ≫ k)
Tactic: rw [← F.map_comp, Category.id_comp, tX.hom_ext (tX.to j ≫ k) (tX.to j')]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsInitial.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
j j' : J
k : j ⟶ j'
rw : 𝟙 (F.obj X) ≫ F.map (tX.to j') = F.map (tX.to j ≫ k)
⊢ 𝟙 (F.obj X) ≫ F.map (tX.to j') = F.map (tX.to j) ≫ F.map k
have rw₁ : F.map (tX.to j') = F.map (tX.to j ≫ k)
Tactic: rw [← F.map_comp, Category.id_comp, tX.hom_ext (tX.to j ≫ k) (tX.to j')]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsInitial.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
j j' : J
k : j ⟶ j'
rw : 𝟙 (F.obj X) ≫ F.map (tX.to j') = F.map (tX.to j ≫ k)
rw₁ : F.map (tX.to j') = F.map (tX.to j ≫ k)
⊢ 𝟙 (F.obj X) ≫ F.map (tX.to j') = F.map (tX.to j) ≫ F.map k
have rw₂ : F.map (tX.to j') = F.map (tX.to j')
Tactic: rw [← F.map_comp, Category.id_comp, tX.hom_ext (tX.to j ≫ k) (tX.to j')]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsInitial.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ (coneOfDiagramInitial tX F).π.app j = s.π.app j
⊢ m = s.π.app X
have simp_rw : m = m ≫ F.map (𝟙 X)
Tactic: simp_rw [← w X, coneOfDiagramInitial_π_app, tX.hom_ext (tX.to X) (𝟙 _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
hX : IsTerminal.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
inst_2 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
⊢ Functor.map (Functor.obj (Functor.const J) (F.obj X)) f ≫ inv (F.map (hX.from j)) = inv (F.map (hX.from i)) ≫ F.map f
have dsimp : 𝟙 (F.obj X) ≫ inv (F.map (hX.from j)) = inv (F.map (hX.from i)) ≫ F.map f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsTerminal.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
j j' : J
k : j ⟶ j'
⊢ F.map k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ Functor.map (Functor.obj (Functor.const J) (F.obj X)) k
have dsimp : F.map k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsTerminal.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
j j' : J
k : j ⟶ j'
⊢ F.map k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)
have rw : F.map (k ≫ tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)
Tactic: rw [← F.map_comp, Category.comp_id, tX.hom_ext (k ≫ tX.from j') (tX.from j)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsTerminal.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
j j' : J
k : j ⟶ j'
rw : F.map (k ≫ tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)
⊢ F.map k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)
have rw₁ : F.map (k ≫ tX.from j') = F.map (tX.from j)
Tactic: rw [← F.map_comp, Category.comp_id, tX.hom_ext (k ≫ tX.from j') (tX.from j)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsTerminal.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
j j' : J
k : j ⟶ j'
rw : F.map (k ≫ tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)
rw₁ : F.map (k ≫ tX.from j') = F.map (tX.from j)
⊢ F.map k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)
have rw₂ : F.map (tX.from j) = F.map (tX.from j)
Tactic: rw [← F.map_comp, Category.comp_id, tX.hom_ext (k ≫ tX.from j') (tX.from j)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
F : Functor.{v, v₁, u, u₁} J C
c : Cocone F
hc : IsColimit c
X : J
hX : IsTerminal.{v, u} X
⊢ IsIso (c.ι.app X)
have change : IsIso ((colimitOfDiagramTerminal hX F).coconePointUniqueUpToIso hc).hom
Tactic: change IsIso (coconePointUniqueUpToIso (colimitOfDiagramTerminal hX F) hc).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
hX : IsInitial.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
inst_2 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
⊢ F.map f ≫ inv (F.map (hX.to j)) = inv (F.map (hX.to i)) ≫ Functor.map (Functor.obj (Functor.const J) (F.obj X)) f
have dsimp : F.map f ≫ inv (F.map (hX.to j)) = inv (F.map (hX.to i)) ≫ 𝟙 (F.obj X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
F : Functor.{v, v₁, u, u₁} J C
c : Cone F
hc : IsLimit c
X : J
hX : IsInitial.{v, u} X
⊢ IsIso (c.π.app X)
have change : IsIso (hc.conePointUniqueUpToIso (limitOfDiagramInitial hX F)).hom
Tactic: change IsIso (conePointUniqueUpToIso hc (limitOfDiagramInitial hX F)).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal.{v₁, u₁} X
hY : IsTerminal.{v₁, u₁} Y
f : X ⟶ Y
⊢ IsIso f
have refine : f ≫ hX.from Y = 𝟙 X ∧ hX.from Y ≫ f = 𝟙 Y
Tactic: refine ⟨⟨IsTerminal.from hX Y, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal.{v₁, u₁} X
hY : IsTerminal.{v₁, u₁} Y
f : X ⟶ Y
⊢ f ≫ hX.from Y = 𝟙 X ∧ hX.from Y ≫ f = 𝟙 Y
have simp : hX.from Y ≫ f = 𝟙 Y
Tactic: simp only [IsTerminal.comp_from, IsTerminal.from_self, true_and]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
hX : IsInitial.{v₁, u₁} X
hY : IsInitial.{v₁, u₁} Y
f : X ⟶ Y
⊢ IsIso f
have refine : f ≫ hY.to X = 𝟙 X ∧ hY.to X ≫ f = 𝟙 Y
Tactic: refine ⟨⟨IsInitial.to hY X, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
hX : IsInitial.{v₁, u₁} X
hY : IsInitial.{v₁, u₁} Y
f : X ⟶ Y
⊢ f ≫ hY.to X = 𝟙 X ∧ hY.to X ≫ f = 𝟙 Y
have simp : f ≫ hY.to X = 𝟙 X
Tactic: simp only [IsInitial.to_comp, IsInitial.to_self, and_true]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
X : D
hX : IsTerminal.{v_2, u_2} X
X_1 : Functor.{v_1, v_2, u_1, u_2} C D
m : X_1 ⟶ obj (const C) X
⊢ m =
    (fun (Y : Functor.{v_1, v_2, u_1, u_2} C D) ↦
        ({ app := fun (Z : C) ↦ hX.from (Y.obj Z), naturality := ⋯ } : NatTrans Y (obj (const C) X)))
      X_1
have w : ∀ (x : C),
  m.app x =
    NatTrans.app
      ((fun (Y : Functor.{v_1, v_2, u_1, u_2} C D) ↦
          ({ app := fun (Z : C) ↦ hX.from (Y.obj Z), naturality := sorry } : NatTrans Y (obj (const C) X)))
        X_1)
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
X : D
hX : IsInitial.{v_2, u_2} X
Y : Functor.{v_1, v_2, u_1, u_2} C D
m : obj (const C) X ⟶ Y
⊢ m =
    (fun (Y : Functor.{v_1, v_2, u_1, u_2} C D) ↦
        { app := fun (Z : C) ↦ hX.to (Y.obj Z), naturality := ⋯ : NatTrans (obj (const C) X) Y })
      Y
have w : ∀ (x : C),
  m.app x =
    NatTrans.app
      ((fun (Y : Functor.{v_1, v_2, u_1, u_2} C D) ↦
          { app := fun (Z : C) ↦ hX.to (Y.obj Z), naturality := sorry : NatTrans (obj (const C) X) Y })
        Y)
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
⊢ { l : s.pt ⟶ (PullbackCone.mk a b comm).pt //
    l ≫ (PullbackCone.mk a b comm).fst = s.fst ∧
      l ≫ (PullbackCone.mk a b comm).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk a b comm).pt},
          m ≫ (PullbackCone.mk a b comm).fst = s.fst → m ≫ (PullbackCone.mk a b comm).snd = s.snd → m = l }
have refine : ∀ {m : s.pt ⟶ (PullbackCone.mk a b comm).pt} (m₁ : m ≫ (PullbackCone.mk a b comm).fst = s.fst)
  (m₂ : m ≫ (PullbackCone.mk a b comm).snd = s.snd), m = (IsPullback.isLimit big_k).lift s'
Tactic: refine ⟨big_k.isLimit.lift s', big_k.isLimit.fac _ WalkingCospan.left,
          big_k.isLimit.fac _ WalkingCospan.right, fun m₁ m₂ => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
m : s.pt ⟶ (PullbackCone.mk a b comm).pt
m₁ : m ≫ (PullbackCone.mk a b comm).fst = s.fst
m₂ : m ≫ (PullbackCone.mk a b comm).snd = s.snd
⊢ m = (IsPullback.isLimit big_k).lift s'
have apply : ∀ (j : WalkingCospan),
  m ≫ (IsPullback.cone big_k).π.app j = (IsPullback.isLimit big_k).lift s' ≫ (IsPullback.cone big_k).π.app j
Tactic: apply big_k.isLimit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
m : s.pt ⟶ (PullbackCone.mk a b comm).pt
m₁ : m ≫ (PullbackCone.mk a b comm).fst = s.fst
m₂ : m ≫ (PullbackCone.mk a b comm).snd = s.snd
⊢ ∀ (j : WalkingCospan),
    m ≫ (IsPullback.cone big_k).π.app j = (IsPullback.isLimit big_k).lift s' ≫ (IsPullback.cone big_k).π.app j
have refine_1 : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
Tactic: refine (PullbackCone.mk a b ?_ : PullbackCone (f₁ ≫ f₂) _).equalizer_ext ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
m : s.pt ⟶ (PullbackCone.mk a b comm).pt
m₁ : m ≫ (PullbackCone.mk a b comm).fst = s.fst
m₂ : m ≫ (PullbackCone.mk a b comm).snd = s.snd
refine_1 : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
⊢ ∀ (j : WalkingCospan),
    m ≫ (IsPullback.cone big_k).π.app j = (IsPullback.isLimit big_k).lift s' ≫ (IsPullback.cone big_k).π.app j
have refine_2 : m ≫ PullbackCone.fst (PullbackCone.mk a b sorry) =
  (IsPullback.isLimit big_k).lift s' ≫ PullbackCone.fst (PullbackCone.mk a b sorry)
Tactic: refine (PullbackCone.mk a b ?_ : PullbackCone (f₁ ≫ f₂) _).equalizer_ext ?_ ?_