awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
refine :
  ∀ (x : ↥X),
    ∃ (i :
      PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
        { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
                PreZeroHypercover.{u_1, u, u + 1} X }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
                PreZeroHypercover.{u_1, u, u + 1} X }
              i))
        x
⊢ (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
          { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
                  PreZeroHypercover.{u_1, u, u + 1} X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
                  PreZeroHypercover.{u_1, u, u + 1} X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
          { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
            PreZeroHypercover.{u_1, u, u + 1} X }
          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
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
⊢ Membership.mem (γ := X.Opens) ⊤ x

Tactic:
trivial
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
⊢ Membership.mem (γ := X.Opens) (⨆ (i : s), U i) x

Tactic:
have hx : x ∈ ⨆ i, U i := hU.symm ▸ show x ∈ (⊤ : X.Opens) by trivial
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
hx : Membership.mem (γ := X.Opens) (⨆ (i : s), U i) x
⊢ ∃ (i : s), x ∈ U i

Tactic:
rw [Opens.mem_iSup] at hx

Premises used: TopologicalSpace.Opens.mem_iSup
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
hx : ∃ (i : s), x ∈ U i
obtain :
  ∀ (i : s) (hi : x ∈ U i),
    ∃ (i :
      PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
        { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
                PreZeroHypercover.{u_1, u, u + 1} X }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
                PreZeroHypercover.{u_1, u, u + 1} X }
              i))
        x
⊢ ∃ (i :
    PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
      { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
      x

Tactic:
obtain ⟨i, hi⟩ := hx
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
i : s
hi : x ∈ U i
h :
  Membership.mem (γ := Set ↥X)
    (Set.range (ι :=
      ↥(PreZeroHypercover.X (S := X)
          { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
            PreZeroHypercover.{u_1, u, u + 1} X }
          i))
      ⇑(PreZeroHypercover.f { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι } i))
    x
⊢ ∃ (i :
    PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
      { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
      x

Tactic:
use i
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
i : s
hi : x ∈ U i
⊢ Membership.mem (γ := Set ↥X)
    (Set.range (ι :=
      ↥(PreZeroHypercover.X (S := X)
          { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
            PreZeroHypercover.{u_1, u, u + 1} X }
          i))
      ⇑(PreZeroHypercover.f { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι } i))
    x

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ Eq.{max 1 (u + 1)} (α := X.Opens → Prop) (fun (U_1 : X.Opens) ↦ U_1 ≤ Scheme.Hom.opensRange U.ι) fun (V : X.Opens) ↦
    V ≤ U

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
⊢ U.ι ''ᵁ (↑U : Scheme).basicOpen r =
    X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        r)

Tactic:
(Scheme.image_basicOpen (X.ofRestrict U.isOpenEmbedding) r).trans ?_

Premises used: TopologicalSpace.Opens.isOpenEmbedding, AlgebraicGeometry.Scheme.image_basicOpen, AlgebraicGeometry.Scheme.ofRestrict, AlgebraicGeometry.Scheme.Opens.toScheme, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
refine :
  X.basicOpen (U := X.ofRestrict ⋯ ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X.restrict ⋯, ⊤)) (Y := Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤))
            (Iso.inv (Hom.appIso (X.ofRestrict ⋯) ⊤)) :
          (a : (↑Γ(X.restrict ⋯, ⊤) : Type u)) → (↑Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤) : Type u))
        r) =
    X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        r)
⊢ U.ι ''ᵁ (↑U : Scheme).basicOpen r =
    X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        r)

Tactic:
refine (Scheme.image_basicOpen (X.ofRestrict U.isOpenEmbedding) r).trans ?_

Premises used: TopologicalSpace.Opens.isOpenEmbedding, AlgebraicGeometry.Scheme.image_basicOpen, AlgebraicGeometry.Scheme.ofRestrict, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
rw :
  X.basicOpen (U := X.ofRestrict ⋯ ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X.restrict ⋯, ⊤)) (Y := Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤))
            (Iso.inv (Hom.appIso (X.ofRestrict ⋯) ⊤)) :
          (a : (↑Γ(X.restrict ⋯, ⊤) : Type u)) → (↑Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤) : Type u))
        r) =
    X.basicOpen (U := ⋯.functor.obj ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, ⋯.functor.obj ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
              (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
            r :
          (↑Γ(X, U) : Type u)))
⊢ X.basicOpen (U := X.ofRestrict ⋯ ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X.restrict ⋯, ⊤)) (Y := Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤))
            (Iso.inv (Hom.appIso (X.ofRestrict ⋯) ⊤)) :
          (a : (↑Γ(X.restrict ⋯, ⊤) : Type u)) → (↑Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤) : Type u))
        r) =
    X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        r)

Tactic:
rw [← Scheme.basicOpen_res_eq _ _ (eqToHom U.isOpenEmbedding_obj_top).op]

Premises used: Quiver.Hom.op, TopologicalSpace.Opens.isOpenEmbedding_obj_top, CategoryTheory.eqToHom, AlgebraicGeometry.Scheme.basicOpen_res_eq
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
rw :
  X.basicOpen (U := X.ofRestrict ⋯ ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X.restrict ⋯, ⊤)) (Y := Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤))
            (Iso.inv (Hom.appIso (X.ofRestrict ⋯) ⊤)) :
          (a : (↑Γ(X.restrict ⋯, ⊤) : Type u)) → (↑Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤) : Type u))
        r) =
    X.basicOpen (U := ⋯.functor.obj ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (𝟙 (op (⋯.functor.obj ⊤)))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, ⋯.functor.obj ⊤) : Type u))
        r)
⊢ X.basicOpen (U := X.ofRestrict ⋯ ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X.restrict ⋯, ⊤)) (Y := Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤))
            (Iso.inv (Hom.appIso (X.ofRestrict ⋯) ⊤)) :
          (a : (↑Γ(X.restrict ⋯, ⊤) : Type u)) → (↑Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤) : Type u))
        r) =
    X.basicOpen (U := ⋯.functor.obj ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, ⋯.functor.obj ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
              (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
            r :
          (↑Γ(X, U) : Type u)))

Tactic:
rw [← CommRingCat.comp_apply, ← CategoryTheory.Functor.map_comp, ← op_comp, eqToHom_trans,
    eqToHom_refl, op_id]

Premises used: CategoryTheory.op_comp, CategoryTheory.eqToHom_refl, CommRingCat.comp_apply, CategoryTheory.Functor.map_comp, CategoryTheory.eqToHom_trans, CategoryTheory.op_id
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
e_f : Iso.inv (Hom.appIso (X.ofRestrict ⋯) ⊤) = X.presheaf.map (𝟙 (op (⋯.functor.obj ⊤)))
⊢ X.basicOpen (U := X.ofRestrict ⋯ ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X.restrict ⋯, ⊤)) (Y := Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤))
            (Iso.inv (Hom.appIso (X.ofRestrict ⋯) ⊤)) :
          (a : (↑Γ(X.restrict ⋯, ⊤) : Type u)) → (↑Γ(X, X.ofRestrict ⋯ ''ᵁ ⊤) : Type u))
        r) =
    X.basicOpen (U := ⋯.functor.obj ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (𝟙 (op (⋯.functor.obj ⊤)))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, ⋯.functor.obj ⊤) : Type u))
        r)

Tactic:
congr
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
⊢ Iso.inv (Hom.appIso (X.ofRestrict ⋯) ⊤) = X.presheaf.map (𝟙 (op (⋯.functor.obj ⊤)))

Tactic:
(PresheafedSpace.IsOpenImmersion.ofRestrict_invApp _ _ _).trans
    (CategoryTheory.Functor.map_id _ _).symm

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp, CategoryTheory.Functor.map_id, Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
⊢ Iso.inv (Hom.appIso (X.ofRestrict ⋯) ⊤) = X.presheaf.map (𝟙 (op (⋯.functor.obj ⊤)))

Tactic:
exact (PresheafedSpace.IsOpenImmersion.ofRestrict_invApp _ _ _).trans
    (CategoryTheory.Functor.map_id _ _).symm

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp, CategoryTheory.Functor.map_id, Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
rw :
  X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        r) =
    X.basicOpen r
rw₁ rw₂ : X.basicOpen r = X.basicOpen r
⊢ U.ι ''ᵁ (↑U : Scheme).basicOpen r = X.basicOpen r

Tactic:
rw [Scheme.Opens.ι_image_basicOpen', Scheme.basicOpen_res_eq]

Premises used: AlgebraicGeometry.Scheme.basicOpen_res_eq, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen'
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
simp :
  U.ι ''ᵁ
      (↑U : Scheme).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) U.topIso.inv :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
          r) =
    X.basicOpen r
⊢ U.ι ''ᵁ
      (↑U : Scheme).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) U.topIso.inv :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
          r) =
    X.basicOpen r

Tactic:
simp only [Scheme.Opens.toScheme_presheaf_obj]

Premises used: AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
rw :
  X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U.ι ''ᵁ ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) U.topIso.inv :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
            r :
          (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))) =
    X.basicOpen r
rw₁ :
  X.basicOpen (U := U.ι ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) U.topIso.inv :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
        r) =
    X.basicOpen r
rw₂ :
  X.basicOpen (U := U.ι ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
        r) =
    X.basicOpen r
rw₃ rw₄ : X.basicOpen r = X.basicOpen r
⊢ U.ι ''ᵁ
      (↑U : Scheme).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) U.topIso.inv :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
          r) =
    X.basicOpen r

Tactic:
rw [ι_image_basicOpen', basicOpen_res_eq, topIso_inv, basicOpen_res_eq X]

Premises used: AlgebraicGeometry.Scheme.Opens.topIso_inv, AlgebraicGeometry.Scheme.basicOpen_res_eq, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen'
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
V : (↑U : Scheme).Opens
r : (↑Γ((↑U : Scheme), V) : Type u)
x : ↥U
rw :
  Membership.mem (γ := (↑U : Scheme).Opens)
      ((↑U : Scheme).basicOpen (U := U.ι ⁻¹ᵁ U.ι ''ᵁ V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ((↑U : Scheme), U.ι ⁻¹ᵁ U.ι ''ᵁ V))
              ((↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
            (a : (↑Γ((↑U : Scheme), V) : Type u)) → (↑Γ((↑U : Scheme), U.ι ⁻¹ᵁ U.ι ''ᵁ V) : Type u))
          r))
      x ↔
    (↑x : ↥X) ∈ X.basicOpen r
⊢ x ∈ (↑U : Scheme).basicOpen r ↔ (↑x : ↥X) ∈ X.basicOpen r

Tactic:
rw [← U.toScheme.basicOpen_res_eq _ (eqToHom (U.ι.preimage_image_eq V)).op]

Premises used: Quiver.Hom.op, CategoryTheory.eqToHom, AlgebraicGeometry.Scheme.Hom.preimage_image_eq, AlgebraicGeometry.Scheme.basicOpen_res_eq, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Opens.toScheme
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
V : (↑U : Scheme).Opens
r : (↑Γ((↑U : Scheme), V) : Type u)
x : ↥U
⊢ Membership.mem (γ := (↑U : Scheme).Opens)
      ((↑U : Scheme).basicOpen (U := U.ι ⁻¹ᵁ U.ι ''ᵁ V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ((↑U : Scheme), U.ι ⁻¹ᵁ U.ι ''ᵁ V))
              ((↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
            (a : (↑Γ((↑U : Scheme), V) : Type u)) → (↑Γ((↑U : Scheme), U.ι ⁻¹ᵁ U.ι ''ᵁ V) : Type u))
          r))
      x ↔
    (↑x : ↥X) ∈ X.basicOpen r

Tactic:
congr(x ∈ $(U.ι.preimage_basicOpen r)).to_iff.symm

Premises used: IsOpenMap.functorMap, congrArg, Set.Mem, Quiver.Hom.op, setOf, Eq.to_iff, Membership.mem, id, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen, Set.preimage, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.Opens.ι, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
V : (↑U : Scheme).Opens
r : (↑Γ((↑U : Scheme), V) : Type u)
x : ↥U
⊢ Membership.mem (γ := (↑U : Scheme).Opens)
      ((↑U : Scheme).basicOpen (U := U.ι ⁻¹ᵁ U.ι ''ᵁ V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ((↑U : Scheme), U.ι ⁻¹ᵁ U.ι ''ᵁ V))
              ((↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
            (a : (↑Γ((↑U : Scheme), V) : Type u)) → (↑Γ((↑U : Scheme), U.ι ⁻¹ᵁ U.ι ''ᵁ V) : Type u))
          r))
      x ↔
    (↑x : ↥X) ∈ X.basicOpen r

Tactic:
exact congr(x ∈ $(U.ι.preimage_basicOpen r)).to_iff.symm

Premises used: congrArg, Eq.to_iff, Membership.mem, id, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen, AlgebraicGeometry.Scheme.Opens.ι, Iff.symm
-- 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
⊢ Subset (α := Set ↥X) (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι) (Set.range (ι := ↥(↑V : Scheme)) ⇑V.ι)

Tactic:
simpa using e
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
⊢ X.homOfLE e ≫ V.ι = U.ι

Tactic:
IsOpenImmersion.lift_fac _ _ _

Premises used: AlgebraicGeometry.IsOpenImmersion.lift_fac
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
rw : X.homOfLE ⋯ ≫ U.ι = 𝟙 (↑U : Scheme) ≫ U.ι
rw₁ : U.ι = 𝟙 (↑U : Scheme) ≫ U.ι
rw₂ rw₃ : U.ι = U.ι
⊢ X.homOfLE ⋯ = 𝟙 (↑U : Scheme)

Tactic:
rw [← cancel_mono U.ι, Scheme.homOfLE_ι, Category.id_comp]

Premises used: AlgebraicGeometry.Scheme.homOfLE_ι, CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
rw : (X.homOfLE e₁ ≫ X.homOfLE e₂) ≫ W.ι = X.homOfLE ⋯ ≫ W.ι
rw₁ : X.homOfLE e₁ ≫ X.homOfLE e₂ ≫ W.ι = X.homOfLE ⋯ ≫ W.ι
rw₂ : X.homOfLE e₁ ≫ V.ι = X.homOfLE ⋯ ≫ W.ι
rw₃ : U.ι = X.homOfLE ⋯ ≫ W.ι
rw₄ rw₅ : U.ι = U.ι
⊢ X.homOfLE e₁ ≫ X.homOfLE e₂ = X.homOfLE ⋯

Tactic:
rw [← cancel_mono W.ι, Category.assoc, Scheme.homOfLE_ι, Scheme.homOfLE_ι, Scheme.homOfLE_ι]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.homOfLE_ι, CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
w :
  ∀ (a : ↥(↑U : Scheme)),
    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))
⊢ (X.homOfLE e).base = CategoryTheory.Functor.map (Opens.toTopCat (↑X.toPresheafedSpace : TopCat)) (homOfLE e)

Tactic:
ext a
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U ≤ V
a : ↥(↑U : Scheme)
⊢ 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:
Subtype.ext ?_

Premises used: Subtype.ext