awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc : c.IsColimit
s : Cocone F
m : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶ s.pt
hm : ∀ (j : J), NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ m = s.ι.app j
⊢ m =
    ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
      hc.desc ((F.coconeTypesEquiv.symm : (a : Cocone F) → F.CoconeTypes) s) x
have h : ∀ (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)),
  (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾fun
            (x :
              Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
          hc.desc ((F.coconeTypesEquiv.symm : (a : Cocone F) → F.CoconeTypes) s) x))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
⊢ c.IsColimit
have mpr : ∀ (x y : F.ColimitType) (h : F.descColimitType c x = F.descColimitType c y), x = y
Tactic: refine ⟨⟨fun x y h ↦ ?_, fun x ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
mpr : ∀ (x y : F.ColimitType) (h : F.descColimitType c x = F.descColimitType c y), x = y
⊢ c.IsColimit
have mpr₁ : ∀ (x : c.pt), ∃ (a : F.ColimitType), F.descColimitType c a = x
Tactic: refine ⟨⟨fun x y h ↦ ?_, fun x ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : (z : F.ColimitType) → ULift.{u, 0} Bool := fun (z : F.ColimitType) ↦ { down := decide (x = z) }
⊢ x = y
have mpr : f x = f y
Tactic: suffices f x = f y by simpa [f] using this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : (z : F.ColimitType) → ULift.{u, 0} Bool := fun (z : F.ColimitType) ↦ { down := decide (x = z) }
this :
  ∀ (z : F.ColimitType),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (hc.desc
              ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
                (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
          (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
            (fun (X : Type u) ↦ X)
              ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
        (F.descColimitType c z) =
      f z
⊢ f x = f y
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (hc.desc
          ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
      (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
        (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
    (F.descColimitType c x) =
  f y
Tactic: rw [← this x, h, ← this y]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : (z : F.ColimitType) → ULift.{u, 0} Bool := fun (z : F.ColimitType) ↦ { down := decide (x = z) }
this :
  ∀ (z : F.ColimitType),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (hc.desc
              ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
                (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
          (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
            (fun (X : Type u) ↦ X)
              ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
        (F.descColimitType c z) =
      f z
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
              (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
        (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
          (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
      (F.descColimitType c x) =
    f y
⊢ f x = f y
have rw₁ : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (hc.desc
          ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
      (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
        (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
    (F.descColimitType c y) =
  f y
Tactic: rw [← this x, h, ← this y]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : (z : F.ColimitType) → ULift.{u, 0} Bool := fun (z : F.ColimitType) ↦ { down := decide (x = z) }
⊢ f x = f y
have mpr : ∀ (z : F.ColimitType),
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
              (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
        (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
          (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
      (F.descColimitType c z) =
    f z
Tactic: suffices ∀ z, hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f))
          (F.descColimitType c z) = f z by rw [← this x, h, ← this y]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : (z : F.ColimitType) → ULift.{u, 0} Bool := fun (z : F.ColimitType) ↦ { down := decide (x = z) }
z : F.ColimitType
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
              (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
        (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
          (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
      (F.descColimitType c z) =
    f z
have mpr : ∀ (j : J) (z : F.obj j),
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
              (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
        (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
          (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
      (F.descColimitType c (F.ιColimitType j z)) =
    f (F.ιColimitType j z)
Tactic: obtain ⟨j, z, rfl⟩ := F.ιColimitType_jointly_surjective z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (hypothesis)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x : c.pt
f₁ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := true }
f₂ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := decide (∃ (a : F.ColimitType), F.descColimitType c a = x) }
this : f₁ = f₂
⊢ ∃ (a : F.ColimitType), F.descColimitType c a = x
have this₁ : Eq (α := ULift.{u, 0} Bool)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
        (a : ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) → ULift.{u, 0} Bool)
      x :
    ULift.{u, 0} Bool)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
        (a : ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) → ULift.{u, 0} Bool)
      x :
    ULift.{u, 0} Bool)
Tactic: have := ConcreteCategory.congr_hom this x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x : c.pt
f₁ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := true }
f₂ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := decide (∃ (a : F.ColimitType), F.descColimitType c a = x) }
⊢ ∃ (a : F.ColimitType), F.descColimitType c a = x
have mpr : f₁ = f₂
Tactic: suffices f₁ = f₂ by
        have := ConcreteCategory.congr_hom this x
        simpa [f₁, f₂] using this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x : c.pt
f₁ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := true }
f₂ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := decide (∃ (a : F.ColimitType), F.descColimitType c a = x) }
⊢ f₁ = f₂
have mpr : ∀ (j : J),
  Eq.{u + 1} (α := F.obj j ⟶ ULift.{u, 0} Bool)
    (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ f₁)
    (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ f₂)
Tactic: refine hc.hom_ext fun j => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x : c.pt
f₁ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := true }
f₂ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := decide (∃ (a : F.ColimitType), F.descColimitType c a = x) }
j : J
⊢ Eq.{u + 1} (α := F.obj j ⟶ ULift.{u, 0} Bool)
    (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ f₁)
    (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ f₂)
have mpr : ∀ (x : F.obj j),
  Eq (α := Bool)
    (ULift.down.{u, 0}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ f₁))
        x))
    (ULift.down.{u, 0}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ f₂))
        x))
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
⊢ c.IsColimit
have mpr : ∀ (x y : F.ColimitType) (h : F.descColimitType c x = F.descColimitType c y), x = y
Tactic: classical
    refine ⟨⟨fun x y h ↦ ?_, fun x ↦ ?_⟩⟩
    · let f (z : F.ColimitType) : ULift.{u} Bool := ULift.up (x = z)
      suffices f x = f y by simpa [f] using this
      suffices ∀ z, hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f))
          (F.descColimitType c z) = f z by rw [← this x, h, ← this y]
      intro z
      obtain ⟨j, z, rfl⟩ := F.ιColimitType_jointly_surjective z
      exact ConcreteCategory.congr_hom (hc.fac _ j) z
    · let f₁ : (F.coconeTypesEquiv c).pt ⟶ (ULift.{u} Bool) :=
        ↾fun _ => ULift.up true
      let f₂ : (F.coconeTypesEquiv c).pt ⟶ (ULift.{u} Bool) :=
        ↾fun x => ULift.up (∃ a, F.descColimitType c a = x)
      suffices f₁ = f₂ by
        have := ConcreteCategory.congr_hom this x
        simpa [f₁, f₂] using this
      refine hc.hom_ext fun j => ?_
      ext x
      simpa [f₁, f₂] using ⟨F.ιColimitType j x, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
mpr : ∀ (x y : F.ColimitType) (h : F.descColimitType c x = F.descColimitType c y), x = y
⊢ c.IsColimit
have mpr₁ : ∀ (x : c.pt), ∃ (a : F.ColimitType), F.descColimitType c a = x
Tactic: classical
    refine ⟨⟨fun x y h ↦ ?_, fun x ↦ ?_⟩⟩
    · let f (z : F.ColimitType) : ULift.{u} Bool := ULift.up (x = z)
      suffices f x = f y by simpa [f] using this
      suffices ∀ z, hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f))
          (F.descColimitType c z) = f z by rw [← this x, h, ← this y]
      intro z
      obtain ⟨j, z, rfl⟩ := F.ιColimitType_jointly_surjective z
      exact ConcreteCategory.congr_hom (hc.fac _ j) z
    · let f₁ : (F.coconeTypesEquiv c).pt ⟶ (ULift.{u} Bool) :=
        ↾fun _ => ULift.up true
      let f₂ : (F.coconeTypesEquiv c).pt ⟶ (ULift.{u} Bool) :=
        ↾fun x => ULift.up (∃ a, F.descColimitType c a = x)
      suffices f₁ = f₂ by
        have := ConcreteCategory.congr_hom this x
        simpa [f₁, f₂] using this
      refine hc.hom_ext fun j => ?_
      ext x
      simpa [f₁, f₂] using ⟨F.ιColimitType j x, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j : J
x : F.obj j
⊢ (colimitEquivColimitType F : (a : colimit F) → F.ColimitType)
      ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x) =
    Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j x)
have a : Eq.{u + 1} (α := colimit F)
  ((Equiv.symm (colimitEquivColimitType F) : (a : F.ColimitType) → colimit F)
      ((colimitEquivColimitType F : (a : colimit F) → F.ColimitType)
        ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
          x)) :
    colimit F)
  ((Equiv.symm (colimitEquivColimitType F) : (a : F.ColimitType) → colimit F)
      (Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j x)) :
    colimit F)
Tactic: apply (colimitEquivColimitType F).symm.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j j' : J
x : F.obj j
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j') :
          (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (colimit F))
        ((hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj j'))
            x :
          (fun (X : Type u) ↦ X) (F.obj j')) :
      (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))
have rw : Eq (α := (fun (X : Type u) ↦ X) (colimit F))
  ((hom (FC := TypeCat.Fun) (F.map f ≫ colimit.ι F j') : (a : (fun (X : Type u) ↦ X) (F.obj j)) → colimit F) x :
    colimit F)
  ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
        (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
      x :
    (fun (X : Type u) ↦ X) (colimit F))
Tactic: rw [← comp_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
f : j ⟶ j'
w :
  (hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj j')) x =
    x'
⊢ Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j') :
          (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (colimit F))
        x' :
      (fun (X : Type u) ↦ X) (colimit F))
have rw : Eq (α := (fun (X : Type u) ↦ X) (colimit F))
  ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
        (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
      x :
    (fun (X : Type u) ↦ X) (colimit F))
  ((hom (FC := TypeCat.Fun) (colimit.ι F j') :
        (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (colimit F))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj j'))
          x :
        (fun (X : Type u) ↦ X) (F.obj j')) :
    (fun (X : Type u) ↦ X) (colimit F))
Tactic: rw [← w, colimit.w_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
f : j ⟶ j'
w :
  (hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj j')) x =
    x'
rw :
  Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j') :
          (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (colimit F))
        ((hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj j'))
            x :
          (fun (X : Type u) ↦ X) (F.obj j')) :
      (fun (X : Type u) ↦ X) (colimit F))
⊢ Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j') :
          (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (colimit F))
        x' :
      (fun (X : Type u) ↦ X) (colimit F))
have rw₁ : Eq (α := (fun (X : Type u) ↦ X) (colimit F))
  ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
        (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
      x :
    (fun (X : Type u) ↦ X) (colimit F))
  ((hom (FC := TypeCat.Fun) (colimit.ι F j) : (a : F.obj j) → colimit F) x : colimit F)
Tactic: rw [← w, colimit.w_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
j'' : J
f : j ⟶ j''
f' : j' ⟶ j''
w :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj j''))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj j''))
        x :
      (fun (X : Type u) ↦ X) (F.obj j''))
    ((hom (FC := TypeCat.Fun) (F.map f') : (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (F.obj j''))
        x' :
      (fun (X : Type u) ↦ X) (F.obj j''))
⊢ Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j') :
          (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (colimit F))
        x' :
      (fun (X : Type u) ↦ X) (colimit F))
have rw : Eq (α := (fun (X : Type u) ↦ X) (colimit F))
  ((hom (FC := TypeCat.Fun) (colimit.ι F j'') : (a : F.obj j'') → colimit F)
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj j) → F.obj j'') x : F.obj j'') :
    colimit F)
  ((hom (FC := TypeCat.Fun) (colimit.ι F j') :
        (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (colimit F))
      x' :
    (fun (X : Type u) ↦ X) (colimit F))
Tactic: rw [← colimit.w_apply _ f, ← colimit.w_apply _ f', w]