awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
app : (j : J) → G.obj j → F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    app j' ∘
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')) =
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j')) ∘
        app j
j j' : J
f : j ⟶ j'
rw :
  c.ι j' ∘
      app j' ∘
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')) =
    c.ι j ∘ app j
rw₁ :
  c.ι j' ∘
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j')) ∘
        app j =
    c.ι j ∘ app j
rw₂ :
  (c.ι j' ∘
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))) ∘
      app j =
    c.ι j ∘ app j
⊢ (c.ι j' ∘ app j') ∘
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
        (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')) =
    c.ι j ∘ app j
have rw₃ : c.ι j ∘ app j = c.ι j ∘ app j
Tactic: rw [Function.comp_assoc, naturality, ← Function.comp_assoc, ι_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
t : F.ColimitType
⊢ ∃ (j : J) (x : F.obj j), F.ιColimitType j x = t
have mk : ∀ (fst : J) (snd : F.obj fst),
  ∃ (j : J) (x : F.obj j), F.ιColimitType j x = Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) fst snd)
Tactic: obtain ⟨_, _⟩ := t
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
⊢ Function.Surjective (F.descColimitType c) ↔ ∀ (z : c.pt), ∃ (i : J) (x : F.obj i), c.ι i x = z
have mp : Function.Surjective (F.descColimitType c) → ∀ (z : c.pt), ∃ (i : J) (x : F.obj i), c.ι i x = z
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
mp : Function.Surjective (F.descColimitType c) → ∀ (z : c.pt), ∃ (i : J) (x : F.obj i), c.ι i x = z
⊢ Function.Surjective (F.descColimitType c) ↔ ∀ (z : c.pt), ∃ (i : J) (x : F.obj i), c.ι i x = z
have mpr : (∀ (z : c.pt), ∃ (i : J) (x : F.obj i), c.ι i x = z) → Function.Surjective (F.descColimitType c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h : Function.Surjective (F.descColimitType c)
z : c.pt
⊢ ∃ (i : J) (x : F.obj i), c.ι i x = z
have mp : ∀ (w : F.ColimitType) (i : J) (x : F.obj i),
  ∃ (i_1 : J) (x_1 : F.obj i_1),
    c.ι i_1 x_1 = F.descColimitType c (Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) i x))
Tactic: obtain ⟨⟨i, x⟩, rfl⟩ := h z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h : ∀ (z : c.pt), ∃ (i : J) (x : F.obj i), c.ι i x = z
z : c.pt
⊢ ∃ (a : F.ColimitType), F.descColimitType c a = z
have mpr : ∀ (i : J) (x : F.obj i), ∃ (a : F.ColimitType), F.descColimitType c a = c.ι i x
Tactic: obtain ⟨i, x, rfl⟩ := h z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
y : c.pt
⊢ ∃ (j : J) (x : F.obj j), c.ι j x = y
have obtain : ∀ (z : F.ColimitType), ∃ (j : J) (x : F.obj j), c.ι j x = (hc.equiv : (a : F.ColimitType) → c.pt) z
Tactic: obtain ⟨z, rfl⟩ := hc.equiv.surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
z : F.ColimitType
⊢ ∃ (j : J) (x : F.obj j), c.ι j x = (hc.equiv : (a : F.ColimitType) → c.pt) z
have obtain : ∀ (j : J) (x : F.obj j),
  ∃ (j_1 : J) (x_1 : F.obj j_1), c.ι j_1 x_1 = (hc.equiv : (a : F.ColimitType) → c.pt) (F.ιColimitType j x)
Tactic: obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
⊢ f = g
have h₁ : ∀ (y : c.pt), f y = g y
Tactic: funext y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
y : c.pt
⊢ f y = g y
have h₁ : ∀ (j : J) (x : F.obj j), f (c.ι j x) = g (c.ι j x)
Tactic: obtain ⟨j, x, rfl⟩ := hc.ι_jointly_surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
e : Equiv.{w₁ + 1, w₂ + 1} c.pt c'.pt
he : ∀ (j : J) (x : F.obj j), c'.ι j x = (e : (a : c.pt) → c'.pt) (c.ι j x)
⊢ Function.Bijective (F.descColimitType c')
have h : F.descColimitType c' = (⇑e : (a : c.pt) → c'.pt) ∘ F.descColimitType c
Tactic: convert! Function.Bijective.comp e.bijective hc.bijective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
e : Equiv.{w₁ + 1, w₂ + 1} c.pt c'.pt
he : ∀ (j : J) (x : F.obj j), c'.ι j x = (e : (a : c.pt) → c'.pt) (c.ι j x)
⊢ F.descColimitType c' = (⇑e : (a : c.pt) → c'.pt) ∘ F.descColimitType c
have h : ∀ (y : F.ColimitType), F.descColimitType c' y = ((⇑e : (a : c.pt) → c'.pt) ∘ F.descColimitType c) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
e : Equiv.{w₁ + 1, w₂ + 1} c.pt c'.pt
he : ∀ (j : J) (x : F.obj j), c'.ι j x = (e : (a : c.pt) → c'.pt) (c.ι j x)
y : F.ColimitType
⊢ F.descColimitType c' y = ((⇑e : (a : c.pt) → c'.pt) ∘ F.descColimitType c) y
have h : ∀ (j : J) (x : F.obj j),
  F.descColimitType c' (F.ιColimitType j x) = ((⇑e : (a : c.pt) → c'.pt) ∘ F.descColimitType c) (F.ιColimitType j x)
Tactic: obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
⊢ c'.IsColimit ↔ Function.Bijective f
have refine : ∀ (hc' : c'.IsColimit), Function.Bijective f
Tactic: refine ⟨fun hc' ↦ ?_, fun h ↦ hc.of_equiv (Equiv.ofBijective _ h) hf⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (hypothesis)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
⊢ Function.Bijective f
have h₁ : Function.Bijective (F.descColimitType c)
Tactic: have h₁ := hc.bijective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
⊢ Function.Bijective f
have rw : Function.Bijective (f ∘ F.descColimitType c)
Tactic: rw [← Function.Bijective.of_comp_iff _ hc.bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
⊢ Function.Bijective (f ∘ F.descColimitType c)
have h : f ∘ F.descColimitType c = F.descColimitType c'
Tactic: convert! hc'.bijective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
⊢ f ∘ F.descColimitType c = F.descColimitType c'
have h : ∀ (x : F.ColimitType), (f ∘ F.descColimitType c) x = F.descColimitType c' x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
x : F.ColimitType
⊢ (f ∘ F.descColimitType c) x = F.descColimitType c' x
have h : ∀ (j : J) (x : F.obj j), (f ∘ F.descColimitType c) (F.ιColimitType j x) = F.descColimitType c' (F.ιColimitType j x)
Tactic: obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
c' : CoconeTypes.{w₂, w₀, v, u} F
j : J
⊢ (Equiv.toFun Equiv.ulift ∘
        hc.desc
          (c'.postcomp (T := ULift.{w₃, w₂} c'.pt) (⇑(Equiv.symm Equiv.ulift) : (a : c'.pt) → ULift.{w₃, w₂} c'.pt))) ∘
      c.ι j =
    c'.ι j
have rw : Equiv.toFun Equiv.ulift ∘
    (c'.postcomp (T := ULift.{w₃, w₂} c'.pt) (⇑(Equiv.symm Equiv.ulift) : (a : c'.pt) → ULift.{w₃, w₂} c'.pt)).ι j =
  c'.ι j
Tactic: rw [Function.comp_assoc, hc.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
this : Equiv.invFun Equiv.ulift ∘ f = Equiv.invFun Equiv.ulift ∘ g
⊢ f = g
have h₁ : ∀ (x : c.pt), f x = g x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
⊢ f = g
have suffices : Equiv.invFun Equiv.ulift ∘ f = Equiv.invFun Equiv.ulift ∘ g
Tactic: suffices Equiv.ulift.{w₃}.invFun.comp f =
        Equiv.ulift.invFun.comp g by
      ext x
      simpa using congr_fun this x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
c' : CoconeTypes.{w₂, w₀', v, u} G
j : J
⊢ Function.comp (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      (ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j) =
    c'.ι j
have rw : Function.comp.{w₀' + 1, w₁ + 1, w₂ + 1} (β :=
    pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) sorry))
    (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) sorry))
    ((fun (j : J) ↦ (c.ι j ∘ (⇑(e j) : (a : G.obj j) → F.obj j) : G.obj j → c.pt)) j) =
  c'.ι j
Tactic: rw [precompose_ι, ← Function.comp_assoc, hc.fac, precompose_ι, Function.comp_assoc,
      Equiv.symm_comp_self, Function.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
c' : CoconeTypes.{w₂, w₀', v, u} G
j : J
rw :
  Function.comp.{w₀' + 1, w₁ + 1, w₂ + 1} (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      ((fun (j : J) ↦ (c.ι j ∘ (⇑(e j) : (a : G.obj j) → F.obj j) : G.obj j → c.pt)) j) =
    c'.ι j
⊢ Function.comp (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      (ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j) =
    c'.ι j
have rw₁ : Function.comp.{w₀' + 1, w₀ + 1, w₂ + 1} (β := F.obj j)
    (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) sorry) ∘ c.ι j)
    (⇑(e j) : (a : G.obj j) → F.obj j) =
  c'.ι j
Tactic: rw [precompose_ι, ← Function.comp_assoc, hc.fac, precompose_ι, Function.comp_assoc,
      Equiv.symm_comp_self, Function.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
c' : CoconeTypes.{w₂, w₀', v, u} G
j : J
rw :
  Function.comp.{w₀' + 1, w₁ + 1, w₂ + 1} (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      ((fun (j : J) ↦ (c.ι j ∘ (⇑(e j) : (a : G.obj j) → F.obj j) : G.obj j → c.pt)) j) =
    c'.ι j
rw₁ :
  Function.comp.{w₀' + 1, w₀ + 1, w₂ + 1} (β := F.obj j)
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯) ∘ c.ι j)
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
⊢ Function.comp (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      (ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j) =
    c'.ι j
have rw₂ : ι (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) sorry) j ∘ (⇑(e j) : (a : G.obj j) → F.obj j) =
  c'.ι j
Tactic: rw [precompose_ι, ← Function.comp_assoc, hc.fac, precompose_ι, Function.comp_assoc,
      Equiv.symm_comp_self, Function.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
c' : CoconeTypes.{w₂, w₀', v, u} G
j : J
rw :
  Function.comp.{w₀' + 1, w₁ + 1, w₂ + 1} (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      ((fun (j : J) ↦ (c.ι j ∘ (⇑(e j) : (a : G.obj j) → F.obj j) : G.obj j → c.pt)) j) =
    c'.ι j
rw₁ :
  Function.comp.{w₀' + 1, w₀ + 1, w₂ + 1} (β := F.obj j)
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯) ∘ c.ι j)
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
rw₂ :
  ι (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯) j ∘
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
⊢ Function.comp (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      (ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j) =
    c'.ι j
have rw₃ : Function.comp.{w₀' + 1, w₀ + 1, w₂ + 1} (β := F.obj j)
    ((fun (j : J) ↦ (c'.ι j ∘ (⇑(e j).symm : (a : F.obj j) → G.obj j) : F.obj j → c'.pt)) j)
    (⇑(e j) : (a : G.obj j) → F.obj j) =
  c'.ι j
Tactic: rw [precompose_ι, ← Function.comp_assoc, hc.fac, precompose_ι, Function.comp_assoc,
      Equiv.symm_comp_self, Function.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
c' : CoconeTypes.{w₂, w₀', v, u} G
j : J
rw :
  Function.comp.{w₀' + 1, w₁ + 1, w₂ + 1} (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      ((fun (j : J) ↦ (c.ι j ∘ (⇑(e j) : (a : G.obj j) → F.obj j) : G.obj j → c.pt)) j) =
    c'.ι j
rw₁ :
  Function.comp.{w₀' + 1, w₀ + 1, w₂ + 1} (β := F.obj j)
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯) ∘ c.ι j)
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
rw₂ :
  ι (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯) j ∘
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
rw₃ :
  Function.comp.{w₀' + 1, w₀ + 1, w₂ + 1} (β := F.obj j)
      ((fun (j : J) ↦ (c'.ι j ∘ (⇑(e j).symm : (a : F.obj j) → G.obj j) : F.obj j → c'.pt)) j)
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
⊢ Function.comp (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      (ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j) =
    c'.ι j
have rw₄ : c'.ι j ∘
    Function.comp.{w₀' + 1, w₀ + 1, w₀' + 1} (β := F.obj j) (⇑(e j).symm : (a : F.obj j) → G.obj j)
      (⇑(e j) : (a : G.obj j) → F.obj j) =
  c'.ι j
Tactic: rw [precompose_ι, ← Function.comp_assoc, hc.fac, precompose_ι, Function.comp_assoc,
      Equiv.symm_comp_self, Function.comp_id]