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
inst_2 : CommRing R
ofLocalizationSpan :
  ∀ [inst : 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 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:
_
-- 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 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))
⊢ Eq.{u + 1} (α := Ideal R) (Ideal.span (Set.range fun (i : (↑s : Type u)) ↦ (↑i : R))) ⊤

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 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))
ofLocalizationSpan :
  ∀ (i : (↑s : Type u)),
    P (X := (↑(Spec.map (CommRingCat.ofHom f) ⁻¹ᵁ basicOpen (↑i : R)) : Scheme))
      (Spec.map (CommRingCat.ofHom f) ∣_ basicOpen (↑i : R))
⊢ P (Spec.map (CommRingCat.ofHom f))

Tactic:
apply IsZariskiLocalAtTarget.of_iSup_eq_top _ (PrimeSpectrum.iSup_basicOpen_eq_top_iff
      (f := fun i : s ↦ (i : R)).mpr (by simpa))

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_iSup_eq_top
-- 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 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))
i : (↑s : Type u)
⊢ P (X := (↑(Spec.map (CommRingCat.ofHom f) ⁻¹ᵁ basicOpen (↑i : R)) : Scheme))
    (Spec.map (CommRingCat.ofHom f) ∣_ basicOpen (↑i : R))

Tactic:
(MorphismProperty.arrow_mk_iso_iff P (SpecMapRestrictBasicOpenIso
      (CommRingCat.ofHom f) i.1)).mpr (H i)

Premises used: Iff.mpr, AlgebraicGeometry.SpecMapRestrictBasicOpenIso, CommRingCat.ofHom, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Subtype.val
-- 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 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))
i : (↑s : Type u)
⊢ P (X := (↑(Spec.map (CommRingCat.ofHom f) ⁻¹ᵁ basicOpen (↑i : R)) : Scheme))
    (Spec.map (CommRingCat.ofHom f) ∣_ basicOpen (↑i : R))

Tactic:
exact (MorphismProperty.arrow_mk_iso_iff P (SpecMapRestrictBasicOpenIso
      (CommRingCat.ofHom f) i.1)).mpr (H i)

Premises used: Iff.mpr, AlgebraicGeometry.SpecMapRestrictBasicOpenIso, CommRingCat.ofHom, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Subtype.val
-- 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 T : Type u
StableUnderCompositionWithLocalizationAwayTarget :
  ∀ [inst : CommRing R] [inst_2 : CommRing S] [inst_3 : CommRing T] [inst_4 : Algebra S T] (s : S)
    [IsLocalization.Away s T] (f : R →+* 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)))
        (RingHom.comp (algebraMap S T) f)
⊢ ∀ [inst : CommRing R] [inst_2 : CommRing S] [inst_3 : CommRing T] [inst_4 : Algebra S T] (s : S)
    [IsLocalization.Away s T] (f : R →+* 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)))
        (RingHom.comp (algebraMap S T) 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 T : Type u
inst_2 : CommRing R
StableUnderCompositionWithLocalizationAwayTarget :
  ∀ [inst : CommRing S] [inst_3 : CommRing T] [inst_4 : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* 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)))
        (RingHom.comp (algebraMap S T) f)
⊢ ∀ [inst : CommRing S] [inst_3 : CommRing T] [inst_4 : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* 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)))
        (RingHom.comp (algebraMap S T) 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 T : Type u
inst_2 : CommRing R
inst_3 : CommRing S
StableUnderCompositionWithLocalizationAwayTarget :
  ∀ [inst : CommRing T] [inst_4 : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* 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)))
        (RingHom.comp (algebraMap S T) f)
⊢ ∀ [inst : CommRing T] [inst_4 : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* 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)))
        (RingHom.comp (algebraMap S T) 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 T : Type u
inst_2 : CommRing R
inst_3 : CommRing S
inst_4 : CommRing T
StableUnderCompositionWithLocalizationAwayTarget :
  ∀ [inst : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* 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)))
        (RingHom.comp (algebraMap S T) f)
⊢ ∀ [inst : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* 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)))
        (RingHom.comp (algebraMap S T) 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 T : Type u
inst_2 : CommRing R
inst_3 : CommRing S
inst_4 : CommRing T
inst_5 : Algebra S T
r : S
StableUnderCompositionWithLocalizationAwayTarget :
  ∀ [IsLocalization.Away r T] (f : R →+* 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)))
        (RingHom.comp (algebraMap S T) f)
⊢ ∀ [IsLocalization.Away r T] (f : R →+* 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)))
        (RingHom.comp (algebraMap S T) 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 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))
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)))
⊢ 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
-- 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 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)))
StableUnderCompositionWithLocalizationAwayTarget :
  P (X := Spec (CommRingCat.of T)) (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap S T)))
⊢ P (X := Spec (CommRingCat.of T)) (Spec.map (CommRingCat.ofHom (RingHom.comp (algebraMap S T) f)))

Tactic:
change P (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap _ _)))

Premises used: Algebra.algebraMap, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, CategoryTheory.CategoryStruct.comp
-- 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 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)))
StableUnderCompositionWithLocalizationAwayTarget :
  P (X := Spec (CommRingCat.of T)) (Spec.map (CommRingCat.ofHom (algebraMap S T)) ≫ Spec.map (CommRingCat.ofHom f))
⊢ P (X := Spec (CommRingCat.of T)) (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap S T)))

Tactic:
rw [Spec.map_comp]

Premises used: AlgebraicGeometry.Spec.map_comp
-- 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 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 (algebraMap S T)) ≫ Spec.map (CommRingCat.ofHom f))

Tactic:
IsZariskiLocalAtSource.comp hf ..

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.comp
-- 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 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 (algebraMap S T)) ≫ Spec.map (CommRingCat.ofHom f))

Tactic:
exact IsZariskiLocalAtSource.comp hf ..

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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))
⊢ 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⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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))
change : P = Q
⊢ P = affineLocally fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P (Spec.map (CommRingCat.ofHom f))

Tactic:
change P = Q
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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))
h : ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y), P f ↔ Q f
⊢ P = Q

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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
wlog : ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), P f ↔ Q f
⊢ P f ↔ Q f

Tactic:
wlog hY : ∃ R, Y = Spec R generalizing X Y
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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
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)
⊢ P f ↔ Q f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := P) Y.affineCover,
        IsZariskiLocalAtTarget.iff_of_openCover (P := Q) Y.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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
⊢ (∀ (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:
forall_congr' fun _ ↦ this _ ⟨_, rfl⟩

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, Exists.intro, forall_congr', AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.Scheme.affineCover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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
⊢ (∀ (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:
refine forall_congr' fun _ ↦ this _ ⟨_, rfl⟩

Premises used: Exists.intro, forall_congr', rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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
obtain : ∀ (S : CommRingCat.{u}) (f : X ⟶ Spec S), P f ↔ Q f
⊢ P f ↔ Q f

Tactic:
obtain ⟨S, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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
wlog : ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec S) (hX : ∃ (R : CommRingCat.{u}), X = Spec R), P f ↔ Q f
⊢ P f ↔ Q f

Tactic:
wlog hX : ∃ R, X = Spec R generalizing X
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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
inr : (∀ (i : X.affineCover.I₀), P (X.affineCover.f i ≫ f)) ↔ ∀ (i : X.affineCover.I₀), Q (X.affineCover.f i ≫ f)
⊢ P f ↔ Q f

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) X.affineCover,
        IsZariskiLocalAtSource.iff_of_openCover (P := Q) X.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover