awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
localizationAwayPreserves :
  ∀ [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S) (r : R) (R' S' : Type u) [inst_3 : CommRing R']
    [inst_4 : CommRing S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S'] [inst_7 : IsLocalization.Away r R']
    [inst_8 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S) (r : R) (R' S' : Type u) [inst_3 : CommRing R']
    [inst_4 : CommRing S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S'] [inst_7 : IsLocalization.Away r R']
    [inst_8 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
localizationAwayPreserves :
  ∀ [inst : CommRing S] (f : R →+* S) (r : R) (R' S' : Type u) [inst_3 : CommRing R'] [inst_4 : CommRing S']
    [inst_5 : Algebra R R'] [inst_6 : Algebra S S'] [inst_7 : IsLocalization.Away r R']
    [inst_8 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst : CommRing S] (f : R →+* S) (r : R) (R' S' : Type u) [inst_3 : CommRing R'] [inst_4 : CommRing S']
    [inst_5 : Algebra R R'] [inst_6 : Algebra S S'] [inst_7 : IsLocalization.Away r R']
    [inst_8 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
r : R
R' S' : Type u
localizationAwayPreserves :
  ∀ [inst : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
    [inst_7 : IsLocalization.Away r R'] [inst_8 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
    [inst_7 : IsLocalization.Away r R'] [inst_8 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_4 : CommRing R'
localizationAwayPreserves :
  ∀ [inst : CommRing S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S'] [inst_7 : IsLocalization.Away r R']
    [inst_8 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst : CommRing S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S'] [inst_7 : IsLocalization.Away r R']
    [inst_8 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_4 : CommRing R'
inst_5 : CommRing S'
localizationAwayPreserves :
  ∀ [inst : Algebra R R'] [inst_6 : Algebra S S'] [inst_7 : IsLocalization.Away r R']
    [inst_8 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst : Algebra R R'] [inst_6 : Algebra S S'] [inst_7 : IsLocalization.Away r R']
    [inst_8 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R R'
localizationAwayPreserves :
  ∀ [inst : Algebra S S'] [inst_7 : IsLocalization.Away r R']
    [inst_8 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst : Algebra S S'] [inst_7 : IsLocalization.Away r R']
    [inst_8 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
localizationAwayPreserves :
  ∀ [inst : IsLocalization.Away r R'] [inst_8 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst : IsLocalization.Away r R'] [inst_8 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : IsLocalization.Away r R'
localizationAwayPreserves :
  ∀ [inst : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
        (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : IsLocalization.Away r R'
inst_9 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
H : P (Spec.map (CommRingCat.ofHom f))
⊢ P (X := Spec (CommRingCat.of S')) (Y := Spec (CommRingCat.of R'))
    (Spec.map (CommRingCat.ofHom (IsLocalization.Away.map R' S' f r)))

Tactic:
(RingHom.RespectsIso.isLocalization_away_iff hP ..).mp ?_

Premises used: Iff.mp, RingHom.RespectsIso.isLocalization_away_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : IsLocalization.Away r R'
inst_9 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
H : P (Spec.map (CommRingCat.ofHom f))
localizationAwayPreserves : P (Spec.map (CommRingCat.ofHom (Localization.awayMap f r)))
⊢ P (X := Spec (CommRingCat.of S')) (Y := Spec (CommRingCat.of R'))
    (Spec.map (CommRingCat.ofHom (IsLocalization.Away.map R' S' f r)))

Tactic:
refine (RingHom.RespectsIso.isLocalization_away_iff hP ..).mp ?_

Premises used: Iff.mp, RingHom.RespectsIso.isLocalization_away_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : IsLocalization.Away r R'
inst_9 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
H : P (Spec.map (CommRingCat.ofHom f))
⊢ P (Spec.map (CommRingCat.ofHom (Localization.awayMap f r)))

Tactic:
(MorphismProperty.arrow_mk_iso_iff P (SpecMapRestrictBasicOpenIso
      (CommRingCat.ofHom f) r)).mp (IsZariskiLocalAtTarget.restrict H (basicOpen r))

Premises used: PrimeSpectrum.basicOpen, AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.SpecMapRestrictBasicOpenIso, CommRingCat.ofHom, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : IsLocalization.Away r R'
inst_9 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
H : P (Spec.map (CommRingCat.ofHom f))
⊢ P (Spec.map (CommRingCat.ofHom (Localization.awayMap f r)))

Tactic:
exact (MorphismProperty.arrow_mk_iso_iff P (SpecMapRestrictBasicOpenIso
      (CommRingCat.ofHom f) r)).mp (IsZariskiLocalAtTarget.restrict H (basicOpen r))

Premises used: PrimeSpectrum.basicOpen, AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.SpecMapRestrictBasicOpenIso, CommRingCat.ofHom, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
ofLocalizationSpanTarget :
  ∀ [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S) (s : Set S),
    Eq (α := Ideal S) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)),
          (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) _
            (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)) →
        (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f
⊢ ∀ [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S) (s : Set S),
    Eq (α := Ideal S) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)),
          (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) _
            (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)) →
        (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
ofLocalizationSpanTarget :
  ∀ [inst : CommRing S] (f : R →+* S) (s : Set S),
    Eq (α := Ideal S) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)),
          (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) _
            (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)) →
        (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f
⊢ ∀ [inst : CommRing S] (f : R →+* S) (s : Set S),
    Eq (α := Ideal S) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)),
          (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) _
            (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)) →
        (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
⊢ Eq.{u + 1} (α := Ideal (↑(CommRingCat.of S) : Type u)) (Ideal.span (Set.range fun (i : (↑s : Type u)) ↦ (↑i : S))) ⊤

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
ofLocalizationSpanTarget :
  ∀ (i : (Scheme.affineOpenCoverOfSpanRangeEqTop (fun (i : (↑s : Type u)) ↦ (↑i : S)) ⋯).openCover.I₀),
    P
      ((Scheme.affineOpenCoverOfSpanRangeEqTop (fun (i : (↑s : Type u)) ↦ (↑i : S)) ⋯).openCover.f i ≫
        Spec.map (CommRingCat.ofHom f))
⊢ P (Spec.map (CommRingCat.ofHom f))

Tactic:
apply IsZariskiLocalAtSource.of_openCover (Scheme.affineOpenCoverOfSpanRangeEqTop
      (fun i : s ↦ (i : S)) (by simpa)).openCover

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.of_openCover, AlgebraicGeometry.Scheme.AffineOpenCover.openCover, AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
i : (Scheme.affineOpenCoverOfSpanRangeEqTop (fun (i : (↑s : Type u)) ↦ (↑i : S)) ⋯).openCover.I₀
ofLocalizationSpanTarget :
  P (X :=
    Spec ((Scheme.affineOpenCoverOfSpanRangeEqTop (fun (i : (↑s : Type u)) ↦ (↑i : S)) ⋯).X (P := IsOpenImmersion) i))
    (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap S (Localization.Away (↑i : S)))))
⊢ P
    ((Scheme.affineOpenCoverOfSpanRangeEqTop (fun (i : (↑s : Type u)) ↦ (↑i : S)) ⋯).openCover.f i ≫
      Spec.map (CommRingCat.ofHom f))

Tactic:
simp only [CommRingCat.coe_of, Scheme.AffineOpenCover.openCover_X, ← Spec.map_comp,
      Scheme.AffineOpenCover.openCover_f, Scheme.affineOpenCoverOfSpanRangeEqTop_f]

Premises used: AlgebraicGeometry.Scheme.AffineOpenCover.openCover_f, CommRingCat.coe_of, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_f, AlgebraicGeometry.Scheme.AffineOpenCover.openCover_X
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
i : (Scheme.affineOpenCoverOfSpanRangeEqTop (fun (i : (↑s : Type u)) ↦ (↑i : S)) ⋯).openCover.I₀
⊢ P (X :=
    Spec ((Scheme.affineOpenCoverOfSpanRangeEqTop (fun (i : (↑s : Type u)) ↦ (↑i : S)) ⋯).X (P := IsOpenImmersion) i))
    (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap S (Localization.Away (↑i : S)))))

Tactic:
H i

Premises used: Set.Mem, OreLocalization, Quotient
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
i : (Scheme.affineOpenCoverOfSpanRangeEqTop (fun (i : (↑s : Type u)) ↦ (↑i : S)) ⋯).openCover.I₀
⊢ P (X :=
    Spec ((Scheme.affineOpenCoverOfSpanRangeEqTop (fun (i : (↑s : Type u)) ↦ (↑i : S)) ⋯).X (P := IsOpenImmersion) i))
    (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap S (Localization.Away (↑i : S)))))

Tactic:
exact H i
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
hP :
  RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
R S : Type u
ofLocalizationSpan :
  ∀ [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S) (s : Set R),
    Eq (α := Ideal R) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)),
          (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
            (Localization.Away (↑r : R)) _ _ _ (Localization.awayMap f (↑r : R))) →
        (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f
⊢ ∀ [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S) (s : Set R),
    Eq (α := Ideal R) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)),
          (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f)))
            (Localization.Away (↑r : R)) _ _ _ (Localization.awayMap f (↑r : R))) →
        (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))) f

Tactic:
_