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 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) j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) gj) :
          (a : (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj l)) →
            (fun (X : Type u) ↦ X) ((𝒰.functorOfLocallyDirected ⋙ forget).obj j))
        y :
      (fun (X : Type u) ↦ X) (Functor.obj.{v_1, u, u_1, u + 1} (𝒰.functorOfLocallyDirected (P := P) ⋙ forget) 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))

Tactic:
simp [← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Category.{v_1, u_1} 𝒰.I₀
inst_1 : Cover.LocallyDirected.{v_1, u, u_1} (P := IsOpenImmersion) 𝒰
i j : 𝒰.I₀
f : i ⟶ j
⊢ IsOpenImmersion (Cover.trans (P := IsOpenImmersion) 𝒰 f)

Tactic:
𝒰.property_trans f

Premises used: AlgebraicGeometry.Scheme.Cover.property_trans
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Category.{v_1, u_1} 𝒰.I₀
inst_1 : Cover.LocallyDirected.{v_1, u, u_1} (P := IsOpenImmersion) 𝒰
i j : 𝒰.I₀
f : i ⟶ j
⊢ IsOpenImmersion (X := Functor.obj.{v_1, u, u_1, u + 1} (Cover.functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)
    (CategoryTheory.Functor.map (Cover.functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) f)

Tactic:
𝒰.property_trans f

Premises used: AlgebraicGeometry.Scheme.Cover.property_trans
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰_1 : X.OpenCover
inst : Category.{v_1, ?u.61286} 𝒰_1.I₀
inst_1 : Cover.LocallyDirected.{v_1, u, ?u.61286} (P := IsOpenImmersion) 𝒰_1
𝒰 : OpenCover.{u_1, u} X
inst_2 : Category.{v_2, u_1} 𝒰.I₀
inst_3 : Cover.LocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰
Y : Scheme
g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y
h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), Cover.trans (P := IsOpenImmersion) 𝒰 hij ≫ g j = g i
i j : 𝒰.I₀
h₁ :
  ∀ (x : (Cover.intersectionOfLocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰 i j).I₀),
    (Cover.intersectionOfLocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰 i j).f x ≫
        pullback.fst (𝒰.f i) (𝒰.f j) ≫ g i =
      (Cover.intersectionOfLocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰 i j).f x ≫
        pullback.snd (𝒰.f i) (𝒰.f j) ≫ g j
⊢ Eq (α := pullback (𝒰.f i) (𝒰.f j) ⟶ Y) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ g i) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ g j)

Tactic:
apply (𝒰.intersectionOfLocallyDirected i j).hom_ext

Premises used: AlgebraicGeometry.Scheme.Cover.hom_ext, AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰_1 : X.OpenCover
inst : Category.{v_1, ?u.61286} 𝒰_1.I₀
inst_1 : Cover.LocallyDirected.{v_1, u, ?u.61286} (P := IsOpenImmersion) 𝒰_1
𝒰 : OpenCover.{u_1, u} X
inst_2 : Category.{v_2, u_1} 𝒰.I₀
inst_3 : Cover.LocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰
Y : Scheme
g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y
h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), Cover.trans (P := IsOpenImmersion) 𝒰 hij ≫ g j = g i
i j : 𝒰.I₀
k : (Cover.intersectionOfLocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰 i j).I₀
⊢ (Cover.intersectionOfLocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰 i j).f k ≫
      pullback.fst (𝒰.f i) (𝒰.f j) ≫ g i =
    (Cover.intersectionOfLocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰 i j).f k ≫
      pullback.snd (𝒰.f i) (𝒰.f j) ≫ g j

Tactic:
simp [h]
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Category.{v_1, u_1} 𝒰.I₀
inst_1 : Cover.LocallyDirected.{v_1, u, u_1} (P := IsOpenImmersion) 𝒰
Y : Scheme
g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y
h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), Cover.trans (P := IsOpenImmersion) 𝒰 hij ≫ g j = g i
i : 𝒰.I₀
⊢ 𝒰.f i ≫ glueMorphismsOfLocallyDirected.{v_1, u, u_1} 𝒰 g ⋯ = g i

Tactic:
simp [glueMorphismsOfLocallyDirected]

Premises used: AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOfLocallyDirected
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Category.{v_1, u_1} 𝒰.I₀
inst_1 : Cover.LocallyDirected.{v_1, u, u_1} (P := IsOpenImmersion) 𝒰
s : Cocone.{v_1, u, u_1, u + 1} (Cover.functorOfLocallyDirected (P := IsOpenImmersion) 𝒰)
m :
  Cocone.pt.{v_1, u, u_1, u + 1} (F := Cover.functorOfLocallyDirected (P := IsOpenImmersion) 𝒰)
      (Cover.coconeOfLocallyDirected (P := IsOpenImmersion) 𝒰) ⟶
    s.pt
hm : ∀ (j : 𝒰.I₀), NatTrans.app (Cocone.ι (Cover.coconeOfLocallyDirected (P := IsOpenImmersion) 𝒰)) j ≫ m = s.ι.app j
j : 𝒰.I₀
⊢ 𝒰.f j ≫ m = 𝒰.f j ≫ glueMorphismsOfLocallyDirected.{v_1, u, u_1} 𝒰 s.ι.app ⋯

Tactic:
simpa using hm j
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X_1 : Scheme
𝒰_1 : X_1.OpenCover
inst : Category.{v_1, ?u.66091} 𝒰_1.I₀
inst_1 : Cover.LocallyDirected.{v_1, u, ?u.66091} (P := IsOpenImmersion) 𝒰_1
S : Scheme
X : Over S
𝒰 : OpenCover.{u_1, u} X.left
inst_2 : Category.{v_2, u_1} 𝒰.I₀
inst_3 : Cover.LocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰
Y : Over S
g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left
h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), Cover.trans (P := IsOpenImmersion) 𝒰 hij ≫ g j = g i
w : ∀ (i : 𝒰.I₀), g i ≫ Y.hom = 𝒰.f i ≫ X.hom
h₁ : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ glueMorphismsOfLocallyDirected.{v_2, u, u_1} 𝒰 g ⋯ ≫ Y.hom = 𝒰.f x ≫ X.hom
⊢ glueMorphismsOfLocallyDirected.{v_2, u, u_1} 𝒰 g ⋯ ≫ Y.hom = X.hom

Tactic:
apply 𝒰.hom_ext

Premises used: AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X_1 : Scheme
𝒰_1 : X_1.OpenCover
inst : Category.{v_1, ?u.66091} 𝒰_1.I₀
inst_1 : Cover.LocallyDirected.{v_1, u, ?u.66091} (P := IsOpenImmersion) 𝒰_1
S : Scheme
X : Over S
𝒰 : OpenCover.{u_1, u} X.left
inst_2 : Category.{v_2, u_1} 𝒰.I₀
inst_3 : Cover.LocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰
Y : Over S
g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left
h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), Cover.trans (P := IsOpenImmersion) 𝒰 hij ≫ g j = g i
w : ∀ (i : 𝒰.I₀), g i ≫ Y.hom = 𝒰.f i ≫ X.hom
i : 𝒰.I₀
⊢ 𝒰.f i ≫ glueMorphismsOfLocallyDirected.{v_2, u, u_1} 𝒰 g ⋯ ≫ Y.hom = 𝒰.f i ≫ X.hom

Tactic:
simp [w]
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
S : Scheme
X : Over S
𝒰 : OpenCover.{u_1, u} X.left
inst : Category.{v_2, u_1} 𝒰.I₀
inst_1 : Cover.LocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰
Y : Over S
g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left
h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), Cover.trans (P := IsOpenImmersion) 𝒰 hij ≫ g j = g i
w : ∀ (i : 𝒰.I₀), g i ≫ Y.hom = 𝒰.f i ≫ X.hom
i : 𝒰.I₀
⊢ 𝒰.f i ≫ Over.Hom.left (glueMorphismsOverOfLocallyDirected.{v_2, u, u_1} 𝒰 g ⋯ w) = g i

Tactic:
simp [glueMorphismsOverOfLocallyDirected]

Premises used: AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOverOfLocallyDirected
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i : 𝒰.I₀
rw : IsOpenImmersion.lift (𝒰.f i) (𝒰.f i) ⋯ ≫ 𝒰.f i = 𝟙 (𝒰.X i) ≫ 𝒰.f i
⊢ IsOpenImmersion.lift (𝒰.f i) (𝒰.f i) ⋯ = 𝟙 (𝒰.X i)

Tactic:
rw [← cancel_mono (𝒰.f i)]

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.cancel_mono, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i : 𝒰.I₀
⊢ IsOpenImmersion.lift (𝒰.f i) (𝒰.f i) ⋯ ≫ 𝒰.f i = 𝟙 (𝒰.X i) ≫ 𝒰.f i

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j k : 𝒰.I₀
hij : i ⟶ j
hjk : j ⟶ k
rw :
  IsOpenImmersion.lift (𝒰.f k) (𝒰.f i) ⋯ ≫ 𝒰.f k =
    (IsOpenImmersion.lift (𝒰.f j) (𝒰.f i) ⋯ ≫ IsOpenImmersion.lift (𝒰.f k) (𝒰.f j) ⋯) ≫ 𝒰.f k
⊢ IsOpenImmersion.lift (𝒰.f k) (𝒰.f i) ⋯ =
    IsOpenImmersion.lift (𝒰.f j) (𝒰.f i) ⋯ ≫ IsOpenImmersion.lift (𝒰.f k) (𝒰.f j) ⋯

Tactic:
rw [← cancel_mono (𝒰.f _)]

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.cancel_mono, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j k : 𝒰.I₀
hij : i ⟶ j
hjk : j ⟶ k
⊢ IsOpenImmersion.lift (𝒰.f k) (𝒰.f i) ⋯ ≫ 𝒰.f k =
    (IsOpenImmersion.lift (𝒰.f j) (𝒰.f i) ⋯ ≫ IsOpenImmersion.lift (𝒰.f k) (𝒰.f j) ⋯) ≫ 𝒰.f k

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
⊢ Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)

Tactic:
have : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈
      (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i).opensRange := ⟨x, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
obtain :
  ∀ (k : 𝒰.I₀)
    (h :
      (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
        Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    (y : ↥(𝒰.X k)) (hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)),
    ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.X k)),
      (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x
⊢ ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.X k)),
    (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x

Tactic:
obtain ⟨k, ⟨k, rfl⟩, ⟨y, hy⟩, h⟩ := TopologicalSpace.Opens.isBasis_iff_nbhd.mp H this

Premises used: TopologicalSpace.Opens.isBasis_iff_nbhd, Iff.mp, rfl
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
⊢ ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.X k)),
    (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x

Tactic:
⟨k, homOfLE <| hle.mpr <| le_trans h ?_, homOfLE <| hle.mpr <| le_trans h ?_, y, ?_⟩

Premises used: Iff.mpr, CategoryTheory.homOfLE, Exists.intro, le_trans
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
refine_1 :
  Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≤ Hom.opensRange (𝒰.f i)
refine_2 :
  Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
refine_3 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.X k)),
    (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x

Tactic:
refine ⟨k, homOfLE <| hle.mpr <| le_trans h ?_, homOfLE <| hle.mpr <| le_trans h ?_, y, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
refine_1 :
  𝒰.f i ''ᵁ Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j)) ≤ Hom.opensRange (𝒰.f i)
⊢ Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≤ Hom.opensRange (𝒰.f i)

Tactic:
rw [Scheme.Hom.opensRange_comp]

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange_comp
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
⊢ 𝒰.f i ''ᵁ Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j)) ≤ Hom.opensRange (𝒰.f i)

Tactic:
Set.image_subset_range _ _

Premises used: Set.Mem, setOf, Set.image_subset_range, Set.Subset, Set.image, Set.range
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
⊢ 𝒰.f i ''ᵁ Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j)) ≤ Hom.opensRange (𝒰.f i)

Tactic:
exact Set.image_subset_range _ _

Premises used: Set.image_subset_range
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
refine_2 :
  𝒰.f j ''ᵁ Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j)) ≤ Hom.opensRange (𝒰.f j)
⊢ Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≤ Hom.opensRange (𝒰.f j)

Tactic:
simp_rw [pullback.condition, Scheme.Hom.opensRange_comp]

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange_comp, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
⊢ 𝒰.f j ''ᵁ Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j)) ≤ Hom.opensRange (𝒰.f j)

Tactic:
Set.image_subset_range _ _

Premises used: Set.Mem, setOf, Set.image_subset_range, Set.Subset, Set.image, Set.range
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
⊢ 𝒰.f j ''ᵁ Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j)) ≤ Hom.opensRange (𝒰.f j)

Tactic:
exact Set.image_subset_range _ _

Premises used: Set.image_subset_range
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
refine_3 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i).isOpenEmbedding.injective

Premises used: CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, CategoryTheory.Limits.pullback.fst, Topology.IsEmbedding.injective, CategoryTheory.CategoryStruct.comp, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
i j : 𝒰.I₀
⊢ i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)

Tactic:
hle
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
⊢ ∀ (hij : i ≤ j), Cover.trans (P := IsOpenImmersion) 𝒰 (homOfLE hij) = IsOpenImmersion.lift (𝒰.f j) (𝒰.f i) ⋯

Tactic:
fun _ ↦ rfl

Premises used: AlgebraicGeometry.Scheme.Cover.trans, rfl