awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
r : J.R
z : d.multispan.obj (WalkingMultispan.right r)
⊢ d.multispan.ιColimitType (WalkingMultispan.right r) z = d.multispan.ιColimitType (WalkingMultispan.right r) z

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
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:
exact ⟨r, z, by simp⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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

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⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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
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
⊢ 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
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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

Tactic:
⟨fun i₁ i₂ x₁ x₂ h ↦ ?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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₂
mp₁ : ∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = 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

Tactic:
refine ⟨fun i₁ i₂ x₁ x₂ h ↦ ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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₂
h :
  d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁) =
    d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂)
⊢ d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂

Tactic:
hc.bijective.1 h

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimit.bijective, And.left
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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₂
h :
  d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁) =
    d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂)
⊢ d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂

Tactic:
exact hc.bijective.1 h

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimit.bijective, And.left
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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
mp :
  ∀ (y : d.multispan.ColimitType),
    ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = d.multispan.descColimitType c y
⊢ ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = x

Tactic:
obtain ⟨y, rfl⟩ := hc.bijective.2 x

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimit.bijective, And.right, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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
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)
⊢ ∃ (i : J.R) (a : d.right i), c.ι (WalkingMultispan.right i) a = d.multispan.descColimitType c y

Tactic:
obtain ⟨i, z, rfl⟩ := this y

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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 : J.R
z : d.right i
⊢ c.ι (WalkingMultispan.right i) z =
    d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i) z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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 : 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:
exact ⟨i, z, by simp⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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

Tactic:
⟨fun x₁ x₂ h ↦ ?_, fun x ↦ ?_⟩

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimit.mk, And.intro
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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₂
mpr₁ : ∀ (x : c.pt), ∃ (a : d.multispan.ColimitType), d.multispan.descColimitType c a = x
⊢ c.IsColimit

Tactic:
refine ⟨fun x₁ x₂ h ↦ ?_, fun x ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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₂
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₂
⊢ x₁ = x₂

Tactic:
obtain ⟨i₁, a₁, rfl⟩ := this x₁

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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₂
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₂
⊢ d.multispan.ιColimitType (WalkingMultispan.right i₁) a₁ = x₂

Tactic:
obtain ⟨i₂, a₂, rfl⟩ := this x₂

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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
i₁ : J.R
a₁ : d.right i₁
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:
h₁ _ _ _ _ h
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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
i₁ : J.R
a₁ : d.right i₁
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:
exact h₁ _ _ _ _ h
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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 : c.pt
mpr :
  ∀ (i : J.R) (y : d.right i),
    ∃ (a : d.multispan.ColimitType), d.multispan.descColimitType c a = c.ι (WalkingMultispan.right i) y
⊢ ∃ (a : d.multispan.ColimitType), d.multispan.descColimitType c a = x

Tactic:
obtain ⟨i, y, rfl⟩ := h₂ x

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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
i : J.R
y : d.right i
⊢ ∃ (a : d.multispan.ColimitType), d.multispan.descColimitType c a = c.ι (WalkingMultispan.right i) y

Tactic:
⟨d.multispan.ιColimitType (.right i) y, rfl⟩

Premises used: CategoryTheory.Limits.WalkingMultispan.right, CategoryTheory.Limits.MultispanIndex.multispan, Exists.intro, CategoryTheory.Functor.ιColimitType, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
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
i : J.R
y : d.right i
⊢ ∃ (a : d.multispan.ColimitType), d.multispan.descColimitType c a = c.ι (WalkingMultispan.right i) y

Tactic:
exact ⟨d.multispan.ιColimitType (.right i) y, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : Functor.{w, u, w, u + 1} (WalkingMultispan (MultispanShape.prod ι)) (Type u) :=
  (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan
h : Nonempty (IsColimit (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
⊢ IsColimit (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes)

Tactic:
apply _root_.Nonempty.some

Premises used: Nonempty.some
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : Functor.{w, u, w, u + 1} (WalkingMultispan (MultispanShape.prod ι)) (Type u) :=
  (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan
i₁ i₂ : ι
x : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i₁
x_1 : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
x₂ : X
h₂ : x₂ ∈ U i₂
h :
  Eq.{u + 1} (α :=
    Functor.CoconeTypes.pt.{u, u, w, w} (J := WalkingMultispan (MultispanShape.prod ι)) (F :=
      (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan)
      (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
          (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
            (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
        (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes)))
    (Functor.CoconeTypes.ι
      (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
          (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
            (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
        (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
      (WalkingMultispan.right i₁)
      (Subtype.mk (p := fun (x : X) ↦ x ∈ c.multispanIndex (x := A) (u := U) (v := V).right i₁) x₁ h₁))
    (Functor.CoconeTypes.ι
      (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
          (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
            (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
        (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
      (WalkingMultispan.right i₂)
      (Subtype.mk (p := fun (x : X) ↦ x ∈ c.multispanIndex (x := A) (u := U) (v := V).right i₂) x₂ h₂))
⊢ x₁ = x₂

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : Functor.{w, u, w, u + 1} (WalkingMultispan (MultispanShape.prod ι)) (Type u) :=
  (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan
i₁ i₂ : ι
x : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i₁
x_1 : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  Eq.{u + 1} (α :=
    Functor.CoconeTypes.pt.{u, u, w, w} (J := WalkingMultispan (MultispanShape.prod ι)) (F :=
      (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan)
      (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
          (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
            (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
        (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes)))
    (Functor.CoconeTypes.ι
      (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
          (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
            (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
        (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
      (WalkingMultispan.right i₁)
      (Subtype.mk (p := fun (x : X) ↦ x ∈ c.multispanIndex (x := A) (u := U) (v := V).right i₁) x₁ h₁))
    (Functor.CoconeTypes.ι
      (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
          (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
            (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
        (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
      (WalkingMultispan.right i₂)
      (Subtype.mk (p := fun (x : X) ↦ x ∈ c.multispanIndex (x := A) (u := U) (v := V).right i₂) x₁ h₂))
dsimp : x₁ ∈ V i₁ i₂
⊢ x₁ ∈ c.multispanIndex (x := A) (u := U) (v := V).left (i₁, i₂)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : Functor.{w, u, w, u + 1} (WalkingMultispan (MultispanShape.prod ι)) (Type u) :=
  (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan
i₁ i₂ : ι
x : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i₁
x_1 : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  Eq.{u + 1} (α :=
    Functor.CoconeTypes.pt.{u, u, w, w} (J := WalkingMultispan (MultispanShape.prod ι)) (F :=
      (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan)
      (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
          (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
            (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
        (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes)))
    (Functor.CoconeTypes.ι
      (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
          (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
            (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
        (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
      (WalkingMultispan.right i₁)
      (Subtype.mk (p := fun (x : X) ↦ x ∈ c.multispanIndex (x := A) (u := U) (v := V).right i₁) x₁ h₁))
    (Functor.CoconeTypes.ι
      (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
          (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
            (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
        (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
      (WalkingMultispan.right i₂)
      (Subtype.mk (p := fun (x : X) ↦ x ∈ c.multispanIndex (x := A) (u := U) (v := V).right i₂) x₁ h₂))
rw : x₁ ∈ U i₁ ⊓ U i₂
⊢ x₁ ∈ V i₁ i₂

Tactic:
rw [c.eq_inf]

Premises used: CompleteLattice.MulticoequalizerDiagram.eq_inf