awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) 𝒰
i j : 𝒰.I₀
z : ↥(pullback (𝒰.f i) (𝒰.f j))
h :
  Eq (α := ↥X) ((𝒰.f i) ((pullback.fst (𝒰.f i) (𝒰.f j)) z : ↥(𝒰.X i)) : ↥X)
    ((𝒰.f j) ((pullback.snd (𝒰.f i) (𝒰.f j)) z : ↥(𝒰.X j)) : ↥X)
obtain :
  ∀ (k : 𝒰.I₀) (fi : k ⟶ i) (fj : k ⟶ j) (xk : ↥(𝒰.X k))
    (h :
      Eq (α := ↥X)
        ((𝒰.f i)
            ((pullback.fst (𝒰.f i) (𝒰.f j))
                ((pullback.lift (𝒰.trans (P := P) fi) (𝒰.trans (P := P) fj) ⋯) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
              ↥(𝒰.X i)) :
          ↥X)
        ((𝒰.f j)
            ((pullback.snd (𝒰.f i) (𝒰.f j))
                ((pullback.lift (𝒰.trans (P := P) fi) (𝒰.trans (P := P) fj) ⋯) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
              ↥(𝒰.X j)) :
          ↥X)),
    ∃ (k_1 : 𝒰.I₀) (fi_1 : k_1 ⟶ i) (fj_1 : k_1 ⟶ j) (xk_1 : ↥(𝒰.X k_1)),
      Eq (α := ↥(𝒰.X i)) ((𝒰.trans (P := P) fi_1) xk_1 : ↥(𝒰.X i))
          ((pullback.fst (𝒰.f i) (𝒰.f j))
              ((pullback.lift (𝒰.trans (P := P) fi) (𝒰.trans (P := P) fj) ⋯) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
            ↥(𝒰.X i)) ∧
        Eq (α := ↥(𝒰.X j)) ((𝒰.trans (P := P) fj_1) xk_1 : ↥(𝒰.X j))
          ((pullback.snd (𝒰.f i) (𝒰.f j))
              ((pullback.lift (𝒰.trans (P := P) fi) (𝒰.trans (P := P) fj) ⋯) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
            ↥(𝒰.X j))
⊢ ∃ (k : 𝒰.I₀) (fi : k ⟶ i) (fj : k ⟶ j) (xk : ↥(𝒰.X k)),
    Eq (α := ↥(𝒰.X i)) ((𝒰.trans (P := P) fi) xk : ↥(𝒰.X i)) ((pullback.fst (𝒰.f i) (𝒰.f j)) z : ↥(𝒰.X i)) ∧
      Eq (α := ↥(𝒰.X j)) ((𝒰.trans (P := P) fj) xk : ↥(𝒰.X j)) ((pullback.snd (𝒰.f i) (𝒰.f j)) z : ↥(𝒰.X j))

Tactic:
obtain ⟨k, fi, fj, xk, rfl⟩ := 𝒰.exists_lift_trans_eq z

Premises used: AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, rfl
-- 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) 𝒰
i j k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
xk : ↥(𝒰.X k)
h :
  Eq (α := ↥X)
    ((𝒰.f i)
        ((pullback.fst (𝒰.f i) (𝒰.f j))
            ((pullback.lift (𝒰.trans (P := P) fi) (𝒰.trans (P := P) fj) ⋯) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
          ↥(𝒰.X i)) :
      ↥X)
    ((𝒰.f j)
        ((pullback.snd (𝒰.f i) (𝒰.f j))
            ((pullback.lift (𝒰.trans (P := P) fi) (𝒰.trans (P := P) fj) ⋯) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
          ↥(𝒰.X j)) :
      ↥X)
h₁ :
  Eq (α := ↥(𝒰.X i)) ((𝒰.trans (P := P) fi) xk : ↥(𝒰.X i))
      ((pullback.fst (𝒰.f i) (𝒰.f j))
          ((pullback.lift (𝒰.trans (P := P) fi) (𝒰.trans (P := P) fj) ⋯) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
        ↥(𝒰.X i)) ∧
    Eq (α := ↥(𝒰.X j)) ((𝒰.trans (P := P) fj) xk : ↥(𝒰.X j))
      ((pullback.snd (𝒰.f i) (𝒰.f j))
          ((pullback.lift (𝒰.trans (P := P) fi) (𝒰.trans (P := P) fj) ⋯) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
        ↥(𝒰.X j))
⊢ ∃ (k_1 : 𝒰.I₀) (fi_1 : k_1 ⟶ i) (fj_1 : k_1 ⟶ j) (xk_1 : ↥(𝒰.X k_1)),
    Eq (α := ↥(𝒰.X i)) ((𝒰.trans (P := P) fi_1) xk_1 : ↥(𝒰.X i))
        ((pullback.fst (𝒰.f i) (𝒰.f j))
            ((pullback.lift (𝒰.trans (P := P) fi) (𝒰.trans (P := P) fj) ⋯) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
          ↥(𝒰.X i)) ∧
      Eq (α := ↥(𝒰.X j)) ((𝒰.trans (P := P) fj_1) xk_1 : ↥(𝒰.X j))
        ((pullback.snd (𝒰.f i) (𝒰.f j))
            ((pullback.lift (𝒰.trans (P := P) fi) (𝒰.trans (P := P) fj) ⋯) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
          ↥(𝒰.X j))

Tactic:
use k, fi, fj, xk
-- 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) 𝒰
i j k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
xk : ↥(𝒰.X k)
h :
  Eq (α := ↥X)
    ((𝒰.f i)
        ((pullback.fst (𝒰.f i) (𝒰.f j))
            ((pullback.lift (𝒰.trans (P := P) fi) (𝒰.trans (P := P) fj) ⋯) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
          ↥(𝒰.X i)) :
      ↥X)
    ((𝒰.f j)
        ((pullback.snd (𝒰.f i) (𝒰.f j))
            ((pullback.lift (𝒰.trans (P := P) fi) (𝒰.trans (P := P) fj) ⋯) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
          ↥(𝒰.X j)) :
      ↥X)
⊢ Eq (α := ↥(𝒰.X i)) ((𝒰.trans (P := P) fi) xk : ↥(𝒰.X i))
      ((pullback.fst (𝒰.f i) (𝒰.f j))
          ((pullback.lift (𝒰.trans (P := P) fi) (𝒰.trans (P := P) fj) ⋯) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
        ↥(𝒰.X i)) ∧
    Eq (α := ↥(𝒰.X j)) ((𝒰.trans (P := P) fj) xk : ↥(𝒰.X j))
      ((pullback.snd (𝒰.f i) (𝒰.f j))
          ((pullback.lift (𝒰.trans (P := P) fi) (𝒰.trans (P := P) fj) ⋯) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
        ↥(𝒰.X j))

Tactic:
simp [← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- 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) 𝒰
i j : 𝒰.I₀
hij : i ⟶ j
⊢ P (𝒰.trans (P := P) hij)

Tactic:
LocallyDirected.property_trans hij

Premises used: AlgebraicGeometry.Scheme.Cover.LocallyDirected.property_trans, AlgebraicGeometry.Scheme.Cover.trans
-- 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₀
k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)
⊢ 𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).1 ≫ 𝒰.f i =
    𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).2 ≫ 𝒰.f j

Tactic:
simp
-- 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₀
⊢ (∀ (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:
⟨fun x ↦ ?_, fun k ↦ ?_⟩

Premises used: And.intro
-- 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₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∃ (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

Tactic:
use ⟨(𝒰.exists_lift_trans_eq x).choose, (𝒰.exists_lift_trans_eq x).choose_spec.choose,
        (𝒰.exists_lift_trans_eq x).choose_spec.choose_spec.choose⟩
-- 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₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
(𝒰.exists_lift_trans_eq x).choose_spec.choose_spec.choose_spec

Premises used: Exists.choose_spec, Set.Mem, setOf, AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, Classical.choose, Set.range
-- 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₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact (𝒰.exists_lift_trans_eq x).choose_spec.choose_spec.choose_spec

Premises used: Exists.choose_spec, AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq
-- 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₀
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) ⋯ }
refine_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 ≫
      pullback.fst (𝒰.f i) (𝒰.f j))
⊢ 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)

Tactic:
apply P.of_postcomp (W' := P) _ (pullback.fst _ _) (P.pullback_fst _ _ (𝒰.map_prop _))

Premises used: CategoryTheory.MorphismProperty.pullback_fst, CategoryTheory.Limits.pullback.fst, AlgebraicGeometry.Scheme.Cover.map_prop, CategoryTheory.MorphismProperty.of_postcomp
-- 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₀
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 (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).1)

Tactic:
𝒰.property_trans _

Premises used: AlgebraicGeometry.Scheme.Cover.property_trans
-- 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₀
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 (𝒰.trans (P := P) k.snd (β := fun (k : 𝒰.I₀) ↦ (k ⟶ i) × (k ⟶ j)).1)

Tactic:
exact 𝒰.property_trans _

Premises used: AlgebraicGeometry.Scheme.Cover.property_trans
-- 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) 𝒰
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) i
xj : Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) j
hxij :
  Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) fi) :
          (a : (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj i)) →
            (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj k))
        xi :
      (fun (X : Type u) ↦ X) (Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) fj) :
          (a : (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj j)) →
            (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj k))
        xj :
      (fun (X : Type u) ↦ X) (Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) k))
⊢ Eq (α := ↥(𝒰.X k)) ((𝒰.trans (P := P) fi) xi : ↥(𝒰.X k)) ((𝒰.trans (P := P) fj) xj : ↥(𝒰.X k))

Tactic:
simp only [Functor.comp_obj, functorOfLocallyDirected_obj, forget_obj, Functor.comp_map,
      functorOfLocallyDirected_map, forget_map, ConcreteCategory.hom_ofHom,
      TypeCat.Fun.coe_mk] at hxij

Premises used: CategoryTheory.Functor.comp_obj, AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_obj, AlgebraicGeometry.Scheme.forget_map, AlgebraicGeometry.Scheme.forget_obj, TypeCat.Fun.coe_mk, AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_map, CategoryTheory.ConcreteCategory.hom_ofHom, CategoryTheory.Functor.comp_map
-- 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) 𝒰
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) i
xj : Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) j
hxij : Eq (α := ↥(𝒰.X k)) ((𝒰.trans (P := P) fi) xi : ↥(𝒰.X k)) ((𝒰.trans (P := P) fj) xj : ↥(𝒰.X k))
rw : Eq (α := ↥X) ((𝒰.trans (P := P) fi ≫ 𝒰.f k) xi : ↥X) ((𝒰.f j) xj : ↥X)
rw₁ : Eq (α := ↥X) ((𝒰.trans (P := P) fi ≫ 𝒰.f k) xi : ↥X) ((𝒰.trans (P := P) fj ≫ 𝒰.f k) xj : ↥X)
rw₂ :
  Eq (α := ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((𝒰.trans (P := P) fi).base ≫ (𝒰.f k).base) :
          (a : ↥(𝒰.X i)) → ↥X)
        xi :
      ↥X)
    ((𝒰.trans (P := P) fj ≫ 𝒰.f k) xj : ↥X)
rw₃ :
  Eq (α := ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((𝒰.trans (P := P) fi).base ≫ (𝒰.f k).base) :
          (a : ↥(𝒰.X i)) → ↥X)
        xi :
      ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((𝒰.trans (P := P) fj).base ≫ (𝒰.f k).base) :
          (a : ↥(𝒰.X j)) → ↥X)
        xj :
      ↥X)
rw₄ :
  Eq (α := ↥X) ((𝒰.f k) ((𝒰.trans (P := P) fi) xi : ↥(𝒰.X k)) : ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((𝒰.trans (P := P) fj).base ≫ (𝒰.f k).base) :
          (a : ↥(𝒰.X j)) → ↥X)
        xj :
      ↥X)
rw₅ :
  Eq (α := ↥X) ((𝒰.f k) ((𝒰.trans (P := P) fj) xj : ↥(𝒰.X k)) : ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((𝒰.trans (P := P) fj).base ≫ (𝒰.f k).base) :
          (a : ↥(𝒰.X j)) → ↥X)
        xj :
      ↥X)
rw₆ rw₇ :
  Eq (α := ↥X) ((𝒰.f k) ((𝒰.trans (P := P) fj) xj : ↥(𝒰.X k)) : ↥X) ((𝒰.f k) ((𝒰.trans (P := P) fj) xj : ↥(𝒰.X k)) : ↥X)
⊢ Eq (α := ↥X) ((𝒰.f i) xi : ↥X) ((𝒰.f j) xj : ↥X)

Tactic:
rw [← 𝒰.trans_map fi, ← 𝒰.trans_map fj, Hom.comp_base, Hom.comp_base,
        ConcreteCategory.comp_apply, hxij, ConcreteCategory.comp_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, AlgebraicGeometry.Scheme.Cover.trans_map, AlgebraicGeometry.Scheme.Hom.comp_base
-- 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) 𝒰
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) i
xj : Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) j
hxij : Eq (α := ↥(𝒰.X k)) ((𝒰.trans (P := P) fi) xi : ↥(𝒰.X k)) ((𝒰.trans (P := P) fj) xj : ↥(𝒰.X k))
⊢ Eq (α := ↥X) ((𝒰.f i) xi : ↥X) ((𝒰.f j) xj : ↥X)

Tactic:
have : 𝒰.f i xi = 𝒰.f j xj := by
      rw [← 𝒰.trans_map fi, ← 𝒰.trans_map fj, Hom.comp_base, Hom.comp_base,
        ConcreteCategory.comp_apply, hxij, ConcreteCategory.comp_apply]
-- 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) 𝒰
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
l : 𝒰.I₀
gi : l ⟶ i
gj : l ⟶ j
y : ↥(𝒰.X l)
hxij :
  Eq (α := ↥(𝒰.X k))
    ((𝒰.trans (P := P) fi)
        ((pullback.fst (𝒰.f i) (𝒰.f j))
            ((pullback.lift (𝒰.trans (P := P) gi) (𝒰.trans (P := P) gj) ⋯) y : ↥(pullback (𝒰.f i) (𝒰.f j))) :
          ↥(Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P)) i)) :
      ↥(𝒰.X k))
    ((𝒰.trans (P := P) fj)
        ((pullback.snd (𝒰.f i) (𝒰.f j))
            ((pullback.lift (𝒰.trans (P := P) gi) (𝒰.trans (P := P) gj) ⋯) y : ↥(pullback (𝒰.f i) (𝒰.f j))) :
          ↥(Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P)) j)) :
      ↥(𝒰.X k))
this :
  Eq (α := ↥X)
    ((𝒰.f i)
        ((pullback.fst (𝒰.f i) (𝒰.f j))
            ((pullback.lift (𝒰.trans (P := P) gi) (𝒰.trans (P := P) gj) ⋯) y : ↥(pullback (𝒰.f i) (𝒰.f j))) :
          ↥(Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P)) i)) :
      ↥X)
    ((𝒰.f j)
        ((pullback.snd (𝒰.f i) (𝒰.f j))
            ((pullback.lift (𝒰.trans (P := P) gi) (𝒰.trans (P := P) gj) ⋯) y : ↥(pullback (𝒰.f i) (𝒰.f j))) :
          ↥(Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P)) j)) :
      ↥X)
⊢ Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) gi) :
          (a : (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj l)) →
            (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj i))
        y :
      (fun (X : Type u) ↦ X) (Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) i))
    ((pullback.fst (𝒰.f i) (𝒰.f j))
        ((pullback.lift (𝒰.trans (P := P) gi) (𝒰.trans (P := P) gj) ⋯) y : ↥(pullback (𝒰.f i) (𝒰.f j))) :
      ↥(Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P)) i))

Tactic:
simp [← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply