Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case single.pair
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := single i, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := single i, hom := a } :: l).getLast ⋯ =
        { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }

pp: case pair.single
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l).getLast ⋯ =
        { left := { as := PUnit.unit }, right := single i', hom := b }

pp: case pair.pair
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: 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⟩
        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 _)))

Goal state after:
case pair.single
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l).getLast ⋯ =
        { left := { as := PUnit.unit }, right := single i', hom := b }

case pair.pair
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l).getLast ⋯ =
        { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }