awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
hf_1 :
  ∀ (x : ↥X),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
x : ↥X
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
hxV : x ∈ (↑V : X.Opens)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f (↑U : Y.Opens) ≫ X.presheaf.map (homOfLE e).op))
⊢ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦
      Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso

Tactic:
haveI : (toMorphismProperty (Locally Q)).RespectsIso := toMorphismProperty_respectsIso_iff.mp <|
      (isLocal_ringHomProperty P).respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : P.Respects IsOpenImmersion
hf_1 :
  ∀ (x : ↥X),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
x : ↥X
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
hxV : x ∈ (↑V : X.Opens)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f (↑U : Y.Opens) ≫ X.presheaf.map (homOfLE e).op))
this :
  (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦
      Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.resLE f (↑U : Y.Opens) (↑V : X.Opens) e)))

Tactic:
(MorphismProperty.arrow_mk_iso_iff (toMorphismProperty (Locally Q))
      (arrowResLEAppIso f U V e)).mpr (locally_of hQi _ hf)

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.arrowResLEAppIso, RingHom.toMorphismProperty, RingHom.Locally, RingHom.locally_of, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : P.Respects IsOpenImmersion
hf_1 :
  ∀ (x : ↥X),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
x : ↥X
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
hxV : x ∈ (↑V : X.Opens)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f (↑U : Y.Opens) ≫ X.presheaf.map (homOfLE e).op))
this :
  (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦
      Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.resLE f (↑U : Y.Opens) (↑V : X.Opens) e)))

Tactic:
exact (MorphismProperty.arrow_mk_iso_iff (toMorphismProperty (Locally Q))
      (arrowResLEAppIso f U V e)).mpr (locally_of hQi _ hf)

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.arrowResLEAppIso, RingHom.toMorphismProperty, RingHom.Locally, RingHom.locally_of, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
haveI inst : HasRingHomProperty P Q := inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst inst₁ : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
e : P = P
e' :
  ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S),
    Q f ↔ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
apply @copy (P := P) (P' := P) (Q := Q) (Q' := Locally Q)

Premises used: AlgebraicGeometry.HasRingHomProperty.copy
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ P = P

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : Type u
e' :
  ∀ [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S),
    Q f ↔ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ ∀ [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S),
    Q f ↔ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst_2 : CommRing R
e' : ∀ [inst : CommRing S] (f : R →+* S), Q f ↔ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ ∀ [inst : CommRing S] (f : R →+* S), Q f ↔ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f_1 : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
⊢ Q f ↔ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
(locally_iff_of_localizationSpanTarget (isLocal_ringHomProperty P).respectsIso
        (isLocal_ringHomProperty P).ofLocalizationSpanTarget _).symm

Premises used: RingHom.locally_iff_of_localizationSpanTarget, AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty, RingHom.PropertyIsLocal.ofLocalizationSpanTarget, Iff.symm, RingHom.PropertyIsLocal.respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f_1 : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
⊢ Q f ↔ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
exact (locally_iff_of_localizationSpanTarget (isLocal_ringHomProperty P).respectsIso
        (isLocal_ringHomProperty P).ofLocalizationSpanTarget _).symm

Premises used: RingHom.locally_iff_of_localizationSpanTarget, AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty, RingHom.PropertyIsLocal.ofLocalizationSpanTarget, Iff.symm, RingHom.PropertyIsLocal.respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
haveI : HasRingHomProperty P (Locally Q) := by
    apply @copy (P := P) (P' := P) (Q := Q) (Q' := Locally Q)
    · infer_instance
    · rfl
    · intro R S _ _ f
      exact (locally_iff_of_localizationSpanTarget (isLocal_ringHomProperty P).respectsIso
        (isLocal_ringHomProperty P).ofLocalizationSpanTarget _).symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ P f ↔
    ∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))

Tactic:
rw [iff_exists_appLE_locally (P := P) hQ]

Premises used: AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
haveI : HasRingHomProperty P Q := inst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
apply (isLocal_ringHomProperty P (Q := Q)).respectsIso

Premises used: AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty, RingHom.PropertyIsLocal.respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQa : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↥X),
        ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
          (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
          Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
⊢ HasRingHomProperty.{u}
    (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦
      Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
haveI : HasRingHomProperty (affineLocally (Locally Q)) (Locally Q) :=
      ⟨locally_propertyIsLocal hQl hQa, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQa : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↥X),
        ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
          (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
          Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
this :
  HasRingHomProperty.{u}
    (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦
      Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h₁ :
  ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y),
    P f ↔
      affineLocally
        (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ P =
    affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦
      Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQa : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↥X),
        ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
          (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
          Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
this :
  HasRingHomProperty.{u}
    (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦
      Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
h₁ :
  (∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))) ↔
    affineLocally
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
h₂ h₃ :
  (∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))) ↔
    ∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
⊢ P f ↔
    affineLocally
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
rw [h, iff_exists_appLE_locally (P := affineLocally (Locally Q)) hQa.left hQa.respectsIso]

Premises used: And.left, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally, RingHom.StableUnderCompositionWithLocalizationAway.respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have : ∀ (hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q), P f
⊢ P f

Tactic:
have hQi := (HasRingHomProperty.isLocal_ringHomProperty P).respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
        (hY : IsAffine Y), P f)
    (hY : ¬IsAffine Y), P f
wlog :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
    (hY : IsAffine Y), P f
⊢ P f

Tactic:
wlog hY : IsAffine Y generalizing X Y f

Premises used: AlgebraicGeometry.IsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
    (hY : IsAffine Y), P f
hY : ¬IsAffine Y
inr : ∀ (i : (↑Y.affineOpens : Type u)), P (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (f ∣_ (↑i : Y.Opens))
⊢ P f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
    (hY : IsAffine Y), P f
hY : ¬IsAffine Y
U : (↑Y.affineOpens : Type u)
⊢ P (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))

Tactic:
this (fun x ↦ ?_) U.2

Premises used: Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
    (hY : IsAffine Y), P f
hY : ¬IsAffine Y
U : (↑Y.affineOpens : Type u)
inr :
  ∀ (x : ↥(↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)),
    Q (R := (↑((↑(↑U : Y.Opens) : Scheme).presheaf.stalk ((f ∣_ (↑U : Y.Opens)) x)) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ∣_ (↑U : Y.Opens)) x))
⊢ P (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))

Tactic:
refine this (fun x ↦ ?_) U.2

Premises used: Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
    (hY : IsAffine Y), P f
hY : ¬IsAffine Y
U : (↑Y.affineOpens : Type u)
x : ↥(↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)
⊢ Q (R := (↑((↑(↑U : Y.Opens) : Scheme).presheaf.stalk ((f ∣_ (↑U : Y.Opens)) x)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ∣_ (↑U : Y.Opens)) x))

Tactic:
(hQi.arrow_mk_iso_iff (AlgebraicGeometry.morphismRestrictStalkMap f U x)).mpr (H x.val)

Premises used: Iff.mpr, AlgebraicGeometry.morphismRestrictStalkMap, Subtype.val, RingHom.RespectsIso.arrow_mk_iso_iff