awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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 }
⊢ ∃ (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
have 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
          sorry =
        { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }
Tactic: rcases B with ⟨⟨⟨⟩⟩, ⟨i'⟩ | ⟨i', j'⟩, b⟩
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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)
⊢ ∃ (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
have 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
          sorry =
        { left := { as := PUnit.unit }, right := single i', hom := b }
Tactic: rcases B with ⟨⟨⟨⟩⟩, ⟨i'⟩ | ⟨i', j'⟩, b⟩
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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 }
⊢ ∃ (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
have 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
          sorry =
        { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }
Tactic: rcases B with ⟨⟨⟨⟩⟩, ⟨i'⟩ | ⟨i', j'⟩, b⟩
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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')
⊢ ∃ (l : List (StructuredArrow V (pairwiseToOpensLeCover U))),
    List.IsChain Zag
        ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i, hom := a :
            Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
          l) ∧
      ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i, hom := a :
                Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
              l).getLast
          ⋯ =
        { left := { as := PUnit.unit }, right := single i', hom := b }
have single : 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 sorry) :
      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: refine
          ⟨[{ left := ⟨⟨⟩⟩
              right := pair i i'
              hom := ObjectProperty.homMk (homOfLE
                (by simpa using le_inf a.hom.le b.hom.le)) }, _], ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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')
⊢ ∃ (l : List (StructuredArrow V (pairwiseToOpensLeCover U))),
    List.IsChain Zag
        ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i, hom := a :
            Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
          l) ∧
      ({ left := { as := PUnit.unit : Discrete PUnit.{1} }, right := single i, hom := a :
                Comma (Functor.fromPUnit V) (pairwiseToOpensLeCover U) } ::
              l).getLast
          ⋯ =
        { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }
have single : 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 sorry) :
      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 sorry) :
      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: 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⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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')
⊢ ∃ (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 }
have 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 sorry) :
      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 sorry) :
      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: 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⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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')
⊢ ∃ (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 }
have 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 sorry) :
      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 sorry) :
      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 sorry) :
      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: 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⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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.IsSheafPairwiseIntersections
have rw : F.IsSheafOpensLeCover ↔ F.IsSheafPairwiseIntersections
Tactic: rw [isSheaf_iff_isSheafOpensLeCover, isSheafOpensLeCover_iff_isSheafPairwiseIntersections]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
rw : F.IsSheafOpensLeCover ↔ F.IsSheafPairwiseIntersections
⊢ F.IsSheaf ↔ F.IsSheafPairwiseIntersections
have rw₁ : F.IsSheafPairwiseIntersections ↔ F.IsSheafPairwiseIntersections
Tactic: rw [isSheaf_iff_isSheafOpensLeCover, isSheafOpensLeCover_iff_isSheafPairwiseIntersections]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
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.IsSheafPreservesLimitPairwiseIntersections
have refine : ∀ (h : F.IsSheafPreservesLimitPairwiseIntersections) (ι : Type w) (U : ι → Opens (↑X : Type w)),
  Nonempty (IsLimit (Functor.mapCone F (Cocone.op (Pairwise.cocone U))))
Tactic: refine ⟨fun h U ↦ h.isSheafPreservesLimitPairwiseIntersections,
    fun h ↦ F.isSheaf_iff_isSheafPairwiseIntersections.mpr fun ι U ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (hypothesis)
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.IsSheafPreservesLimitPairwiseIntersections
ι : Type w
U : ι → Opens (↑X : Type w)
⊢ Nonempty (IsLimit (Functor.mapCone F (Cocone.op (Pairwise.cocone U))))
have this : PreservesLimit (Functor.op (Pairwise.diagram U)) F
Tactic: haveI := h U
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
⊢ Eq (α :=
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V)) ⟶
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊓ V)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯)) ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯)) ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (homOfLE ⋯)))
have rw : Eq (α :=
  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V)) ⟶
    F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊓ V)))
  (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
    (Quiver.Hom.op (homOfLE sorry) ≫ Quiver.Hom.op (homOfLE sorry)))
  (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
    (Quiver.Hom.op (homOfLE sorry) ≫ Quiver.Hom.op (homOfLE sorry)))
Tactic: rw [← F.1.map_comp, ← F.1.map_comp]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
⊢ U ⊔ V = iSup ι
have h : ∀ (x : (↑X : Type w)), x ∈ (↑(U ⊔ V) : Set (↑X : Type w)) ↔ x ∈ (↑(iSup ι) : Set (↑X : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
x : (↑X : Type w)
⊢ x ∈ (↑(U ⊔ V) : Set (↑X : Type w)) ↔ x ∈ (↑(iSup ι) : Set (↑X : Type w))
have h : x ∈ (↑(U ⊔ V) : Set (↑X : Type w)) ↔
  ∃ (i : ULift.{w, 0} WalkingPair),
    x ∈
      (↑(WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) i.down U V : Opens (↑X : Type w)) :
        Set (↑X : Type w))
Tactic: rw [Opens.coe_iSup, Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
x : (↑X : Type w)
⊢ x ∈ (↑(U ⊔ V) : Set (↑X : Type w)) ↔
    ∃ (i : ULift.{w, 0} WalkingPair),
      x ∈
        (↑(WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) i.down U V :
              Opens (↑X : Type w)) :
          Set (↑X : Type w))
have h : x ∈ (↑(U ⊔ V) : Set (↑X : Type w)) →
  ∃ (i : ULift.{w, 0} WalkingPair),
    x ∈
      (↑(WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) i.down U V : Opens (↑X : Type w)) :
        Set (↑X : Type w))
Tactic: constructor