-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
inst : Category.{v_1, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{v_1, u, u_1} (P := P) 𝒰
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.HasOfPostcompProperty P
i j : 𝒰.I₀
refine_1 :
  ∀ (x : ↥(pullback (𝒰.f i) (𝒰.f j))),
    ∃ (i_1 :
      PreZeroHypercover.I₀ (C := Scheme) (S := pullback (𝒰.f i) (𝒰.f j))
        { I₀ := (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j),
          X := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦ 𝒰.X (k.fst (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j))),
          f := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦
            pullback.lift (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).1)
              (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).2) ⋯ }),
      Membership.mem (γ := Set ↥(pullback (𝒰.f i) (𝒰.f j)))
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j),
                X := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦ 𝒰.X (k.fst (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j))),
                f := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦
                  pullback.lift (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).1)
                    (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).2) ⋯ :
                PreZeroHypercover (pullback (𝒰.f i) (𝒰.f j)) }
              i_1))
          ⇑(PreZeroHypercover.f
              { I₀ := (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j),
                X := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦ 𝒰.X (k.fst (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j))),
                f := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦
                  pullback.lift (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).1)
                    (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).2) ⋯ :
                PreZeroHypercover (pullback (𝒰.f i) (𝒰.f j)) }
              i_1))
        x
refine_2 :
  ∀
    (k :
      PreZeroHypercover.I₀ (C := Scheme) (S := pullback (𝒰.f i) (𝒰.f j))
        { I₀ := (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j),
          X := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦ 𝒰.X (k.fst (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j))),
          f := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦
            pullback.lift (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).1)
              (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).2) ⋯ }),
    P
      (PreZeroHypercover.f
        { I₀ := (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j),
          X := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦ 𝒰.X (k.fst (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j))),
          f := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦
            pullback.lift (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).1)
              (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).2) ⋯ :
          PreZeroHypercover (pullback (𝒰.f i) (𝒰.f j)) }
        k)
⊢ (∀ (x : ↥(pullback (𝒰.f i) (𝒰.f j))),
      ∃ (i_1 :
        PreZeroHypercover.I₀ (C := Scheme) (S := pullback (𝒰.f i) (𝒰.f j))
          { I₀ := (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j),
            X := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦ 𝒰.X (k.fst (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j))),
            f := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦
              pullback.lift (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).1)
                (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).2) ⋯ }),
        Membership.mem (γ := Set ↥(pullback (𝒰.f i) (𝒰.f j)))
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j),
                  X := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦ 𝒰.X (k.fst (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j))),
                  f := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦
                    pullback.lift (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).1)
                      (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).2) ⋯ :
                  PreZeroHypercover (pullback (𝒰.f i) (𝒰.f j)) }
                i_1))
            ⇑(PreZeroHypercover.f
                { I₀ := (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j),
                  X := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦ 𝒰.X (k.fst (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j))),
                  f := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦
                    pullback.lift (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).1)
                      (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).2) ⋯ :
                  PreZeroHypercover (pullback (𝒰.f i) (𝒰.f j)) }
                i_1))
          x) ∧
    ∀
      (i_1 :
        PreZeroHypercover.I₀ (C := Scheme) (S := pullback (𝒰.f i) (𝒰.f j))
          { I₀ := (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j),
            X := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦ 𝒰.X (k.fst (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j))),
            f := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦
              pullback.lift (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).1)
                (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).2) ⋯ }),
      P
        (PreZeroHypercover.f
          { I₀ := (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j),
            X := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦ 𝒰.X (k.fst (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j))),
            f := fun (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) ↦
              pullback.lift (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).1)
                (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).2) ⋯ :
            PreZeroHypercover (pullback (𝒰.f i) (𝒰.f j)) }
          i_1)

Tactic:
refine ⟨fun x ↦ ?_, fun k ↦ ?_⟩