awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
Y : Opens (↑X : Type w)
R : Presieve Y
hR : Sieve.generate R ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) Y
h h₁ :
  IsLimit (Functor.mapCone F (Sieve.generate R).arrows.cocone.op) =
    IsLimit (Functor.mapCone F (Sieve.generate R).arrows.cocone.op)
⊢ IsLimit (Functor.mapCone F (Sieve.generate R).arrows.cocone.op) =
    IsLimit (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux (coveringOfPresieve Y R) Y)).arrows.cocone.op)

Tactic:
rw [covering_presieve_eq_self R]

Premises used: TopCat.Presheaf.covering_presieve_eq_self
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
h : F.IsSheaf
rw :
  Nonempty
    (IsLimit (J :=
      (Presieve.category (X := iSup U) (Sieve.arrows (Sieve.generate (presieveOfCoveringAux U (iSup U)))))ᵒᵖ)
      (Functor.mapCone F
        (Cocone.op (Presieve.cocone (Sieve.arrows (Sieve.generate (presieveOfCoveringAux U (iSup U))))))))
⊢ Nonempty (IsLimit (Functor.mapCone F (opensLeCoverCocone U).op))

Tactic:
rw [(isLimitOpensLeEquivGenerate₁ F U rfl).nonempty_congr]

Premises used: TopCat.Presheaf.isLimitOpensLeEquivGenerate₁, Equiv.nonempty_congr, rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
h : F.IsSheaf
a :
  Membership.mem (γ := Set (Sieve (iSup U)))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) (iSup U))
    (Sieve.generate (presieveOfCoveringAux U (iSup U)))
⊢ Nonempty
    (IsLimit (J :=
      (Presieve.category (X := iSup U) (Sieve.arrows (Sieve.generate (presieveOfCoveringAux U (iSup U)))))ᵒᵖ)
      (Functor.mapCone F
        (Cocone.op (Presieve.cocone (Sieve.arrows (Sieve.generate (presieveOfCoveringAux U (iSup U))))))))

Tactic:
apply (Presheaf.isSheaf_iff_isLimit _ _).mp h

Premises used: CategoryTheory.Presheaf.isSheaf_iff_isLimit, Iff.mp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
h : F.IsSheaf
⊢ Membership.mem (γ := Set (Sieve (iSup U)))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) (iSup U))
    (Sieve.generate (presieveOfCoveringAux U (iSup U)))

Tactic:
apply presieveOfCovering.mem_grothendieckTopology

Premises used: TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
⊢ F.IsSheaf ↔ F.IsSheafOpensLeCover

Tactic:
⟨fun h _ ↦ h.isSheafOpensLeCover,
    fun h ↦ (Presheaf.isSheaf_iff_isLimit _ _).mpr fun Y S ↦ ?_⟩

Premises used: Iff.mpr, Opens.grothendieckTopology, CategoryTheory.Presheaf.isSheaf_iff_isLimit, TopCat.carrier, Iff.intro, TopCat.Presheaf.IsSheaf.isSheafOpensLeCover
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
refine :
  ∀ (h : F.IsSheafOpensLeCover) (Y : Opens (↑X : Type w)),
    ∀ S ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) Y,
      Nonempty (IsLimit (Functor.mapCone F S.arrows.cocone.op))
⊢ F.IsSheaf ↔ F.IsSheafOpensLeCover

Tactic:
refine ⟨fun h _ ↦ h.isSheafOpensLeCover,
    fun h ↦ (Presheaf.isSheaf_iff_isLimit _ _).mpr fun Y S ↦ ?_⟩
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
h : F.IsSheafOpensLeCover
Y : Opens (↑X : Type w)
S : Sieve Y
rw :
  Sieve.generate S.arrows ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) Y →
    Nonempty (IsLimit (Functor.mapCone F (Sieve.generate S.arrows).arrows.cocone.op))
⊢ S ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) Y →
    Nonempty (IsLimit (Functor.mapCone F S.arrows.cocone.op))

Tactic:
rw [← Sieve.generate_sieve S]

Premises used: CategoryTheory.Sieve.generate_sieve
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
h : F.IsSheafOpensLeCover
Y : Opens (↑X : Type w)
S : Sieve Y
hS : Sieve.generate S.arrows ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) Y
rw :
  Nonempty
    (IsLimit (J :=
      (ObjectProperty.FullSubcategory (C := Opens (↑X : Type w)) fun (V : Opens (↑X : Type w)) ↦
          ∃ (i : (V : Opens (↑X : Type w)) × { f : V ⟶ Y // S.arrows f }), V ≤ coveringOfPresieve Y S.arrows i)ᵒᵖ)
      (Functor.mapCone F (Cocone.op (opensLeCoverCocone (coveringOfPresieve Y S.arrows)))))
⊢ Nonempty (IsLimit (Functor.mapCone F (Sieve.generate S.arrows).arrows.cocone.op))

Tactic:
rw [← (isLimitOpensLeEquivGenerate₂ F S.1 hS).nonempty_congr]

Premises used: CategoryTheory.Sieve.arrows, Equiv.nonempty_congr, TopCat.Presheaf.isLimitOpensLeEquivGenerate₂
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
h : F.IsSheafOpensLeCover
Y : Opens (↑X : Type w)
S : Sieve Y
hS : Sieve.generate S.arrows ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) Y
⊢ Nonempty
    (IsLimit (J :=
      (ObjectProperty.FullSubcategory (C := Opens (↑X : Type w)) fun (V : Opens (↑X : Type w)) ↦
          ∃ (i : (V : Opens (↑X : Type w)) × { f : V ⟶ Y // S.arrows f }), V ≤ coveringOfPresieve Y S.arrows i)ᵒᵖ)
      (Functor.mapCone F (Cocone.op (opensLeCoverCocone (coveringOfPresieve Y S.arrows)))))

Tactic:
apply h
-- 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
⊢ Nonempty (StructuredArrow V (pairwiseToOpensLeCover U))

Tactic:
⟨StructuredArrow.mk (Y := single V.index) (ObjectProperty.homMk V.homToIndex)⟩

Premises used: TopCat.Presheaf.SheafCondition.OpensLeCover.homToIndex, Nonempty.intro, CategoryTheory.ObjectProperty.homMk, CategoryTheory.StructuredArrow.mk
-- 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
A B : StructuredArrow V (pairwiseToOpensLeCover U)
single :
  ∀ (i : ι)
    (a :
      Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
        (pairwiseToOpensLeCover U).obj (Pairwise.single i)),
    ∃ (l : List (StructuredArrow V (pairwiseToOpensLeCover U))),
      List.IsChain Zag
          ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.single i, hom := a :
              Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
            l) ∧
        ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.single i, hom := a :
                  Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
                l).getLast
            ⋯ =
          B
pair :
  ∀ (i j : ι)
    (a :
      Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
        (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)),
    ∃ (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
            ⋯ =
          B
⊢ ∃ (l : List (StructuredArrow V (pairwiseToOpensLeCover U))), List.IsChain Zag (A :: l) ∧ (A :: l).getLast ⋯ = B

Tactic:
rcases A with ⟨⟨⟨⟩⟩, ⟨i⟩ | ⟨i, j⟩, a⟩
-- 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
B : StructuredArrow V (pairwiseToOpensLeCover U)
i : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.single i)
single :
  ∀ (i' : ι)
    (b :
      Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
        (pairwiseToOpensLeCover U).obj (Pairwise.single i')),
    ∃ (l : List (StructuredArrow V (pairwiseToOpensLeCover U))),
      List.IsChain Zag
          ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.single i, hom := a :
              Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
            l) ∧
        ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.single i, hom := a :
                  Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
                l).getLast
            ⋯ =
          { left := { as := PUnit.unit }, right := Pairwise.single i', hom := b }
single₁ :
  ∀ (i' j' : ι)
    (b :
      Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
        (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')),
    ∃ (l : List (StructuredArrow V (pairwiseToOpensLeCover U))),
      List.IsChain Zag
          ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.single i, hom := a :
              Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
            l) ∧
        ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.single i, hom := a :
                  Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
                l).getLast
            ⋯ =
          { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }
⊢ ∃ (l : List (StructuredArrow V (pairwiseToOpensLeCover U))),
    List.IsChain Zag
        ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.single i, hom := a :
            Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
          l) ∧
      ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.single i, hom := a :
                Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
              l).getLast
          ⋯ =
        B

Tactic:
rcases B with ⟨⟨⟨⟩⟩, ⟨i'⟩ | ⟨i', j'⟩, b⟩
-- 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
B : StructuredArrow V (pairwiseToOpensLeCover U)
i j : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
pair :
  ∀ (i' : ι)
    (b :
      Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
        (pairwiseToOpensLeCover U).obj (single i')),
    ∃ (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 }
pair₁ :
  ∀ (i' j' : ι)
    (b :
      Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
        (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')),
    ∃ (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 }
⊢ ∃ (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
          ⋯ =
        B

Tactic:
rcases B with ⟨⟨⟨⟩⟩, ⟨i'⟩ | ⟨i', j'⟩, b⟩
-- 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' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (single i')
⊢ (Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} }).obj (P :=
      fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i) ≤
    ((pairwiseToOpensLeCover U).obj (Pairwise.pair i i')).obj (P := fun (V : Opens (↑X : Type w)) ↦ ∃ (i : ι), V ≤ U i)

Tactic:
simpa using le_inf a.hom.le b.hom.le

Premises used: Quiver.Hom.le, le_inf, CategoryTheory.InducedCategory.Hom.hom
-- 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 (Pairwise.single i)
i' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.single i')
single :
  List.IsChain Zag
    [{ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.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 := Pairwise.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.single i, hom := a :
            Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
          l) ∧
      ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.single i, hom := a :
                Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
              l).getLast
          ⋯ =
        { left := { as := PUnit.unit }, right := Pairwise.single i', hom := b }

Tactic:
refine
          ⟨[{ left := ⟨⟨⟩⟩
              right := pair i i'
              hom := ObjectProperty.homMk (homOfLE
                (by simpa using le_inf a.hom.le 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 : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (single i)
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 := 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 := b :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) }]

Tactic:
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, Eq.mpr, CategoryTheory.Pairwise.Hom.right, CategoryTheory.Pairwise.Hom.left, Quiver.Hom.le, CategoryTheory.Comma.left, CategoryTheory.CategoryStruct.id, Eq.mp, id, CategoryTheory.CommaMorphism.mk, List.IsChain.singleton, Nonempty.intro, le_inf, CategoryTheory.Discrete.mk, CategoryTheory.homOfLE, CategoryTheory.ObjectProperty.homMk, CategoryTheory.Comma.mk, PUnit.unit, Or.inl, CategoryTheory.InducedCategory.Hom.hom, le_inf_iff._simp_1, 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' : ι
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 := 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 := b :
        Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) }]

Tactic:
exact
          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 : ι
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')
⊢ ((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 : ι
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')
⊢ ((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 : ι
a :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.single i)
i' j' : ι
b :
  Functor.obj (Functor.fromPUnit V) { as := PUnit.unit : Discrete PUnit.{1} } ⟶
    (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
single :
  List.IsChain Zag
    [{ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.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 := Pairwise.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.single i, hom := a :
            Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
          l) ∧
      ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := Pairwise.single i, 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 := pair i' i
                hom := ObjectProperty.homMk (homOfLE
                  (le_inf (b.hom.le.trans (by simp)) a.hom.le)) },
              { left := ⟨⟨⟩⟩
                right := single i'
                hom := ObjectProperty.homMk (homOfLE (b.hom.le.trans (by simp))) }, _], ?_, rfl⟩