awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : Cone F
t : IsLimit c
x : (↑F.sections : Type (max u v))
j : J
⊢ (hom (FC := TypeCat.Fun) (c.π.app j) : (a : c.pt) → F.obj j)
      (((isLimitEquivSections t).symm : (a : (↑F.sections : Type (max u v))) → c.pt) x : c.pt) =
    (↑x : (j : J) → F.obj j) j
have conv_rhs : (hom (FC := TypeCat.Fun) (c.π.app j) : (a : c.pt) → F.obj j)
    (((isLimitEquivSections t).symm : (a : (↑F.sections : Type (max u v))) → c.pt) x : c.pt) =
  (↑((isLimitEquivSections t).toFun ((isLimitEquivSections t).invFun x)) : (j : J) → F.obj j) j
Tactic: conv_rhs => rw [← (isLimitEquivSections t).right_inv x]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : Small.{u, max u v} (↑F.sections : Type (max u v))
x : Cone F
x_1 : x.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x_1 ≫ (limitCone F).π.app j = x.π.app j
⊢ x_1 =
    ↾fun (v : x.pt) ↦
      (equivShrink (↑F.sections : Type (max u v)) :
          (a : (↑F.sections : Type (max u v))) → Shrink.{u, max u v} (↑F.sections : Type (max u v)))
        (Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
          (fun (j : J) ↦
            (hom (FC := TypeCat.Fun) (x.π.app j) :
                (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj x.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
              v)
          ⋯)
have h : ∀ (x_2 : x.pt) (j : J),
  Eq.{u + 1} (α := F.obj j)
    ((↑((Equiv.symm (equivShrink (↑F.sections : Type (max u v))) :
              (a : Shrink.{u, max u v} (↑F.sections : Type (max u v))) → (↑F.sections : Type (max u v)))
            ((hom (FC := TypeCat.Fun) x_1).toFun x_2)) :
        (j : J) → F.obj j)
      j)
    ((↑((Equiv.symm (equivShrink (↑F.sections : Type (max u v))) :
              (a : Shrink.{u, max u v} (↑F.sections : Type (max u v))) → (↑F.sections : Type (max u v)))
            (TypeCat.Fun.toFun
              (hom (FC := TypeCat.Fun)
                (↾fun (v : x.pt) ↦
                  (equivShrink (↑F.sections : Type (max u v)) :
                      (a : (↑F.sections : Type (max u v))) → Shrink.{u, max u v} (↑F.sections : Type (max u v)))
                    (Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
                      (fun (j : J) ↦
                        (hom (FC := TypeCat.Fun) (x.π.app j) :
                            (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj x.pt).obj j)) →
                              (fun (X : Type u) ↦ X) (F.obj j))
                          v)
                      sorry)))
              x_2)) :
        (j : J) → F.obj j)
      j)
Tactic: ext x j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ Type (max v u)
x : Cone F
x_1 : x.pt ⟶ (limitCone.{v, u, w} F).pt
w : ∀ (j : J), x_1 ≫ (limitCone.{v, u, w} F).π.app j = x.π.app j
⊢ x_1 =
    ↾fun (v : x.pt) ↦
      Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
        (fun (j : J) ↦
          (hom (FC := TypeCat.Fun) (x.π.app j) :
              (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj x.pt).obj j)) →
                (fun (X : Type (max u v)) ↦ X) (F.obj j))
            v)
        ⋯
have h : ∀ (x_2 : x.pt),
  (hom (FC := TypeCat.Fun) x_1).toFun x_2 =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (↾fun (v : x.pt) ↦
          Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
            (fun (j : J) ↦
              (hom (FC := TypeCat.Fun) (x.π.app j) :
                  (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj x.pt).obj j)) →
                    (fun (X : Type (max u v)) ↦ X) (F.obj j))
                v)
            sorry))
      x_2
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ Type (max v u)
x_1 : Cone F
x_2 : x_1.pt ⟶ (limitCone.{v, u, w} F).pt
w : ∀ (j : J), x_2 ≫ (limitCone.{v, u, w} F).π.app j = x_1.π.app j
x : x_1.pt
⊢ (hom (FC := TypeCat.Fun) x_2).toFun x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (↾fun (v : x_1.pt) ↦
          Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
            (fun (j : J) ↦
              (hom (FC := TypeCat.Fun) (x_1.π.app j) :
                  (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj x_1.pt).obj j)) →
                    (fun (X : Type (max u v)) ↦ X) (F.obj j))
                v)
            ⋯))
      x
have h : (↑((hom (FC := TypeCat.Fun) x_2).toFun x) : (j : J) → F.obj j) =
  (↑(TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (↾fun (v : x_1.pt) ↦
            Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
              (fun (j : J) ↦
                (hom (FC := TypeCat.Fun) (x_1.π.app j) :
                    (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj x_1.pt).obj j)) →
                      (fun (X : Type (max u v)) ↦ X) (F.obj j))
                  v)
              sorry))
        x) :
    (j : J) → F.obj j)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ Type (max v u)
x_1 : Cone F
x_2 : x_1.pt ⟶ (limitCone.{v, u, w} F).pt
w : ∀ (j : J), x_2 ≫ (limitCone.{v, u, w} F).π.app j = x_1.π.app j
x : x_1.pt
⊢ (↑((hom (FC := TypeCat.Fun) x_2).toFun x) : (j : J) → F.obj j) =
    (↑(TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun)
            (↾fun (v : x_1.pt) ↦
              Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
                (fun (j : J) ↦
                  (hom (FC := TypeCat.Fun) (x_1.π.app j) :
                      (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj x_1.pt).obj j)) →
                        (fun (X : Type (max u v)) ↦ X) (F.obj j))
                    v)
                ⋯))
          x) :
      (j : J) → F.obj j)
have h : ∀ (j : J),
  (↑((hom (FC := TypeCat.Fun) x_2).toFun x) : (j : J) → F.obj j) j =
    (↑(TypeCat.Fun.toFun
            (hom (FC := TypeCat.Fun)
              (↾fun (v : x_1.pt) ↦
                Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
                  (fun (j : J) ↦
                    (hom (FC := TypeCat.Fun) (x_1.π.app j) :
                        (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj x_1.pt).obj j)) →
                          (fun (X : Type (max u v)) ↦ X) (F.obj j))
                      v)
                  sorry))
            x) :
        (j : J) → F.obj j)
      j
Tactic: funext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
X Y : J ⥤ Type (max u v)
f : X ⟶ Y
⊢ Eq (α := Functor.obj lim X ⟶ Functor.obj (Functor.sectionsFunctor J) Y)
    (Functor.map lim f ≫
      Iso.hom
        ((fun (F : J ⥤ Type (max u v)) ↦
            (Equiv.toIso (limitEquivSections F) : limit F ≅ (↑F.sections : Type (max u v))))
          Y))
    (Iso.hom
        ((fun (F : J ⥤ Type (max u v)) ↦
            (Equiv.toIso (limitEquivSections F) : limit F ≅ (↑F.sections : Type (max u v))))
          X) ≫
      Functor.map (Functor.sectionsFunctor J) f)
have h : ∀ (x : Functor.obj lim X),
  Eq (α := Functor.obj (Functor.sectionsFunctor J) Y)
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (Functor.map lim f ≫
          Iso.hom
            ((fun (F : J ⥤ Type (max u v)) ↦
                (Equiv.toIso (limitEquivSections F) : limit F ≅ (↑F.sections : Type (max u v))))
              Y)))
      x)
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (F : J ⥤ Type (max u v)) ↦
                (Equiv.toIso (limitEquivSections F) : limit F ≅ (↑F.sections : Type (max u v))))
              X) ≫
          Functor.map (Functor.sectionsFunctor J) f))
      x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
x y : limit F
w :
  ∀ (j : J),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (limit.π F j) :
            (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j))
          x :
        (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (limit.π F j) :
            (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j))
          y :
        (fun (X : Type u) ↦ X) (F.obj j))
⊢ x = y
have a : Eq (α := (↑F.sections : Type (max u v)))
  ((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) x : (↑F.sections : Type (max u v)))
  ((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) y : (↑F.sections : Type (max u v)))
Tactic: apply (limitEquivSections F).injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
x y : limit F
w :
  ∀ (j : J),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (limit.π F j) :
            (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j))
          x :
        (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (limit.π F j) :
            (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j))
          y :
        (fun (X : Type u) ↦ X) (F.obj j))
⊢ Eq (α := (↑F.sections : Type (max u v)))
    ((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) x : (↑F.sections : Type (max u v)))
    ((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) y : (↑F.sections : Type (max u v)))
have a : ∀ (j : J),
  Eq.{u + 1} (α := F.obj j)
    ((↑((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) x) : (j : J) → F.obj j) j)
    ((↑((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) y) : (j : J) → F.obj j) j)
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
x : d.multispan.ColimitType
⊢ ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (WalkingMultispan.right i) a = x
have left : ∀ (l : J.L) (z : d.multispan.obj (WalkingMultispan.left l)),
  ∃ (i : J.R) (a : d.right i),
    d.multispan.ιColimitType (WalkingMultispan.right i) a = d.multispan.ιColimitType (WalkingMultispan.left l) z
Tactic: obtain ⟨(l | r), z, rfl⟩ := d.multispan.ιColimitType_jointly_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
x : d.multispan.ColimitType
left :
  ∀ (l : J.L) (z : d.multispan.obj (WalkingMultispan.left l)),
    ∃ (i : J.R) (a : d.right i),
      d.multispan.ιColimitType (WalkingMultispan.right i) a = d.multispan.ιColimitType (WalkingMultispan.left l) z
⊢ ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (WalkingMultispan.right i) a = x
have right : ∀ (r : J.R) (z : d.multispan.obj (WalkingMultispan.right r)),
  ∃ (i : J.R) (a : d.right i),
    d.multispan.ιColimitType (WalkingMultispan.right i) a = d.multispan.ιColimitType (WalkingMultispan.right r) z
Tactic: obtain ⟨(l | r), z, rfl⟩ := d.multispan.ιColimitType_jointly_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
l : J.L
z : d.multispan.obj (WalkingMultispan.left l)
⊢ d.multispan.ιColimitType (WalkingMultispan.right (J.fst l))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (d.multispan.map (WalkingMultispan.Hom.fst l)) :
          (a : (fun (X : Type u) ↦ X) (d.multispan.obj (WalkingMultispan.left l))) →
            (fun (X : Type u) ↦ X) (d.multispan.obj (WalkingMultispan.right (J.fst l))))
        z) =
    d.multispan.ιColimitType (WalkingMultispan.left l) z
have rw : d.multispan.ιColimitType (WalkingMultispan.left l) z = d.multispan.ιColimitType (WalkingMultispan.left l) z
Tactic: rw [ιColimitType_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (hypothesis)
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
⊢ c.IsColimit ↔
    (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
        c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
          d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
            d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
      ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x
have this : ∀ (x : d.multispan.ColimitType), ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (WalkingMultispan.right i) a = x
Tactic: have (x : d.multispan.ColimitType) :
      ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (.right i) a = x := by
    obtain ⟨(l | r), z, rfl⟩ := d.multispan.ιColimitType_jointly_surjective x
    · exact ⟨J.fst l, d.multispan.map (WalkingMultispan.Hom.fst l) z, by rw [ιColimitType_map]⟩
    · exact ⟨r, z, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this :
  ∀ (x : d.multispan.ColimitType),
    ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (WalkingMultispan.right i) a = x
⊢ c.IsColimit ↔
    (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
        c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
          d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
            d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
      ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x
have mp : c.IsColimit →
  (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
      c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
        d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
          d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
    ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this :
  ∀ (x : d.multispan.ColimitType),
    ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (WalkingMultispan.right i) a = x
mp :
  c.IsColimit →
    (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
        c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
          d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
            d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
      ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x
⊢ c.IsColimit ↔
    (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
        c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
          d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
            d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
      ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x
have mpr : ((∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
      c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
        d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
          d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
    ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x) →
  c.IsColimit
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this :
  ∀ (x : d.multispan.ColimitType),
    ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
⊢ (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
      c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
        d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
          d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
    ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x
have mp : ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂)
  (h : c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂),
  d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
Tactic: refine ⟨fun i₁ i₂ x₁ x₂ h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this :
  ∀ (x : d.multispan.ColimitType),
    ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
mp :
  ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂)
    (h : c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂),
    d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
⊢ (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
      c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
        d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
          d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
    ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x
have mp₁ : ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x
Tactic: refine ⟨fun i₁ i₂ x₁ x₂ h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this :
  ∀ (x : d.multispan.ColimitType),
    ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
x : c.pt
⊢ ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x
have mp : ∀ (y : d.multispan.ColimitType),
  ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = d.multispan.descColimitType c y
Tactic: obtain ⟨y, rfl⟩ := hc.bijective.2 x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this :
  ∀ (x : d.multispan.ColimitType),
    ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
y : d.multispan.ColimitType
⊢ ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = d.multispan.descColimitType c y
have mp : ∀ (i : J.R) (z : d.right i),
  ∃ (i_1 : J.R) (a : d.right i_1),
    c.ι (WalkingMultispan.right i_1) a =
      d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i) z)
Tactic: obtain ⟨i, z, rfl⟩ := this y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this :
  ∀ (x : d.multispan.ColimitType),
    ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (WalkingMultispan.right i) a = x
h₁ :
  ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
    c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
      d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
h₂ : ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x
⊢ c.IsColimit
have mpr : ∀ (x₁ x₂ : d.multispan.ColimitType) (h : d.multispan.descColimitType c x₁ = d.multispan.descColimitType c x₂), x₁ = x₂
Tactic: refine ⟨fun x₁ x₂ h ↦ ?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this :
  ∀ (x : d.multispan.ColimitType),
    ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (WalkingMultispan.right i) a = x
h₁ :
  ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
    c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
      d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
h₂ : ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x
mpr :
  ∀ (x₁ x₂ : d.multispan.ColimitType) (h : d.multispan.descColimitType c x₁ = d.multispan.descColimitType c x₂), x₁ = x₂
⊢ c.IsColimit
have mpr₁ : ∀ (x : c.pt), ∃ (a : d.multispan.ColimitType), d.multispan.descColimitType c a = x
Tactic: refine ⟨fun x₁ x₂ h ↦ ?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this :
  ∀ (x : d.multispan.ColimitType),
    ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (WalkingMultispan.right i) a = x
h₁ :
  ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
    c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
      d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
h₂ : ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x
x₁ x₂ : d.multispan.ColimitType
h : d.multispan.descColimitType c x₁ = d.multispan.descColimitType c x₂
⊢ x₁ = x₂
have mpr : ∀ (i₁ : J.R) (a₁ : d.right i₁)
  (h :
    d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i₁) a₁) =
      d.multispan.descColimitType c x₂),
  d.multispan.ιColimitType (WalkingMultispan.right i₁) a₁ = x₂
Tactic: obtain ⟨i₁, a₁, rfl⟩ := this x₁
Cleared hypotheses: x₁, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this :
  ∀ (x : d.multispan.ColimitType),
    ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (WalkingMultispan.right i) a = x
h₁ :
  ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
    c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
      d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
h₂ : ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x
x₂ : d.multispan.ColimitType
i₁ : J.R
a₁ : d.right i₁
h :
  d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i₁) a₁) =
    d.multispan.descColimitType c x₂
⊢ d.multispan.ιColimitType (WalkingMultispan.right i₁) a₁ = x₂
have mpr : ∀ (i₂ : J.R) (a₂ : d.right i₂)
  (h :
    d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i₁) a₁) =
      d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i₂) a₂)),
  d.multispan.ιColimitType (WalkingMultispan.right i₁) a₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) a₂
Tactic: obtain ⟨i₂, a₂, rfl⟩ := this x₂
Cleared hypotheses: x₂, h