awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
hf_1 :
  ∀ (x : ↥X),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
x : ↥X
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
hxV : x ∈ (↑V : X.Opens)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f (↑U : Y.Opens) ≫ X.presheaf.map (homOfLE e).op))
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.resLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
have this₁ : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
Tactic: haveI : (toMorphismProperty (Locally Q)).RespectsIso := toMorphismProperty_respectsIso_iff.mp <|
      (isLocal_ringHomProperty P).respectsIso
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst inst₁ : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
have e : P = P
Tactic: apply @copy (P := P) (P' := P) (Q := Q) (Q' := Locally Q)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst inst₁ : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
e : P = P
⊢ HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
have e' : ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S),
  Q f ↔ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
Tactic: apply @copy (P := P) (P' := P) (Q := Q) (Q' := Locally Q)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ P f ↔
    ∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
have this : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
  Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Tactic: haveI : HasRingHomProperty P (Locally Q) := by
    apply @copy (P := P) (P' := P) (Q := Q) (Q' := Locally Q)
    · infer_instance
    · rfl
    · intro R S _ _ f
      exact (locally_iff_of_localizationSpanTarget (isLocal_ringHomProperty P).respectsIso
        (isLocal_ringHomProperty P).ofLocalizationSpanTarget _).symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ P f ↔
    ∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
have hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Tactic: rw [iff_exists_appLE_locally (P := P) hQ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQa : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↥X),
        ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
          (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
          Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
⊢ P =
    affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦
      Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
have this : HasRingHomProperty.{u}
  (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
  fun {R S : Type u} [CommRing R] [CommRing S] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Tactic: haveI : HasRingHomProperty (affineLocally (Locally Q)) (Locally Q) :=
      ⟨locally_propertyIsLocal hQl hQa, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQa : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↥X),
        ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
          (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
          Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
this :
  HasRingHomProperty.{u}
    (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦
      Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ P =
    affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦
      Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
have h₁ : ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y),
  P f ↔
    affineLocally
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQa : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↥X),
        ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
          (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
          Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
this :
  HasRingHomProperty.{u}
    (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦
      Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔
    affineLocally
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
have h₁ : (∀ (x : ↥X),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      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] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
Tactic: rw [h, iff_exists_appLE_locally (P := affineLocally (Locally Q)) hQa.left hQa.respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQa : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↥X),
        ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
          (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
          Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
this :
  HasRingHomProperty.{u}
    (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦
      Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
h₁ :
  (∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        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] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ P f ↔
    affineLocally
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
have h₂ : (∀ (x : ↥X),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))) ↔
  ∀ (x : ↥X),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
Tactic: rw [h, iff_exists_appLE_locally (P := affineLocally (Locally Q)) hQa.left hQa.respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ P f
have have : ∀ (hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q), P f
Tactic: have hQi := (HasRingHomProperty.isLocal_ringHomProperty P).respectsIso
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ P f
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
      (hY : IsAffine Y), P f)
  (hY : ¬IsAffine Y), P f
Tactic: wlog hY : IsAffine Y generalizing X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
        (hY : IsAffine Y), P f)
    (hY : ¬IsAffine Y), P f
⊢ P f
have wlog : ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hY : IsAffine Y),
  P f
Tactic: wlog hY : IsAffine Y generalizing X Y f
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
    (hY : IsAffine Y), P f
hY : ¬IsAffine Y
⊢ P f
have inr : ∀ (i : (↑Y.affineOpens : Type u)), P (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (f ∣_ (↑i : Y.Opens))
Tactic: rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
    (hY : IsAffine Y), P f
hY : ¬IsAffine Y
U : (↑Y.affineOpens : Type u)
⊢ P (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
have inr : ∀ (x : ↥(↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)),
  Q (R := (↑((↑(↑U : Y.Opens) : Scheme).presheaf.stalk ((f ∣_ (↑U : Y.Opens)) x)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ∣_ (↑U : Y.Opens)) x))
Tactic: refine this (fun x ↦ ?_) U.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
⊢ P f
have inr : ∀
  (this :
    ∀ {X : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
      (hX : IsAffine X), P f)
  (hX : ¬IsAffine X), P f
Tactic: wlog hX : IsAffine X generalizing X f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
        (hX : IsAffine X), P f)
    (hX : ¬IsAffine X), P f
⊢ P f
have wlog : ∀ {X : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X),
  P f
Tactic: wlog hX : IsAffine X generalizing X f
Cleared hypotheses: X, f, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this :
  ∀ {X : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X),
    P f
hX : ¬IsAffine X
⊢ P f
have inr : ∀ (i : (↑X.affineOpens : Type u)), P ((↑i : X.Opens).ι ≫ f)
Tactic: rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this :
  ∀ {X : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X),
    P f
hX : ¬IsAffine X
U : (↑X.affineOpens : Type u)
⊢ P ((↑U : X.Opens).ι ≫ f)
have inr : ∀ (x : ↥(↑(↑U : X.Opens) : Scheme)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap ((↑U : X.Opens).ι ≫ f) x))
Tactic: refine this ?_ U.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this :
  ∀ {X : Scheme.{u}} {f : X ⟶ Y} (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X),
    P f
hX : ¬IsAffine X
U : (↑X.affineOpens : Type u)
x : ↥(↑(↑U : X.Opens) : Scheme)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap ((↑U : X.Opens).ι ≫ f) x))
have inr : Q (R := (↑(Y.presheaf.stalk (((↑U : X.Opens).ι ≫ f) x)) : Type u))
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f ((↑U : X.Opens).ι x)))
Tactic: rw [Scheme.Hom.stalkMap_comp, CommRingCat.hom_comp, hQi.cancel_right_isIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
⊢ P f
have inr : ∀
  (this :
    ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
      (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
      (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f)
  (hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
Tactic: wlog hXY : ∃ R S, Y = Spec R ∧ X = Spec S generalizing X Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
inr :
  ∀
    (this :
      ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
        (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
        (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f)
    (hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
⊢ P f
have wlog : ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
  (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
  (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
Tactic: wlog hXY : ∃ R S, Y = Spec R ∧ X = Spec S generalizing X Y
Cleared hypotheses: Y, hY, X, f, H, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
⊢ P f
have inr : P (f ≫ Y.isoSpec.hom)
Tactic: rw [← P.cancel_right_of_respectsIso (g := Y.isoSpec.hom)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
⊢ P (f ≫ Y.isoSpec.hom)
have inr : P (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom)
Tactic: rw [← P.cancel_left_of_respectsIso (f := X.isoSpec.inv)]