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_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X Y S : Scheme
inst_1 : IsAffine S
hP' :
  ∀ [inst : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) g →
      sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := pullback f g) (pullback.fst f g)
⊢ ∀ [inst : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) g →
      sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := pullback f g) (pullback.fst f g)

Tactic:
_
-- 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
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X Y S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) g
hP' : ∀ (H : P g), P (X := pullback f g) (pullback.fst f g)
⊢ sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := pullback f g) (pullback.fst f g)

Tactic:
rw [← HasAffineProperty.iff_of_isAffine (P := P)] at H ⊢

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
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X Y S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
hP' :
  ∀ (this : ∀ ⦃Y : Scheme.{u}⦄ (g : Y ⟶ S) (H : P g) (hX : IsAffine Y), P (X := pullback f g) (pullback.fst f g))
    (hX : ¬IsAffine Y), P (X := pullback f g) (pullback.fst f g)
wlog : ∀ ⦃Y : Scheme.{u}⦄ (g : Y ⟶ S) (H : P g) (hX : IsAffine Y), P (X := pullback f g) (pullback.fst f g)
⊢ P (X := pullback f g) (pullback.fst f g)

Tactic:
wlog hX : IsAffine Y generalizing Y

Premises used: AlgebraicGeometry.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
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X Y S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
this : ∀ ⦃Y : Scheme.{u}⦄ (g : Y ⟶ S) (H : P g) (hX : IsAffine Y), P (X := pullback f g) (pullback.fst f g)
hX : ¬IsAffine Y
hP' :
  ∀ (i : (Scheme.Pullback.openCoverOfRight Y.affineCover f g).I₀),
    P ((Scheme.Pullback.openCoverOfRight Y.affineCover f g).f i ≫ pullback.fst f g)
⊢ P (X := pullback f g) (pullback.fst f g)

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := P)
      (Scheme.Pullback.openCoverOfRight Y.affineCover f g)]

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight
-- 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
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X Y S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
this : ∀ ⦃Y : Scheme.{u}⦄ (g : Y ⟶ S) (H : P g) (hX : IsAffine Y), P (X := pullback f g) (pullback.fst f g)
hX : ¬IsAffine Y
i : (Scheme.Pullback.openCoverOfRight Y.affineCover f g).I₀
hP' : P (X := pullback f (Y.affineCover.f i ≫ g)) (pullback.fst f (Y.affineCover.f i ≫ g))
⊢ P ((Scheme.Pullback.openCoverOfRight Y.affineCover f g).f i ≫ pullback.fst f g)

Tactic:
simp only [Scheme.Pullback.openCoverOfRight_X, Scheme.Pullback.openCoverOfRight_f,
      limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, Category.comp_id]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_f, CategoryTheory.Category.comp_id, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_X, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π
-- 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
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X Y S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
this : ∀ ⦃Y : Scheme.{u}⦄ (g : Y ⟶ S) (H : P g) (hX : IsAffine Y), P (X := pullback f g) (pullback.fst f g)
hX : ¬IsAffine Y
i : (Scheme.Pullback.openCoverOfRight Y.affineCover f g).I₀
⊢ P (X := pullback f (Y.affineCover.f i ≫ g)) (pullback.fst f (Y.affineCover.f i ≫ g))

Tactic:
apply this _ (comp_of_isOpenImmersion _ _ _ H) inferInstance

Premises used: AlgebraicGeometry.HasRingHomProperty.comp_of_isOpenImmersion, inferInstance
-- 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
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
Y : Scheme
g : Y ⟶ S
H : P g
hX : IsAffine Y
rw :
  ∀ (H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))) (hX : IsAffine Y),
    Q (S := (↑Γ(pullback f g, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst f g)))
⊢ P (X := pullback f g) (pullback.fst f g)

Tactic:
rw [iff_of_isAffine (P := P)] at H ⊢

Premises used: AlgebraicGeometry.HasRingHomProperty.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
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
Y : Scheme
g : Y ⟶ S
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hX : IsAffine Y
⊢ Q (S := (↑Γ(pullback f g, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst f g)))

Tactic:
hP.pullback_fst_appTop _ (isLocal_ringHomProperty P).respectsIso _ _ H

Premises used: RingHom.IsStableUnderBaseChange.pullback_fst_appTop, AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty, 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
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
Y : Scheme
g : Y ⟶ S
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hX : IsAffine Y
⊢ Q (S := (↑Γ(pullback f g, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst f g)))

Tactic:
exact hP.pullback_fst_appTop _ (isLocal_ringHomProperty P).respectsIso _ _ H

Premises used: RingHom.IsStableUnderBaseChange.pullback_fst_appTop, AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty, RingHom.PropertyIsLocal.respectsIso
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
        (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι))
    (hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
wlog :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
⊢ P (f ≫ U.ι)

Tactic:
wlog hYa : ∃ (a : Γ(Y, ⊤)), U = Y.basicOpen a generalizing X Y
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
inr :
  ∀ (Us : Set Y.Opens) (hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen) (heq : U = sSup Us), P (f ≫ U.ι)
⊢ P (f ≫ U.ι)

Tactic:
obtain ⟨(Us : Set Y.Opens), hUs, heq⟩ := Opens.isBasis_iff_cover.mp (isBasis_basicOpen Y) U

Premises used: AlgebraicGeometry.isBasis_basicOpen, Iff.mp, TopologicalSpace.Opens.isBasis_iff_cover, AlgebraicGeometry.Scheme.Opens, Set
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
inr : P (f ≫ U.ι)
⊢ P (f ≫ U.ι)

Tactic:
let V (s : Us) : X.Opens := f ⁻¹ᵁ U.ι ⁻¹ᵁ s
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
inr : ∀ (i : (↑Us : Type u)), P ((V i).ι ≫ f ≫ U.ι)
inr₁ : iSup V = ⊤
⊢ P (f ≫ U.ι)

Tactic:
rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := P) V]

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_iSup_eq_top
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
s : (↑Us : Type u)
inr : P ((V s).ι ≫ f ≫ U.ι)
⊢ P ((V s).ι ≫ f ≫ U.ι)

Tactic:
let f' : (V s).toScheme ⟶ U.ι ⁻¹ᵁ s := f ∣_ U.ι ⁻¹ᵁ s
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
s : (↑Us : Type u)
f' : (↑(V s) : Scheme) ⟶ (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) := f ∣_ U.ι ⁻¹ᵁ (↑s : Y.Opens)
⊢ P f'

Tactic:
have hf' : P f' := IsZariskiLocalAtTarget.restrict hf _
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
s : (↑Us : Type u)
f' : (↑(V s) : Scheme) ⟶ (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) := f ∣_ U.ι ⁻¹ᵁ (↑s : Y.Opens)
hf' : P f'
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥(↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme)) ⇑((U.ι ⁻¹ᵁ (↑s : Y.Opens)).ι ≫ U.ι))
    (Set.range (ι := ↥(↑(↑s : Y.Opens) : Scheme)) ⇑(↑s : Y.Opens).ι)

Tactic:
simpa only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, Scheme.Opens.range_ι,
          Opens.map_coe, Set.image_preimage_eq_iff, heq, Opens.coe_sSup] using le_sSup s.2

Premises used: TopologicalSpace.Opens.map_coe, Set.range_comp, TopologicalSpace.Opens.coe_sSup, AlgebraicGeometry.Scheme.Opens.range_ι, le_sSup, Set.image_preimage_eq_iff, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp, 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
s : (↑Us : Type u)
f' : (↑(V s) : Scheme) ⟶ (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) := f ∣_ U.ι ⁻¹ᵁ (↑s : Y.Opens)
hf' : P f'
e : (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) ≅ (↑(↑s : Y.Opens) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ (↑s : Y.Opens)).ι ≫ U.ι) (↑s : Y.Opens).ι ⋯
⊢ (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s : Y.Opens).ι

Tactic:
simp only [V, IsOpenImmersion.isoOfRangeEq_hom_fac, f', e, morphismRestrict_ι_assoc]

Premises used: AlgebraicGeometry.morphismRestrict_ι_assoc, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
s : (↑Us : Type u)
f' : (↑(V s) : Scheme) ⟶ (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) := f ∣_ U.ι ⁻¹ᵁ (↑s : Y.Opens)
hf' : P f'
e : (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) ≅ (↑(↑s : Y.Opens) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ (↑s : Y.Opens)).ι ≫ U.ι) (↑s : Y.Opens).ι ⋯
⊢ (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s : Y.Opens).ι

Tactic:
have heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ s.1.ι := by
        simp only [V, IsOpenImmersion.isoOfRangeEq_hom_fac, f', e, morphismRestrict_ι_assoc]
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq_1 : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
s : (↑Us : Type u)
f' : (↑(V s) : Scheme) ⟶ (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) := f ∣_ U.ι ⁻¹ᵁ (↑s : Y.Opens)
hf' : P f'
e : (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) ≅ (↑(↑s : Y.Opens) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ (↑s : Y.Opens)).ι ≫ U.ι) (↑s : Y.Opens).ι ⋯
heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s : Y.Opens).ι
inr : P ((f' ≫ e.hom) ≫ (↑s : Y.Opens).ι)
⊢ P ((V s).ι ≫ f ≫ U.ι)

Tactic:
rw [heq, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq_1 : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
s : (↑Us : Type u)
f' : (↑(V s) : Scheme) ⟶ (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) := f ∣_ U.ι ⁻¹ᵁ (↑s : Y.Opens)
hf' : P f'
e : (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) ≅ (↑(↑s : Y.Opens) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ (↑s : Y.Opens)).ι ≫ U.ι) (↑s : Y.Opens).ι ⋯
heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s : Y.Opens).ι
⊢ P ((f' ≫ e.hom) ≫ (↑s : Y.Opens).ι)

Tactic:
this _ ?_ ?_
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq_1 : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
s : (↑Us : Type u)
f' : (↑(V s) : Scheme) ⟶ (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) := f ∣_ U.ι ⁻¹ᵁ (↑s : Y.Opens)
hf' : P f'
e : (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) ≅ (↑(↑s : Y.Opens) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ (↑s : Y.Opens)).ι ≫ U.ι) (↑s : Y.Opens).ι ⋯
heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s : Y.Opens).ι
inr : P (f' ≫ e.hom)
inr₁ : ∃ (a : (↑Γ(Y, ⊤) : Type u)), (↑s : Y.Opens) = Y.basicOpen a
⊢ P ((f' ≫ e.hom) ≫ (↑s : Y.Opens).ι)

Tactic:
refine this _ ?_ ?_
-- 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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq_1 : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
s : (↑Us : Type u)
f' : (↑(V s) : Scheme) ⟶ (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) := f ∣_ U.ι ⁻¹ᵁ (↑s : Y.Opens)
hf' : P f'
e : (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) ≅ (↑(↑s : Y.Opens) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ (↑s : Y.Opens)).ι ≫ U.ι) (↑s : Y.Opens).ι ⋯
heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s : Y.Opens).ι
inr inr₁ inr₂ inr₃ : P f'
⊢ P (f' ≫ e.hom)

Tactic:
rwa [P.cancel_right_of_respectsIso]

Premises used: CategoryTheory.MorphismProperty.cancel_right_of_respectsIso