awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
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)
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))
⊢ 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

Premises used: AlgebraicGeometry.affineLocally_iff_affineOpens_le, AlgebraicGeometry.HasRingHomProperty.eq_affineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))

Tactic:
H _ _ _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))

Tactic:
exact H _ _ _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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
rw : Q (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (f ⁻¹ᵁ ⊤) ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
rw [Scheme.Hom.appTop, Scheme.Hom.app_eq_appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.appTop, AlgebraicGeometry.Scheme.Hom.app_eq_appLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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 (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (f ⁻¹ᵁ ⊤) ⋯))

Tactic:
appLE P f H ⟨_, isAffineOpen_top _⟩ ⟨_, isAffineOpen_top _⟩ _

Premises used: AlgebraicGeometry.isAffineOpen_top, Set.Mem, Set.univ, setOf, AlgebraicGeometry.HasRingHomProperty.appLE, Subtype.mk, Set.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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 (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (f ⁻¹ᵁ ⊤) ⋯))

Tactic:
exact appLE P f H ⟨_, isAffineOpen_top _⟩ ⟨_, isAffineOpen_top _⟩ _

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.HasRingHomProperty.appLE, Subtype.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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
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))
⊢ P (f ≫ g)

Tactic:
rw [eq_affineLocally P, affineLocally_iff_affineOpens_le] at H ⊢

Premises used: AlgebraicGeometry.affineLocally_iff_affineOpens_le, AlgebraicGeometry.HasRingHomProperty.eq_affineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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)
have :
  ∀ (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))
⊢ 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))
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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) ⋯)
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)) ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U : Z.Opens) (↑V : X.Opens) e))

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]

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, Iff.mpr, Eq.ge, RingHom.RespectsIso.cancel_right_isIso, AlgebraicGeometry.Scheme.Hom.preimage_image_eq, AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty, CommRingCat.hom_comp, Set.image_subset_iff, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE, Subtype.val, RingHom.PropertyIsLocal.respectsIso, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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 (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)) ⋯))

Tactic:
H _ ⟨_, V.2.image_of_isOpenImmersion _⟩ _

Premises used: AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, Subtype.mk, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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 (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)) ⋯))

Tactic:
exact H _ ⟨_, V.2.image_of_isOpenImmersion _⟩ _

Premises used: AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, Subtype.mk, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
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))
rw₁ 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))
⊢ 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))

Tactic:
rw [eq_affineLocally P, affineLocally_iff_affineOpens_le]

Premises used: AlgebraicGeometry.affineLocally_iff_affineOpens_le, AlgebraicGeometry.HasRingHomProperty.eq_affineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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)))
rw : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ P f

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := P)]

Premises used: AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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)))
U : (↑X.affineOpens : Type u)
let :
  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, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))

Tactic:
let S i : X.affineOpens := ⟨_, isAffineOpen_opensRange (𝒰.f i)⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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) ⋯))
basicOpen :
  Q (R := (↑Γ(Y, ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op))
⊢ 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) ⋯))

Tactic:
simp_rw [Scheme.affineBasicOpen_coe,
      ← f.appLE_map (U := ⊤) le_top (homOfLE (X.basicOpen_le r)).op]

Premises used: Quiver.Hom.op, AlgebraicGeometry.Scheme.basicOpen_le, AlgebraicGeometry.Scheme.affineBasicOpen_coe, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.Hom.appLE_map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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) ⋯))
⊢ IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)

Tactic:
have := U.2.isLocalization_basicOpen r
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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) ⋯))
this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
⊢ Q (R := (↑Γ(Y, ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op))

Tactic:
(isLocal_ringHomProperty P).StableUnderCompositionWithLocalizationAwayTarget _ r _ H

Premises used: RingHom.PropertyIsLocal.StableUnderCompositionWithLocalizationAwayTarget, AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty, AlgebraicGeometry.RingedSpace.basicOpen, AlgebraicGeometry.Scheme.basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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) ⋯))
this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
⊢ Q (R := (↑Γ(Y, ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op))

Tactic:
exact (isLocal_ringHomProperty P).StableUnderCompositionWithLocalizationAwayTarget _ r _ H

Premises used: RingHom.PropertyIsLocal.StableUnderCompositionWithLocalizationAwayTarget, AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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) ⋯))
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) ⋯)))
⊢ Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))

Tactic:
apply (isLocal_ringHomProperty P).ofLocalizationSpanTarget.ofIsLocalization
      (isLocal_ringHomProperty P).respectsIso _ _ hs

Premises used: AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty, RingHom.OfLocalizationSpanTarget.ofIsLocalization, RingHom.PropertyIsLocal.ofLocalizationSpanTarget, RingHom.PropertyIsLocal.respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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) ⋯))
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) ⋯)))

Tactic:
⟨_, _, _, IsAffineOpen.isLocalization_basicOpen U.2 r, ?_⟩

Premises used: AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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) ⋯))
r : (↑(↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)
openCover :
  Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, X.basicOpen (↑r : (↑Γ(X, (↑U : X.Opens)) : Type u))) : Type u))
    (RingHom.comp (β := (↑Γ(X, (↑U : X.Opens)) : Type u))
      (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u)
        (↑Γ(X, X.basicOpen (↑r : (↑Γ(X, (↑U : X.Opens)) : Type u))) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯)))
⊢ ∃ (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) ⋯)))

Tactic:
refine ⟨_, _, _, IsAffineOpen.isLocalization_basicOpen U.2 r, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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) ⋯))
r : (↑(↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)
openCover : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (X.basicOpen (↑r : (↑Γ(X, (↑U : X.Opens)) : Type u))) ⋯))
⊢ Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, X.basicOpen (↑r : (↑Γ(X, (↑U : X.Opens)) : Type u))) : Type u))
    (RingHom.comp (β := (↑Γ(X, (↑U : X.Opens)) : Type u))
      (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u)
        (↑Γ(X, X.basicOpen (↑r : (↑Γ(X, (↑U : X.Opens)) : Type u))) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯)))

Tactic:
rw [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Scheme.Hom.appLE_map]

Premises used: CommRingCat.hom_comp, RingHom.algebraMap_toAlgebra, AlgebraicGeometry.Scheme.Hom.appLE_map