awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
⊢ RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
have hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
Tactic: have hP : RingHom.RespectsIso (fun f ↦ P (Spec.map (CommRingCat.ofHom f))) :=
    RingHom.toMorphismProperty_respectsIso_iff.mpr
      (inferInstanceAs (P.inverseImage Scheme.Spec).unop.RespectsIso)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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))
⊢ RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
have localizationAwayPreserves : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
  P (Spec.map (CommRingCat.ofHom f))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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))
localizationAwayPreserves :
  RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
have ofLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
  P (Spec.map (CommRingCat.ofHom f))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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))
localizationAwayPreserves :
  RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
ofLocalizationSpanTarget :
  RingHom.OfLocalizationSpanTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
have ofLocalizationSpan : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
  P (Spec.map (CommRingCat.ofHom f))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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))
localizationAwayPreserves :
  RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
ofLocalizationSpanTarget :
  RingHom.OfLocalizationSpanTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
ofLocalizationSpan :
  RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    P (Spec.map (CommRingCat.ofHom f))
have StableUnderCompositionWithLocalizationAwayTarget : RingHom.StableUnderCompositionWithLocalizationAwayTarget.{u}
  fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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)))
have localizationAwayPreserves : P (Spec.map (CommRingCat.ofHom (Localization.awayMap f r)))
Tactic: refine (RingHom.RespectsIso.isLocalization_away_iff hP ..).mp ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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)
⊢ P (Spec.map (CommRingCat.ofHom f))
have ofLocalizationSpanTarget : ∀ (i : (Scheme.affineOpenCoverOfSpanRangeEqTop (fun (i : (↑s : Type u)) ↦ (↑i : S)) sorry).openCover.I₀),
  P
    ((Scheme.affineOpenCoverOfSpanRangeEqTop (fun (i : (↑s : Type u)) ↦ (↑i : S)) sorry).openCover.f i ≫
      Spec.map (CommRingCat.ofHom f))
Tactic: apply IsZariskiLocalAtSource.of_openCover (Scheme.affineOpenCoverOfSpanRangeEqTop
      (fun i : s ↦ (i : S)) (by simpa)).openCover
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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
    ((Scheme.affineOpenCoverOfSpanRangeEqTop (fun (i : (↑s : Type u)) ↦ (↑i : S)) ⋯).openCover.f i ≫
      Spec.map (CommRingCat.ofHom f))
have ofLocalizationSpanTarget : P (X :=
  Spec ((Scheme.affineOpenCoverOfSpanRangeEqTop (fun (i : (↑s : Type u)) ↦ (↑i : S)) sorry).X (P := IsOpenImmersion) i))
  (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap S (Localization.Away (↑i : S)))))
Tactic: simp only [CommRingCat.coe_of, Scheme.AffineOpenCover.openCover_X, ← Spec.map_comp,
      Scheme.AffineOpenCover.openCover_f, Scheme.affineOpenCoverOfSpanRangeEqTop_f]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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 R
hs : Eq (α := Ideal R) (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 : R)) _ _ _ (Localization.awayMap f (↑r : R))
⊢ P (Spec.map (CommRingCat.ofHom f))
have ofLocalizationSpan : ∀ (i : (↑s : Type u)),
  P (X := (↑(Spec.map (CommRingCat.ofHom f) ⁻¹ᵁ basicOpen (↑i : R)) : Scheme))
    (Spec.map (CommRingCat.ofHom f) ∣_ basicOpen (↑i : R))
Tactic: apply IsZariskiLocalAtTarget.of_iSup_eq_top _ (PrimeSpectrum.iSup_basicOpen_eq_top_iff
      (f := fun i : s ↦ (i : R)).mpr (by simpa))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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 T : Type u
inst_2 : CommRing R
inst_3 : CommRing S
inst_4 : CommRing T
inst_5 : Algebra S T
r : S
inst_6 : IsLocalization.Away r T
f : R →+* S
hf : P (Spec.map (CommRingCat.ofHom f))
⊢ P (X := Spec (CommRingCat.of T)) (Spec.map (CommRingCat.ofHom (RingHom.comp (algebraMap S T) f)))
have StableUnderCompositionWithLocalizationAwayTarget : ∀
  (this :
    IsOpenImmersion (X := Spec (CommRingCat.of T)) (Y := Spec (CommRingCat.of S))
      (Spec.map (CommRingCat.ofHom (algebraMap S T)))),
  P (X := Spec (CommRingCat.of T)) (Spec.map (CommRingCat.ofHom (RingHom.comp (algebraMap S T) f)))
Tactic: have := AlgebraicGeometry.IsOpenImmersion.of_isLocalization (S := T) r
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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 T : Type u
inst_2 : CommRing R
inst_3 : CommRing S
inst_4 : CommRing T
inst_5 : Algebra S T
r : S
inst_6 : IsLocalization.Away r T
f : R →+* S
hf : P (Spec.map (CommRingCat.ofHom f))
this :
  IsOpenImmersion (X := Spec (CommRingCat.of T)) (Y := Spec (CommRingCat.of S))
    (Spec.map (CommRingCat.ofHom (algebraMap S T)))
⊢ P (X := Spec (CommRingCat.of T)) (Spec.map (CommRingCat.ofHom (RingHom.comp (algebraMap S T) f)))
have StableUnderCompositionWithLocalizationAwayTarget : P (X := Spec (CommRingCat.of T)) (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap S T)))
Tactic: change P (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap _ _)))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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 T : Type u
inst_2 : CommRing R
inst_3 : CommRing S
inst_4 : CommRing T
inst_5 : Algebra S T
r : S
inst_6 : IsLocalization.Away r T
f : R →+* S
hf : P (Spec.map (CommRingCat.ofHom f))
this :
  IsOpenImmersion (X := Spec (CommRingCat.of T)) (Y := Spec (CommRingCat.of S))
    (Spec.map (CommRingCat.ofHom (algebraMap S T)))
⊢ P (X := Spec (CommRingCat.of T)) (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap S T)))
have StableUnderCompositionWithLocalizationAwayTarget : P (X := Spec (CommRingCat.of T)) (Spec.map (CommRingCat.ofHom (algebraMap S T)) ≫ Spec.map (CommRingCat.ofHom f))
Tactic: rw [Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme :=
  affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ P = affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
have this : HasRingHomProperty Q fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
Tactic: have : HasRingHomProperty Q (fun f ↦ P (Spec.map (CommRingCat.ofHom f))) :=
      ⟨isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget P, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme :=
  affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
this :
  HasRingHomProperty Q fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ P = Q
have h : ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y), P f ↔ Q f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme :=
  affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
this :
  HasRingHomProperty Q fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔ Q f
have h : ∀ (this : ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), P f ↔ Q f)
  (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), P f ↔ Q f
Tactic: wlog hY : ∃ R, Y = Spec R generalizing X Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme :=
  affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
this :
  HasRingHomProperty Q fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
X Y : Scheme
f : X ⟶ Y
h :
  ∀ (this : ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), P f ↔ Q f)
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), P f ↔ Q f
⊢ P f ↔ Q f
have wlog : ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), P f ↔ Q f
Tactic: wlog hY : ∃ R, Y = Spec R generalizing X Y
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme :=
  affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
this_1 :
  HasRingHomProperty Q fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
X Y : Scheme
f : X ⟶ Y
this : ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), P f ↔ Q f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ P f ↔ Q f
have h : (∀ (i : Y.affineCover.toPreZeroHypercover.1),
    P (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)) ↔
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    Q (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
Tactic: rw [IsZariskiLocalAtTarget.iff_of_openCover (P := P) Y.affineCover,
        IsZariskiLocalAtTarget.iff_of_openCover (P := Q) Y.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme :=
  affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
this :
  HasRingHomProperty Q fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
X Y : Scheme
f : X ⟶ Y
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ P f ↔ Q f
have obtain : ∀ (S : CommRingCat.{u}) (f : X ⟶ Spec S), P f ↔ Q f
Tactic: obtain ⟨S, rfl⟩ := hY
Cleared hypotheses: Y, f, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme :=
  affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
this :
  HasRingHomProperty Q fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
⊢ P f ↔ Q f
have inr : ∀ (this : ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec S) (hX : ∃ (R : CommRingCat.{u}), X = Spec R), P f ↔ Q f)
  (hX : ¬∃ (R : CommRingCat.{u}), X = Spec R), P f ↔ Q f
Tactic: wlog hX : ∃ R, X = Spec R generalizing X
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme :=
  affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
this :
  HasRingHomProperty Q fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inr :
  ∀ (this : ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec S) (hX : ∃ (R : CommRingCat.{u}), X = Spec R), P f ↔ Q f)
    (hX : ¬∃ (R : CommRingCat.{u}), X = Spec R), P f ↔ Q f
⊢ P f ↔ Q f
have wlog : ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec S) (hX : ∃ (R : CommRingCat.{u}), X = Spec R), P f ↔ Q f
Tactic: wlog hX : ∃ R, X = Spec R generalizing X
Cleared hypotheses: X, f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme :=
  affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
this_1 :
  HasRingHomProperty Q fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
this : ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec S) (hX : ∃ (R : CommRingCat.{u}), X = Spec R), P f ↔ Q f
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
⊢ P f ↔ Q f
have inr : (∀ (i : X.affineCover.I₀), P (X.affineCover.f i ≫ f)) ↔ ∀ (i : X.affineCover.I₀), Q (X.affineCover.f i ≫ f)
Tactic: rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) X.affineCover,
        IsZariskiLocalAtSource.iff_of_openCover (P := Q) X.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme :=
  affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
this :
  HasRingHomProperty Q fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
S : CommRingCat
X : Scheme
f : X ⟶ Spec S
hX : ∃ (R : CommRingCat.{u}), X = Spec R
⊢ P f ↔ Q f
have obtain : ∀ (R : CommRingCat.{u}) (f : Spec R ⟶ Spec S), P f ↔ Q f
Tactic: obtain ⟨R, rfl⟩ := hX
Cleared hypotheses: X, f, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme :=
  affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
this :
  HasRingHomProperty Q fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
S R : CommRingCat
f : Spec R ⟶ Spec S
⊢ P f ↔ Q f
have obtain : ∀ (φ : S ⟶ R), P (Spec.map φ) ↔ Q (Spec.map φ)
Tactic: obtain ⟨φ, rfl⟩ : ∃ φ, Spec.map φ = f := ⟨_, Spec.map_preimage _⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme :=
  affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
this :
  HasRingHomProperty Q fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))
S R : CommRingCat
φ : S ⟶ R
⊢ P (Spec.map φ) ↔ Q (Spec.map φ)
have rw : P (Spec.map φ) ↔ P (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom φ)))
Tactic: rw [HasRingHomProperty.Spec_iff (P := Q)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst_1 : HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
⊢ P ⊓ P' = affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ Q f ∧ Q' f
have rw : ((affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊓
    affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q') =
  affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ Q f ∧ Q' f
Tactic: rw [HasRingHomProperty.eq_affineLocally P, HasRingHomProperty.eq_affineLocally P']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst_1 : HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
⊢ ((affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊓
      affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q') =
    affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ Q f ∧ Q' f
have h : ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y),
  ((affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊓
        affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q')
      f ↔
    affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ Q f ∧ Q' f) f
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst_1 : HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
X Y : Scheme
f : X ⟶ Y
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ∧
      affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q') f ↔
    affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ Q f ∧ Q' f) f
have h : ((∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))) ∧
    ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q' (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))) ↔
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)) ∧
      Q' (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
Tactic: simp_rw [affineLocally_iff_affineOpens_le]