mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
rₐ : (a : ↑s) → Localization.Away ↑a := fun a ↦ (algebraMap S (Localization.Away ↑a)) (f r)
Sₐ : ↑s → Type u := fun a ↦ Localization.Away (rₐ a)
this✝² : ∀ (a : ↑s), IsLocalization.Away (((algebraMap S (Localization.Away ↑a)).comp f) r) (Sₐ a)
this✝¹ :
  ∀ (a : ↑s),
    IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
H : ∀ (a : ↑s), Submonoid.powers (f r) ≤ Submonoid.comap (algebraMap S (Localization.Away ↑a)) (Submonoid.powers (rₐ a))
this✝ : (a : ↑s) → Algebra S' (Sₐ a) :=
  fun a ↦ (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away ↑a)) ⋯).toAlgebra
this : ∀ (a : ↑s), IsScalarTower S S' (Sₐ a)
a : ↑s
⊢ P ((IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away ↑a)) ⋯).comp (IsLocalization.Away.map R' S' f r))

Tactic:
IsLocalization.Away.map,

Goal state after:
case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
rₐ : (a : ↑s) → Localization.Away ↑a := fun a ↦ (algebraMap S (Localization.Away ↑a)) (f r)
Sₐ : ↑s → Type u := fun a ↦ Localization.Away (rₐ a)
this✝² : ∀ (a : ↑s), IsLocalization.Away (((algebraMap S (Localization.Away ↑a)).comp f) r) (Sₐ a)
this✝¹ :
  ∀ (a : ↑s),
    IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
H : ∀ (a : ↑s), Submonoid.powers (f r) ≤ Submonoid.comap (algebraMap S (Localization.Away ↑a)) (Submonoid.powers (rₐ a))
this✝ : (a : ↑s) → Algebra S' (Sₐ a) :=
  fun a ↦ (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away ↑a)) ⋯).toAlgebra
this : ∀ (a : ↑s), IsScalarTower S S' (Sₐ a)
a : ↑s
⊢ P ((IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away ↑a)) ⋯).comp (IsLocalization.map S' f ⋯))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ P).toProperty.RespectsIso

Tactic:
apply AffineTargetMorphismProperty.respectsIso_mk

Goal state after:
case h₁
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z],
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)

case h₂
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y],
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ U i)
x : ↥X
⊢ f x ∈ iSup U

Tactic:
rw [hU]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ U i)
x : ↥X
⊢ f x ∈ ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)
x : ↥X
⊢ x ∈ iSup U

Tactic:
rw [hU]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)
x : ↥X
⊢ x ∈ ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
⊢ IsCompact ↑(X.basicOpen f)

Tactic:
refine isCompact_iff_finite_and_eq_biUnion_affineOpens.mpr ?_

Goal state after:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
⊢ ∃ s, s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, ↑i
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case respectsIso
X Y : Scheme
f : X ⟶ Y
⊢ (AffineTargetMorphismProperty.toProperty fun X x x_1 x_2 ↦ CompactSpace ↥X).RespectsIso

Tactic:
apply AffineTargetMorphismProperty.respectsIso_mk

Goal state after:
case respectsIso.h₁
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [IsAffine Z], CompactSpace ↥Y → CompactSpace ↥X

case respectsIso.h₂
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [IsAffine Y], CompactSpace ↥X → CompactSpace ↥X
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑f = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑f = ↑U
⊢ (fun a ↦ U.ι a) '' Set.range ⇑(IsOpenImmersion.lift U.ι f ⋯) = ↑U

Tactic:
rwa [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, IsOpenImmersion.lift_fac]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ IsClosedMap ⇑f ↔ SpecializingMap ⇑f

Tactic:
refine ⟨fun h ↦ h.specializingMap, fun H ↦ ?_⟩
  wlog hY : ∃ R, Y = Spec R
  · change topologically @IsClosedMap f
    rw [IsZariskiLocalAtTarget.iff_of_openCover (P := topologically @IsClosedMap) Y.affineCover]
    intro i
    have _ : QuasiCompact (Y.affineCover.pullbackHom f i) := MorphismProperty.pullback_snd _ _ ‹_›
    refine this (Y.affineCover.pullbackHom f i) ?_ ⟨_, rfl⟩
    exact IsZariskiLocalAtTarget.of_isPullback
      (P := topologically @SpecializingMap) (.of_hasPullback _ _) H
  obtain ⟨S, rfl⟩ := hY
  intro Z hZ
  replace H := hZ.stableUnderSpecialization.image H
  wlog hX : ∃ R, X = Spec R
  · obtain ⟨R, g, hg⟩ := compactSpace_iff_exists.mp (QuasiCompact.compactSpace_of_compactSpace f)
    have inst : QuasiCompact (g ≫ f) := HasAffineProperty.iff_of_isAffine.mpr (by infer_instance)
    have := this _ (g ≫ f) (g ⁻¹' Z) (hZ.preimage g.continuous)
    simp_rw [Scheme.Hom.comp_base, TopCat.comp_app, ← Set.image_image,
      Set.image_preimage_eq _ hg] at this
    exact this H ⟨_, rfl⟩
  obtain ⟨R, rfl⟩ := hX
  obtain ⟨φ, rfl⟩ := Spec.homEquiv.symm.surjective f
  exact PrimeSpectrum.isClosed_image_of_stableUnderSpecialization φ.hom Z hZ H

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
Y : Scheme
g : Y ⟶ S
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hX : IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst f g)))

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

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
h : I.ideal = J.ideal
⊢ I = J

Tactic:
obtain ⟨i, _, s, hs⟩ := I

Goal state after:
X : Scheme
J : X.IdealSheafData
i : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen✝ :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (i U) = i (X.affineBasicOpen f)
s : Set ↥X
hs : s = ⋂ U, X.zeroLocus ↑(i U)
h :
  { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝, supportSet := s,
        supportSet_eq_iInter_zeroLocus := hs }.ideal =
    J.ideal
⊢ { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝, supportSet := s, supportSet_eq_iInter_zeroLocus := hs } = J
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
hf : P f
x : ↥X
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
obtain ⟨U, hU, hfx, _⟩ := Opens.isBasis_iff_nbhd.mp Y.isBasis_affineOpens
      (Opens.mem_top <| f x)
    obtain ⟨V, hV, hx, e⟩ := Opens.isBasis_iff_nbhd.mp X.isBasis_affineOpens
      (show x ∈ f ⁻¹ᵁ U from hfx)
    simp_rw [HasRingHomProperty.iff_appLE (P := P), locally_iff_isLocalization hQi] at hf
    obtain ⟨s, hs, hfs⟩ := hf ⟨U, hU⟩ ⟨V, hV⟩ e
    apply iSup_basicOpen_of_span_eq_top at hs
    have : x ∈ (⨆ i ∈ s, X.basicOpen i) := hs.symm ▸ hx
    have : ∃ r ∈ s, x ∈ X.basicOpen r := by simpa using this
    obtain ⟨r, hr, hrs⟩ := this
    refine ⟨⟨U, hU⟩, ⟨X.basicOpen r, hV.basicOpen r⟩, hrs, (X.basicOpen_le r).trans e, ?_⟩
    rw [← f.appLE_map e (homOfLE (X.basicOpen_le r)).op]
    have : IsLocalization.Away r Γ(X, X.basicOpen r) := hV.isLocalization_basicOpen r
    exact hfs r hr _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case hQi
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
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
this : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q

Tactic:
have : HasRingHomProperty P Q := inst

Goal state after:
case hQi
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
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
this✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case pos
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
x : ↥X
hxU : x ∈ ↑U
⊢ x ∈ I.supportSet ∩ ↑↑U ↔ x ∈ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Tactic:
simp [hxU, mem_supportSet_iff_of_mem hxU]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: 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
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine (Spec R)
hX : IsAffine (Spec S)
φ : R ⟶ S
P : Ideal ↑S
hP : P.IsPrime
H : Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) { asIdeal := P, isPrime := hP }))
⊢ Q (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯)

Tactic:
rwa [hQi.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso φ _)] at H

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (ConcreteCategory.hom (residueFieldMap f ↑x))
      ((ConcreteCategory.hom (Y.evaluation ⟨(ConcreteCategory.hom f.base) ↑x, ⋯⟩)) a) =
    (ConcreteCategory.hom (X.evaluation x)) ((ConcreteCategory.hom (f.c.app (op V))) a)

Tactic:
simpa using! congrFun (congrArg (DFunLike.coe ∘ CommRingCat.Hom.hom) <|
    evaluation_naturality f x) a

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ (ΓSpecIso Γ(X, ↑V)).inv ≫ Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫ X.presheaf.map (homOfLE ⋯).op ≫ Hom.app F ⊤ =
    Hom.app (↑U).ι ↑V ≫ Hom.appLE (F ≫ X.homOfLE ⋯) ((↑U).ι ⁻¹ᵁ ↑V) ⊤ ⋯

Tactic:
simp only [homOfLE_leOfHom, Opens.ι_app, Hom.comp_appLE, homOfLE_app]

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ (ΓSpecIso Γ(X, ↑V)).inv ≫ Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫ X.presheaf.map (homOfLE ⋯).op ≫ Hom.app F ⊤ =
    X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE F (X.homOfLE ⋯ ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V) ⊤ ⋯
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ Spec.map (stalkClosedPointIso R).inv = (Spec R).fromSpecStalk (closedPoint ↑R)

Tactic:
rw [stalkClosedPointIso_inv, Spec.fromSpecStalk_eq']

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Set.range ⇑(pullback.fst f g ≫ f) = Set.range ⇑f ∩ Set.range ⇑g

Tactic:
range_fst_comp

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Set.range ⇑f ∩ Set.range ⇑g = Set.range ⇑f ∩ Set.range ⇑g
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ Set.range ⇑f ⊆ ↑(ker f).support

Tactic:
exact f.range_subset_ker_support

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ ↑(ker f).support = closure (Set.range ⇑f)

Tactic:
apply subset_antisymm
  · wlog hY : ∃ S, Y = Spec S
    · intro x hx
      let 𝒰 := Y.affineCover
      obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
      have inst : QuasiCompact (𝒰.pullbackHom f i) :=
        MorphismProperty.pullback_snd _ _ inferInstance
      have := this (𝒰.pullbackHom f i) ⟨_, rfl⟩
        ((coe_support_inter _ ⟨⊤, isAffineOpen_top _⟩).ge ⟨?_, Set.mem_univ x⟩).1
      · have := image_closure_subset_closure_image (f := 𝒰.f i)
          (𝒰.f i).continuous (Set.mem_image_of_mem _ this)
        rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, 𝒰.pullbackHom_map] at this
        exact closure_mono (Set.range_comp_subset_range _ _) this
      · rw [← (𝒰.f i).isOpenEmbedding.injective.mem_set_image, Scheme.image_zeroLocus,
          ker_ideal_of_isPullback_of_isOpenImmersion f (𝒰.pullbackHom f i)
            ((𝒰.pullback₁ f).f i) (𝒰.f i),
          Ideal.coe_comap, Set.image_preimage_eq]
        · exact ⟨((coe_support_inter _ _).le ⟨hx, by simp⟩).1, ⟨_, rfl⟩⟩
        · exact (ConcreteCategory.bijective_of_isIso ((𝒰.f i).appIso ⊤).inv).2
        · exact (IsPullback.of_hasPullback _ _).flip
    obtain ⟨S, rfl⟩ := hY
    wlog hX : ∃ R, X = Spec R generalizing X S
    · intro x hx
      have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›
      let 𝒰 := X.affineCover.finiteSubcover
      obtain ⟨_, ⟨i, rfl⟩, hx⟩ := (f.iUnion_support_ker_openCover_map_comp 𝒰).ge hx
      have inst : QuasiCompact (𝒰.f i ≫ f) := HasAffineProperty.iff_of_isAffine.mpr
        (inferInstanceAs <| CompactSpace (Spec _))
      exact closure_mono (Set.range_comp_subset_range _ _) (this S (𝒰.f i ≫ f) ⟨_, rfl⟩ hx)
    obtain ⟨R, rfl⟩ := hX
    obtain ⟨φ, rfl⟩ := Spec.map_surjective f
    rw [ker_of_isAffine, coe_support_ofIdealTop, Spec_zeroLocus, ← Ideal.coe_comap,
      RingHom.comap_ker, ← PrimeSpectrum.closure_range_comap, ← CommRingCat.hom_comp,
      ← Scheme.ΓSpecIso_inv_naturality]
    simp only [CommRingCat.hom_comp, PrimeSpectrum.comap_comp]
    exact closure_mono (Set.range_comp_subset_range _ (Spec.map φ))
  · rw [(support _).isClosed.closure_subset_iff]
    exact f.range_subset_ker_support

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case respectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (AffineTargetMorphismProperty.toProperty fun X x x_1 x_2 ↦ IsAffine X).RespectsIso

Tactic:
apply AffineTargetMorphismProperty.respectsIso_mk

Goal state after:
case respectsIso.h₁
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [IsAffine Z], IsAffine Y → IsAffine X

case respectsIso.h₂
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [IsAffine Y], IsAffine X → IsAffine X
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case to_basicOpen
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (r : ↑Γ(Y, ⊤)), IsAffine X → IsAffine ↑(f ⁻¹ᵁ Y.basicOpen r)

Tactic:
intro X Y _ f r H
      have : IsAffine X := H
      change IsAffineOpen _
      rw [Scheme.preimage_basicOpen]
      exact (isAffineOpen_top X).basicOpen _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
this : IsAffine X
a : ↑↑s
⊢ ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
    ∃ (x_4 : IsLocalization.Away (↑a) Rᵣ) (x_5 :
      IsLocalization.Away ((CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ↑a) Sᵣ),
      Q (IsLocalization.Away.map Rᵣ Sᵣ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ↑a)

Tactic:
refine ⟨Γ(Y, Y.basicOpen a.val), Γ(X, X.basicOpen (f.appTop a.val)), inferInstance,
      inferInstance, inferInstance, inferInstance, inferInstance, ?_, ?_⟩

Goal state after:
case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
this : IsAffine X
a : ↑↑s
⊢ IsLocalization.Away ((CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ↑a)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) ↑a))

case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
this : IsAffine X
a : ↑↑s
⊢ Q
    (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen ↑a))
      (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) ↑a))) (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
      ↑a)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
    IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
targetAffineLocally_affineAnd_iff hQi,

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
targetAffineLocally_affineAnd_iff hQi,

Goal state after:
case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔ ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))