awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : (↑X.affineOpens : Type u)
h : (↑V : X.Opens) ≤ f ⁻¹ᵁ U
this :
  Eq (α := { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U })
    ((affineOpensRestrict (f ⁻¹ᵁ U) :
          (a : (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u)) →
            { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U })
        (((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
            (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
              (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
          (Subtype.mk (p := fun (V : (↑X.affineOpens : Type u)) ↦ (↑V : X.Opens) ≤ f ⁻¹ᵁ U) V h)) :
      { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U })
    (Subtype.mk (p := fun (V : (↑X.affineOpens : Type u)) ↦ (↑V : X.Opens) ≤ f ⁻¹ᵁ U) V h :
      { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U })
⊢ P (R := (↑Γ((↑U : Scheme), ⊤) : Type u)) (S :=
      (↑Γ((↑(f ⁻¹ᵁ U) : Scheme),
            (↑(((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
                    (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
                      (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
                  (Subtype.mk (p := fun (a : (↑X.affineOpens : Type u)) ↦ (↑a : X.Opens) ≤ f ⁻¹ᵁ U) V h)) :
              (↑(f ⁻¹ᵁ U) : Scheme).Opens)) :
        Type u))
      (CommRingCat.Hom.hom
        (Hom.appLE f (U.ι ''ᵁ ⊤)
          ((f ⁻¹ᵁ U).ι ''ᵁ
            (↑(((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
                    (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
                      (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
                  (Subtype.mk (p := fun (a : (↑X.affineOpens : Type u)) ↦ (↑a : X.Opens) ≤ f ⁻¹ᵁ U) V h)) :
              (↑(f ⁻¹ᵁ U) : Scheme).Opens))
          ⋯)) ↔
    P (CommRingCat.Hom.hom (Hom.appLE f U (↑V : X.Opens) h))

Tactic:
f.appLE_congr _ (Opens.ι_image_top _) congr($(this).1.1) (fun f => P f.hom)

Premises used: CommRingCat.Hom.hom, congrArg, Set.Mem, id, AlgebraicGeometry.Scheme.Hom.appLE_congr, AlgebraicGeometry.Scheme.Opens.ι_image_top, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : (↑X.affineOpens : Type u)
h : (↑V : X.Opens) ≤ f ⁻¹ᵁ U
this :
  Eq (α := { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U })
    ((affineOpensRestrict (f ⁻¹ᵁ U) :
          (a : (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u)) →
            { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U })
        (((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
            (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
              (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
          (Subtype.mk (p := fun (V : (↑X.affineOpens : Type u)) ↦ (↑V : X.Opens) ≤ f ⁻¹ᵁ U) V h)) :
      { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U })
    (Subtype.mk (p := fun (V : (↑X.affineOpens : Type u)) ↦ (↑V : X.Opens) ≤ f ⁻¹ᵁ U) V h :
      { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U })
⊢ P (R := (↑Γ((↑U : Scheme), ⊤) : Type u)) (S :=
      (↑Γ((↑(f ⁻¹ᵁ U) : Scheme),
            (↑(((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
                    (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
                      (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
                  (Subtype.mk (p := fun (a : (↑X.affineOpens : Type u)) ↦ (↑a : X.Opens) ≤ f ⁻¹ᵁ U) V h)) :
              (↑(f ⁻¹ᵁ U) : Scheme).Opens)) :
        Type u))
      (CommRingCat.Hom.hom
        (Hom.appLE f (U.ι ''ᵁ ⊤)
          ((f ⁻¹ᵁ U).ι ''ᵁ
            (↑(((affineOpensRestrict (f ⁻¹ᵁ U)).symm :
                    (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ f ⁻¹ᵁ U }) →
                      (↑(↑(f ⁻¹ᵁ U) : Scheme).affineOpens : Type u))
                  (Subtype.mk (p := fun (a : (↑X.affineOpens : Type u)) ↦ (↑a : X.Opens) ≤ f ⁻¹ᵁ U) V h)) :
              (↑(f ⁻¹ᵁ U) : Scheme).Opens))
          ⋯)) ↔
    P (CommRingCat.Hom.hom (Hom.appLE f U (↑V : X.Opens) h))

Tactic:
exact f.appLE_congr _ (Opens.ι_image_top _) congr($(this).1.1) (fun f => P f.hom)

Premises used: CommRingCat.Hom.hom, congrArg, id, AlgebraicGeometry.Scheme.Hom.appLE_congr, AlgebraicGeometry.Scheme.Opens.ι_image_top, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f ↔
    ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))

Tactic:
forall_congr' fun U ↦ sourceAffineLocally_morphismRestrict P f U U.2

Premises used: AlgebraicGeometry.targetAffineLocally, forall_congr', Subtype.val, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f ↔
    ∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), P (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))

Tactic:
simp [affineLocally_iff_affineOpens_le, Scheme.affineOpens]

Premises used: AlgebraicGeometry.affineLocally_iff_affineOpens_le, AlgebraicGeometry.Scheme.affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
respectsIso : (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).toProperty.RespectsIso
to_basicOpen :
  ∀ {X Y : Scheme.{u}} [inst : IsAffine Y] (f : X ⟶ Y) (r : (↑Γ(Y, ⊤) : Type u)),
    sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X := (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme))
        (f ∣_ Y.basicOpen r)
of_basicOpenCover :
  ∀ {X Y : Scheme.{u}} [inst : IsAffine Y] (f : X ⟶ Y) (s : Finset (↑Γ(Y, ⊤) : Type u)),
    Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤ →
      (∀ (r : ↥s),
          sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X :=
            (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme)) (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) →
        sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
⊢ AffineTargetMorphismProperty.IsLocal.{u} (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
⊢ (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).toProperty.RespectsIso

Tactic:
sourceAffineLocally_respectsIso P h₁

Premises used: AlgebraicGeometry.sourceAffineLocally_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
⊢ (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).toProperty.RespectsIso

Tactic:
exact sourceAffineLocally_respectsIso P h₁

Premises used: AlgebraicGeometry.sourceAffineLocally_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
to_basicOpen :
  ∀ [inst : IsAffine Y] (f : X ⟶ Y) (r : (↑Γ(Y, ⊤) : Type u)),
    sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X := (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme))
        (f ∣_ Y.basicOpen r)
⊢ ∀ [inst : IsAffine Y] (f : X ⟶ Y) (r : (↑Γ(Y, ⊤) : Type u)),
    sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X := (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme))
        (f ∣_ Y.basicOpen r)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
to_basicOpen :
  ∀ (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑V : X.Opens) e))
⊢ sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X := (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme))
    (f ∣_ Y.basicOpen r)

Tactic:
rw [sourceAffineLocally_morphismRestrict]

Premises used: AlgebraicGeometry.sourceAffineLocally_morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
⊢ (↑U : X.Opens) ≤ f ⁻¹ᵁ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
simp :
  X.basicOpen (U := (↑U : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r :
          (↑Γ(X, ⊤) : Type u))) =
    (↑U : X.Opens)
⊢ X.basicOpen (U := (↑U : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens))) (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
        r) =
    (↑U : X.Opens)

Tactic:
simp only [Scheme.Hom.appLE, Opens.map_top, CommRingCat.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE, CommRingCat.comp_apply, TopologicalSpace.Opens.map_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
rw :
  (↑U : X.Opens) ⊓
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          r) =
    (↑U : X.Opens)
⊢ X.basicOpen (U := (↑U : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r :
          (↑Γ(X, ⊤) : Type u))) =
    (↑U : X.Opens)

Tactic:
rw [Scheme.basicOpen_res]

Premises used: AlgebraicGeometry.Scheme.basicOpen_res
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
⊢ (↑U : X.Opens) ⊓
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          r) =
    (↑U : X.Opens)

Tactic:
simpa using hU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
to_basicOpen :
  ∀
    (this :
      X.basicOpen (U := (↑U : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
            r) =
        (↑U : X.Opens)),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑U : X.Opens) hU))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑U : X.Opens) hU))

Tactic:
have : X.basicOpen (f.appLE ⊤ U (by simp) r) = U := by
      simp only [Scheme.Hom.appLE, Opens.map_top, CommRingCat.comp_apply]
      rw [Scheme.basicOpen_res]
      simpa using hU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
this :
  X.basicOpen (U := (↑U : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens))) (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
        r) =
    (↑U : X.Opens)
⊢ X.basicOpen (U := (↑U : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens))) (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
        r) ≤
    f ⁻¹ᵁ Y.basicOpen r

Tactic:
simp [Scheme.Hom.appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
this :
  X.basicOpen (U := (↑U : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens))) (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
        r) =
    (↑U : X.Opens)
to_basicOpen :
  P (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (S :=
    (↑Γ(X,
          X.basicOpen (U := (↑U : X.Opens))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                  (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
              r)) :
      Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))) : Type u) (P := (↑Γ(X, (↑U : X.Opens)) : Type u))
          (↑(X.presheaf.1
                (op
                  (X.basicOpen (U := (↑U : X.Opens))
                    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                          (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
                        (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
                      r)))) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯)) r)))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑U : X.Opens) hU))

Tactic:
rw [← f.appLE_congr (by simp [Scheme.Hom.appLE]) rfl this (fun f => P f.hom),
      IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2 _ r]

Premises used: AlgebraicGeometry.isAffineOpen_top, CommRingCat.Hom.hom, AlgebraicGeometry.Scheme.Hom.appLE_congr, rfl, Subtype.property, AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
this :
  X.basicOpen (U := (↑U : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens))) (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
        r) =
    (↑U : X.Opens)
to_basicOpen :
  P (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))
⊢ P (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (S :=
    (↑Γ(X,
          X.basicOpen (U := (↑U : X.Opens))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                  (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
              r)) :
      Type u))
    (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))) : Type u) (P := (↑Γ(X, (↑U : X.Opens)) : Type u))
      (↑(X.presheaf.1
            (op
              (X.basicOpen (U := (↑U : X.Opens))
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                      (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
                    (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
                  r)))) :
        Type u)
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯)) r)

Tactic:
apply +allowSynthFailures h₂