awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
a : ↥(↑U : Scheme)
w :
  Eq.{u + 1} (α := ↥X) (↑((X.homOfLE e) a) : ↥X)
    (↑(((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (X := (↑(↑U : Scheme).toPresheafedSpace : TopCat)) (Y := (↑(↑V : Scheme).toPresheafedSpace : TopCat))
                (CategoryTheory.Functor.map (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) (homOfLE e) :
                  Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) U ⟶
                    Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) V) :
              C(↥(↑U : Scheme), ↥(↑V : Scheme))) :
            (a : ↥(↑U : Scheme)) → ↥(↑V : Scheme))
          a) :
      ↥X)
⊢ Eq (α := ↥(↑V : Scheme)) ((X.homOfLE e) a : ↥(↑V : Scheme))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := (↑(↑U : Scheme).toPresheafedSpace : TopCat)) (Y := (↑(↑V : Scheme).toPresheafedSpace : TopCat))
              (CategoryTheory.Functor.map (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) (homOfLE e) :
                Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) U ⟶
                  Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) V) :
            C(↥(↑U : Scheme), ↥(↑V : Scheme))) :
          (a : ↥(↑U : Scheme)) → ↥(↑V : Scheme))
        a :
      ↥(↑V : Scheme))

Tactic:
refine Subtype.ext ?_

Premises used: Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
a : ↥(↑U : Scheme)
⊢ Eq.{u + 1} (α := ↥X) (↑((X.homOfLE e) a) : ↥X)
    (↑(((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (X := (↑(↑U : Scheme).toPresheafedSpace : TopCat)) (Y := (↑(↑V : Scheme).toPresheafedSpace : TopCat))
                (CategoryTheory.Functor.map (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) (homOfLE e) :
                  Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) U ⟶
                    Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) V) :
              C(↥(↑U : Scheme), ↥(↑V : Scheme))) :
            (a : ↥(↑U : Scheme)) → ↥(↑V : Scheme))
          a) :
      ↥X)

Tactic:
congr($(X.homOfLE_ι e) a)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.homOfLE_ι, id, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
a : ↥(↑U : Scheme)
⊢ Eq.{u + 1} (α := ↥X) (↑((X.homOfLE e) a) : ↥X)
    (↑(((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (X := (↑(↑U : Scheme).toPresheafedSpace : TopCat)) (Y := (↑(↑V : Scheme).toPresheafedSpace : TopCat))
                (CategoryTheory.Functor.map (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) (homOfLE e) :
                  Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) U ⟶
                    Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) V) :
              C(↥(↑U : Scheme), ↥(↑V : Scheme))) :
            (a : ↥(↑U : Scheme)) → ↥(↑V : Scheme))
          a) :
      ↥X)

Tactic:
exact congr($(X.homOfLE_ι e) a)
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥X
hx : x ∈ U
rw :
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑U : Scheme).toPresheafedSpace : TopCat)) (Y := (↑(↑V : Scheme).toPresheafedSpace : TopCat))
            (CategoryTheory.Functor.map (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) (homOfLE e) :
              Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) U ⟶
                Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) V) :
          C(↥(↑U : Scheme), ↥(↑V : Scheme))) :
        (a : ↥(↑U : Scheme)) → ↥(↑V : Scheme))
      (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) =
    Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x ⋯
⊢ (X.homOfLE e) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) = Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x ⋯

Tactic:
rw [homOfLE_base]

Premises used: AlgebraicGeometry.Scheme.homOfLE_base
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥X
hx : x ∈ U
⊢ ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑U : Scheme).toPresheafedSpace : TopCat)) (Y := (↑(↑V : Scheme).toPresheafedSpace : TopCat))
            (CategoryTheory.Functor.map (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) (homOfLE e) :
              Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) U ⟶
                Functor.obj (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) V) :
          C(↥(↑U : Scheme), ↥(↑V : Scheme))) :
        (a : ↥(↑U : Scheme)) → ↥(↑V : Scheme))
      (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) =
    Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x ⋯

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥U
rw rw₁ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) (↑x : ↥X) ⋯) : ↥X) = (↑x : ↥X)
⊢ (↑((X.homOfLE e) x) : ↥X) = (↑x : ↥X)

Tactic:
rw [Scheme.homOfLE_apply']

Premises used: AlgebraicGeometry.Scheme.homOfLE_apply'
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
x : ↥X
h : x ∈ (↑(U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W) : Set ↥X) → x ∈ (↑(V.ι ''ᵁ W ⊓ U) : Set ↥X)
h₁ : x ∈ (↑(V.ι ''ᵁ W ⊓ U) : Set ↥X) → x ∈ (↑(U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W) : Set ↥X)
⊢ x ∈ (↑(U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(V.ι ''ᵁ W ⊓ U) : Set ↥X)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
y : ↥X
hyU : y ∈ U
hyW : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) y hyU ∈ (↑(X.homOfLE e ⁻¹ᵁ W) : Set ↥(↑U : Scheme))
⊢ Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) y ⋯ ∈ (↑W : Set ↥(↑V : Scheme))

Tactic:
simpa [homOfLE_apply'] using hyW

Premises used: AlgebraicGeometry.Scheme.homOfLE_apply'
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
y : ↥X
hyU : y ∈ U
hyW : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) y hyU ∈ (↑(X.homOfLE e ⁻¹ᵁ W) : Set ↥(↑U : Scheme))
⊢ Membership.mem (α := ↥X) (↑(V.ι ''ᵁ W ⊓ U) : Set ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom U.ι)).hom.base :
          (a : ↥(↑U : Scheme)) → ↥X)
        (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) y hyU) :
      ↥X)

Tactic:
exact ⟨⟨⟨y, e hyU⟩, by simpa [homOfLE_apply'] using hyW, rfl⟩, hyU⟩
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
y : ↥(↑V : Scheme)
hyW : y ∈ (↑W : Set ↥(↑V : Scheme))
hyU :
  Membership.mem (α := ↥X) (↑U : Set ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom V.ι)).hom.base :
          (a : ↥(↑V : Scheme)) → ↥X)
        y :
      ↥X)
⊢ Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (↑y : ↥X) hyU ∈ (↑(X.homOfLE e ⁻¹ᵁ W) : Set ↥(↑U : Scheme))

Tactic:
simpa [homOfLE_apply'] using hyW

Premises used: AlgebraicGeometry.Scheme.homOfLE_apply'
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
y : ↥(↑V : Scheme)
hyW : y ∈ (↑W : Set ↥(↑V : Scheme))
hyU :
  Membership.mem (α := ↥X) (↑U : Set ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom V.ι)).hom.base :
          (a : ↥(↑V : Scheme)) → ↥X)
        y :
      ↥X)
⊢ Membership.mem (α := ↥X) (↑(U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W) : Set ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom V.ι)).hom.base :
          (a : ↥(↑V : Scheme)) → ↥X)
        y :
      ↥X)

Tactic:
exact ⟨⟨y.1, hyU⟩, by simpa [homOfLE_apply'] using hyW, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
⊢ U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W ≤ V.ι ''ᵁ W

Tactic:
simp [Scheme.ι_image_homOfLE_eq_ι_image_inf]

Premises used: AlgebraicGeometry.Scheme.ι_image_homOfLE_eq_ι_image_inf
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
⊢ Eq (α := Γ(X, V.ι ''ᵁ W) ⟶ Γ((↑U : Scheme), (X.homOfLE e ≫ V.ι) ⁻¹ᵁ V.ι ''ᵁ W))
    (Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W))
    (Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
have e₁ := Scheme.Hom.congr_app (X.homOfLE_ι e) (V.ι ''ᵁ W)
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
e₁ :
  Eq (α := Γ(X, V.ι ''ᵁ W) ⟶ Γ((↑U : Scheme), (X.homOfLE e ≫ V.ι) ⁻¹ᵁ V.ι ''ᵁ W))
    (Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W))
    (Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ V.ι ⁻¹ᵁ V.ι ''ᵁ W = W

Tactic:
have : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W := W.map_functor_eq (U := V)
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
e₁ :
  Eq (α := Γ(X, V.ι ''ᵁ W) ⟶ Γ((↑U : Scheme), (X.homOfLE e ≫ V.ι) ⁻¹ᵁ V.ι ''ᵁ W))
    (Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W))
    (Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
⊢ (↑V : Scheme).presheaf.map (Quiver.Hom.op (Iso.hom (eqToIso this))) ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫
      (↑U : Scheme).presheaf.map
        ((Opens.map (X.homOfLE e).base).map (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (eqToIso this))))).op

Tactic:
have e₂ := (X.homOfLE e).naturality (eqToIso this).hom.op
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
e₁ :
  Eq (α := Γ(X, V.ι ''ᵁ W) ⟶ Γ((↑U : Scheme), (X.homOfLE e ≫ V.ι) ⁻¹ᵁ V.ι ''ᵁ W))
    (Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W))
    (Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V : Scheme).presheaf.map (Quiver.Hom.op (Iso.hom (eqToIso this))) ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫
      (↑U : Scheme).presheaf.map
        ((Opens.map (X.homOfLE e).base).map (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (eqToIso this))))).op
⊢ Hom.app (X.homOfLE e) W ≫
      (↑U : Scheme).presheaf.map
        ((Opens.map (X.homOfLE e).base).map (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (eqToIso this))))).op =
    Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
have e₃ := e₂.symm.trans e₁
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
e₁ :
  Eq (α := Γ(X, V.ι ''ᵁ W) ⟶ Γ((↑U : Scheme), (X.homOfLE e ≫ V.ι) ⁻¹ᵁ V.ι ''ᵁ W))
    (Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W))
    (Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V : Scheme).presheaf.map (Quiver.Hom.op (Iso.hom (eqToIso this))) ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫
      (↑U : Scheme).presheaf.map
        ((Opens.map (X.homOfLE e).base).map (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (eqToIso this))))).op
e₃ :
  Hom.app (X.homOfLE e) W ≫
      X.presheaf.map ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op =
    CategoryStruct.comp (Y := Γ((↑U : Scheme), U.ι ⁻¹ᵁ V.ι ''ᵁ W)) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (X.presheaf.map (Quiver.Hom.op ((Hom.opensFunctor U.ι).map (eqToHom ⋯))))
⊢ Hom.app (X.homOfLE e) W =
    X.presheaf.map
        (CategoryStruct.comp (Y := op (U.ι ''ᵁ U.ι ⁻¹ᵁ V.ι ''ᵁ W)) (Quiver.Hom.op (homOfLE ⋯))
          (Quiver.Hom.op ((Hom.opensFunctor U.ι).map (eqToHom ⋯)))) ≫
      X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)

Tactic:
rw [← IsIso.eq_comp_inv, ← Functor.map_inv, ← Functor.map_comp] at e₃

Premises used: CategoryTheory.Functor.map_inv, CategoryTheory.IsIso.eq_comp_inv, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
e₁ :
  Eq (α := Γ(X, V.ι ''ᵁ W) ⟶ Γ((↑U : Scheme), (X.homOfLE e ≫ V.ι) ⁻¹ᵁ V.ι ''ᵁ W))
    (Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W))
    (Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V : Scheme).presheaf.map (Quiver.Hom.op (Iso.hom (eqToIso this))) ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫
      (↑U : Scheme).presheaf.map
        ((Opens.map (X.homOfLE e).base).map (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (eqToIso this))))).op
e₃ :
  Hom.app (X.homOfLE e) W =
    X.presheaf.map
        (CategoryStruct.comp (Y := op (U.ι ''ᵁ U.ι ⁻¹ᵁ V.ι ''ᵁ W)) (Quiver.Hom.op (homOfLE ⋯))
          (Quiver.Hom.op ((Hom.opensFunctor U.ι).map (eqToHom ⋯)))) ≫
      X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
rw :
  X.presheaf.map
      (CategoryStruct.comp (Y := op (U.ι ''ᵁ U.ι ⁻¹ᵁ V.ι ''ᵁ W)) (Quiver.Hom.op (homOfLE ⋯))
          (Quiver.Hom.op ((Hom.opensFunctor U.ι).map (eqToHom ⋯))) ≫
        inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op) =
    X.presheaf.map (homOfLE ⋯).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [e₃, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
e₁ :
  Eq (α := Γ(X, V.ι ''ᵁ W) ⟶ Γ((↑U : Scheme), (X.homOfLE e ≫ V.ι) ⁻¹ᵁ V.ι ''ᵁ W))
    (Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W))
    (Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V : Scheme).presheaf.map (Quiver.Hom.op (Iso.hom (eqToIso this))) ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫
      (↑U : Scheme).presheaf.map
        ((Opens.map (X.homOfLE e).base).map (Quiver.Hom.unop (Quiver.Hom.op (Iso.hom (eqToIso this))))).op
e₃ :
  Hom.app (X.homOfLE e) W =
    X.presheaf.map
        (CategoryStruct.comp (Y := op (U.ι ''ᵁ U.ι ⁻¹ᵁ V.ι ''ᵁ W)) (Quiver.Hom.op (homOfLE ⋯))
          (Quiver.Hom.op ((Hom.opensFunctor U.ι).map (eqToHom ⋯)))) ≫
      X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
⊢ X.presheaf.map
      (CategoryStruct.comp (Y := op (U.ι ''ᵁ U.ι ⁻¹ᵁ V.ι ''ᵁ W)) (Quiver.Hom.op (homOfLE ⋯))
          (Quiver.Hom.op ((Hom.opensFunctor U.ι).map (eqToHom ⋯))) ≫
        inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op) =
    X.presheaf.map (homOfLE ⋯).op

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V : Scheme).Opens
W' : (↑U : Scheme).Opens
e' : W' ≤ X.homOfLE e ⁻¹ᵁ W
⊢ Hom.appLE (X.homOfLE e) W W' e' = X.presheaf.map (homOfLE ⋯).op

Tactic:
simp [Scheme.Hom.appLE, Scheme.homOfLE_app, ← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.Scheme.homOfLE_app, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
⊢ Hom.appTop (X.homOfLE e) = X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
homOfLE_app ..

Premises used: Set.Mem, Set.univ, setOf, AlgebraicGeometry.Scheme.homOfLE_app, Set.preimage
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
X : Scheme
U V : X.Opens
e : U ≤ V
⊢ IsOpenImmersion (IsOpenImmersion.lift V.ι U.ι ⋯)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
⊢ Eq.{u + 1} (α := X.Opens) ((fun (x : (↑V : Scheme).Opens) ↦ V.ι ''ᵁ x) (Hom.opensRange (X.homOfLE e)))
    ((fun (x : (↑V : Scheme).Opens) ↦ V.ι ''ᵁ x) (V.ι ⁻¹ᵁ U))

Tactic:
simp [← Hom.opensRange_comp, Hom.image_preimage_eq_opensRange_inf, e]

Premises used: AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.Scheme.Hom.opensRange_comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
rw :
  (∀ (x : ↥(↑(⨆ (i : J), U i) : Scheme)),
      ∃ (i :
        PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
          { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ }),
        Membership.mem (γ := Set ↥(↑(⨆ (i : J), U i) : Scheme))
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
                  PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
                  PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
          { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
            PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
          i)
⊢ Membership.mem (γ := Set (Presieve (↑(⨆ (i : J), U i) : Scheme)))
    ((precoverage IsOpenImmersion).coverings (↑(⨆ (i : J), U i) : Scheme))
    (PreZeroHypercover.presieve₀.{u_1, u_2, u_2 + 1}
      { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ })

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
⊢ (∀ (x : ↥(↑(⨆ (i : J), U i) : Scheme)),
      ∃ (i :
        PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
          { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ }),
        Membership.mem (γ := Set ↥(↑(⨆ (i : J), U i) : Scheme))
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
                  PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
                  PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
          { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
            PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
          i)

Tactic:
⟨fun x ↦ ?_, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
refine :
  ∀ (x : ↥(↑(⨆ (i : J), U i) : Scheme)),
    ∃ (i :
      PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
        { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ }),
      Membership.mem (γ := Set ↥(↑(⨆ (i : J), U i) : Scheme))
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
                PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
                PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
              i))
        x
⊢ (∀ (x : ↥(↑(⨆ (i : J), U i) : Scheme)),
      ∃ (i :
        PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
          { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ }),
        Membership.mem (γ := Set ↥(↑(⨆ (i : J), U i) : Scheme))
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
                  PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
                  PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
          { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
            PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
          i)

Tactic:
refine ⟨fun x ↦ ?_, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
x : ↥(↑(⨆ (i : J), U i) : Scheme)
obtain :
  ∀ (i : J) (hi : (↑x : ↥X) ∈ U i),
    ∃ (i :
      PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
        { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ }),
      Membership.mem (γ := Set ↥(↑(⨆ (i : J), U i) : Scheme))
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
                PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
                PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
              i))
        x
⊢ ∃ (i :
    PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
      { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ }),
    Membership.mem (γ := Set ↥(↑(⨆ (i : J), U i) : Scheme))
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
              PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
              PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
            i))
      x

Tactic:
obtain ⟨i, hi⟩ := TopologicalSpace.Opens.mem_iSup.mp x.2

Premises used: TopologicalSpace.Opens.mem_iSup, Iff.mp, Subtype.property