awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
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₀
xi : ↥(𝒰.X i)
xj : ↥(𝒰.X j)
h : Eq (α := ↥X) ((𝒰.f i) xi : ↥X) ((𝒰.f j) xj : ↥X)
⊢ ∃ (k : 𝒰.I₀) (fi : k ⟶ i) (fj : k ⟶ j) (xk : ↥(𝒰.X k)), (𝒰.trans (P := P) fi) xk = xi ∧ (𝒰.trans (P := P) fj) xk = xj
have obtain : ∀ (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)),
  ∃ (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 ⟨z, rfl, rfl⟩ := Scheme.Pullback.exists_preimage_pullback xi xj h
Cleared hypotheses: xi, xj, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
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)
⊢ ∃ (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))
have 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) sorry) 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) sorry) 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) sorry) 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) sorry) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
          ↥(𝒰.X j))
Tactic: obtain ⟨k, fi, fj, xk, rfl⟩ := 𝒰.exists_lift_trans_eq z
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
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)
⊢ ∃ (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))
have 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) sorry) 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) sorry) xk : ↥(pullback (𝒰.f i) (𝒰.f j))) :
      ↥(𝒰.X j))
Tactic: use k, fi, fj, xk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
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
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
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
    (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)
have 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) sorry :
        PreZeroHypercover (pullback (𝒰.f i) (𝒰.f j)) }
      k ≫
    pullback.fst (𝒰.f i) (𝒰.f j))
Tactic: apply P.of_postcomp (W' := P) _ (pullback.fst _ _) (P.pullback_fst _ _ (𝒰.map_prop _))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (hypothesis)
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))
⊢ ∃ (l : 𝒰.I₀) (fli : l ⟶ i) (flj : l ⟶ j) (x :
    Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) l),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) fli) :
            (a : (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj l)) →
              (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj i))
          x =
        xi ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) flj) :
            (a : (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj l)) →
              (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj j))
          x =
        xj
have hxij₁ : 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
Cleared hypotheses: hxij
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
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)
have rw : Eq (α := ↥X) ((𝒰.trans (P := P) fi ≫ 𝒰.f k) 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
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)
⊢ Eq (α := ↥X) ((𝒰.f i) xi : ↥X) ((𝒰.f j) xj : ↥X)
have rw₁ : Eq (α := ↥X) ((𝒰.trans (P := P) fi ≫ 𝒰.f k) xi : ↥X) ((𝒰.trans (P := P) fj ≫ 𝒰.f k) xj : ↥X)
Tactic: rw [← 𝒰.trans_map fi, ← 𝒰.trans_map fj, Hom.comp_base, Hom.comp_base,
        ConcreteCategory.comp_apply, hxij, ConcreteCategory.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
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)
⊢ Eq (α := ↥X) ((𝒰.f i) xi : ↥X) ((𝒰.f j) xj : ↥X)
have 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)
Tactic: rw [← 𝒰.trans_map fi, ← 𝒰.trans_map fj, Hom.comp_base, Hom.comp_base,
        ConcreteCategory.comp_apply, hxij, ConcreteCategory.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
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)
⊢ Eq (α := ↥X) ((𝒰.f i) xi : ↥X) ((𝒰.f j) xj : ↥X)
have 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)
Tactic: rw [← 𝒰.trans_map fi, ← 𝒰.trans_map fj, Hom.comp_base, Hom.comp_base,
        ConcreteCategory.comp_apply, hxij, ConcreteCategory.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
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)
⊢ Eq (α := ↥X) ((𝒰.f i) xi : ↥X) ((𝒰.f j) xj : ↥X)
have 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)
Tactic: rw [← 𝒰.trans_map fi, ← 𝒰.trans_map fj, Hom.comp_base, Hom.comp_base,
        ConcreteCategory.comp_apply, hxij, ConcreteCategory.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
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)
⊢ Eq (α := ↥X) ((𝒰.f i) xi : ↥X) ((𝒰.f j) xj : ↥X)
have 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)
Tactic: rw [← 𝒰.trans_map fi, ← 𝒰.trans_map fj, Hom.comp_base, Hom.comp_base,
        ConcreteCategory.comp_apply, hxij, ConcreteCategory.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
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)
⊢ Eq (α := ↥X) ((𝒰.f i) xi : ↥X) ((𝒰.f j) xj : ↥X)
have rw₆ : Eq (α := ↥X) ((𝒰.f k) ((𝒰.trans (P := P) fj) xj : ↥(𝒰.X k)) : ↥X) ((𝒰.f k) ((𝒰.trans (P := P) fj) xj : ↥(𝒰.X k)) : ↥X)
Tactic: rw [← 𝒰.trans_map fi, ← 𝒰.trans_map fj, Hom.comp_base, Hom.comp_base,
        ConcreteCategory.comp_apply, hxij, ConcreteCategory.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (hypothesis)
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))
⊢ ∃ (l : 𝒰.I₀) (fli : l ⟶ i) (flj : l ⟶ j) (x :
    Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) l),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) fli) :
            (a : (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj l)) →
              (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj i))
          x =
        xi ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) flj) :
            (a : (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj l)) →
              (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj j))
          x =
        xj
have this : 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]