awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
H :
  ∀ ⦃X Y S : Scheme.{u_1}⦄ [inst : IsAffine S] [inst_3 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    P g → P (X := pullback f g) (pullback.fst f g)
Z X Y S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
g' : Z ⟶ X
h : IsPullback g' f' f g
hg : P g
rw : P (X := pullback f g) (pullback.fst f g)
⊢ P g'

Tactic:
rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_fst]

Premises used: CategoryTheory.IsPullback.isoPullback_inv_fst, CategoryTheory.IsPullback.isoPullback, AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
H :
  ∀ ⦃X Y S : Scheme.{u_1}⦄ [inst : IsAffine S] [inst_3 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    P g → P (X := pullback f g) (pullback.fst f g)
Z X Y S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
g' : Z ⟶ X
h : IsPullback g' f' f g
hg : P g
⊢ P (X := pullback f g) (pullback.fst f g)

Tactic:
H f g hg
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
H :
  ∀ ⦃X Y S : Scheme.{u_1}⦄ [inst : IsAffine S] [inst_3 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    P g → P (X := pullback f g) (pullback.fst f g)
Z X Y S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
g' : Z ⟶ X
h : IsPullback g' f' f g
hg : P g
⊢ P (X := pullback f g) (pullback.fst f g)

Tactic:
exact H f g hg
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.IsLocal
X Y UX UY : Scheme
inst_1 : IsAffine UY
f : X ⟶ Y
iY : UY ⟶ Y
inst_2 : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
hf : targetAffineLocally P f
rw : P (X := pullback f iY) (pullback.snd f iY)
⊢ P f'

Tactic:
rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_snd]

Premises used: CategoryTheory.IsPullback.isoPullback_inv_snd, CategoryTheory.IsPullback.isoPullback, AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.IsLocal
X Y UX UY : Scheme
inst_1 : IsAffine UY
f : X ⟶ Y
iY : UY ⟶ Y
inst_2 : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
hf : targetAffineLocally P f
⊢ P (X := pullback f iY) (pullback.snd f iY)

Tactic:
(P.arrow_mk_iso_iff
    (morphismRestrictOpensRange f _)).mp (hf ⟨_, isAffineOpen_opensRange iY⟩)

Premises used: AlgebraicGeometry.isAffineOpen_opensRange, AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff, Subtype.mk, AlgebraicGeometry.morphismRestrictOpensRange, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.IsLocal
X Y UX UY : Scheme
inst_1 : IsAffine UY
f : X ⟶ Y
iY : UY ⟶ Y
inst_2 : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
hf : targetAffineLocally P f
⊢ P (X := pullback f iY) (pullback.snd f iY)

Tactic:
exact (P.arrow_mk_iso_iff
    (morphismRestrictOpensRange f _)).mp (hf ⟨_, isAffineOpen_opensRange iY⟩)

Premises used: AlgebraicGeometry.isAffineOpen_opensRange, AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff, Subtype.mk, AlgebraicGeometry.morphismRestrictOpensRange, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
hprecomp : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z), targetAffineLocally P f → targetAffineLocally P (e.hom ≫ f)
hpostcomp :
  ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y), targetAffineLocally P f → targetAffineLocally P (f ≫ e.hom)
⊢ (targetAffineLocally P).RespectsIso

Tactic:
apply MorphismProperty.RespectsIso.mk

Premises used: CategoryTheory.MorphismProperty.RespectsIso.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
H : targetAffineLocally P f
U : (↑Z.affineOpens : Type u_1)
hprecomp : P (X := (↑(f ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ (↑U : Z.Opens))
⊢ P (X := (↑((e.hom ≫ f) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) ((e.hom ≫ f) ∣_ (↑U : Z.Opens))

Tactic:
rw [morphismRestrict_comp, P.cancel_left_of_respectsIso]

Premises used: AlgebraicGeometry.morphismRestrict_comp, AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
H : targetAffineLocally P f
U : (↑Z.affineOpens : Type u_1)
⊢ P (X := (↑(f ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ (↑U : Z.Opens))

Tactic:
H U
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
H : targetAffineLocally P f
U : (↑Z.affineOpens : Type u_1)
⊢ P (X := (↑(f ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ (↑U : Z.Opens))

Tactic:
exact H U
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
hpostcomp : P ((f ≫ e.hom) ∣_ U)
⊢ P (X := (↑((f ≫ e.hom) ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Z.Opens) ↦ x ∈ Z.affineOpens) U hU) : Z.Opens)) : Scheme))
    ((f ≫ e.hom) ∣_ (↑(Subtype.mk (p := fun (x : Z.Opens) ↦ x ∈ Z.affineOpens) U hU) : Z.Opens))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
hpostcomp : ∀ (this : IsAffine.{u_1} (↑(e.hom ⁻¹ᵁ U) : Scheme)), P ((f ≫ e.hom) ∣_ U)
⊢ P ((f ≫ e.hom) ∣_ U)

Tactic:
haveI : IsAffine _ := hU.preimage_of_isIso e.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
this : IsAffine.{u_1} (↑(e.hom ⁻¹ᵁ U) : Scheme)
hpostcomp : P (X := (↑((Opens.map f.base).obj ((Opens.map e.hom.base).obj U)) : Scheme)) (f ∣_ e.hom ⁻¹ᵁ U)
⊢ P ((f ≫ e.hom) ∣_ U)

Tactic:
rw [morphismRestrict_comp, P.cancel_right_of_respectsIso]

Premises used: AlgebraicGeometry.morphismRestrict_comp, AlgebraicGeometry.AffineTargetMorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
this : IsAffine.{u_1} (↑(e.hom ⁻¹ᵁ U) : Scheme)
⊢ P (X := (↑((Opens.map f.base).obj ((Opens.map e.hom.base).obj U)) : Scheme)) (f ∣_ e.hom ⁻¹ᵁ U)

Tactic:
H ⟨(Opens.map e.hom.base).obj U, hU.preimage_of_isIso e.hom⟩

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Subtype.mk, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
this : IsAffine.{u_1} (↑(e.hom ⁻¹ᵁ U) : Scheme)
⊢ P (X := (↑((Opens.map f.base).obj ((Opens.map e.hom.base).obj U)) : Scheme)) (f ∣_ e.hom ⁻¹ᵁ U)

Tactic:
exact H ⟨(Opens.map e.hom.base).obj U, hU.preimage_of_isIso e.hom⟩

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Subtype.mk, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q_1 : AffineTargetMorphismProperty
inst : HasAffineProperty P Q_1
X Y : Scheme
f : X ⟶ Y
Q : AffineTargetMorphismProperty
inst_1 : Q.IsLocal
⊢ HasAffineProperty (targetAffineLocally Q) Q

Tactic:
⟨inferInstance, rfl⟩

Premises used: AlgebraicGeometry.HasAffineProperty.mk, inferInstance, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
⊢ P = targetAffineLocally Q

Tactic:
eq_targetAffineLocally'

Premises used: AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
h : ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y), P f ↔ targetAffineLocally (AffineTargetMorphismProperty.of P) f
⊢ P = targetAffineLocally (AffineTargetMorphismProperty.of P)

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
h : P f → targetAffineLocally (AffineTargetMorphismProperty.of P) f
h₁ : targetAffineLocally (AffineTargetMorphismProperty.of P) f → P f
⊢ P f ↔ targetAffineLocally (AffineTargetMorphismProperty.of P) f

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : P f
h :
  ∀ (U : Y.Opens) (hU : U ∈ Y.affineOpens),
    AffineTargetMorphismProperty.of P (X :=
      (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Scheme))
      (f ∣_ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens))
⊢ targetAffineLocally (AffineTargetMorphismProperty.of P) f

Tactic:
⟨U, hU⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : P f
U : Y.Opens
hU : U ∈ Y.affineOpens
⊢ AffineTargetMorphismProperty.of P (X :=
    (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Scheme))
    (f ∣_ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens))

Tactic:
IsZariskiLocalAtTarget.restrict hf _

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.AffineTargetMorphismProperty.of
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : P f
U : Y.Opens
hU : U ∈ Y.affineOpens
⊢ AffineTargetMorphismProperty.of P (X :=
    (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Scheme))
    (f ∣_ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens))

Tactic:
exact IsZariskiLocalAtTarget.restrict hf _

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : targetAffineLocally (AffineTargetMorphismProperty.of P) f
⊢ P f

Tactic:
P.of_zeroHypercover_target Y.affineCover
        fun i ↦ of_targetAffineLocally_of_isPullback (.of_hasPullback _ _) hf

Premises used: AlgebraicGeometry.of_targetAffineLocally_of_isPullback, CategoryTheory.PreZeroHypercover.f, CategoryTheory.MorphismProperty.of_zeroHypercover_target, CategoryTheory.IsPullback.of_hasPullback, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : targetAffineLocally (AffineTargetMorphismProperty.of P) f
⊢ P f

Tactic:
exact P.of_zeroHypercover_target Y.affineCover
        fun i ↦ of_targetAffineLocally_of_isPullback (.of_hasPullback _ _) hf

Premises used: AlgebraicGeometry.of_targetAffineLocally_of_isPullback, CategoryTheory.PreZeroHypercover.f, CategoryTheory.MorphismProperty.of_zeroHypercover_target, CategoryTheory.IsPullback.of_hasPullback, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
UX UY : Scheme
inst_1 : IsAffine UY
iY : UY ⟶ Y
inst_2 : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
hf : P f
⊢ Q f'

Tactic:
letI := isLocal_affineProperty P
  of_targetAffineLocally_of_isPullback h (eq_targetAffineLocally (P := P) ▸ hf)

Premises used: AlgebraicGeometry.of_targetAffineLocally_of_isPullback, Eq.rec, AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
hf : P f
U : (↑Y.affineOpens : Type u)
⊢ Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))

Tactic:
of_isPullback (isPullback_morphismRestrict f U).flip hf

Premises used: AlgebraicGeometry.HasAffineProperty.of_isPullback, CategoryTheory.IsPullback.flip, AlgebraicGeometry.isPullback_morphismRestrict, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
rw : (targetAffineLocally Q).RespectsIso
⊢ P.RespectsIso

Tactic:
rw [eq_targetAffineLocally P]

Premises used: AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ (targetAffineLocally Q).RespectsIso

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U i) : Y.Opens))
letI : P f
⊢ P f

Tactic:
letI := isLocal_affineProperty P
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U i) : Y.Opens))
this : Q.IsLocal := ⋯
rw : targetAffineLocally Q f
⊢ P f

Tactic:
rw [eq_targetAffineLocally P]

Premises used: AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U_1 : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U_1 i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U_1 i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U_1 i) : Y.Opens))
this : Q.IsLocal := ⋯
U : (↑Y.affineOpens : Type u)
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
h : Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
basicOpen :
  ∀
    (this :
      Q (X :=
        (↑((f ∣_ (↑U : Y.Opens)) ⁻¹ᵁ
              (↑(↑U : Y.Opens) : Scheme).basicOpen (U := ⊤)
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (↑U : Y.Opens).topIso.inv :
                    (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
                  r)) :
          Scheme))
        (f ∣_ (↑U : Y.Opens) ∣_
          (↑(↑U : Y.Opens) : Scheme).basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (↑U : Y.Opens).topIso.inv :
                (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
              r))),
    Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen r) : Y.Opens)) : Scheme)) (f ∣_ (↑(Y.affineBasicOpen r) : Y.Opens))
⊢ Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen r) : Y.Opens)) : Scheme)) (f ∣_ (↑(Y.affineBasicOpen r) : Y.Opens))

Tactic:
have := AffineTargetMorphismProperty.IsLocal.to_basicOpen (f ∣_ U.1) (U.1.topIso.inv r) h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U_1 : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U_1 i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U_1 i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U_1 i) : Y.Opens))
this_1 : Q.IsLocal := ⋯
U : (↑Y.affineOpens : Type u)
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
h : Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
this :
  Q (X :=
    (↑((f ∣_ (↑U : Y.Opens)) ⁻¹ᵁ
          (↑(↑U : Y.Opens) : Scheme).basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (↑U : Y.Opens).topIso.inv :
                (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
              r)) :
      Scheme))
    (f ∣_ (↑U : Y.Opens) ∣_
      (↑(↑U : Y.Opens) : Scheme).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (↑U : Y.Opens).topIso.inv :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
          r))
⊢ Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen r) : Y.Opens)) : Scheme)) (f ∣_ (↑(Y.affineBasicOpen r) : Y.Opens))

Tactic:
(Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r)).mp this

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.RingedSpace.basicOpen, AlgebraicGeometry.Scheme.basicOpen, Iff.mp, AlgebraicGeometry.morphismRestrictRestrictBasicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U_1 : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U_1 i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U_1 i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U_1 i) : Y.Opens))
this_1 : Q.IsLocal := ⋯
U : (↑Y.affineOpens : Type u)
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
h : Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
this :
  Q (X :=
    (↑((f ∣_ (↑U : Y.Opens)) ⁻¹ᵁ
          (↑(↑U : Y.Opens) : Scheme).basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (↑U : Y.Opens).topIso.inv :
                (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
              r)) :
      Scheme))
    (f ∣_ (↑U : Y.Opens) ∣_
      (↑(↑U : Y.Opens) : Scheme).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (↑U : Y.Opens).topIso.inv :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
          r))
⊢ Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen r) : Y.Opens)) : Scheme)) (f ∣_ (↑(Y.affineBasicOpen r) : Y.Opens))

Tactic:
exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r)).mp this

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff, Iff.mp, AlgebraicGeometry.morphismRestrictRestrictBasicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U_1 : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U_1 i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U_1 i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U_1 i) : Y.Opens))
this : Q.IsLocal := ⋯
U : (↑Y.affineOpens : Type u)
s : Finset (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, (↑U : Y.Opens)) : Type u))) ⊤
H :
  ∀ (f_1 : ↥s),
    Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen (↑f_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u))) : Y.Opens)) : Scheme))
      (f ∣_ (↑(Y.affineBasicOpen (↑f_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u))) : Y.Opens))
⊢ Eq (α := Ideal (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
    (Ideal.span
      (↑(Finset.image
            (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (↑U : Y.Opens).topIso.inv) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
            s) :
        Set (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u)))
    ⊤

Tactic:
simp [← Ideal.map_span, hs, Ideal.map_top]

Premises used: Ideal.map_span, Ideal.map_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U_1 : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U_1 i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U_1 i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U_1 i) : Y.Opens))
this : Q.IsLocal := ⋯
U : (↑Y.affineOpens : Type u)
s : Finset (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, (↑U : Y.Opens)) : Type u))) ⊤
H :
  ∀ (f_1 : ↥s),
    Q (X := (↑(f ⁻¹ᵁ (↑(Y.affineBasicOpen (↑f_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u))) : Y.Opens)) : Scheme))
      (f ∣_ (↑(Y.affineBasicOpen (↑f_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u))) : Y.Opens))
openCover :
  ∀
    (r :
      ↥(Finset.image
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (↑U : Y.Opens).topIso.inv) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
          s)),
    Q (X :=
      (↑((f ∣_ (↑U : Y.Opens)) ⁻¹ᵁ
            (↑(↑U : Y.Opens) : Scheme).basicOpen (↑r : (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))) :
        Scheme))
      (f ∣_ (↑U : Y.Opens) ∣_ (↑(↑U : Y.Opens) : Scheme).basicOpen (↑r : (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u)))
⊢ Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))

Tactic:
apply AffineTargetMorphismProperty.IsLocal.of_basicOpenCover _
      (s.image (Scheme.Opens.topIso _).inv) (by simp [← Ideal.map_span, hs, Ideal.map_top])

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Opens.topIso, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.of_basicOpenCover, DFunLike.coe, Finset.image, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → (↑Y.affineOpens : Type u)
hU : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ι), (↑(U i) : Y.Opens)) ⊤
hU' : ∀ (i : ι), Q (X := (↑(f ⁻¹ᵁ (↑(U i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U i) : Y.Opens))
this : Q.IsLocal := ⋯
i : ι
⊢ Q (X := (↑(f ⁻¹ᵁ (↑(U i) : Y.Opens)) : Scheme)) (f ∣_ (↑(U i) : Y.Opens))

Tactic:
hU' i