awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
| U.ι ''ᵁ ⊤
have rw : sSup Us
Tactic: rw [Scheme.Hom.image_top_eq_opensRange, Scheme.Opens.opensRange_ι, heq]
-- 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 : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
⊢ ⨆ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens) = U.ι ''ᵁ ⊤
have inr : ⨆ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens) = sSup Us
Tactic: conv_rhs => rw [Scheme.Hom.image_top_eq_opensRange, Scheme.Opens.opensRange_ι, heq]
-- 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 : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
⊢ ⨆ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens) = sSup Us
have inr : (↑(⨆ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens)) : Set ↥Y) = (↑(sSup Us) : Set ↥Y)
Tactic: ext : 1
-- 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 : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
⊢ (↑(⨆ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens)) : Set ↥Y) = (↑(sSup Us) : Set ↥Y)
have this₁ : ∀ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens) = (↑i : Y.Opens)
Tactic: have (i : Us) : U ⊓ i.1 = i.1 := by simp [heq, le_sSup i.property]
-- 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 : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
⊢ P (f ≫ U.ι)
have obtain : ∀ (a : (↑Γ(Y, ⊤) : Type u)) (f : X ⟶ (↑(Y.basicOpen a) : Scheme)) (hf : P f), P (f ≫ (Y.basicOpen a).ι)
Tactic: obtain ⟨a, rfl⟩ := hYa
Cleared hypotheses: U, f, hf, hYa
-- 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 : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
a : (↑Γ(Y, ⊤) : Type u)
f : X ⟶ (↑(Y.basicOpen a) : Scheme)
hf : P f
⊢ P (f ≫ (Y.basicOpen a).ι)
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} [IsAffine Y] (a : (↑Γ(Y, ⊤) : Type u)) (f : X ⟶ (↑(Y.basicOpen a) : Scheme)) (hf : P f)
      (hX : IsAffine X), P (f ≫ (Y.basicOpen a).ι))
  (hX : ¬IsAffine X), P (f ≫ (Y.basicOpen a).ι)
Tactic: wlog hX : IsAffine X 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_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
a : (↑Γ(Y, ⊤) : Type u)
f : X ⟶ (↑(Y.basicOpen a) : Scheme)
hf : P f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} [IsAffine Y] (a : (↑Γ(Y, ⊤) : Type u)) (f : X ⟶ (↑(Y.basicOpen a) : Scheme)) (hf : P f)
        (hX : IsAffine X), P (f ≫ (Y.basicOpen a).ι))
    (hX : ¬IsAffine X), P (f ≫ (Y.basicOpen a).ι)
⊢ P (f ≫ (Y.basicOpen a).ι)
have wlog : ∀ {X Y : Scheme.{u}} [IsAffine Y] (a : (↑Γ(Y, ⊤) : Type u)) (f : X ⟶ (↑(Y.basicOpen a) : Scheme)) (hf : P f)
  (hX : IsAffine X), P (f ≫ (Y.basicOpen a).ι)
Tactic: wlog hX : IsAffine X generalizing X Y
Cleared hypotheses: X, Y, inst_1, a, f, hf
-- 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 : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
a : (↑Γ(Y, ⊤) : Type u)
f : X ⟶ (↑(Y.basicOpen a) : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] (a : (↑Γ(Y, ⊤) : Type u)) (f : X ⟶ (↑(Y.basicOpen a) : Scheme)) (hf : P f)
    (hX : IsAffine X), P (f ≫ (Y.basicOpen a).ι)
hX : ¬IsAffine X
⊢ P (f ≫ (Y.basicOpen a).ι)
have inr : ∀ (i : (↑X.affineOpens : Type u)), P ((↑i : X.Opens).ι ≫ f ≫ (Y.basicOpen a).ι)
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_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
a : (↑Γ(Y, ⊤) : Type u)
f : X ⟶ (↑(Y.basicOpen a) : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] (a : (↑Γ(Y, ⊤) : Type u)) (f : X ⟶ (↑(Y.basicOpen a) : Scheme)) (hf : P f)
    (hX : IsAffine X), P (f ≫ (Y.basicOpen a).ι)
hX : ¬IsAffine X
V : (↑X.affineOpens : Type u)
⊢ P ((↑V : X.Opens).ι ≫ f ≫ (Y.basicOpen a).ι)
have inr : P (((↑V : X.Opens).ι ≫ f) ≫ (Y.basicOpen a).ι)
Tactic: rw [← Category.assoc]
-- 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 : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
a : (↑Γ(Y, ⊤) : Type u)
f : X ⟶ (↑(Y.basicOpen a) : Scheme)
hf : P f
hX : IsAffine X
⊢ P (f ≫ (Y.basicOpen a).ι)
have rw : ∀ (hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))) (hX : IsAffine X),
  Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ≫ (Y.basicOpen a).ι)))
Tactic: rw [HasRingHomProperty.iff_of_isAffine (P := P)] at hf ⊢
Cleared hypotheses: hf, 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
⊢ P (f ≫ i)
have inr : ∀
  (this :
    ∀ {X Y Z : Scheme.{u}} (i : Y ⟶ Z) (hi : IsOpenImmersion i) (f : X ⟶ Y) (hf : P f) (hZ : IsAffine Z), P (f ≫ i))
  (hZ : ¬IsAffine Z), P (f ≫ i)
Tactic: wlog hZ : IsAffine Z generalizing X Y Z
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
inr :
  ∀
    (this :
      ∀ {X Y Z : Scheme.{u}} (i : Y ⟶ Z) (hi : IsOpenImmersion i) (f : X ⟶ Y) (hf : P f) (hZ : IsAffine Z), P (f ≫ i))
    (hZ : ¬IsAffine Z), P (f ≫ i)
⊢ P (f ≫ i)
have wlog : ∀ {X Y Z : Scheme.{u}} (i : Y ⟶ Z) (hi : IsOpenImmersion i) (f : X ⟶ Y) (hf : P f) (hZ : IsAffine Z), P (f ≫ i)
Tactic: wlog hZ : IsAffine Z generalizing X Y Z
Cleared hypotheses: X, Y, Z, i, hi, f, hf
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme.{u}} (i : Y ⟶ Z) (hi : IsOpenImmersion i) (f : X ⟶ Y) (hf : P f) (hZ : IsAffine Z), P (f ≫ i)
hZ : ¬IsAffine Z
⊢ P (f ≫ i)
have inr : ∀ (i_1 : (↑Z.affineOpens : Type u)), P (X := (↑((f ≫ i) ⁻¹ᵁ (↑i_1 : Z.Opens)) : Scheme)) ((f ≫ i) ∣_ (↑i_1 : Z.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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme.{u}} (i : Y ⟶ Z) (hi : IsOpenImmersion i) (f : X ⟶ Y) (hf : P f) (hZ : IsAffine Z), P (f ≫ i)
hZ : ¬IsAffine Z
U : (↑Z.affineOpens : Type u)
⊢ P (X := (↑((f ≫ i) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) ((f ≫ i) ∣_ (↑U : Z.Opens))
have inr : P (X := (↑((f ≫ i) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ i ⁻¹ᵁ (↑U : Z.Opens) ≫ i ∣_ (↑U : Z.Opens))
Tactic: rw [morphismRestrict_comp]
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
e : Y ≅ (↑(Scheme.Hom.opensRange i) : Scheme) := IsOpenImmersion.isoOfRangeEq i (Scheme.Hom.opensRange i).ι ⋯
⊢ P (f ≫ i)
have rw : P ((f ≫ e.hom) ≫ (Scheme.Hom.opensRange i).ι)
Tactic: rw [show f ≫ i = f ≫ e.hom ≫ i.opensRange.ι by simp [e], ← Category.assoc]
-- 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
⊢ 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 : P.Respects IsOpenImmersion
Tactic: have := respects_isOpenImmersion (P := P)
    (RingHom.locally_stableUnderCompositionWithLocalizationAwaySource hQ)
-- 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
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
⊢ 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 refine_1 : ∀ (hf : 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))
Tactic: refine ⟨fun hf x ↦ ?_,
      fun hf ↦ (IsZariskiLocalAtSource.iff_exists_resLE (P := P)).mpr <| fun x ↦ ?_⟩
-- 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
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
refine_1 :
  ∀ (hf : 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 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 refine_2 : ∀
  (hf :
    ∀ (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.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)
Tactic: refine ⟨fun hf x ↦ ?_,
      fun hf ↦ (IsZariskiLocalAtSource.iff_exists_resLE (P := P)).mpr <| fun x ↦ ?_⟩
-- 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
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 : 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 refine_1 : ∀ (U : Opens ↥Y) (hU : U ∈ Y.affineOpens) (hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)),
  U ≤ ⊤ →
    ∃ (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: obtain ⟨U, hU, hfx, _⟩ := Opens.isBasis_iff_nbhd.mp Y.isBasis_affineOpens
      (Opens.mem_top <| f x)
-- 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
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 : P f
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
⊢ ∃ (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 refine_1 : ∀ (V : Opens ↥X) (hV : V ∈ X.affineOpens) (hx : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
  ∃ (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: obtain ⟨V, hV, hx, e⟩ := Opens.isBasis_iff_nbhd.mp X.isBasis_affineOpens
      (show x ∈ f ⁻¹ᵁ U from hfx)
-- 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 : P f
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
⊢ ∃ (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 hf₁ : ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
  ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
    Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
    ∀ t ∈ s,
      ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
        [IsLocalization.Away t Sₜ],
        Q
          (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
            (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
Tactic: simp_rw [HasRingHomProperty.iff_appLE (P := P), locally_iff_isLocalization hQi] at hf
Cleared hypotheses: hf
-- 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
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
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
⊢ ∃ (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 refine_1 : ∀ (s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u))
  (hs :
    Eq (α := Ideal (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u))
      (Ideal.span (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u))) ⊤)
  (hfs :
    ∀ t ∈ s,
      ∀ (Sₜ : Type u) [inst : CommRing Sₜ]
        [inst_1 :
          Algebra (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ]
        [IsLocalization.Away t Sₜ],
        Q
          (comp
            (algebraMap (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
              Sₜ)
            (CommRingCat.Hom.hom
              (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
                (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens) e)))),
  ∃ (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: obtain ⟨s, hs, hfs⟩ := hf ⟨U, hU⟩ ⟨V, hV⟩ e