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
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)))
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))
have hs₁ : ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
  (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
Tactic: apply iSup_basicOpen_of_span_eq_top at hs
Cleared hypotheses: hs
-- 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
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)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) 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)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
⊢ ∃ (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₁ : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x
Tactic: have : x ∈ (⨆ i ∈ s, X.basicOpen i) := hs.symm ▸ hx
-- 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_1 : 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)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) 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)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
this : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) 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₁ : ∃ r ∈ s, x ∈ X.basicOpen r
Tactic: have : ∃ r ∈ s, x ∈ X.basicOpen r := by simpa using this
-- 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_1 : 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)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) 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)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
this_2 : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x
this : ∃ r ∈ s, x ∈ X.basicOpen r
⊢ ∃ (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 : ∀ (r : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)) (hr : r ∈ s)
  (hrs : x ∈ X.basicOpen r),
  ∃ (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 ⟨r, hr, hrs⟩ := this
Cleared hypotheses: this
-- 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_1 : 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)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) 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)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
this : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x
r : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hr : r ∈ s
hrs : x ∈ X.basicOpen r
⊢ ∃ (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 : Q
  (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) (X.basicOpen r) sorry) : X.Opens) sorry))
Tactic: refine ⟨⟨U, hU⟩, ⟨X.basicOpen r, hV.basicOpen r⟩, hrs, (X.basicOpen_le r).trans e, ?_⟩
-- 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_1 : 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)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) 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)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
this : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x
r : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hr : r ∈ s
hrs : x ∈ X.basicOpen r
⊢ Q
    (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) (X.basicOpen r) ⋯) : X.Opens) ⋯))
have refine_1 : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (homOfLE sorry).op))
Tactic: rw [← f.appLE_map e (homOfLE (X.basicOpen_le r)).op]
-- 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_1 : 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)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) 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)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
this : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x
r : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hr : r ∈ s
hrs : x ∈ X.basicOpen r
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (homOfLE ⋯).op))
have refine_1 : ∀ (this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)),
  Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (homOfLE sorry).op))
Tactic: haveI : IsLocalization.Away r Γ(X, X.basicOpen r) := hV.isLocalization_basicOpen r
-- 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 :
  ∀ (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)
have refine_2 : ∀ (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.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))),
  ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)
Tactic: obtain ⟨U, V, hxV, e, hf⟩ := hf 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_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.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
⊢ ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)
have h : P (Scheme.Hom.resLE f (↑U : Y.Opens) (↑V : X.Opens) e)
Tactic: use U, V, hxV, e
-- 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_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.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
⊢ P (Scheme.Hom.resLE f (↑U : Y.Opens) (↑V : X.Opens) e)
have h : 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)))
Tactic: simp only [iff_of_isAffine (P := P), Scheme.Hom.appLE, homOfLE_leOfHom] at hf ⊢