awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
V : OpensLeCover U
i : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (single i)
i' j' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ List.IsChain Zag
    [{ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i, hom := a :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i' i,
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i',
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i' j', hom := b :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) }]

Tactic:
List.IsChain.cons_cons
            (Or.inr
              ⟨{  left := 𝟙 _
                  right := right i' i }⟩)
            (List.IsChain.cons_cons
              (Or.inl
                ⟨{  left := 𝟙 _
                    right := left i' i }⟩)
              (List.IsChain.cons_cons
                (Or.inr
                  ⟨{  left := 𝟙 _
                      right := left i' j' }⟩)
                (List.IsChain.singleton _)))

Premises used: List.IsChain.cons_cons, CategoryTheory.Pairwise.Hom.right, CategoryTheory.Pairwise.Hom.left, Quiver.Hom.le, CategoryTheory.Comma.left, CategoryTheory.CategoryStruct.id, inf_le_left._simp_1, CategoryTheory.CommaMorphism.mk, List.IsChain.singleton, Nonempty.intro, le_inf, CategoryTheory.Discrete.mk, CategoryTheory.homOfLE, CategoryTheory.ObjectProperty.homMk, of_eq_true, CategoryTheory.Comma.mk, PUnit.unit, Or.inl, LE.le.trans, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Pairwise.pair, Or.inr
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
V : OpensLeCover U
i : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (single i)
i' j' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ List.IsChain Zag
    [{ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i, hom := a :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i' i,
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i',
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i' j', hom := b :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) }]

Tactic:
exact
          List.IsChain.cons_cons
            (Or.inr
              ⟨{  left := 𝟙 _
                  right := right i' i }⟩)
            (List.IsChain.cons_cons
              (Or.inl
                ⟨{  left := 𝟙 _
                    right := left i' i }⟩)
              (List.IsChain.cons_cons
                (Or.inr
                  ⟨{  left := 𝟙 _
                      right := left i' j' }⟩)
                (List.IsChain.singleton _)))

Premises used: List.IsChain.cons_cons, List.IsChain.singleton, Or.inl, Or.inr
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
V : OpensLeCover U
i j : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (single i')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i j)).obj (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) ≤
    ((pairwiseToOpensLeCover U).obj (single i)).obj (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i)

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
V : OpensLeCover U
i j : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (single i')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i j)).obj (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) ≤
    U i

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
V : OpensLeCover U
i j : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (single i')
pair :
  List.IsChain Zag
    [{ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i j, hom := a :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i,
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i i',
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i', hom := b :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) }]
⊢ ∃ (l : List (StructuredArrow V (pairwiseToOpensLeCover U))),
    List.IsChain Zag
        ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i j, hom := a :
            Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
          l) ∧
      ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i j, hom := a :
                Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
              l).getLast
          ⋯ =
        { left := { as := PUnit.unit }, right := single i', hom := b }

Tactic:
refine
          ⟨[{   left := ⟨⟨⟩⟩
                right := single i
                hom := ObjectProperty.homMk (homOfLE (a.hom.le.trans (by simp))) },
              { left := ⟨⟨⟩⟩
                right := pair i i'
                hom := ObjectProperty.homMk (homOfLE
                  (le_inf ((a.hom.le).trans (by simp)) b.hom.le)) }, _],
                ?_, rfl⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
V : OpensLeCover U
i j : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (single i')
⊢ List.IsChain Zag
    [{ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i j, hom := a :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i,
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i i',
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i', hom := b :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) }]

Tactic:
List.IsChain.cons_cons
            (Or.inl
              ⟨{  left := 𝟙 _
                  right := left i j }⟩)
            (List.IsChain.cons_cons
              (Or.inr
                ⟨{  left := 𝟙 _
                    right := left i i' }⟩)
              (List.IsChain.cons_cons
                (Or.inl
                  ⟨{  left := 𝟙 _
                      right := right i i' }⟩)
                (List.IsChain.singleton _)))

Premises used: List.IsChain.cons_cons, CategoryTheory.Pairwise.Hom.right, CategoryTheory.Pairwise.Hom.left, Quiver.Hom.le, CategoryTheory.Comma.left, CategoryTheory.CategoryStruct.id, inf_le_left._simp_1, CategoryTheory.CommaMorphism.mk, List.IsChain.singleton, Nonempty.intro, le_inf, CategoryTheory.Discrete.mk, CategoryTheory.homOfLE, CategoryTheory.ObjectProperty.homMk, of_eq_true, CategoryTheory.Comma.mk, PUnit.unit, Or.inl, LE.le.trans, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Pairwise.pair, Or.inr
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
V : OpensLeCover U
i j : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (single i')
⊢ List.IsChain Zag
    [{ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i j, hom := a :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i,
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i i',
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i', hom := b :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) }]

Tactic:
exact
          List.IsChain.cons_cons
            (Or.inl
              ⟨{  left := 𝟙 _
                  right := left i j }⟩)
            (List.IsChain.cons_cons
              (Or.inr
                ⟨{  left := 𝟙 _
                    right := left i i' }⟩)
              (List.IsChain.cons_cons
                (Or.inl
                  ⟨{  left := 𝟙 _
                      right := right i i' }⟩)
                (List.IsChain.singleton _)))

Premises used: List.IsChain.cons_cons, List.IsChain.singleton, Or.inl, Or.inr
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
V : OpensLeCover U
i j : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i j)).obj (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) ≤
    ((pairwiseToOpensLeCover U).obj (single i)).obj (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i)

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
V : OpensLeCover U
i j : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i j)).obj (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) ≤
    U i

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
V : OpensLeCover U
i j : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')).obj (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) ≤
    U i'

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
V : OpensLeCover U
i j : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')).obj (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) ≤
    ((pairwiseToOpensLeCover U).obj (single i')).obj (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i)

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
V : OpensLeCover U
i j : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
pair :
  List.IsChain Zag
    [{ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i j, hom := a :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i,
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i i',
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i',
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i' j', hom := b :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) }]
⊢ ∃ (l : List (StructuredArrow V (pairwiseToOpensLeCover U))),
    List.IsChain Zag
        ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i j, hom := a :
            Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
          l) ∧
      ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i j, hom := a :
                Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
              l).getLast
          ⋯ =
        { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }

Tactic:
refine
          ⟨[{   left := ⟨⟨⟩⟩
                right := single i
                hom := ObjectProperty.homMk (homOfLE (a.hom.le.trans (by simp))) },
              { left := ⟨⟨⟩⟩
                right := pair i i'
                hom := ObjectProperty.homMk (homOfLE
                  (le_inf (a.hom.le.trans (by simp)) (b.hom.le.trans (by simp)))) },
              { left := ⟨⟨⟩⟩
                right := single i'
                hom := ObjectProperty.homMk (homOfLE (b.hom.le.trans (by simp))) }, _], ?_, rfl⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
V : OpensLeCover U
i j : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ List.IsChain Zag
    [{ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i j, hom := a :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i,
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i i',
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i',
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i' j', hom := b :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) }]

Tactic:
List.IsChain.cons_cons
            (Or.inl
              ⟨{  left := 𝟙 _
                  right := left i j }⟩)
            (List.IsChain.cons_cons
              (Or.inr
                ⟨{  left := 𝟙 _
                    right := left i i' }⟩)
              (List.IsChain.cons_cons
                (Or.inl
                  ⟨{  left := 𝟙 _
                      right := right i i' }⟩)
                (List.IsChain.cons_cons
                  (Or.inr
                    ⟨{  left := 𝟙 _
                        right := left i' j' }⟩)
                  (List.IsChain.singleton _))))

Premises used: List.IsChain.cons_cons, CategoryTheory.Pairwise.Hom.right, CategoryTheory.Pairwise.Hom.left, Quiver.Hom.le, CategoryTheory.Comma.left, CategoryTheory.CategoryStruct.id, inf_le_left._simp_1, CategoryTheory.CommaMorphism.mk, List.IsChain.singleton, Nonempty.intro, le_inf, CategoryTheory.Discrete.mk, CategoryTheory.homOfLE, CategoryTheory.ObjectProperty.homMk, of_eq_true, CategoryTheory.Comma.mk, PUnit.unit, Or.inl, LE.le.trans, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Pairwise.pair, Or.inr
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
V : OpensLeCover U
i j : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ List.IsChain Zag
    [{ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i j, hom := a :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i,
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i i',
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i',
        hom := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) (homOfLE ⋯) :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) },
      { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.pair i' j', hom := b :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) }]

Tactic:
exact
          List.IsChain.cons_cons
            (Or.inl
              ⟨{  left := 𝟙 _
                  right := left i j }⟩)
            (List.IsChain.cons_cons
              (Or.inr
                ⟨{  left := 𝟙 _
                    right := left i i' }⟩)
              (List.IsChain.cons_cons
                (Or.inl
                  ⟨{  left := 𝟙 _
                      right := right i i' }⟩)
                (List.IsChain.cons_cons
                  (Or.inr
                    ⟨{  left := 𝟙 _
                        right := left i' j' }⟩)
                  (List.IsChain.singleton _))))

Premises used: List.IsChain.cons_cons, List.IsChain.singleton, Or.inl, Or.inr
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
i : ι
⊢ Functor.obj (diagram U) (single i) ⟶
    (pairwiseToOpensLeCover U ⋙ ObjectProperty.ι fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i).obj (single i)

Tactic:
exact 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
i j : ι
⊢ Functor.obj (diagram U) (Pairwise.pair i j) ⟶
    (pairwiseToOpensLeCover U ⋙ ObjectProperty.ι fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i).obj
      (Pairwise.pair i j)

Tactic:
exact 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
i : ι
⊢ (pairwiseToOpensLeCover U ⋙ ObjectProperty.ι fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i).obj (single i) ⟶
    Functor.obj (diagram U) (single i)

Tactic:
exact 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens (↑X : Type w)
i j : ι
⊢ (pairwiseToOpensLeCover U ⋙ ObjectProperty.ι fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i).obj
      (Pairwise.pair i j) ⟶
    Functor.obj (diagram U) (Pairwise.pair i j)

Tactic:
exact 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id