awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
⊢ Eq (α := Γ((↑U : Scheme), U.ι ⁻¹ᵁ U.ι ''ᵁ V) ⟶ Γ((↑(f ⁻¹ᵁ U) : Scheme), (f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V))
    (Hom.app (f ∣_ U) (U.ι ⁻¹ᵁ U.ι ''ᵁ V))
    (Hom.app f (U.ι ''ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
simpa [← Functor.map_comp_assoc, ← Functor.map_comp] using
    congr(Y.presheaf.map (eqToHom (congr_arg (U.ι ''ᵁ ·) (U.ι.preimage_image_eq V).symm)).op ≫
      $(Scheme.Hom.congr_app (morphismRestrict_ι f U) (U.ι ''ᵁ V)))

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, Quiver.Hom.op, CategoryTheory.eqToHom, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.Scheme.Hom.preimage_image_eq, AlgebraicGeometry.morphismRestrict_ι, CategoryTheory.Functor.map, congr_arg, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.Functor.map_comp_assoc, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.Functor.map_comp, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Eq.symm, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Scheme.Hom.appTop (f ∣_ U) = Scheme.Hom.app f (U.ι ''ᵁ ⊤) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
morphismRestrict_app ..

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, AlgebraicGeometry.morphismRestrict_app
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↥(↑U : Scheme)
⊢ Scheme.Hom.app (f ∣_ U) V = Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) ⋯

Tactic:
morphismRestrict_app f U V

Premises used: Set.Mem, CategoryTheory.eqToHom, setOf, AlgebraicGeometry.Scheme.Hom.appLE, CategoryTheory.homOfLE, Set.image, AlgebraicGeometry.PresheafedSpace.restrict, AlgebraicGeometry.morphismRestrict_app
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
W : (↑(f ⁻¹ᵁ U) : Scheme).Opens
e : W ≤ (f ∣_ U) ⁻¹ᵁ V
rw :
  Scheme.Hom.app (f ∣_ U) V ≫ (↑(f ⁻¹ᵁ U) : Scheme).presheaf.map (homOfLE e).op =
    Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯
rw₁ :
  Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) ⋯ ≫
      (↑(f ⁻¹ᵁ U) : Scheme).presheaf.map (homOfLE e).op =
    Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯
rw₂ :
  Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) ⋯ ≫
      X.presheaf.map ((Scheme.Hom.opensFunctor (f ⁻¹ᵁ U).ι).map (homOfLE e).op.unop).op =
    Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯
rw₃ rw₄ :
  Eq (α := Γ((↑U : Scheme), V) ⟶ Γ((↑(f ⁻¹ᵁ U) : Scheme), W))
    (Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ unop (op W)) ⋯ :
      Γ(Y, U.ι ''ᵁ V) ⟶ Γ(X, (f ⁻¹ᵁ U).ι ''ᵁ unop (op W)))
    (Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯ : Γ(Y, U.ι ''ᵁ V) ⟶ Γ(X, (f ⁻¹ᵁ U).ι ''ᵁ W))
⊢ Scheme.Hom.appLE (f ∣_ U) V W e = Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯

Tactic:
rw [Scheme.Hom.appLE, morphismRestrict_app', Scheme.Opens.toScheme_presheaf_map,
    Scheme.Hom.appLE_map]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map, AlgebraicGeometry.Scheme.Hom.appLE_map
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
rw : f = 𝟙 X ≫ f
rw₁ rw₂ : f = f
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
rw [Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
rw : g = e.hom ≫ V.ι
rw₁ rw₂ : g = g
⊢ g ≫ 𝟙 Y = e.hom ≫ V.ι

Tactic:
rw [Category.comp_id, IsOpenImmersion.isoOfRangeEq_hom_fac]

Premises used: CategoryTheory.Category.comp_id, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
symm :
  Arrow.mk (X := pullback f g) (pullback.snd f g) ≅
    Arrow.mk (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) (f ∣_ Scheme.Hom.opensRange g)
⊢ Arrow.mk (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) (f ∣_ Scheme.Hom.opensRange g) ≅
    Arrow.mk (X := pullback f g) (pullback.snd f g)

Tactic:
symm
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
refine :
  (asIso t ≪≫ pullbackRestrictIsoRestrict f V).hom ≫
      (Arrow.mk (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) (f ∣_ Scheme.Hom.opensRange g)).hom =
    (Arrow.mk (X := pullback f g) (pullback.snd f g)).hom ≫ e.hom
⊢ Arrow.mk (X := pullback f g) (pullback.snd f g) ≅
    Arrow.mk (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) (f ∣_ Scheme.Hom.opensRange g)

Tactic:
refine Arrow.isoMk (asIso t ≪≫ pullbackRestrictIsoRestrict f V) e ?_

Premises used: CategoryTheory.Iso.trans, CategoryTheory.asIso, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
rw :
  (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫
          (Arrow.mk (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) (f ∣_ Scheme.Hom.opensRange g)).hom) ≫
        e.inv) ≫
      g =
    (Arrow.mk (X := pullback f g) (pullback.snd f g)).hom ≫ g
⊢ (asIso t ≪≫ pullbackRestrictIsoRestrict f V).hom ≫
      (Arrow.mk (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) (f ∣_ Scheme.Hom.opensRange g)).hom =
    (Arrow.mk (X := pullback f g) (pullback.snd f g)).hom ≫ e.hom

Tactic:
rw [Iso.trans_hom, asIso_hom, ← Iso.comp_inv_eq, ← cancel_mono g]

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.cancel_mono, CategoryTheory.Iso.trans_hom, CategoryTheory.asIso_hom
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
dsimp :
  (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv) ≫ g = pullback.snd f g ≫ g
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫
          (Arrow.mk (X := (↑(f ⁻¹ᵁ Scheme.Hom.opensRange g) : Scheme)) (f ∣_ Scheme.Hom.opensRange g)).hom) ≫
        e.inv) ≫
      g =
    (Arrow.mk (X := pullback f g) (pullback.snd f g)).hom ≫ g

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst_1 : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ (↑V : Scheme) := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
rw : ((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₁ : (t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₂ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
rw₃ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.snd f g ≫ g
rw₄ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.fst f g ≫ f
rw₅ : t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ (f ⁻¹ᵁ Scheme.Hom.opensRange g).ι ≫ f = pullback.fst f g ≫ f
rw₆ : t ≫ pullback.fst f V.ι ≫ f = pullback.fst f g ≫ f
rw₇ : Eq (α := pullback f g ⟶ Y) ((pullback.fst f g ≫ 𝟙 X) ≫ f) (pullback.fst f g ≫ f)
rw₈ rw₉ : Eq (α := pullback f g ⟶ Y) (pullback.fst f g ≫ f) (pullback.fst f g ≫ f)
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv) ≫ g = pullback.snd f g ≫ g

Tactic:
rw [Category.assoc, Category.assoc, Category.assoc, IsOpenImmersion.isoOfRangeEq_inv_fac,
    ← pullback.condition, morphismRestrict_ι,
    pullbackRestrictIsoRestrict_hom_ι_assoc, pullback.lift_fst_assoc, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_fst_assoc, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
e : U = V
subst : Arrow.mk (f ∣_ U) = Arrow.mk (f ∣_ U)
⊢ Arrow.mk (f ∣_ U) = Arrow.mk (f ∣_ V)

Tactic:
subst e
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Arrow.mk (f ∣_ U) = Arrow.mk (f ∣_ U)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
refine_1 : (f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V = f ⁻¹ᵁ U.ι ''ᵁ V
refine_2 :
  (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V) ≪≫ X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)
⊢ Arrow.mk (f ∣_ U ∣_ V) ≅ Arrow.mk (X := (↑(f ⁻¹ᵁ U.ι ''ᵁ V) : Scheme)) (f ∣_ U.ι ''ᵁ V)

Tactic:
refine Arrow.isoMk' _ _ ((Scheme.Opens.ι _).isoImage _ ≪≫ Scheme.isoOfEq _ ?_)
    ((Scheme.Opens.ι _).isoImage _) ?_

Premises used: CategoryTheory.Iso.trans, AlgebraicGeometry.Scheme.isoOfEq, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.Arrow.isoMk', AlgebraicGeometry.Scheme.Hom.isoImage
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
⊢ (f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V = f ⁻¹ᵁ U.ι ''ᵁ V

Tactic:
image_morphismRestrict_preimage f U V

Premises used: AlgebraicGeometry.image_morphismRestrict_preimage
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
⊢ (f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V = f ⁻¹ᵁ U.ι ''ᵁ V

Tactic:
exact image_morphismRestrict_preimage f U V

Premises used: AlgebraicGeometry.image_morphismRestrict_preimage
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
refine_2 :
  ((Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V) ≪≫ X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V) ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₁ :
  ((Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom) ≫ f ∣_ U.ι ''ᵁ V) ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₂ :
  (Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom) ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₃ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
    (f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)) ≫ (U.ι ''ᵁ V).ι
refine_2₄ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V ≫ (U.ι ''ᵁ V).ι =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₅ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ (X.isoOfEq ⋯).hom ≫ (f ⁻¹ᵁ U.ι ''ᵁ V).ι ≫ f =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₆ :
  Iso.hom (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V)) ≫ ((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V).ι ≫ f =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₇ : ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V) ≫ (U.ι ''ᵁ V).ι
refine_2₈ : ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ∣_ V ≫ V.ι ≫ U.ι
refine_2₉ : ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f = ((f ∣_ U) ⁻¹ᵁ V).ι ≫ f ∣_ U ≫ U.ι
refine_2₁₀ refine_2₁₁ : ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f = ((f ∣_ U) ⁻¹ᵁ V).ι ≫ (f ⁻¹ᵁ U).ι ≫ f
⊢ (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V) ≪≫ X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V =
    f ∣_ U ∣_ V ≫ Iso.hom (Scheme.Hom.isoImage U.ι V)

Tactic:
rw [← cancel_mono (Scheme.Opens.ι _), Iso.trans_hom, Category.assoc, Category.assoc,
      Category.assoc, morphismRestrict_ι, Scheme.isoOfEq_hom_ι_assoc,
      Scheme.Hom.isoImage_hom_ι_assoc,
      Scheme.Hom.isoImage_hom_ι,
      morphismRestrict_ι_assoc, morphismRestrict_ι]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.morphismRestrict_ι_assoc, AlgebraicGeometry.morphismRestrict_ι, CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.isoOfEq_hom_ι_assoc, CategoryTheory.Iso.trans_hom, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι_assoc
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
r : (↑Γ(Y, U) : Type u)
refine :
  U.ι ''ᵁ
      (↑U : Scheme).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
            (a : (↑(Y.presheaf.obj (op U)) : Type u)) → (↑(Y.presheaf.obj (op (⋯.functor.obj ⊤))) : Type u))
          r) =
    Y.basicOpen r
⊢ Arrow.mk (X :=
      (↑((f ∣_ U) ⁻¹ᵁ
            (↑U : Scheme).basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
                  (a : (↑(Y.presheaf.obj (op U)) : Type u)) → (↑(Y.presheaf.obj (op (⋯.functor.obj ⊤))) : Type u))
                r)) :
        Scheme))
      (f ∣_ U ∣_
        (↑U : Scheme).basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
              (a : (↑(Y.presheaf.obj (op U)) : Type u)) → (↑(Y.presheaf.obj (op (⋯.functor.obj ⊤))) : Type u))
            r)) ≅
    Arrow.mk (X := (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)) (f ∣_ Y.basicOpen r)

Tactic:
refine morphismRestrictRestrict _ _ _ ≪≫ morphismRestrictEq _ ?_

Premises used: AlgebraicGeometry.morphismRestrictEq, AlgebraicGeometry.morphismRestrictRestrict
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
r : (↑Γ(Y, U) : Type u)
⊢ U.ι ''ᵁ
      (↑U : Scheme).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
            (a : (↑(Y.presheaf.obj (op U)) : Type u)) → (↑(Y.presheaf.obj (op (⋯.functor.obj ⊤))) : Type u))
          r) =
    Y.basicOpen r

Tactic:
simp [Scheme.Opens.ι_image_basicOpen]

Premises used: AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
x : ↥(↑(f ⁻¹ᵁ U) : Scheme)
V : Opens ↥(↑U : Scheme)
hxV : Membership.mem (α := ↥(↑U : Scheme)) V ((f ∣_ U) x : ↥(↑U : Scheme))
⊢ (↑U : Scheme).presheaf.germ V ((f ∣_ U) x) hxV ≫
      (U.stalkIso ((f ∣_ U) x) ≪≫ Y.presheaf.stalkCongr ⋯).hom ≫ Scheme.Hom.stalkMap f (↑x : ↥X) =
    (↑U : Scheme).presheaf.germ V ((f ∣_ U) x) hxV ≫ Scheme.Hom.stalkMap (f ∣_ U) x ≫ ((f ⁻¹ᵁ U).stalkIso x).hom

Tactic:
simp [Scheme.Hom.germ_stalkMap_assoc, Scheme.Hom.appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc, AlgebraicGeometry.Scheme.Hom.appLE
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
inst_1 : IsOpenImmersion f
⊢ IsOpenImmersion ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι)

Tactic:
PresheafedSpace.IsOpenImmersion.comp _ _

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
inst_1 : IsOpenImmersion f
⊢ IsOpenImmersion ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι)

Tactic:
exact PresheafedSpace.IsOpenImmersion.comp _ _

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ resLE f U (f ⁻¹ᵁ U) ⋯ = f ∣_ U

Tactic:
simp [resLE]

Premises used: AlgebraicGeometry.Scheme.Hom.resLE
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
V V' : X.Opens
i : V ≤ V'
simp : X.homOfLE i ≫ 𝟙 (↑(𝟙 X ⁻¹ᵁ V') : Scheme) = X.homOfLE i
⊢ resLE (𝟙 X) V' V i = X.homOfLE i

Tactic:
simp only [resLE, morphismRestrict_id]

Premises used: AlgebraicGeometry.Scheme.Hom.resLE, AlgebraicGeometry.morphismRestrict_id
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
V V' : X.Opens
i : V ≤ V'
⊢ X.homOfLE i ≫ 𝟙 (↑(𝟙 X ⁻¹ᵁ V') : Scheme) = X.homOfLE i

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ resLE f U V e ≫ U.ι = V.ι ≫ f

Tactic:
simp [resLE]

Premises used: AlgebraicGeometry.Scheme.Hom.resLE
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
Z : Scheme
g : Y ⟶ Z
W : Z.Opens
e' : U ≤ g ⁻¹ᵁ W
⊢ resLE f U V e ≫ resLE g W U e' = resLE (f ≫ g) W V ⋯

Tactic:
simp [← cancel_mono W.ι]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : V' ≤ V
simp_rw : resLE (𝟙 X) V V' i ≫ resLE f U V e = resLE f U V' ⋯
simp_rw₁ : resLE (𝟙 X ≫ f) U V' ⋯ = resLE f U V' ⋯
⊢ X.homOfLE i ≫ resLE f U V e = resLE f U V' ⋯

Tactic:
simp_rw [← resLE_id, resLE_comp_resLE, Category.id_comp]

Premises used: AlgebraicGeometry.Scheme.Hom.resLE_id, AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : U ≤ U'
simp_rw : resLE f U V e ≫ resLE (𝟙 Y) U' U i = resLE f U' V ⋯
simp_rw₁ : resLE (f ≫ 𝟙 Y) U' V ⋯ = resLE f U' V ⋯
⊢ resLE f U V e ≫ Y.homOfLE i = resLE f U' V ⋯

Tactic:
simp_rw [← resLE_id, resLE_comp_resLE, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, AlgebraicGeometry.Scheme.Hom.resLE_id, AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₁ : U = U'
e₂ : V = V'
P : MorphismProperty Scheme
subst : P (resLE f U V e) ↔ P (resLE f U V' ⋯)
⊢ P (resLE f U V e) ↔ P (resLE f U' V' ⋯)

Tactic:
subst e₁
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₂ : V = V'
P : MorphismProperty Scheme
subst : P (resLE f U V e) ↔ P (resLE f U V ⋯)
⊢ P (resLE f U V e) ↔ P (resLE f U V' ⋯)

Tactic:
subst e₂
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
P : MorphismProperty Scheme
⊢ P (resLE f U V e) ↔ P (resLE f U V ⋯)

Tactic:
rfl
-- 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
rw : resLE f U V e ⁻¹ᵁ O = (V.ι ≫ f) ⁻¹ᵁ U.ι ''ᵁ O
rw₁ : resLE f U V e ⁻¹ᵁ O = (resLE f U V e ≫ U.ι) ⁻¹ᵁ U.ι ''ᵁ O
rw₂ : resLE f U V e ⁻¹ᵁ O = resLE f U V e ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ O
rw₃ rw₄ : resLE f U V e ⁻¹ᵁ O = resLE f U V e ⁻¹ᵁ O
⊢ resLE f U V e ⁻¹ᵁ O = V.ι ⁻¹ᵁ f ⁻¹ᵁ U.ι ''ᵁ O

Tactic:
rw [← comp_preimage, ← resLE_comp_ι f e, comp_preimage, preimage_image_eq]

Premises used: AlgebraicGeometry.Scheme.Hom.preimage_image_eq, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Hom.resLE_comp_ι
-- 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
⊢ W ≤ resLE f U V e ⁻¹ᵁ O ↔ V.ι ''ᵁ W ≤ f ⁻¹ᵁ U.ι ''ᵁ O

Tactic:
simp [resLE_preimage, ← image_le_image_iff V.ι, image_preimage_eq_opensRange_inf, V.ι_image_le]

Premises used: AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.Scheme.Hom.resLE_preimage, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Opens.ι_image_le, AlgebraicGeometry.Scheme.Hom.image_le_image_iff
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ app (resLE f U V e) ⊤ = U.topIso.hom ≫ appLE f U V e ≫ V.topIso.inv

Tactic:
simp [Scheme.Hom.resLE]

Premises used: AlgebraicGeometry.Scheme.Hom.resLE
-- 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
dsimp :
  (app (f ∣_ U) O ≫ app (X.homOfLE e) ((f ∣_ U) ⁻¹ᵁ O)) ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op
⊢ appLE (resLE f U V e) O W e' = appLE f (U.ι ''ᵁ O) (V.ι ''ᵁ W) ⋯

Tactic:
dsimp [appLE, resLE]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.Scheme.Hom.resLE
-- 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
simp :
  app f (U.ι ''ᵁ O) ≫
      X.presheaf.map (homOfLE ⋯).op ≫
        X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op
⊢ (app (f ∣_ U) O ≫ app (X.homOfLE e) ((f ∣_ U) ⁻¹ᵁ O)) ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [morphismRestrict_app', appLE, homOfLE_leOfHom, homOfLE_app, Category.assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.appLE, CategoryTheory.homOfLE_leOfHom, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.Scheme.homOfLE_app
-- 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
rw :
  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
⊢ app f (U.ι ''ᵁ O) ≫
      X.presheaf.map (homOfLE ⋯).op ≫
        X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [← X.presheaf.map_comp, ← X.presheaf.map_comp]

Premises used: AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace