awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : c.pt
⊢ ∃ (a : d.multispan.ColimitType), d.multispan.descColimitType c a = x
have mpr : ∀ (i : J.R) (y : d.right i),
  ∃ (a : d.multispan.ColimitType), d.multispan.descColimitType c a = c.ι (WalkingMultispan.right i) y
Tactic: obtain ⟨i, y, rfl⟩ := h₂ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
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
⊢ IsColimit (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes)
have h : Nonempty (IsColimit (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
Tactic: apply _root_.Nonempty.some
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
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₂))
⊢ x₁ ∈ c.multispanIndex (x := A) (u := U) (v := V).left (i₁, i₂)
have dsimp : x₁ ∈ V i₁ i₂
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
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₂))
⊢ x₁ ∈ V i₁ i₂
have rw : x₁ ∈ U i₁ ⊓ U i₂
Tactic: rw [c.eq_inf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
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₂))
eq₁ :
  e.ιColimitType (WalkingMultispan.right ((MultispanShape.prod ι).fst (i₁, i₂)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.map (WalkingMultispan.Hom.fst (i₁, i₂))) :
          (a : (fun (X : Type u) ↦ X) (e.obj (WalkingMultispan.left (i₁, i₂)))) →
            (fun (X : Type u) ↦ X) (e.obj (WalkingMultispan.right ((MultispanShape.prod ι).fst (i₁, i₂)))))
        (Subtype.mk (p := fun (x : X) ↦ x ∈ c.multispanIndex (x := A) (u := U) (v := V).left (i₁, i₂)) x₁ ⋯)) =
    e.ιColimitType (WalkingMultispan.left (i₁, i₂))
      (Subtype.mk (p := fun (x : X) ↦ x ∈ c.multispanIndex (x := A) (u := U) (v := V).left (i₁, i₂)) x₁ ⋯)
⊢ x₁ ∈ c.multispanIndex (x := A) (u := U) (v := V).left (i₁, i₂)
have dsimp : x₁ ∈ V i₁ i₂
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
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₂))
eq₁ :
  e.ιColimitType (WalkingMultispan.right ((MultispanShape.prod ι).fst (i₁, i₂)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.map (WalkingMultispan.Hom.fst (i₁, i₂))) :
          (a : (fun (X : Type u) ↦ X) (e.obj (WalkingMultispan.left (i₁, i₂)))) →
            (fun (X : Type u) ↦ X) (e.obj (WalkingMultispan.right ((MultispanShape.prod ι).fst (i₁, i₂)))))
        (Subtype.mk (p := fun (x : X) ↦ x ∈ c.multispanIndex (x := A) (u := U) (v := V).left (i₁, i₂)) x₁ ⋯)) =
    e.ιColimitType (WalkingMultispan.left (i₁, i₂))
      (Subtype.mk (p := fun (x : X) ↦ x ∈ c.multispanIndex (x := A) (u := U) (v := V).left (i₁, i₂)) x₁ ⋯)
⊢ x₁ ∈ V i₁ i₂
have rw : x₁ ∈ U i₁ ⊓ U i₂
Tactic: rw [c.eq_inf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (hypothesis)
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
x_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))
x : X
hx : x ∈ c.multicofork (x := A) (u := U) (v := V).pt
⊢ ∃ (i : (MultispanShape.prod ι).R) (a : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i),
    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) a =
      Subtype.mk (p := fun (x : X) ↦ x ∈ c.multicofork (x := A) (u := U) (v := V).pt) x hx
have hx₁ : ∃ (i : ι), x ∈ U i
Tactic: simp only [MulticoequalizerDiagram.multicofork_pt, ← c.iSup_eq,
      Set.iSup_eq_iUnion, Set.mem_iUnion] at hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
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
x_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))
x : X
hx_1 : x ∈ c.multicofork (x := A) (u := U) (v := V).pt
hx : ∃ (i : ι), x ∈ U i
⊢ ∃ (i : (MultispanShape.prod ι).R) (a : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i),
    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) a =
      Subtype.mk (p := fun (x : X) ↦ x ∈ c.multicofork (x := A) (u := U) (v := V).pt) x hx_1
have h : ∀ (i : ι) (hi : x ∈ U i),
  ∃ (i : (MultispanShape.prod ι).R) (a : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i),
    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) a =
      Subtype.mk (p := fun (x : X) ↦ x ∈ c.multicofork (x := A) (u := U) (v := V).pt) x hx_1
Tactic: obtain ⟨i, hi⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
inst : LinearOrder ι
c : MulticoequalizerDiagram A U V
i j : ι
⊢ c.multispanIndex (x := A) (u := U) (v := V).left (i, j) = c.multispanIndex (x := A) (u := U) (v := V).left (j, i)
have dsimp : V i j = V j i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
inst : LinearOrder ι
c : MulticoequalizerDiagram A U V
i j : ι
⊢ V i j = V j i
have rw : U i ⊓ U j = V j i
Tactic: rw [c.eq_inf, c.eq_inf, inf_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
inst : LinearOrder ι
c : MulticoequalizerDiagram A U V
i j : ι
rw : U i ⊓ U j = V j i
⊢ V i j = V j i
have rw₁ : U i ⊓ U j = U j ⊓ U i
Tactic: rw [c.eq_inf, c.eq_inf, inf_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
inst : LinearOrder ι
c : MulticoequalizerDiagram A U V
i j : ι
rw : U i ⊓ U j = V j i
rw₁ : U i ⊓ U j = U j ⊓ U i
⊢ V i j = V j i
have rw₂ : U j ⊓ U i = U j ⊓ U i
Tactic: rw [c.eq_inf, c.eq_inf, inf_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ Eq (α := Set (MultispanShape.ofLinearOrder Bool).R)
    {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} Set.univ
have h₁ : Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
    {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false ↔
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
h₁ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false ↔
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false
⊢ Eq (α := Set (MultispanShape.ofLinearOrder Bool).R)
    {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} Set.univ
have h₂ : Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
    {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} true ↔
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false ↔
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false
have h₁ : Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
    {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false →
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
h₁ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false
⊢ Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false ↔
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false
have h₂ : Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false →
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
    {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
h₁ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false
h₂ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false
h₃ h₄ h₅ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false
h₆ h₇ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false
⊢ Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false ↔
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false
have h₈ : Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false →
  ¬false = (MultispanShape.ofLinearOrder Bool).fst default →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) {(MultispanShape.ofLinearOrder Bool).snd default}
      false
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} true ↔
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true
have h₁ : Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
    {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} true →
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Multicoequalizer (goal)
Goal:
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
h₁ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} true →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true
⊢ Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} true ↔
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true
have h₂ : Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true →
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
    {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} true
Tactic: tauto