awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (∀ (i : X.affineCover.I₀), P (X.affineCover.f i ≫ f)) ↔ ∀ (i : X.affineCover.I₀), Q (X.affineCover.f i ≫ f)

Tactic:
forall_congr' fun _ ↦ this _ ⟨_, rfl⟩

Premises used: CategoryTheory.PreZeroHypercover.f, Exists.intro, CategoryTheory.CategoryStruct.comp, forall_congr', AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, 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 : 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
⊢ (∀ (i : X.affineCover.I₀), P (X.affineCover.f i ≫ f)) ↔ ∀ (i : X.affineCover.I₀), Q (X.affineCover.f i ≫ f)

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))
S : CommRingCat
X : Scheme
f : X ⟶ Spec S
hX : ∃ (R : CommRingCat.{u}), X = Spec R
obtain : ∀ (R : CommRingCat.{u}) (f : Spec R ⟶ Spec S), P f ↔ Q f
⊢ P f ↔ Q f

Tactic:
obtain ⟨R, rfl⟩ := hX

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))
S R : CommRingCat
f : Spec R ⟶ Spec S
⊢ ∃ (φ : S ⟶ R), Spec.map φ = f

Tactic:
⟨_, Spec.map_preimage _⟩

Premises used: Exists.intro, AlgebraicGeometry.Spec.map_preimage
-- 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))
S R : CommRingCat
f : Spec R ⟶ Spec S
obtain : ∀ (φ : S ⟶ R), P (Spec.map φ) ↔ Q (Spec.map φ)
⊢ P f ↔ Q f

Tactic:
obtain ⟨φ, rfl⟩ : ∃ φ, Spec.map φ = f := ⟨_, Spec.map_preimage _⟩

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))
S R : CommRingCat
φ : S ⟶ R
rw : P (Spec.map φ) ↔ P (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom φ)))
⊢ P (Spec.map φ) ↔ Q (Spec.map φ)

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

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- 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))
S R : CommRingCat
φ : S ⟶ R
⊢ P (Spec.map φ) ↔ P (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom φ)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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'
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
⊢ P ⊓ P' = 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']

Premises used: AlgebraicGeometry.HasRingHomProperty.eq_affineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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'
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
⊢ ((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:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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
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))
⊢ 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

Tactic:
simp_rw [affineLocally_iff_affineOpens_le]

Premises used: AlgebraicGeometry.affineLocally_iff_affineOpens_le
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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
⊢ ((∀ (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:
grind
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso @P
⊢ IsZariskiLocalAtTarget.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)

Tactic:
have := stalkwiseIsZariskiLocalAtTarget_of_respectsIso hP
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso @P
this : IsZariskiLocalAtTarget.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
⊢ IsZariskiLocalAtSource.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)

Tactic:
have := stalkwise_isZariskiLocalAtSource_of_respectsIso hP
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso @P
this_1 : IsZariskiLocalAtTarget.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
this : IsZariskiLocalAtSource.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
⊢ HasRingHomProperty.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
    fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
    AlgebraicGeometry.stalkwise (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P) (Spec.map (CommRingCat.ofHom f))

Tactic:
of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget (P := AlgebraicGeometry.stalkwise P)

Premises used: AlgebraicGeometry.stalkwise, AlgebraicGeometry.HasRingHomProperty.of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso @P
this_1 : IsZariskiLocalAtTarget.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
this : IsZariskiLocalAtSource.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
h :
  ∀ (R S : Type u_1) (x : CommRing R) (x_1 : CommRing S) (φ : R →+* S),
    (∀ (p : Ideal S) (x_2 : p.IsPrime),
        P (R := Localization.AtPrime (Ideal.comap φ p)) (S := Localization.AtPrime p)
          (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)) ↔
      AlgebraicGeometry.stalkwise (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P) (Spec.map (CommRingCat.ofHom φ))
⊢ HasRingHomProperty.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
    fun {x S : Type u_1} {x_1 : CommRing x} {x_2 : CommRing S} (φ : x →+* S) ↦
    ∀ (p : Ideal S) (x_3 : p.IsPrime),
      P (R := Localization.AtPrime (Ideal.comap φ p)) (S := Localization.AtPrime p)
        (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)

Tactic:
convert!
    of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget (P := AlgebraicGeometry.stalkwise P) with R
    S _ _ φ

Premises used: AlgebraicGeometry.stalkwise, AlgebraicGeometry.HasRingHomProperty.of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso @P
this_1 : IsZariskiLocalAtTarget.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
this : IsZariskiLocalAtSource.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
R S : Type u_1
x : CommRing R
x_1 : CommRing S
φ : R →+* S
⊢ (∀ (p : Ideal S) (x_2 : p.IsPrime),
      P (R := Localization.AtPrime (Ideal.comap φ p)) (S := Localization.AtPrime p)
        (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)) ↔
    AlgebraicGeometry.stalkwise (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P) (Spec.map (CommRingCat.ofHom φ))

Tactic:
(stalkwise_SpecMap_iff hP (CommRingCat.ofHom φ)).symm

Premises used: AlgebraicGeometry.stalkwise_SpecMap_iff, CommRingCat.ofHom, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso @P
this_1 : IsZariskiLocalAtTarget.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
this : IsZariskiLocalAtSource.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
R S : Type u_1
x : CommRing R
x_1 : CommRing S
φ : R →+* S
⊢ (∀ (p : Ideal S) (x_2 : p.IsPrime),
      P (R := Localization.AtPrime (Ideal.comap φ p)) (S := Localization.AtPrime p)
        (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)) ↔
    AlgebraicGeometry.stalkwise (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P) (Spec.map (CommRingCat.ofHom φ))

Tactic:
exact (stalkwise_SpecMap_iff hP (CommRingCat.ofHom φ)).symm

Premises used: AlgebraicGeometry.stalkwise_SpecMap_iff, CommRingCat.ofHom, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
inr :
  ∀ (this : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g))
    (hZ : ¬IsAffine Z), P (f ≫ g)
wlog : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
⊢ P (f ≫ g)

Tactic:
wlog hZ : IsAffine Z generalizing X Y Z

Premises used: AlgebraicGeometry.IsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
hZ : ¬IsAffine Z
inr : ∀ (i : (↑Z.affineOpens : Type u)), P (X := (↑((f ≫ g) ⁻¹ᵁ (↑i : Z.Opens)) : Scheme)) ((f ≫ g) ∣_ (↑i : Z.Opens))
⊢ P (f ≫ g)

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

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
hZ : ¬IsAffine Z
U : (↑Z.affineOpens : Type u)
inr : P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens) ≫ g ∣_ (↑U : Z.Opens))
⊢ P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) ((f ≫ g) ∣_ (↑U : Z.Opens))

Tactic:
rw [morphismRestrict_comp]

Premises used: AlgebraicGeometry.morphismRestrict_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
hZ : ¬IsAffine Z
U : (↑Z.affineOpens : Type u)
⊢ P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens) ≫ g ∣_ (↑U : Z.Opens))

Tactic:
this _ _ (IsZariskiLocalAtTarget.restrict hf _)
        (IsZariskiLocalAtTarget.restrict hg _) U.2

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, Set.Mem, setOf, Set.preimage, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
hZ : ¬IsAffine Z
U : (↑Z.affineOpens : Type u)
⊢ P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens) ≫ g ∣_ (↑U : Z.Opens))

Tactic:
exact this _ _ (IsZariskiLocalAtTarget.restrict hf _)
        (IsZariskiLocalAtTarget.restrict hg _) U.2

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
inr :
  ∀ (this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hY : IsAffine Y), P (f ≫ g))
    (hY : ¬IsAffine Y), P (f ≫ g)
wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hY : IsAffine Y), P (f ≫ g)
⊢ P (f ≫ g)

Tactic:
wlog hY : IsAffine Y generalizing X Y

Premises used: AlgebraicGeometry.IsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hY : IsAffine Y), P (f ≫ g)
hY : ¬IsAffine Y
inr :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    P ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i ≫ f ≫ g)
⊢ P (f ≫ g)

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (Y.affineCover.pullback₁ f)]

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hY : IsAffine Y), P (f ≫ g)
hY : ¬IsAffine Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
inr :
  P (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i ≫ Y.affineCover.f i ≫ g :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Z)
⊢ P ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i ≫ f ≫ g)

Tactic:
rw [← Scheme.Cover.pullbackHom_map_assoc]

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom_map_assoc
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hY : IsAffine Y), P (f ≫ g)
hY : ¬IsAffine Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
⊢ P (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i ≫ Y.affineCover.f i ≫ g :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Z)

Tactic:
this _ _ (IsZariskiLocalAtTarget.of_isPullback (.of_hasPullback _ _) hf)
        (comp_of_isOpenImmersion _ _ _ hg) inferInstance

Premises used: AlgebraicGeometry.HasRingHomProperty.comp_of_isOpenImmersion, inferInstance, AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hY : IsAffine Y), P (f ≫ g)
hY : ¬IsAffine Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
⊢ P (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i ≫ Y.affineCover.f i ≫ g :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Z)

Tactic:
exact this _ _ (IsZariskiLocalAtTarget.of_isPullback (.of_hasPullback _ _) hf)
        (comp_of_isOpenImmersion _ _ _ hg) inferInstance

Premises used: AlgebraicGeometry.HasRingHomProperty.comp_of_isOpenImmersion, inferInstance, AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hY : IsAffine Y
inr : ∀ (this : ∀ {X : Scheme.{u}} (f : X ⟶ Y) (hf : P f) (hX : IsAffine X), P (f ≫ g)) (hX : ¬IsAffine X), P (f ≫ g)
wlog : ∀ {X : Scheme.{u}} (f : X ⟶ Y) (hf : P f) (hX : IsAffine X), P (f ≫ g)
⊢ P (f ≫ g)

Tactic:
wlog hX : IsAffine X generalizing X

Premises used: AlgebraicGeometry.IsAffine