awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U : Scheme).Opens
W : (↑V : Scheme).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ app f (U.ι ''ᵁ O) ≫ X.presheaf.map ((homOfLE ⋯).op ≫ Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)) =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ Eq (α := ↥Y) ((↑((resLE f U V e) x) : ↥Y) : ↥Y) (f (↑x : ↥X) : ↥Y)

Tactic:
simp [resLE, morphismRestrict_base]

Premises used: AlgebraicGeometry.morphismRestrict_base, AlgebraicGeometry.Scheme.Hom.resLE
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ Eq (α := ↥Y) ((↑((resLE f U V e) x) : ↥Y) : ↥Y) (f (↑x : ↥X) : ↥Y)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
rw :
  (Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f (↑x : ↥X)) ≫ stalkMap V.ι x =
    Iso.hom (Y.presheaf.stalkCongr ⋯) ≫ stalkMap f (V.ι x) ≫ stalkMap V.ι x
⊢ (Iso.hom (U.stalkIso ((resLE f U V e) x)) ≫ Y.presheaf.stalkSpecializes ⋯) ≫ stalkMap f (↑x : ↥X) =
    stalkMap (resLE f U V e) x ≫ (V.stalkIso x).hom

Tactic:
rw [Category.assoc, ← Iso.eq_inv_comp, ← Category.assoc, ← Iso.comp_inv_eq,
      Opens.stalkIso_inv, Opens.stalkIso_inv, ← stalkMap_comp,
      stalkMap_congr_hom _ _ (resLE_comp_ι f e), stalkMap_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, AlgebraicGeometry.Scheme.Opens.stalkIso_inv, AlgebraicGeometry.Scheme.Hom.stalkMap_comp, AlgebraicGeometry.Scheme.Hom.resLE_comp_ι, CategoryTheory.Iso.eq_inv_comp, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ (Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f (↑x : ↥X)) ≫ stalkMap V.ι x =
    Iso.hom (Y.presheaf.stalkCongr ⋯) ≫ stalkMap f (V.ι x) ≫ stalkMap V.ι x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
simp : Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.appTop (Scheme.Hom.resLE f U V e) ≫ X.presheaf.map (eqToHom ⋯)
⊢ U.topIso.hom ≫ (Arrow.mk (Scheme.Hom.appLE f U V e)).hom =
    (Arrow.mk (Scheme.Hom.appTop (Scheme.Hom.resLE f U V e))).hom ≫ V.topIso.hom

Tactic:
simp only [Arrow.mk_left, Arrow.mk_right, Scheme.Opens.topIso_hom,
    eqToHom_op, Arrow.mk_hom, Scheme.Hom.map_appLE]

Premises used: CategoryTheory.Arrow.mk_right, CategoryTheory.Arrow.mk_hom, CategoryTheory.eqToHom_op, CategoryTheory.Arrow.mk_left, AlgebraicGeometry.Scheme.Hom.map_appLE, AlgebraicGeometry.Scheme.Opens.topIso_hom
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
rw : Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.app (Scheme.Hom.resLE f U V e) ⊤ ≫ X.presheaf.map (eqToHom ⋯)
rw₁ :
  Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ =
    Scheme.Hom.appLE (Scheme.Hom.resLE f U V e) ⊤ (Scheme.Hom.resLE f U V e ⁻¹ᵁ ⊤) ⋯ ≫ X.presheaf.map (eqToHom ⋯)
rw₂ :
  Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ =
    Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) (V.ι ''ᵁ Scheme.Hom.resLE f U V e ⁻¹ᵁ ⊤) ⋯ ≫ X.presheaf.map (eqToHom ⋯)
rw₃ rw₄ : Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯
⊢ Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.appTop (Scheme.Hom.resLE f U V e) ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
rw [Scheme.Hom.appTop, ← Scheme.Hom.appLE_eq_app, Scheme.Hom.resLE_appLE, Scheme.Hom.appLE_map]

Premises used: AlgebraicGeometry.Scheme.Hom.appTop, AlgebraicGeometry.Scheme.Hom.resLE_appLE, AlgebraicGeometry.Scheme.Hom.appLE_map, AlgebraicGeometry.Scheme.Hom.appLE_eq_app
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 Y_1 X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ UY ≤ g ⁻¹ᵁ UX

Tactic:
simp [*]
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 Y_1 X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ UY ≤ iY ⁻¹ᵁ UT

Tactic:
simp [*]
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (resLE g UX UY ⋯) (resLE iY UT UY ⋯) (resLE iX US UX hUSX) (resLE f US UT hUST)

Tactic:
.paste_horiz (v₁₂ := iY.resLE _ _
    ((g.preimage_mono hUSX).trans_eq congr(($H.w) ⁻¹ᵁ US) :)) ?_ ?_

Premises used: CategoryTheory.IsPullback.paste_horiz, AlgebraicGeometry.Scheme.Hom.resLE
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
refine_1 : IsPullback (Y.homOfLE ⋯) (resLE iY UT UY ⋯) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (T.homOfLE hUST)
refine_2 : IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (resLE iX US UX hUSX) (f ∣_ US)
⊢ IsPullback (resLE g UX UY ⋯) (resLE iY UT UY ⋯) (resLE iX US UX hUSX) (resLE f US UT hUST)

Tactic:
refine .paste_horiz (v₁₂ := iY.resLE _ _
    ((g.preimage_mono hUSX).trans_eq congr(($H.w) ⁻¹ᵁ US) :)) ?_ ?_
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ Y.homOfLE ⋯ ≫ resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ = resLE iY UT UY ⋯ ≫ T.homOfLE hUST

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
refine_1 : resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ ⁻¹ᵁ opensRange (T.homOfLE hUST) = opensRange (Y.homOfLE ⋯)
⊢ IsPullback (Y.homOfLE ⋯) (resLE iY UT UY ⋯) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (T.homOfLE hUST)

Tactic:
refine (IsOpenImmersion.isPullback _ _ _ _ (by simp) ?_).flip

Premises used: AlgebraicGeometry.IsOpenImmersion.isPullback, CategoryTheory.IsPullback.flip
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
refine_1 : Eq (α := (↑(g ⁻¹ᵁ UX) : Scheme).Opens) (((g ⁻¹ᵁ UX).ι ≫ iY) ⁻¹ᵁ UT) ((g ⁻¹ᵁ UX).ι ⁻¹ᵁ UY)
⊢ resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ ⁻¹ᵁ opensRange (T.homOfLE hUST) = opensRange (Y.homOfLE ⋯)

Tactic:
simp only [Scheme.opensRange_homOfLE, ← Scheme.Hom.comp_preimage, Scheme.Hom.resLE_comp_ι]

Premises used: AlgebraicGeometry.Scheme.opensRange_homOfLE, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Hom.resLE_comp_ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
refine_1 : (g ⁻¹ᵁ UX).ι ''ᵁ (g ⁻¹ᵁ UX).ι ⁻¹ᵁ iY ⁻¹ᵁ UT = (g ⁻¹ᵁ UX).ι ''ᵁ (g ⁻¹ᵁ UX).ι ⁻¹ᵁ UY
⊢ Eq (α := (↑(g ⁻¹ᵁ UX) : Scheme).Opens) (((g ⁻¹ᵁ UX).ι ≫ iY) ⁻¹ᵁ UT) ((g ⁻¹ᵁ UX).ι ⁻¹ᵁ UY)

Tactic:
rw [Scheme.Hom.comp_preimage, ← (g ⁻¹ᵁ UX).ι.image_injective.eq_iff]

Premises used: Function.Injective.eq_iff, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Hom.image_injective, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
refine_1 : g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT = g ⁻¹ᵁ UX ⊓ UY
⊢ (g ⁻¹ᵁ UX).ι ''ᵁ (g ⁻¹ᵁ UX).ι ⁻¹ᵁ iY ⁻¹ᵁ UT = (g ⁻¹ᵁ UX).ι ''ᵁ (g ⁻¹ᵁ UX).ι ⁻¹ᵁ UY

Tactic:
simp only [Scheme.Hom.image_preimage_eq_opensRange_inf, Scheme.Opens.opensRange_ι]

Premises used: AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.Scheme.Opens.opensRange_ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT = g ⁻¹ᵁ UX ⊓ UY

Tactic:
simp [hUY]
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (resLE iX US UX hUSX) (f ∣_ US)

Tactic:
.of_bot ?_ ?_ (isPullback_morphismRestrict f US)

Premises used: CategoryTheory.IsPullback.of_bot, AlgebraicGeometry.isPullback_morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
refine_2 : IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ ≫ (f ⁻¹ᵁ US).ι) (resLE iX US UX hUSX ≫ US.ι) f
refine_2₁ : g ∣_ UX ≫ resLE iX US UX hUSX = resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ ≫ f ∣_ US
⊢ IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (resLE iX US UX hUSX) (f ∣_ US)

Tactic:
refine .of_bot ?_ ?_ (isPullback_morphismRestrict f US)
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ ≫ (f ⁻¹ᵁ US).ι) (resLE iX US UX hUSX ≫ US.ι) f

Tactic:
simpa using (isPullback_morphismRestrict g UX).paste_vert H

Premises used: CategoryTheory.IsPullback.paste_vert, AlgebraicGeometry.isPullback_morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ g ∣_ UX ≫ resLE iX US UX hUSX = resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ ≫ f ∣_ US

Tactic:
simp [← cancel_mono US.ι, H.w]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
𝒰 : OpenCover.{u_1, u} X
U : X.Opens
refine_1 :
  ∀ (i : 𝒰.I₀),
    Eq (α := Set ↥(𝒰.X i)) (Set.range (ι := ↥(↑(𝒰.f i ⁻¹ᵁ U) : Scheme)) ⇑(𝒰.f i ⁻¹ᵁ U).ι)
      (Set.range (ι :=
        ↥((Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
            ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
        ⇑(pullback.snd U.ι (𝒰.f ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i))))
refine_2 :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑(𝒰.f i ⁻¹ᵁ U) : Scheme) ⟶ (↑U : Scheme)) ((fun (x : 𝒰.I₀) ↦ 𝒰.f x ∣_ U) i)
      (CategoryStruct.comp (Y :=
        (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
          ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i))
        (Iso.hom
          ((fun (i : 𝒰.I₀) ↦
              (IsOpenImmersion.isoOfRangeEq (𝒰.f i ⁻¹ᵁ U).ι
                  (pullback.snd U.ι
                    (𝒰.f ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
                  ⋯ :
                (↑(𝒰.f i ⁻¹ᵁ U) : Scheme) ≅
                  (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
                    ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
            i))
        ((Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).f
          ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
⊢ OpenCover.{u_1, u} (↑U : Scheme)

Tactic:
refine Cover.copy (𝒰.pullback₁ U.ι) 𝒰.I₀ _ (𝒰.f · ∣_ U) (Equiv.refl _)
    (fun i ↦ IsOpenImmersion.isoOfRangeEq (Opens.ι _) (pullback.snd _ _) ?_) ?_

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.Scheme.Cover.copy, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.PreZeroHypercover.I₀, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, TopologicalSpace.Opens.map, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, Equiv.refl, DFunLike.coe, AlgebraicGeometry.morphismRestrict, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
𝒰 : OpenCover.{u_1, u} X
U : X.Opens
i : 𝒰.I₀
refine_1 :
  Eq (α := Set ↥(𝒰.X i)) (Set.range (ι := ↥(↑(𝒰.f i ⁻¹ᵁ U) : Scheme)) ⇑(𝒰.f i ⁻¹ᵁ U).ι)
    (Set.range (ι := ↥(pullback U.ι (𝒰.f i))) ⇑(pullback.snd U.ι (𝒰.f i)))
⊢ Eq (α := Set ↥(𝒰.X i)) (Set.range (ι := ↥(↑(𝒰.f i ⁻¹ᵁ U) : Scheme)) ⇑(𝒰.f i ⁻¹ᵁ U).ι)
    (Set.range (ι :=
      ↥((Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
          ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
      ⇑(pullback.snd U.ι (𝒰.f ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i))))

Tactic:
dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
      PreZeroHypercover.pullback₁_I₀, Equiv.refl_apply, PreZeroHypercover.pullback₁_X]

Premises used: CategoryTheory.Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover, CategoryTheory.PreZeroHypercover.pullback₁_X, Equiv.refl_apply, CategoryTheory.PreZeroHypercover.pullback₁_I₀
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
𝒰 : OpenCover.{u_1, u} X
U : X.Opens
i : 𝒰.I₀
refine_1 : Set.range (ι := ↥(↑(𝒰.f i ⁻¹ᵁ U) : Scheme)) ⇑(𝒰.f i ⁻¹ᵁ U).ι = (↑(𝒰.f i ⁻¹ᵁ U) : Set ↥(𝒰.X i))
⊢ Eq (α := Set ↥(𝒰.X i)) (Set.range (ι := ↥(↑(𝒰.f i ⁻¹ᵁ U) : Scheme)) ⇑(𝒰.f i ⁻¹ᵁ U).ι)
    (Set.range (ι := ↥(pullback U.ι (𝒰.f i))) ⇑(pullback.snd U.ι (𝒰.f i)))

Tactic:
rw [IsOpenImmersion.range_pullbackSnd U.ι (𝒰.f i), Opens.opensRange_ι]

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.Scheme.Opens.opensRange_ι, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
𝒰 : OpenCover.{u_1, u} X
U : X.Opens
i : 𝒰.I₀
⊢ Set.range (ι := ↥(↑(𝒰.f i ⁻¹ᵁ U) : Scheme)) ⇑(𝒰.f i ⁻¹ᵁ U).ι = (↑(𝒰.f i ⁻¹ᵁ U) : Set ↥(𝒰.X i))

Tactic:
Subtype.range_val

Premises used: Subtype.range_val
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
𝒰 : OpenCover.{u_1, u} X
U : X.Opens
i : 𝒰.I₀
⊢ Set.range (ι := ↥(↑(𝒰.f i ⁻¹ᵁ U) : Scheme)) ⇑(𝒰.f i ⁻¹ᵁ U).ι = (↑(𝒰.f i ⁻¹ᵁ U) : Set ↥(𝒰.X i))

Tactic:
exact Subtype.range_val

Premises used: Subtype.range_val
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
𝒰 : OpenCover.{u_1, u} X
U : X.Opens
i : 𝒰.I₀
refine_2 :
  Eq (α := (↑(𝒰.f i ⁻¹ᵁ U) : Scheme) ⟶ X) ((fun (x : 𝒰.I₀) ↦ 𝒰.f x ∣_ U) i ≫ U.ι)
    (CategoryStruct.comp (Y :=
        (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
          ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i))
        (Iso.hom
          ((fun (i : 𝒰.I₀) ↦
              (IsOpenImmersion.isoOfRangeEq (𝒰.f i ⁻¹ᵁ U).ι
                  (pullback.snd U.ι
                    (𝒰.f ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
                  ⋯ :
                (↑(𝒰.f i ⁻¹ᵁ U) : Scheme) ≅
                  (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
                    ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
            i))
        ((Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).f
          ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)) ≫
      U.ι)
⊢ Eq (α := (↑(𝒰.f i ⁻¹ᵁ U) : Scheme) ⟶ (↑U : Scheme)) ((fun (x : 𝒰.I₀) ↦ 𝒰.f x ∣_ U) i)
    (CategoryStruct.comp (Y :=
      (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
        ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i))
      (Iso.hom
        ((fun (i : 𝒰.I₀) ↦
            (IsOpenImmersion.isoOfRangeEq (𝒰.f i ⁻¹ᵁ U).ι
                (pullback.snd U.ι
                  (𝒰.f ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
                ⋯ :
              (↑(𝒰.f i ⁻¹ᵁ U) : Scheme) ≅
                (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
                  ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
          i))
      ((Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).f
        ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))

Tactic:
rw [← cancel_mono U.ι]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
𝒰 : OpenCover.{u_1, u} X
U : X.Opens
i : 𝒰.I₀
⊢ Eq (α := (↑(𝒰.f i ⁻¹ᵁ U) : Scheme) ⟶ X) ((fun (x : 𝒰.I₀) ↦ 𝒰.f x ∣_ U) i ≫ U.ι)
    (CategoryStruct.comp (Y :=
        (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
          ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i))
        (Iso.hom
          ((fun (i : 𝒰.I₀) ↦
              (IsOpenImmersion.isoOfRangeEq (𝒰.f i ⁻¹ᵁ U).ι
                  (pullback.snd U.ι
                    (𝒰.f ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
                  ⋯ :
                (↑(𝒰.f i ⁻¹ᵁ U) : Scheme) ≅
                  (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).X
                    ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)))
            i))
        ((Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).f
          ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).I₀) i)) ≫
      U.ι)

Tactic:
simp [morphismRestrict_ι, Equiv.refl_apply, Category.assoc, pullback.condition]

Premises used: CategoryTheory.Category.assoc, Equiv.refl_apply, AlgebraicGeometry.morphismRestrict_ι, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
⊢ Subsingleton.{u + 1} (↑Γ(X, ⊥) : Type u)

Tactic:
CommRingCat.subsingleton_of_isTerminal X.sheaf.isTerminalOfEmpty

Premises used: TopCat.Sheaf.isTerminalOfEmpty, CommRingCat.subsingleton_of_isTerminal, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.SheafedSpace.sheaf, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ Continuous (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
f.base.hom.2

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', ContinuousMap.continuous_toFun, TopCat.Hom.hom, AlgebraicGeometry.PresheafedSpace.Hom.base
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
a b : ↥X
⊢ a ≤ b ↔ b ⤳ a

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
x : ↥X
hx : IsClosed (X := ↥X) {x}
simp : IsMin x
⊢ height x = 0

Tactic:
simp only [height_eq_zero]

Premises used: Order.height_eq_zero
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
x : ↥X
hx : IsClosed (X := ↥X) {x}
b : ↥X
_ : b ≤ x → x ≤ b
⊢ b ≤ x → x ≤ b

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
x : ↥X
hx : IsClosed (X := ↥X) {x}
b : ↥X
h : b ≤ x
inl : ∀ (hx : IsClosed (X := ↥X) {b}), b ≤ b → b ≤ b
inr : ∀ (h : b ≠ x), x ≤ b
⊢ x ≤ b

Tactic:
obtain rfl | h := eq_or_ne b x

Premises used: eq_or_ne, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
b : ↥X
hx : IsClosed (X := ↥X) {b}
h : b ≤ b
⊢ b ≤ b

Tactic:
assumption
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
x : ↥X
hx : IsClosed (X := ↥X) {x}
b : ↥X
h_1 : b ≤ x
h : b ≠ x
⊢ ¬x ⤳ b

Tactic:
have := IsClosed.not_specializes hx rfl h
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
x : ↥X
hx : IsClosed (X := ↥X) {x}
b : ↥X
h_1 : b ≤ x
h : b ≠ x
this : ¬x ⤳ b
⊢ x ≤ b

Tactic:
contradiction
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
i : op U' ⟶ op U
⊢ Y.presheaf.map i ≫ app f U = app f U' ≫ X.presheaf.map ((Opens.map f.base).map i.unop).op

Tactic:
f.c.naturality i

Premises used: Set.Mem, Quiver.Hom.op, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.NatTrans.naturality, AlgebraicGeometry.PresheafedSpace.Hom.c
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op V ⟶ op V'
rw : app f U ≫ X.presheaf.map ((homOfLE e).op ≫ i) = appLE f U V' ⋯
⊢ appLE f U V e ≫ X.presheaf.map i = appLE f U V' ⋯

Tactic:
rw [Hom.appLE, Category.assoc, ← Functor.map_comp]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.appLE, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op V ⟶ op V'
⊢ app f U ≫ X.presheaf.map ((homOfLE e).op ≫ i) = appLE f U V' ⋯

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : V = V'
⊢ appLE f U V' ⋯ ≫ X.presheaf.map (Quiver.Hom.op (eqToHom i)) = appLE f U V e

Tactic:
appLE_map _ _ _

Premises used: AlgebraicGeometry.Scheme.Hom.appLE_map
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op U' ⟶ op U
rw : app f U' ≫ X.presheaf.map (((Opens.map f.base).map i.unop).op ≫ (homOfLE e).op) = appLE f U' V ⋯
⊢ Y.presheaf.map i ≫ appLE f U V e = appLE f U' V ⋯

Tactic:
rw [Hom.appLE, f.naturality_assoc, ← Functor.map_comp]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.Scheme.Hom.naturality_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op U' ⟶ op U
⊢ app f U' ≫ X.presheaf.map (((Opens.map f.base).map i.unop).op ≫ (homOfLE e).op) = appLE f U' V ⋯

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : U' = U
⊢ Y.presheaf.map (Quiver.Hom.op (eqToHom i)) ≫ appLE f U' V ⋯ = appLE f U V e

Tactic:
map_appLE _ _ _

Premises used: AlgebraicGeometry.Scheme.Hom.map_appLE
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ app f U = appLE f U (f ⁻¹ᵁ U) ⋯

Tactic:
simp [Hom.appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE