awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
refine_1 :
  Scheme.Spec.map
        (Quiver.Hom.op
          (Hom.appLE f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
            (X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑r : (↑Γ(Y, ⊤) : Type u))))
            ⋯)) ≫
      ⋯.isoSpec.symm.hom =
    e.symm.hom ≫ Cover.pullbackHom (P := IsOpenImmersion) Y.openCoverBasicOpenTop f r
refine_2 :
  Scheme.Spec.map (Quiver.Hom.op (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) ≫
      Iso.hom (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(X, ⊤)))) =
    e.symm.hom ≫ (Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ
⊢ IsPullback (Cover.pullbackHom (P := IsOpenImmersion) Y.openCoverBasicOpenTop f r)
    ((Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ)
    (Y.openCoverBasicOpenTop.f r ≫ Y.toSpecΓ) (Spec.map (Hom.appTop f))

Tactic:
refine .of_iso ((this r.1).op.map Scheme.Spec) e.symm r.2.isoSpec.symm (.refl _) (.refl _)
    ?_ ?_ (by simp) (by simp)
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
refine_1 :
  e.hom ≫
      Scheme.Spec.map
        (Quiver.Hom.op
          (Hom.appLE f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
            (X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑r : (↑Γ(Y, ⊤) : Type u))))
            ⋯)) =
    Cover.pullbackHom (P := IsOpenImmersion) Y.openCoverBasicOpenTop f r ≫ ⋯.isoSpec.hom
⊢ Scheme.Spec.map
        (Quiver.Hom.op
          (Hom.appLE f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
            (X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑r : (↑Γ(Y, ⊤) : Type u))))
            ⋯)) ≫
      ⋯.isoSpec.symm.hom =
    e.symm.hom ≫ Cover.pullbackHom (P := IsOpenImmersion) Y.openCoverBasicOpenTop f r

Tactic:
simp only [Iso.symm_hom, Iso.eq_inv_comp, ← Category.assoc, Iso.comp_inv_eq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
refine_1 :
  (Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫
        Iso.hom (X.isoOfEq ⋯) ≫
          (X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑r : (↑Γ(Y, ⊤) : Type u)))).toSpecΓ) ≫
      Spec.map (Hom.app f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) =
    pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ
⊢ e.hom ≫
      Scheme.Spec.map
        (Quiver.Hom.op
          (Hom.appLE f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
            (X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑r : (↑Γ(Y, ⊤) : Type u))))
            ⋯)) =
    Cover.pullbackHom (P := IsOpenImmersion) Y.openCoverBasicOpenTop f r ≫ ⋯.isoSpec.hom

Tactic:
dsimp [e, Scheme.Cover.pullbackHom, IsAffineOpen.isoSpec_hom, Scheme.Hom.appLE]

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.IsAffineOpen.isoSpec_hom
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
refine_1 :
  Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫
      Iso.hom (X.isoOfEq ⋯) ≫
        X.homOfLE ⋯ ≫ f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)) ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ =
    pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ
⊢ (Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫
        Iso.hom (X.isoOfEq ⋯) ≫
          (X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑r : (↑Γ(Y, ⊤) : Type u)))).toSpecΓ) ≫
      Spec.map (Hom.app f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) =
    pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ

Tactic:
simp only [homOfLE_leOfHom, Spec.map_comp, Category.assoc,
      Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, Scheme.Opens.toSpecΓ_naturality]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, CategoryTheory.homOfLE_leOfHom, AlgebraicGeometry.Spec.map_comp
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
refine_1 :
  (((Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫ Iso.hom (X.isoOfEq ⋯)) ≫
          X.homOfLE ⋯) ≫
        f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≫
      (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ =
    pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ
⊢ Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫
      Iso.hom (X.isoOfEq ⋯) ≫
        X.homOfLE ⋯ ≫ f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)) ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ =
    pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ

Tactic:
simp_rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
refine_1 :
  ((Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫ Iso.hom (X.isoOfEq ⋯)) ≫
        X.homOfLE ⋯) ≫
      f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)) =
    pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι
⊢ (((Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫ Iso.hom (X.isoOfEq ⋯)) ≫
          X.homOfLE ⋯) ≫
        f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≫
      (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ =
    pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).toSpecΓ

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
refine_1 :
  (((Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫ Iso.hom (X.isoOfEq ⋯)) ≫
          X.homOfLE ⋯) ≫
        f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≫
      (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι =
    pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι
⊢ ((Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫ Iso.hom (X.isoOfEq ⋯)) ≫
        X.homOfLE ⋯) ≫
      f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)) =
    pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι

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

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ (((Iso.hom (pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) ≫ Iso.hom (X.isoOfEq ⋯)) ≫
          X.homOfLE ⋯) ≫
        f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≫
      (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι =
    pullback.snd f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≫ (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
refine_2 :
  e.hom ≫
      Scheme.Spec.map (Quiver.Hom.op (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) ≫
        Iso.hom (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(X, ⊤)))) =
    (Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ
⊢ Scheme.Spec.map (Quiver.Hom.op (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) ≫
      Iso.hom (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(X, ⊤)))) =
    e.symm.hom ≫ (Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ

Tactic:
simp only [Iso.symm_hom, Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ e.hom ≫
      Scheme.Spec.map (Quiver.Hom.op (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) ≫
        Iso.hom (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(X, ⊤)))) =
    (Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ

Tactic:
simp [e, IsAffineOpen.isoSpec_hom]

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec_hom
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : X.IsQuasiAffine
inst_2 : Y.IsQuasiAffine
⊢ Spec.map (Hom.appTop f) ⁻¹ᵁ Hom.opensRange Y.toSpecΓ = Hom.opensRange X.toSpecΓ

Tactic:
simpa using (IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback
    (isPullback_toSpecΓ_toSpecΓ f) ⊤).symm

Premises used: AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ, AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback, Top.top, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F G : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
s : F ⟶ G
inst_1 : Quiver.IsThin.{u_1, u_2} J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective (α := ↥(F.obj i)) (β := ↥(F.obj j)) ⇑(F.map hij)
inst_2 : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq :
  Eq (α := ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fi)) : (a : ↥(F.obj i)) → ↥(F.obj k)) xi : ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fj)) : (a : ↥(F.obj j)) → ↥(F.obj k)) xj : ↥(F.obj k))
simp :
  Eq (α := ↥(G.obj k)) ((G.map fi) ((s.app i) xi : ↥(G.obj i)) : ↥(G.obj k))
    ((G.map fj) ((s.app j) xj : ↥(G.obj j)) : ↥(G.obj k))
⊢ Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map fi) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj k))
        ((s.app i) xi : ↥(G.obj i)) :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map fj) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj k))
        ((s.app j) xj : ↥(G.obj j)) :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj k))

Tactic:
simp only [Functor.comp_obj, forget_obj, Functor.comp_map, forget_map,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]

Premises used: CategoryTheory.Functor.comp_obj, AlgebraicGeometry.Scheme.forget_map, AlgebraicGeometry.Scheme.forget_obj, TypeCat.Fun.coe_mk, CategoryTheory.ConcreteCategory.hom_ofHom, CategoryTheory.Functor.comp_map
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F G : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
s : F ⟶ G
inst_1 : Quiver.IsThin.{u_1, u_2} J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective (α := ↥(F.obj i)) (β := ↥(F.obj j)) ⇑(F.map hij)
inst_2 : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : Eq (α := ↥(F.obj k)) ((F.map fi) xi : ↥(F.obj k)) ((F.map fj) xj : ↥(F.obj k))
rw : Eq (α := ↥(G.obj k)) ((s.app j ≫ G.map fj) xj : ↥(G.obj k)) ((G.map fj) ((s.app j) xj : ↥(G.obj j)) : ↥(G.obj k))
⊢ Eq (α := ↥(G.obj k)) ((G.map fi) ((s.app i) xi : ↥(G.obj i)) : ↥(G.obj k))
    ((G.map fj) ((s.app j) xj : ↥(G.obj j)) : ↥(G.obj k))

Tactic:
rw [← Scheme.Hom.comp_apply, ← s.naturality, Scheme.Hom.comp_apply, heq,
        ← Scheme.Hom.comp_apply, s.naturality]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.NatTrans.naturality