awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : (↑Y.affineOpens : Type u)
V₁ V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ (↑V₁ : X.Opens)
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) (↑U₁ : Y.Opens) (f x : ↥Y)
r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)
r' : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) (f x : ↥Y)
ha :
  IsAffineOpen
    (X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r'))
hxa :
  x ∈
    X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r')
s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)
s' :
  (↑Γ(X,
        X.basicOpen (U := (↑V₂ : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
              (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
            r')) :
    Type u)
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
⊢ ∃ (r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)) (s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)) (_ : x ∈ X.basicOpen s) (e :
    X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r), P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))
have this : IsLocalization.Away (R := (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
        (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
      r' :
    (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
  (↑Γ(X,
        X.basicOpen (U := (↑V₂ : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
              (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
            r')) :
    Type u)
Tactic: haveI := V₂.2.isLocalization_basicOpen (f.appLE U₂ V₂ e₂ r')
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : (↑Y.affineOpens : Type u)
V₁ V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ (↑V₁ : X.Opens)
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) (↑U₁ : Y.Opens) (f x : ↥Y)
r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)
r' : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) (f x : ↥Y)
ha :
  IsAffineOpen
    (X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r'))
hxa :
  x ∈
    X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r')
s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)
s' :
  (↑Γ(X,
        X.basicOpen (U := (↑V₂ : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
              (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
            r')) :
    Type u)
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this_1 :
  IsLocalization.Away (R := (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r' :
      (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
    (↑Γ(X,
          X.basicOpen (U := (↑V₂ : X.Opens))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
                (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
              r')) :
      Type u)
this_2 : IsLocalization.Away r' (↑Γ(Y, Y.basicOpen r') : Type u)
this : IsLocalization.Away s' (↑Γ(X, X.basicOpen s') : Type u)
⊢ X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
have rw : X.basicOpen s' ≤ f ⁻¹ᵁ Y.basicOpen r'
Tactic: rw [hBss', hBrr']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ : Y.Opens
U₂ : (↑Y.affineOpens : Type u)
V₁ : X.Opens
V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ V₁
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) U₁.carrier (f x : ↥Y)
⊢ ∃ (U' : (↑Y.affineOpens : Type u)) (V' : (↑X.affineOpens : Type u)) (_ : (↑U' : Y.Opens) ≤ U₁) (_ :
    (↑V' : X.Opens) ≤ V₁) (_ : x ∈ (↑V' : X.Opens)) (e : (↑V' : X.Opens) ≤ f ⁻¹ᵁ (↑U' : Y.Opens)),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U' : Y.Opens) (↑V' : X.Opens) e))
have obtain : ∀ (r : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) (hBr : Y.basicOpen r ≤ U₁)
  (hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U₁) (f x) hfx₁) : ↥Y) : ↥Y)),
  ∃ (U' : (↑Y.affineOpens : Type u)) (V' : (↑X.affineOpens : Type u)) (_ : (↑U' : Y.Opens) ≤ U₁) (_ :
    (↑V' : X.Opens) ≤ V₁) (_ : x ∈ (↑V' : X.Opens)) (e : (↑V' : X.Opens) ≤ f ⁻¹ᵁ (↑U' : Y.Opens)),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U' : Y.Opens) (↑V' : X.Opens) e))
Tactic: obtain ⟨r, hBr, hBfx⟩ := U₂.2.exists_basicOpen_le ⟨f x, hfx₁⟩ (e₂ hx₂)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ : Y.Opens
U₂ : (↑Y.affineOpens : Type u)
V₁ : X.Opens
V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ V₁
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) U₁.carrier (f x : ↥Y)
r : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBr : Y.basicOpen r ≤ U₁
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U₁) (f x) hfx₁) : ↥Y) : ↥Y)
⊢ ∃ (U' : (↑Y.affineOpens : Type u)) (V' : (↑X.affineOpens : Type u)) (_ : (↑U' : Y.Opens) ≤ U₁) (_ :
    (↑V' : X.Opens) ≤ V₁) (_ : x ∈ (↑V' : X.Opens)) (e : (↑V' : X.Opens) ≤ f ⁻¹ᵁ (↑U' : Y.Opens)),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U' : Y.Opens) (↑V' : X.Opens) e))
have obtain : ∀ (s : (↑Γ(X, (↑V₂ : X.Opens)) : Type u)) (hBs : X.basicOpen s ≤ V₁)
  (hBx : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V₁) x hx₁) : ↥X) ∈ X.basicOpen s),
  ∃ (U' : (↑Y.affineOpens : Type u)) (V' : (↑X.affineOpens : Type u)) (_ : (↑U' : Y.Opens) ≤ U₁) (_ :
    (↑V' : X.Opens) ≤ V₁) (_ : x ∈ (↑V' : X.Opens)) (e : (↑V' : X.Opens) ≤ f ⁻¹ᵁ (↑U' : Y.Opens)),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U' : Y.Opens) (↑V' : X.Opens) e))
Tactic: obtain ⟨s, hBs, hBx⟩ := V₂.2.exists_basicOpen_le ⟨x, hx₁⟩ hx₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ : Y.Opens
U₂ : (↑Y.affineOpens : Type u)
V₁ : X.Opens
V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ V₁
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) U₁.carrier (f x : ↥Y)
r : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBr : Y.basicOpen r ≤ U₁
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U₁) (f x) hfx₁) : ↥Y) : ↥Y)
s : (↑Γ(X, (↑V₂ : X.Opens)) : Type u)
hBs : X.basicOpen s ≤ V₁
hBx : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V₁) x hx₁) : ↥X) ∈ X.basicOpen s
⊢ ∃ (U' : (↑Y.affineOpens : Type u)) (V' : (↑X.affineOpens : Type u)) (_ : (↑U' : Y.Opens) ≤ U₁) (_ :
    (↑V' : X.Opens) ≤ V₁) (_ : x ∈ (↑V' : X.Opens)) (e : (↑V' : X.Opens) ≤ f ⁻¹ᵁ (↑U' : Y.Opens)),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U' : Y.Opens) (↑V' : X.Opens) e))
have obtain : ∀ (r' : (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (Y.basicOpen r) sorry) : Y.Opens)) : Type u))
  (s' : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (X.basicOpen s) sorry) : X.Opens)) : Type u))
  (hBx' : x ∈ X.basicOpen s') (e' : X.basicOpen s' ≤ f ⁻¹ᵁ Y.basicOpen r')
  (hf' : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen s') e'))),
  ∃ (U' : (↑Y.affineOpens : Type u)) (V' : (↑X.affineOpens : Type u)) (_ : (↑U' : Y.Opens) ≤ U₁) (_ :
    (↑V' : X.Opens) ≤ V₁) (_ : x ∈ (↑V' : X.Opens)) (e : (↑V' : X.Opens) ≤ f ⁻¹ᵁ (↑U' : Y.Opens)),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U' : Y.Opens) (↑V' : X.Opens) e))
Tactic: obtain ⟨r', s', hBx', e', hf'⟩ := exists_basicOpen_le_appLE_of_appLE_of_isAffine hPa hPl x
    ⟨Y.basicOpen r, U₂.2.basicOpen _⟩ U₂ ⟨X.basicOpen s, V₂.2.basicOpen _⟩ V₂ hBx hx₂ e₂ h₂ hBfx
-- 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
P' : MorphismProperty Scheme
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e : P = P'
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
⊢ HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
have subst : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
Tactic: subst e
Cleared hypotheses: P', e
-- 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
inst : HasRingHomProperty P @Q
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
⊢ HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
have heq : @Q = @Q'
Tactic: have heq : @Q = @Q' := by
    ext R S _ _ f
    exact (e' 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
H : P f
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))
have rw : ∀
  (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))
Tactic: rw [eq_affineLocally P, affineLocally_iff_affineOpens_le] at H
Cleared hypotheses: H, U, V, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
H : P f
inst_1 : IsAffine X
inst_2 : IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
have rw : Q (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (f ⁻¹ᵁ ⊤) sorry))
Tactic: rw [Scheme.Hom.appTop, Scheme.Hom.app_eq_appLE]
-- 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
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsOpenImmersion f
H : P g
⊢ P (f ≫ g)
have rw : ∀
  (H :
    ∀ (U : (↑Z.affineOpens : Type u)) (V : (↑Y.affineOpens : Type u)) (e : (↑V : Y.Opens) ≤ g ⁻¹ᵁ (↑U : Z.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U : Z.Opens) (↑V : Y.Opens) e)))
  (U : (↑Z.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ (f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)),
  Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U : Z.Opens) (↑V : X.Opens) e))
Tactic: rw [eq_affineLocally P, affineLocally_iff_affineOpens_le] at H ⊢
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_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsOpenImmersion f
H :
  ∀ (U : (↑Z.affineOpens : Type u)) (V : (↑Y.affineOpens : Type u)) (e : (↑V : Y.Opens) ≤ g ⁻¹ᵁ (↑U : Z.Opens)),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U : Z.Opens) (↑V : Y.Opens) e))
U : (↑Z.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
e : (↑V : X.Opens) ≤ (f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U : Z.Opens) (↑V : X.Opens) e))
have have : ∀ (this : IsIso (X := Γ(Y, f ''ᵁ (↑V : X.Opens))) (Scheme.Hom.appLE f (f ''ᵁ (↑V : X.Opens)) (↑V : X.Opens) sorry)),
  Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U : Z.Opens) (↑V : X.Opens) e))
Tactic: have : IsIso (f.appLE (f ''ᵁ V) V.1 (f.preimage_image_eq _).ge) :=
    inferInstanceAs (IsIso (f.app _ ≫
      X.presheaf.map (eqToHom (f.preimage_image_eq _).symm).op))
-- 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
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsOpenImmersion f
H :
  ∀ (U : (↑Z.affineOpens : Type u)) (V : (↑Y.affineOpens : Type u)) (e : (↑V : Y.Opens) ≤ g ⁻¹ᵁ (↑U : Z.Opens)),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U : Z.Opens) (↑V : Y.Opens) e))
U : (↑Z.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
e : (↑V : X.Opens) ≤ (f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)
this : IsIso (X := Γ(Y, f ''ᵁ (↑V : X.Opens))) (Scheme.Hom.appLE f (f ''ᵁ (↑V : X.Opens)) (↑V : X.Opens) ⋯)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U : Z.Opens) (↑V : X.Opens) e))
have rw : Q (R := (↑Γ(Z, (↑U : Z.Opens)) : Type u)) (S := (↑Γ(Y, f ''ᵁ (↑V : X.Opens)) : Type u))
  (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U : Z.Opens) (f ''ᵁ (↑V : X.Opens)) sorry))
Tactic: rw [← Scheme.Hom.appLE_comp_appLE _ _ _ (f ''ᵁ V) V.1
    (Set.image_subset_iff.mpr e) (f.preimage_image_eq _).ge,
    CommRingCat.hom_comp,
    (isLocal_ringHomProperty P).respectsIso.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 Y : Scheme
f : X ⟶ Y
⊢ P f ↔
    ∀ (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))
have rw : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
  ∀ (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))
Tactic: rw [eq_affineLocally P, affineLocally_iff_affineOpens_le]
-- 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
rw :
  affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
    ∀ (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))
⊢ P f ↔
    ∀ (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))
have rw₁ : (∀ (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))
Tactic: rw [eq_affineLocally P, affineLocally_iff_affineOpens_le]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
⊢ P f
have rw : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := P)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
H_1 : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
U : (↑X.affineOpens : Type u)
r : (↑Γ(X, (↑U : X.Opens)) : Type u)
H :
  Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))
⊢ Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(X.affineBasicOpen r) : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(X.affineBasicOpen r) : X.Opens) ⋯))
have basicOpen : Q (R := (↑Γ(Y, ⊤) : Type u))
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry ≫ X.presheaf.map (homOfLE sorry).op))
Tactic: simp_rw [Scheme.affineBasicOpen_coe,
      ← f.appLE_map (U := ⊤) le_top (homOfLE (X.basicOpen_le r)).op]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
H_1 : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
U : (↑X.affineOpens : Type u)
r : (↑Γ(X, (↑U : X.Opens)) : Type u)
H :
  Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))
⊢ Q (R := (↑Γ(Y, ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op))
have this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
Tactic: have := U.2.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_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
H_1 : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
U : (↑X.affineOpens : Type u)
s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u)
hs : Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) ⊤
H :
  ∀ (f_1 : ↥s),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S :=
      (↑Γ(X, (↑(X.affineBasicOpen (↑f_1 : (↑Γ(X, (↑U : X.Opens)) : Type u))) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom
        (Scheme.Hom.appLE f ⊤ (↑(X.affineBasicOpen (↑f_1 : (↑Γ(X, (↑U : X.Opens)) : Type u))) : X.Opens) ⋯))
⊢ Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))
have openCover : ∀ (r : (↑(↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)),
  ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) T) (_ :
    IsLocalization.Away (↑r : (↑Γ(X, (↑U : X.Opens)) : Type u)) T),
    Q (R := (↑Γ(Y, ⊤) : Type u))
      (RingHom.comp (β := (↑Γ(X, (↑U : X.Opens)) : Type u)) (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) T)
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry)))
Tactic: apply (isLocal_ringHomProperty P).ofLocalizationSpanTarget.ofIsLocalization
      (isLocal_ringHomProperty P).respectsIso _ _ hs