awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
R : CommRingCat
f g x : (↑R : Type u)
⊢ Eq (α := Localization.Away (f * g))
    ((algebraMap (↑R : Type u) (Localization.Away (f * g)) : (a : (↑R : Type u)) → Localization.Away (f * g)) x :
      Localization.Away (f * g))
    ((@RingHom.comp _ (Localization.Away f) _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.awayToAwayRight f g)
            (algebraMap (↑R : Type u) (Localization.Away f)) :
          (a : (↑R : Type u)) → Localization.Away (f * g))
        x :
      Localization.Away (f * g))

Tactic:
(IsLocalization.Away.awayToAwayRight_eq f g x (S := Localization.Away f)).symm

Premises used: Set.Mem, IsLocalization.Away.awayToAwayRight_eq, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
R : CommRingCat
f g x : (↑R : Type u)
⊢ Eq (α := Localization.Away (f * g))
    ((algebraMap (↑R : Type u) (Localization.Away (f * g)) : (a : (↑R : Type u)) → Localization.Away (f * g)) x :
      Localization.Away (f * g))
    ((@RingHom.comp _ (Localization.Away f) _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.awayToAwayRight f g)
            (algebraMap (↑R : Type u) (Localization.Away f)) :
          (a : (↑R : Type u)) → Localization.Away (f * g))
        x :
      Localization.Away (f * g))

Tactic:
exact (IsLocalization.Away.awayToAwayRight_eq f g x (S := Localization.Away f)).symm

Premises used: IsLocalization.Away.awayToAwayRight_eq, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
refine :
  Eq (α := Set ↥X) (Set.range (ι := ↥(pullback f U.ι)) ⇑(pullback.fst f U.ι))
    (Set.range (ι := ↥(↑(f ⁻¹ᵁ U) : Scheme)) ⇑(f ⁻¹ᵁ U).ι)
⊢ pullback f U.ι ≅ (↑(f ⁻¹ᵁ U) : Scheme)

Tactic:
refine IsOpenImmersion.isoOfRangeEq (pullback.fst f _) (Scheme.Opens.ι _) ?_

Premises used: CategoryTheory.Limits.pullback.fst, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Eq (α := Set ↥X) (Set.range (ι := ↥(pullback f U.ι)) ⇑(pullback.fst f U.ι))
    (Set.range (ι := ↥(↑(f ⁻¹ᵁ U) : Scheme)) ⇑(f ⁻¹ᵁ U).ι)

Tactic:
simp [IsOpenImmersion.range_pullbackFst]

Premises used: AlgebraicGeometry.IsOpenImmersion.range_pullbackFst
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (IsOpenImmersion.isoOfRangeEq (pullback.fst f U.ι) (f ⁻¹ᵁ U).ι ⋯).inv ≫ pullback.fst f U.ι = (f ⁻¹ᵁ U).ι

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (IsOpenImmersion.isoOfRangeEq (pullback.fst f U.ι) (f ⁻¹ᵁ U).ι ⋯).hom ≫ (f ⁻¹ᵁ U).ι = pullback.fst f U.ι

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (pullbackRestrictIsoRestrict f U).hom ≫ f ∣_ U = pullback.snd f U.ι

Tactic:
Iso.hom_inv_id_assoc _ _

Premises used: CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
rw : (pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f
rw₁ : (pullbackRestrictIsoRestrict f U).inv ≫ pullback.fst f U.ι ≫ f = (f ⁻¹ᵁ U).ι ≫ f
rw₂ rw₃ : (f ⁻¹ᵁ U).ι ≫ f = (f ⁻¹ᵁ U).ι ≫ f
⊢ ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι) ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f

Tactic:
rw [Category.assoc, pullback.condition.symm, pullbackRestrictIsoRestrict_inv_fst_assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, CategoryTheory.Limits.pullback.condition, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
H : (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ≫ U.ι
H' : f ⁻¹ᵁ Scheme.Hom.opensRange U.ι = Scheme.Hom.opensRange (f ⁻¹ᵁ U).ι
⊢ IsPullback (f ∣_ U) (f ⁻¹ᵁ U).ι U.ι f

Tactic:
apply IsOpenImmersion.isPullback

Premises used: AlgebraicGeometry.IsOpenImmersion.isPullback
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ≫ U.ι

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange U.ι = Scheme.Hom.opensRange (f ⁻¹ᵁ U).ι

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) (X.homOfLE hU) (X.homOfLE hV)

Tactic:
(isPullback_morphismRestrict (X.homOfLE hV) (W.ι ⁻¹ᵁ U)).of_iso (V.ι.isoImage _ ≪≫
    X.isoOfEq ?_) (W.ι.isoImage _ ≪≫ X.isoOfEq ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_ ?_

Premises used: AlgebraicGeometry.Scheme.homOfLE, CategoryTheory.Iso.refl, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.IsPullback.of_iso, CategoryTheory.Iso.trans, AlgebraicGeometry.Scheme.isoOfEq, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, TopologicalSpace.Opens.map, AlgebraicGeometry.Scheme.Hom.isoImage, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
refine_1 : V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U = U ⊓ V
refine_2 : W.ι ''ᵁ W.ι ⁻¹ᵁ U = U
refine_3 :
  X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom =
    CategoryStruct.comp (Y := (↑(U ⊓ V) : Scheme))
      (Iso.hom
          (Iso.trans (Y := (↑(V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme))
            (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U)) (X.isoOfEq ⋯)) :
        (↑(X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme) ⟶ (↑(U ⊓ V) : Scheme))
      (X.homOfLE ⋯ : (↑(U ⊓ V) : Scheme) ⟶ (↑U : Scheme))
refine_4 :
  (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U).ι ≫ Iso.hom (Iso.refl (↑V : Scheme)) =
    CategoryStruct.comp (Y := (↑(U ⊓ V) : Scheme))
      (Iso.hom
          (Iso.trans (Y := (↑(V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme))
            (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U)) (X.isoOfEq ⋯)) :
        (↑(X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme) ⟶ (↑(U ⊓ V) : Scheme))
      (X.homOfLE ⋯ : (↑(U ⊓ V) : Scheme) ⟶ (↑V : Scheme))
refine_5 :
  (W.ι ⁻¹ᵁ U).ι ≫ Iso.hom (Iso.refl (↑W : Scheme)) =
    (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE hU
refine_6 : X.homOfLE hV ≫ Iso.hom (Iso.refl (↑W : Scheme)) = Iso.hom (Iso.refl (↑V : Scheme)) ≫ X.homOfLE hV
⊢ IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) (X.homOfLE hU) (X.homOfLE hV)

Tactic:
refine (isPullback_morphismRestrict (X.homOfLE hV) (W.ι ⁻¹ᵁ U)).of_iso (V.ι.isoImage _ ≪≫
    X.isoOfEq ?_) (W.ι.isoImage _ ≪≫ X.isoOfEq ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_ ?_

Premises used: AlgebraicGeometry.Scheme.homOfLE, CategoryTheory.Iso.refl, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.IsPullback.of_iso, CategoryTheory.Iso.trans, AlgebraicGeometry.Scheme.isoOfEq, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, TopologicalSpace.Opens.map, AlgebraicGeometry.Scheme.Hom.isoImage, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
refine_1 : V.ι ''ᵁ (Opens.map V.ι.base).obj U = U ⊓ V
⊢ V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U = U ⊓ V

Tactic:
rw [← TopologicalSpace.Opens.map_comp_obj, ← Scheme.Hom.comp_base, Scheme.homOfLE_ι]

Premises used: AlgebraicGeometry.Scheme.homOfLE_ι, TopologicalSpace.Opens.map_comp_obj, AlgebraicGeometry.Scheme.Hom.comp_base
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ V.ι ''ᵁ (Opens.map V.ι.base).obj U = U ⊓ V

Tactic:
V.functor_map_eq_inf U

Premises used: TopologicalSpace.Opens.functor_map_eq_inf
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ V.ι ''ᵁ (Opens.map V.ι.base).obj U = U ⊓ V

Tactic:
exact V.functor_map_eq_inf U

Premises used: TopologicalSpace.Opens.functor_map_eq_inf
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ U ⊓ W = U

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ W.ι ''ᵁ W.ι ⁻¹ᵁ U = U

Tactic:
exact (W.functor_map_eq_inf U).trans (by simpa)

Premises used: TopologicalSpace.Opens.functor_map_eq_inf, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom =
    CategoryStruct.comp (Y := (↑(U ⊓ V) : Scheme))
      (Iso.hom
          (Iso.trans (Y := (↑(V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme))
            (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U)) (X.isoOfEq ⋯)) :
        (↑(X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme) ⟶ (↑(U ⊓ V) : Scheme))
      (X.homOfLE ⋯ : (↑(U ⊓ V) : Scheme) ⟶ (↑U : Scheme))

Tactic:
simp [← cancel_mono (Scheme.Opens.ι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom =
    CategoryStruct.comp (Y := (↑(U ⊓ V) : Scheme))
      (Iso.hom
          (Iso.trans (Y := (↑(V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme))
            (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U)) (X.isoOfEq ⋯)) :
        (↑(X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme) ⟶ (↑(U ⊓ V) : Scheme))
      (X.homOfLE ⋯ : (↑(U ⊓ V) : Scheme) ⟶ (↑U : Scheme))

Tactic:
{ simp [← cancel_mono (Scheme.Opens.ι _)] }

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U).ι ≫ Iso.hom (Iso.refl (↑V : Scheme)) =
    CategoryStruct.comp (Y := (↑(U ⊓ V) : Scheme))
      (Iso.hom
          (Iso.trans (Y := (↑(V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme))
            (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U)) (X.isoOfEq ⋯)) :
        (↑(X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme) ⟶ (↑(U ⊓ V) : Scheme))
      (X.homOfLE ⋯ : (↑(U ⊓ V) : Scheme) ⟶ (↑V : Scheme))

Tactic:
simp [← cancel_mono (Scheme.Opens.ι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U).ι ≫ Iso.hom (Iso.refl (↑V : Scheme)) =
    CategoryStruct.comp (Y := (↑(U ⊓ V) : Scheme))
      (Iso.hom
          (Iso.trans (Y := (↑(V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme))
            (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U)) (X.isoOfEq ⋯)) :
        (↑(X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) : Scheme) ⟶ (↑(U ⊓ V) : Scheme))
      (X.homOfLE ⋯ : (↑(U ⊓ V) : Scheme) ⟶ (↑V : Scheme))

Tactic:
{ simp [← cancel_mono (Scheme.Opens.ι _)] }

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (W.ι ⁻¹ᵁ U).ι ≫ Iso.hom (Iso.refl (↑W : Scheme)) =
    (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE hU

Tactic:
simp [← cancel_mono (Scheme.Opens.ι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (W.ι ⁻¹ᵁ U).ι ≫ Iso.hom (Iso.refl (↑W : Scheme)) =
    (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE hU

Tactic:
{ simp [← cancel_mono (Scheme.Opens.ι _)] }

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ≫ Iso.hom (Iso.refl (↑W : Scheme)) = Iso.hom (Iso.refl (↑V : Scheme)) ≫ X.homOfLE hV

Tactic:
simp [← cancel_mono (Scheme.Opens.ι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ≫ Iso.hom (Iso.refl (↑W : Scheme)) = Iso.hom (Iso.refl (↑V : Scheme)) ≫ X.homOfLE hV

Tactic:
{ simp [← cancel_mono (Scheme.Opens.ι _)] }

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
⊢ V.ι ∣_ U ≫ Iso.hom (Iso.refl (↑U : Scheme)) = (Scheme.Hom.isoImage V.ι (V.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

Tactic:
simp [← cancel_mono U.ι]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
⊢ (V.ι ⁻¹ᵁ U).ι ≫ Iso.hom (Iso.refl (↑V : Scheme)) =
    (Scheme.Hom.isoImage V.ι (V.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

Tactic:
simp [← cancel_mono V.ι]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
⊢ U.ι ≫ Iso.hom (Iso.refl X) = Iso.hom (Iso.refl (↑U : Scheme)) ≫ U.ι

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
⊢ V.ι ≫ Iso.hom (Iso.refl X) = Iso.hom (Iso.refl (↑V : Scheme)) ≫ V.ι

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
rw : (𝟙 X ⁻¹ᵁ U).ι = U.ι
⊢ 𝟙 X ∣_ U = 𝟙 (↑(𝟙 X ⁻¹ᵁ U) : Scheme)

Tactic:
rw [← cancel_mono U.ι, morphismRestrict_ι, Category.comp_id, Category.id_comp]

Premises used: AlgebraicGeometry.morphismRestrict_ι, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
⊢ (𝟙 X ⁻¹ᵁ U).ι = U.ι

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
rw :
  (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
        (Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
        (pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.snd g (Scheme.Opens.ι U)) =
    (Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ pullback.snd (f ≫ g) (Scheme.Opens.ι U) =
    (Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)

Tactic:
rw [← pullbackRightPullbackFstIso_inv_snd_snd]

Premises used: CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
simp_rw :
  CategoryStruct.comp (Y := pullback g (Scheme.Opens.ι U))
      (CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
        ((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
        (pullback.snd f (pullback.fst g (Scheme.Opens.ι U))))
      (pullback.snd g (Scheme.Opens.ι U)) =
    ((Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.snd g (Scheme.Opens.ι U)
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
        (Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
        (pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.snd g (Scheme.Opens.ι U)) =
    (Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)

Tactic:
simp_rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
e_a :
  CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
      ((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
      (pullback.snd f (pullback.fst g (Scheme.Opens.ι U))) =
    (Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv
⊢ CategoryStruct.comp (Y := pullback g (Scheme.Opens.ι U))
      (CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
        ((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
        (pullback.snd f (pullback.fst g (Scheme.Opens.ι U))))
      (pullback.snd g (Scheme.Opens.ι U)) =
    ((Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.snd g (Scheme.Opens.ι U)

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
e_a :
  CategoryStruct.comp (Y := pullback g (Scheme.Opens.ι U))
      (CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
        ((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
        (pullback.snd f (pullback.fst g (Scheme.Opens.ι U))))
      (pullback.fst g (Scheme.Opens.ι U)) =
    ((Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.fst g (Scheme.Opens.ι U)
⊢ CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
      ((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
      (pullback.snd f (pullback.fst g (Scheme.Opens.ι U))) =
    (Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv

Tactic:
rw [← cancel_mono (pullback.fst _ _)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
e_a :
  (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
        (Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
        (pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.fst g (Scheme.Opens.ι U)) =
    CategoryStruct.comp (Y := pullback f (g ⁻¹ᵁ U).ι) (Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)))
      (pullback.snd f (g ⁻¹ᵁ U).ι ≫ (pullbackRestrictIsoRestrict g U).inv ≫ pullback.fst g (Scheme.Opens.ι U))
⊢ CategoryStruct.comp (Y := pullback g (Scheme.Opens.ι U))
      (CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
        ((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
        (pullback.snd f (pullback.fst g (Scheme.Opens.ι U))))
      (pullback.fst g (Scheme.Opens.ι U)) =
    ((Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)) ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.fst g (Scheme.Opens.ι U)

Tactic:
simp_rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
e_a : ((f ≫ g) ⁻¹ᵁ U).ι ≫ f = (f ⁻¹ᵁ g ⁻¹ᵁ U).ι ≫ f
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      CategoryStruct.comp (Y := pullback (Y := pullback g (Scheme.Opens.ι U)) f (pullback.fst g (Scheme.Opens.ι U)))
        (Iso.inv (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f))
        (pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.fst g (Scheme.Opens.ι U)) =
    CategoryStruct.comp (Y := pullback f (g ⁻¹ᵁ U).ι) (Iso.inv (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)))
      (pullback.snd f (g ⁻¹ᵁ U).ι ≫ (pullbackRestrictIsoRestrict g U).inv ≫ pullback.fst g (Scheme.Opens.ι U))

Tactic:
rw [pullbackRestrictIsoRestrict_inv_fst, pullbackRightPullbackFstIso_inv_snd_fst, ←
    pullback.condition, pullbackRestrictIsoRestrict_inv_fst_assoc,
    pullbackRestrictIsoRestrict_inv_fst_assoc]

Premises used: AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, CategoryTheory.Limits.pullback.condition, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ ((f ≫ g) ⁻¹ᵁ U).ι ≫ f = (f ⁻¹ᵁ g ⁻¹ᵁ U).ι ≫ f

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

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
x : ↥(↑(f ⁻¹ᵁ U) : Scheme)
⊢ Eq (α := ↥Y) ((↑((f ∣_ U) x) : ↥Y) : ↥Y) (f (↑x : ↥X) : ↥Y)

Tactic:
congr_arg (fun f => (Scheme.Hom.toLRSHom f).base x)
    (morphismRestrict_ι f U)

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, congr_arg, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Eq (α := (a : ↥(↑(f ⁻¹ᵁ U) : Scheme)) → ↥(↑U : Scheme)) (⇑(f ∣_ U)) (U.carrier.restrictPreimage ⇑f)

Tactic:
funext fun x => Subtype.ext (morphismRestrict_base_coe f U x)

Premises used: AlgebraicGeometry.morphismRestrict_base_coe, funext, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↥(↑U : Scheme)
⊢ (f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V = f ⁻¹ᵁ U.ι ''ᵁ V

Tactic:
IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback (isPullback_morphismRestrict f U) V

Premises used: AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
⊢ ∃ (V' : (↑U : Scheme).Opens), U.ι ⁻¹ᵁ U.ι ''ᵁ V' = V

Tactic:
⟨_, U.ι.preimage_image_eq V⟩

Premises used: AlgebraicGeometry.Scheme.Hom.preimage_image_eq, Exists.intro, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U : Scheme).Opens
obtain :
  ∀ (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 ⋯)))
⊢ Hom.app (f ∣_ U) V = Hom.app f (U.ι ''ᵁ V) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
obtain ⟨V, rfl⟩ : ∃ V', U.ι ⁻¹ᵁ U.ι ''ᵁ V' = V := ⟨_, U.ι.preimage_image_eq V⟩

Premises used: AlgebraicGeometry.Scheme.Opens.ι, rfl