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)
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''))
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))
⊢ 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 : 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)
Tactic: rw [← colimit.w_apply _ f, ← colimit.w_apply _ f', w]
-- 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''))
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))
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 : 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)
⊢ 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 : (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'')) :
    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)
Tactic: rw [← colimit.w_apply _ f, ← colimit.w_apply _ f', w]
-- 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'
w :
  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))
⊢ Relation.EqvGen F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j x)
    (Sigma.mk (β := fun (j : J) ↦ F.obj j) j' x')
have apply : Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j x) =
  Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j' x')
Tactic: apply Quot.eq.1
-- 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)
t : Cocone F
h : IsColimit t
x : t.pt
⊢ ∃ (j : J) (y : (fun (X : Type u) ↦ X) (F.obj j)),
    (hom (FC := TypeCat.Fun) (t.ι.app j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
        y =
      x
have by_contra : ∀
  (hx :
    ¬∃ (j : J) (y : (fun (X : Type u) ↦ X) (F.obj j)),
        (hom (FC := TypeCat.Fun) (t.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
            y =
          x),
  False
Tactic: by_contra hx
-- 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)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ¬∃ (j : J) (y : (fun (X : Type u) ↦ X) (F.obj j)),
      (hom (FC := TypeCat.Fun) (t.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
          y =
        x
⊢ False
have hx₁ : ∀ (x_1 : J) (x_2 : F.obj x_1),
  ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
Tactic: simp_rw [not_exists] at hx
Cleared hypotheses: hx
-- 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)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
⊢ False
have apply : Eq.{u + 1} (α := t.pt ⟶ ULift.{u, 0} Prop) (↾fun (x : t.pt) ↦ { down := True }) (↾fun (y : t.pt) ↦ { down := y ≠ x })
Tactic: apply (_ : (↾fun _ ↦ ULift.up True :
      t.pt ⟶ (ULift.{u} Prop)) ≠
    (↾fun y ↦ ULift.up (y ≠ 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)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
apply :
  Eq.{u + 1} (α := t.pt ⟶ ULift.{u, 0} Prop) (↾fun (x : t.pt) ↦ { down := True }) (↾fun (y : t.pt) ↦ { down := y ≠ x })
⊢ False
have apply₁ : Ne.{u + 1} (α := t.pt ⟶ ULift.{u, 0} Prop) (↾fun (x : t.pt) ↦ { down := True }) (↾fun (y : t.pt) ↦ { down := y ≠ x })
Tactic: apply (_ : (↾fun _ ↦ ULift.up True :
      t.pt ⟶ (ULift.{u} Prop)) ≠
    (↾fun y ↦ ULift.up (y ≠ 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)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
⊢ Eq.{u + 1} (α := t.pt ⟶ ULift.{u, 0} Prop) (↾fun (x : t.pt) ↦ { down := True }) (↾fun (y : t.pt) ↦ { down := y ≠ x })
have refine : ∀ (j : J),
  Eq (α := F.obj j ⟶ ULift.{u, 0} Prop) (t.ι.app j ≫ ↾fun (x : t.pt) ↦ { down := True })
    (t.ι.app j ≫ ↾fun (y : t.pt) ↦ { down := y ≠ x })
Tactic: refine h.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)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
j : J
⊢ Eq (α := F.obj j ⟶ ULift.{u, 0} Prop) (t.ι.app j ≫ ↾fun (x : t.pt) ↦ { down := True })
    (t.ι.app j ≫ ↾fun (y : t.pt) ↦ { down := y ≠ x })
have h₁ : ∀ (y : F.obj j),
  ULift.down.{u, 0}
      (TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (t.ι.app j ≫ ↾fun (x : t.pt) ↦ { down := True : ULift.{u, 0} Prop }))
        y) ↔
    ULift.down.{u, 0}
      (TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (t.ι.app j ≫ ↾fun (y : t.pt) ↦ { down := y ≠ x : ULift.{u, 0} Prop }))
        y)
Tactic: ext 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)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
j : J
y : F.obj j
⊢ ULift.down.{u, 0}
      (TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (t.ι.app j ≫ ↾fun (x : t.pt) ↦ { down := True : ULift.{u, 0} Prop }))
        y) ↔
    ULift.down.{u, 0}
      (TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (t.ι.app j ≫ ↾fun (y : t.pt) ↦ { down := y ≠ x : ULift.{u, 0} Prop }))
        y)
have h₁ : ¬(hom (FC := TypeCat.Fun) (t.ι.app j) : (a : F.obj j) → t.pt) y = x
Tactic: simp only [Functor.const_obj_obj, TypeCat.Fun.toFun_apply, comp_apply, hom_ofHom,
      TypeCat.Fun.coe_mk, ne_eq, true_iff]
-- 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)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
he :
  Eq.{u + 1} (α := t.pt ⟶ ULift.{u, 0} Prop) (↾fun (x : t.pt) ↦ { down := True }) (↾fun (y : t.pt) ↦ { down := y ≠ x })
⊢ False
have this : Eq (α := ULift.{u, 0} Prop)
  ((hom (FC := TypeCat.Fun) (↾fun (x : t.pt) ↦ { down := True : ULift.{u, 0} Prop }) : (a : t.pt) → ULift.{u, 0} Prop)
      x :
    ULift.{u, 0} Prop)
  ((hom (FC := TypeCat.Fun) (↾fun (y : t.pt) ↦ { down := y ≠ x : ULift.{u, 0} Prop }) : (a : t.pt) → ULift.{u, 0} Prop)
      x :
    ULift.{u, 0} Prop)
Tactic: have := ConcreteCategory.congr_hom he x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
i j : C
f : { as := i : Discrete C } ⟶ { as := j }
⊢ Eq (α := Functor.obj (Discrete.functor F) { as := i : Discrete C } → (i : C) × F i)
    ((fun (x : Functor.obj (Discrete.functor F) { as := j : Discrete C }) ↦
        match (motive := (x : Discrete C) → (x : Functor.obj (Discrete.functor F) x) → (i : C) × F i) { as := j },
          x with
        | { as := i }, x => Sigma.mk (β := fun (i : C) ↦ F i) i x) ∘
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Discrete.functor F) f)) :
        (a : (fun (X : Type v) ↦ X) ((Discrete.functor F).obj { as := i })) →
          (fun (X : Type v) ↦ X) ((Discrete.functor F).obj { as := j })))
    fun (x : Functor.obj (Discrete.functor F) { as := i : Discrete C }) ↦
    match (motive := (x : Discrete C) → (x : Functor.obj (Discrete.functor F) x) → (i : C) × F i) { as := i }, x with
    | { as := i }, x => Sigma.mk (β := fun (i : C) ↦ F i) i x
have obtain : ∀ (f : { as := i : Discrete C } ⟶ { as := i }),
  Eq (α := Functor.obj (Discrete.functor F) { as := i : Discrete C } → (i : C) × F i)
    ((fun (x : Functor.obj (Discrete.functor F) { as := i : Discrete C }) ↦
        match (motive := (x : Discrete C) → (x : Functor.obj (Discrete.functor F) x) → (i : C) × F i) { as := i },
          x with
        | { as := i }, x => Sigma.mk (β := fun (i : C) ↦ F i) i x) ∘
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Discrete.functor F) f)) :
        (a : (fun (X : Type v) ↦ X) ((Discrete.functor F).obj { as := i })) →
          (fun (X : Type v) ↦ X) ((Discrete.functor F).obj { as := i })))
    fun (x : Functor.obj (Discrete.functor F) { as := i : Discrete C }) ↦
    match (motive := (x : Discrete C) → (x : Functor.obj (Discrete.functor F) x) → (i : C) × F i) { as := i }, x with
    | { as := i }, x => Sigma.mk (β := fun (i : C) ↦ F i) i x
Tactic: obtain rfl : i = j := by simpa using Discrete.eq_of_hom f
Cleared hypotheses: j, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
h₁ : ∀ (x : c.pt), ∃ (i : C) (y : F i), c.inj (F := F) i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj (F := F) i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj (F := F) i x = c.inj (F := F) j y → i = j
⊢ Function.Bijective (Functor.descColimitType (Discrete.functor F) c)
have left : Function.Injective (Functor.descColimitType (Discrete.functor F) c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
h₁ : ∀ (x : c.pt), ∃ (i : C) (y : F i), c.inj (F := F) i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj (F := F) i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj (F := F) i x = c.inj (F := F) j y → i = j
left : Function.Injective (Functor.descColimitType (Discrete.functor F) c)
⊢ Function.Bijective (Functor.descColimitType (Discrete.functor F) c)
have right : Function.Surjective (Functor.descColimitType (Discrete.functor F) c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
h₁ : ∀ (x : c.pt), ∃ (i : C) (y : F i), c.inj (F := F) i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj (F := F) i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj (F := F) i x = c.inj (F := F) j y → i = j
x y : Functor.ColimitType (Discrete.functor F)
h : Functor.descColimitType (Discrete.functor F) c x = Functor.descColimitType (Discrete.functor F) c y
⊢ x = y
have left : ∀ (i : C) (x : Functor.obj (Discrete.functor F) { as := i : Discrete C })
  (h :
    Functor.descColimitType (Discrete.functor F) c
        (Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x) =
      Functor.descColimitType (Discrete.functor F) c y),
  Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x = y
Tactic: obtain ⟨⟨i⟩, x, rfl⟩ := (Discrete.functor F).ιColimitType_jointly_surjective x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
h₁ : ∀ (x : c.pt), ∃ (i : C) (y : F i), c.inj (F := F) i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj (F := F) i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj (F := F) i x = c.inj (F := F) j y → i = j
y : Functor.ColimitType (Discrete.functor F)
i : C
x : Functor.obj (Discrete.functor F) { as := i : Discrete C }
h :
  Functor.descColimitType (Discrete.functor F) c
      (Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x) =
    Functor.descColimitType (Discrete.functor F) c y
⊢ Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x = y
have left : ∀ (j : C) (y : Functor.obj (Discrete.functor F) { as := j : Discrete C })
  (h :
    Functor.descColimitType (Discrete.functor F) c
        (Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x) =
      Functor.descColimitType (Discrete.functor F) c (Functor.ιColimitType (Discrete.functor F) { as := j } y)),
  Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x =
    Functor.ιColimitType (Discrete.functor F) { as := j } y
Tactic: obtain ⟨⟨j⟩, y, rfl⟩ := (Discrete.functor F).ιColimitType_jointly_surjective y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
h₁ : ∀ (x : c.pt), ∃ (i : C) (y : F i), c.inj (F := F) i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj (F := F) i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj (F := F) i x = c.inj (F := F) j y → i = j
i : C
x : Functor.obj (Discrete.functor F) { as := i : Discrete C }
j : C
y : Functor.obj (Discrete.functor F) { as := j : Discrete C }
h :
  Functor.descColimitType (Discrete.functor F) c
      (Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x) =
    Functor.descColimitType (Discrete.functor F) c (Functor.ιColimitType (Discrete.functor F) { as := j } y)
⊢ Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x =
    Functor.ιColimitType (Discrete.functor F) { as := j } y
have left : ∀ (y : Functor.obj (Discrete.functor F) { as := i : Discrete C })
  (h :
    Functor.descColimitType (Discrete.functor F) c
        (Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x) =
      Functor.descColimitType (Discrete.functor F) c (Functor.ιColimitType (Discrete.functor F) { as := i } y)),
  Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x =
    Functor.ιColimitType (Discrete.functor F) { as := i } y
Tactic: obtain rfl := h₃ _ _ _ _ h
Cleared hypotheses: j, y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
h₁ : ∀ (x : c.pt), ∃ (i : C) (y : F i), c.inj (F := F) i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj (F := F) i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj (F := F) i x = c.inj (F := F) j y → i = j
i : C
x y : Functor.obj (Discrete.functor F) { as := i : Discrete C }
h :
  Functor.descColimitType (Discrete.functor F) c
      (Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x) =
    Functor.descColimitType (Discrete.functor F) c (Functor.ιColimitType (Discrete.functor F) { as := i } y)
⊢ Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x =
    Functor.ιColimitType (Discrete.functor F) { as := i } y
have left : ∀
  (h :
    Functor.descColimitType (Discrete.functor F) c
        (Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x) =
      Functor.descColimitType (Discrete.functor F) c (Functor.ιColimitType (Discrete.functor F) { as := i } x)),
  Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x =
    Functor.ιColimitType (Discrete.functor F) { as := i } x
Tactic: obtain rfl := h₂ _ h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
h₁ : ∀ (x : c.pt), ∃ (i : C) (y : F i), c.inj (F := F) i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj (F := F) i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj (F := F) i x = c.inj (F := F) j y → i = j
x : c.pt
⊢ ∃ (a : Functor.ColimitType (Discrete.functor F)), Functor.descColimitType (Discrete.functor F) c a = x
have right : ∀ (i : C) (y : F i),
  ∃ (a : Functor.ColimitType (Discrete.functor F)),
    Functor.descColimitType (Discrete.functor F) c a = c.inj (F := F) i y
Tactic: obtain ⟨i, y, rfl⟩ := h₁ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (hypothesis)
Goal:
C : Type u
F : C → Type v
x : C
x_1 x_2 : F x
h : (sigma F).inj (F := F) x x_1 = (sigma F).inj (F := F) x x_2
⊢ x_1 = x_2
have h₁ : ((sigma F).inj (F := F) x x_1).fst (β := fun (i : C) ↦ F i) =
    ((sigma F).inj (F := F) x x_2).fst (β := fun (i : C) ↦ F i) ∧
  ((sigma F).inj (F := F) x x_1).snd (β := fun (i : C) ↦ F i) ≍
    ((sigma F).inj (F := F) x x_2).snd (β := fun (i : C) ↦ F i)
Tactic: rw [Sigma.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
⊢ Functor.CoconeTypes.IsColimit c ↔ Function.Bijective (fromSigma F c)
have hf : ∀ (j : Discrete C) (x : Functor.obj (Discrete.functor F) j), c.ι j x = fromSigma F c ((sigma F).ι j x)
Tactic: rw [(isColimit_sigma F).iff_bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
x : c.pt
⊢ ∃ (i : C) (y : F i), c.inj (F := F) i y = x
have obtain : ∀ (i : C) (y : Functor.obj (Discrete.functor F) { as := i : Discrete C }),
  ∃ (i_1 : C) (y_1 : F i_1), c.inj (F := F) i_1 y_1 = c.ι { as := i } y
Tactic: obtain ⟨⟨i⟩, y, rfl⟩ := hc.ι_jointly_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h : i₁ = i₂
⊢ F i₁ = F i₂
have rw : F i₂ = F i₂
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h : ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁
h₁ : i₁ = i₂
h₂ : y₂ = cast ⋯ y₁
⊢ c.inj (F := F) i₁ y₁ = c.inj (F := F) i₂ y₂
have subst : ∀ (y₂ : F i₁), (∃ (h : i₁ = i₁), y₂ = cast sorry y₂) → c.inj (F := F) i₁ y₂ = c.inj (F := F) i₁ y₂
Tactic: subst h₁ h₂
Cleared hypotheses: i₂, y₁, y₂, h, h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
⊢ c.inj (F := F) i₁ y₁ = c.inj (F := F) i₂ y₂ ↔ ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁
have refine : ∀ (h : c.inj (F := F) i₁ y₁ = c.inj (F := F) i₂ y₂), ∃ (h : i₁ = i₂), y₂ = cast sorry y₁
Tactic: refine ⟨fun h ↦ ?_, fun ⟨h₁, h₂⟩ ↦ by subst h₁ h₂; rfl⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h : c.inj (F := F) i₁ y₁ = c.inj (F := F) i₂ y₂
⊢ ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁
have obtain : ∀ (y₂ : F i₁) (h : c.inj (F := F) i₁ y₁ = c.inj (F := F) i₁ y₂), ∃ (h : i₁ = i₁), y₂ = cast sorry y₁
Tactic: obtain rfl := eq_of_inj_apply_eq_of_isColimit hc _ _ h
Cleared hypotheses: i₂, y₂, h