mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝³ : IsZariskiLocalAtTarget P
inst✝² : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
R' S' : Type u
⊢ ∀ [inst : CommRing R'] [inst_1 : CommRing S'] [inst_2 : Algebra R R'] [inst_3 : Algebra S S']
    [inst_4 : IsLocalization.Away r R'] [inst_5 : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (IsLocalization.Away.map R' S' f r)

Tactic:
_

Goal state after:
case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁴ : IsZariskiLocalAtTarget P
inst✝³ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝ : CommRing R'
⊢ ∀ [inst : CommRing S'] [inst_1 : Algebra R R'] [inst_2 : Algebra S S'] [inst_3 : IsLocalization.Away r R']
    [inst_4 : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (IsLocalization.Away.map R' S' f r)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁴ : IsZariskiLocalAtTarget P
inst✝³ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝ : CommRing R'
⊢ ∀ [inst : CommRing S'] [inst_1 : Algebra R R'] [inst_2 : Algebra S S'] [inst_3 : IsLocalization.Away r R']
    [inst_4 : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (IsLocalization.Away.map R' S' f r)

Tactic:
_

Goal state after:
case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtTarget P
inst✝⁴ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝¹ : CommRing R'
inst✝ : CommRing S'
⊢ ∀ [inst : Algebra R R'] [inst_1 : Algebra S S'] [inst_2 : IsLocalization.Away r R']
    [inst_3 : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (IsLocalization.Away.map R' S' f r)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
H : ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n
q : Ideal R
hq : q.IsPrime
e : q < p
⊢ (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n

Tactic:
_

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
H : ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n
q : Ideal R
hq : q.IsPrime
e : q < p
a✝ : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p
⊢ q.height < ↑n
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtTarget P
inst✝⁴ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝¹ : CommRing R'
inst✝ : CommRing S'
⊢ ∀ [inst : Algebra R R'] [inst_1 : Algebra S S'] [inst_2 : IsLocalization.Away r R']
    [inst_3 : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (IsLocalization.Away.map R' S' f r)

Tactic:
_

Goal state after:
case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁶ : IsZariskiLocalAtTarget P
inst✝⁵ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R R'
⊢ ∀ [inst : Algebra S S'] [inst_1 : IsLocalization.Away r R'] [inst_2 : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (IsLocalization.Away.map R' S' f r)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁶ : IsZariskiLocalAtTarget P
inst✝⁵ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R R'
⊢ ∀ [inst : Algebra S S'] [inst_1 : IsLocalization.Away r R'] [inst_2 : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (IsLocalization.Away.map R' S' f r)

Tactic:
_

Goal state after:
case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁷ : IsZariskiLocalAtTarget P
inst✝⁶ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝³ : CommRing R'
inst✝² : CommRing S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
⊢ ∀ [inst : IsLocalization.Away r R'] [inst_1 : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (IsLocalization.Away.map R' S' f r)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁷ : IsZariskiLocalAtTarget P
inst✝⁶ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝³ : CommRing R'
inst✝² : CommRing S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
⊢ ∀ [inst : IsLocalization.Away r R'] [inst_1 : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (IsLocalization.Away.map R' S' f r)

Tactic:
_

Goal state after:
case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁸ : IsZariskiLocalAtTarget P
inst✝⁷ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R R'
inst✝¹ : Algebra S S'
inst✝ : IsLocalization.Away r R'
⊢ ∀ [inst : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (IsLocalization.Away.map R' S' f r)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁸ : IsZariskiLocalAtTarget P
inst✝⁷ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R R'
inst✝¹ : Algebra S S'
inst✝ : IsLocalization.Away r R'
⊢ ∀ [inst : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (IsLocalization.Away.map R' S' f r)

Tactic:
_

Goal state after:
case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝⁹ : IsZariskiLocalAtTarget P
inst✝⁸ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
⊢ (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (IsLocalization.Away.map R' S' f r)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case ofLocalizationSpanTarget
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f)))
            ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f

Tactic:
_

Goal state after:
case ofLocalizationSpanTarget
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
inst✝¹ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] (f : R →+* S) (s : Set S),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f)))
            ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case ofLocalizationSpanTarget
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
inst✝¹ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] (f : R →+* S) (s : Set S),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f)))
            ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f

Tactic:
_

Goal state after:
case ofLocalizationSpanTarget
P : MorphismProperty Scheme
inst✝³ : IsZariskiLocalAtTarget P
inst✝² : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (f : R →+* S) (s : Set S),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f)))
            ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set R),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (Localization.awayMap f ↑r)) →
        (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f

Tactic:
_

Goal state after:
case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
inst✝¹ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] (f : R →+* S) (s : Set R),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (Localization.awayMap f ↑r)) →
        (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
inst✝¹ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] (f : R →+* S) (s : Set R),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (Localization.awayMap f ↑r)) →
        (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f

Tactic:
_

Goal state after:
case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝³ : IsZariskiLocalAtTarget P
inst✝² : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (f : R →+* S) (s : Set R),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (Localization.awayMap f ↑r)) →
        (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra S T] (s : S)
    [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) ((algebraMap S T).comp f)

Tactic:
_

Goal state after:
case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
inst✝¹ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] [inst_1 : CommRing T] [inst_2 : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) ((algebraMap S T).comp f)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
inst✝¹ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] [inst_1 : CommRing T] [inst_2 : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) ((algebraMap S T).comp f)

Tactic:
_

Goal state after:
case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝³ : IsZariskiLocalAtTarget P
inst✝² : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ [inst : CommRing T] [inst_1 : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) ((algebraMap S T).comp f)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝³ : IsZariskiLocalAtTarget P
inst✝² : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ [inst : CommRing T] [inst_1 : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) ((algebraMap S T).comp f)

Tactic:
_

Goal state after:
case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝⁴ : IsZariskiLocalAtTarget P
inst✝³ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
⊢ ∀ [inst : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) ((algebraMap S T).comp f)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝⁴ : IsZariskiLocalAtTarget P
inst✝³ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
⊢ ∀ [inst : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) ((algebraMap S T).comp f)

Tactic:
_

Goal state after:
case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtTarget P
inst✝⁴ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
⊢ ∀ (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) ((algebraMap S T).comp f)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtTarget P
inst✝⁴ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
r : S
⊢ ∀ [IsLocalization.Away r T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) ((algebraMap S T).comp f)

Tactic:
_

Goal state after:
case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝⁶ : IsZariskiLocalAtTarget P
inst✝⁵ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
r : S
inst✝ : IsLocalization.Away r T
⊢ ∀ (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) ((algebraMap S T).comp f)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
S R : CommRingCat
φ : S ⟶ R
⊢ P (Spec.map φ) ↔ Q (Spec.map φ)

Tactic:
rw [HasRingHomProperty.Spec_iff (P := Q)]

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
S R : CommRingCat
φ : S ⟶ R
⊢ P (Spec.map φ) ↔ P (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom φ)))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X Y S : Scheme
⊢ ∀ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (pullback.fst f g)

Tactic:
_

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X Y S : Scheme
inst✝ : IsAffine S
⊢ ∀ [inst : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (pullback.fst f g)