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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
⊢ ∀ (g : S →+* T),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) g →
        (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) (g.comp f)

Tactic:
g

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) g →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) (g.comp f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y} f U ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
i : ι
⊢ P (pullback.diagonal ((U i).ι ≫ f) ≫ pullback.map ((U i).ι ≫ f) ((U i).ι ≫ f) f f (U i).ι (U i).ι (𝟙 Y) ⋯ ⋯)

Tactic:
exact RespectsRight.postcomp (P := P) (Q := @IsOpenImmersion) (g _ _) inferInstance _ (hf i)

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
⊢ IsZariskiLocalAtSource P.diagonal

Tactic:
by
  let g {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) :=
    pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) (by simp) (by simp)
  refine IsZariskiLocalAtSource.mk' (fun {X Y} f U hf ↦ ?_) (fun {X Y} f {ι} U hU hf ↦ ?_)
  · change P _
    apply P.of_postcomp (W' := @IsOpenImmersion) (pullback.diagonal (U.ι ≫ f)) (g f U) inferInstance
    rw [← pullback.comp_diagonal]
    apply IsZariskiLocalAtSource.comp
    exact hf
  · change P _
    refine IsZariskiLocalAtSource.of_iSup_eq_top U hU fun i ↦ ?_
    rw [pullback.comp_diagonal]
    exact RespectsRight.postcomp (P := P) (Q := @IsOpenImmersion) (g _ _) inferInstance _ (hf i)

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)).comp g
a' : Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)) (g ↑a)
⊢ P
    ((algebraMap T
          ((fun x ↦
              match x with
              | (a, b) => Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))
            (a, b))).comp
      (g.comp f))

Tactic:
have : (algebraMap T <| Localization.Away a').comp (g.comp f) =
        (Localization.awayMap g' a.val).comp ((algebraMap S (Localization.Away a.val)).comp f) := by
      ext x
      simp only [coe_comp, Function.comp_apply, a']
      change _ = Localization.awayMap g' a.val (algebraMap S _ (f x))
      simp only [Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_eq]
      rfl

Goal state after:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)).comp g
a' : Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)) (g ↑a)
this :
  (algebraMap T (Localization.Away a')).comp (g.comp f) =
    (Localization.awayMap g' ↑a).comp ((algebraMap S (Localization.Away ↑a)).comp f)
⊢ P
    ((algebraMap T
          ((fun x ↦
              match x with
              | (a, b) => Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))
            (a, b))).comp
      (g.comp f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
T : Scheme
⊢ ∀ (f_1 : T ⟶ Y) [inst : HasPullback f_1 (𝒰.f i ≫ f)], P (pullback.fst f_1 (𝒰.f i ≫ f))

Tactic:
g

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
T : Scheme
g : T ⟶ Y
⊢ ∀ [inst : HasPullback g (𝒰.f i ≫ f)], P (pullback.fst g (𝒰.f i ≫ f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
T : Scheme
⊢ ∀ (f_1 : T ⟶ Y) [inst : HasPullback f_1 f], P (pullback.fst f_1 f)

Tactic:
g

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
T : Scheme
g : T ⟶ Y
⊢ ∀ [inst : HasPullback g f], P (pullback.fst g f)
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: case e'_5.fst
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑B := (CommRingCat.Hom.hom ψ).toAlgebra
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ ((pullbackSpecIso ↑R ↑A ↑B).inv ≫ pullback.fst (Spec.map φ) (Spec.map ψ) ≫ iX) x =
    (Prod.map (⇑iX) (⇑iY)
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B) ((𝟙 (Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))) x))).1

Tactic:
pullbackSpecIso_inv_fst_assoc

Goal state after:
case e'_5.fst
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑B := (CommRingCat.Hom.hom ψ).toAlgebra
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ (Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom) ≫ iX) x =
    (Prod.map (⇑iX) (⇑iY)
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B) ((𝟙 (Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))) x))).1
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
⊢ ∀ (g : Y ⟶ S), CompactSpace ↥Y → CompactSpace ↥(pullback f g)

Tactic:
g

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
⊢ CompactSpace ↥Y → CompactSpace ↥(pullback f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case inr
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (⇑f '' Z)
this✝ :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X),
    IsClosed Z → StableUnderSpecialization (⇑f '' Z) → (∃ R, X = Spec R) → IsClosed (⇑f '' Z)
hX : ¬∃ R, X = Spec R
R : CommRingCat
g : Spec R ⟶ X
hg : Function.Surjective ⇑g
inst : QuasiCompact (g ≫ f)
this :
  StableUnderSpecialization ((fun a ↦ (ConcreteCategory.hom (g.base ≫ f.base)) a) '' ⇑g ⁻¹' Z) →
    (∃ R_1, Spec R = Spec R_1) → IsClosed ((fun a ↦ (ConcreteCategory.hom (g.base ≫ f.base)) a) '' ⇑g ⁻¹' Z)
⊢ IsClosed (⇑f '' Z)

Tactic:
TopCat.comp_app,

Goal state after:
case inr
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (⇑f '' Z)
this✝ :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X),
    IsClosed Z → StableUnderSpecialization (⇑f '' Z) → (∃ R, X = Spec R) → IsClosed (⇑f '' Z)
hX : ¬∃ R, X = Spec R
R : CommRingCat
g : Spec R ⟶ X
hg : Function.Surjective ⇑g
inst : QuasiCompact (g ≫ f)
this :
  StableUnderSpecialization ((fun a ↦ f (g a)) '' ⇑g ⁻¹' Z) →
    (∃ R_1, Spec R = Spec R_1) → IsClosed ((fun a ↦ f (g a)) '' ⇑g ⁻¹' Z)
⊢ IsClosed (⇑f '' Z)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ↑(⨆ I, ⨆ (x : I.IsPrime), I.primeHeight) = ringKrullDim R

Tactic:
by
  simp [← Ideal.height_eq_primeHeight, Ideal.sup_isPrime_height_eq_ringKrullDim]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (s ^ n) = (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)) 0
V : Opens ↥X
hxV : x ∈ V
iU iV : V ⟶ U
e' : (ConcreteCategory.hom (X.presheaf.map iU.op)) s ^ n = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s = 0

Tactic:
replace e' := (IsNilpotent.mk _ _ e').eq_zero (R := Γ(X, V))

Goal state after:
X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (s ^ n) = (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)) 0
V : Opens ↥X
hxV : x ∈ V
iU iV : V ⟶ U
e' : (ConcreteCategory.hom (X.presheaf.map iU.op)) s = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s = 0
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 Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
⊢ ∀ (g : Y ⟶ S),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (pullback.fst f g)

Tactic:
g

Goal state after:
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 Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
⊢ sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (pullback.fst f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := ⋯
⊢ (fun x ↦ U.ι ''ᵁ x) (⨆ i, U.ι ⁻¹ᵁ ↑i) = (fun x ↦ U.ι ''ᵁ x) ⊤

Tactic:
simp only [U.ι.image_iSup, U.ι.image_preimage_eq_opensRange_inf, Scheme.Opens.opensRange_ι]

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ ⨆ i, U ⊓ ↑i = U.ι ''ᵁ ⊤
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
hQl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQa : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
this :
  HasRingHomProperty
    (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q)
    fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))) ↔
    affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
iff_exists_appLE_locally (P := affineLocally (Locally Q)) hQa.left hQa.respectsIso

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQa : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
this :
  HasRingHomProperty
    (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q)
    fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))) ↔
    ∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
h : IsIso (Spec.map f)
⊢ isomorphisms CommRingCat f

Tactic:
(isomorphisms _).arrow_mk_iso_iff (arrowIsoΓSpecOfIsAffine f),

Goal state after:
R S : CommRingCat
f : R ⟶ S
h : IsIso (Spec.map f)
⊢ isomorphisms CommRingCat (Scheme.Hom.appTop (Spec.map f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case refine_3
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ IsAffine ↑(X.basicOpen ↑i)

Tactic:
exact hs₂ _ i.2

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this✝ : IsIso (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V =
    I.glueData.ι U
⊢ I.glueDataObjMap h ≫ I.glueData.ι V = I.glueData.ι U

Tactic:
← Category.id_comp (I.glueData.ι U),

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this✝ : IsIso (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V =
    I.glueData.ι U
⊢ I.glueDataObjMap h ≫ I.glueData.ι V = 𝟙 (I.glueData.U U) ≫ I.glueData.ι U
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ IsAffine X

Tactic:
constructor
    · apply AffineTargetMorphismProperty.respectsIso_mk
      · rintro X Y Z e _ _ H
        have : IsAffine _ := H
        exact .of_isIso e.hom
      · exact fun _ _ _ ↦ id
    · intro X Y _ f r H
      have : IsAffine X := H
      change IsAffineOpen _
      rw [Scheme.preimage_basicOpen]
      exact (isAffineOpen_top X).basicOpen _
    · intro X Y _ f S hS hS'
      apply_fun Ideal.map (f.appTop).hom at hS
      rw [Ideal.map_span, Ideal.map_top] at hS
      apply isAffine_of_isAffineOpen_basicOpen _ hS
      have : ∀ i : S, IsAffineOpen (f ⁻¹ᵁ Y.basicOpen i.1) := hS'
      simpa [Scheme.preimage_basicOpen] using! this

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↥Y → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ IsAffineHom f

Tactic:
HasAffineProperty.iff_of_iSup_eq_top (P := @IsAffineHom) fun i ↦ ⟨U i, hU i⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↥Y → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ∀ (i : ↥Y), IsAffine ↑(f ⁻¹ᵁ ↑⟨U i, ⋯⟩)

X Y : Scheme
f : X ⟶ Y
U : ↥Y → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ⨆ i, ↑⟨U i, ⋯⟩ = ⊤
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Epi (pullbackComparison forgetToTop f g)

Tactic:
refine (CategoryTheory.forget TopCat).epi_of_epi_map ?_
  rw [← CategoryTheory.epi_comp_iff_of_isIso _
    (pullbackComparison (CategoryTheory.forget TopCat) (forgetToTop.map f) (forgetToTop.map g)),
    ← _root_.CategoryTheory.Limits.pullbackComparison_comp, epi_iff_surjective]
  apply Scheme.pullbackComparison_forget_surjective _ _

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
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
⊢ ∀ (g : Y ⟶ S),
    affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) (Limits.pullback.fst f g)

Tactic:
g

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
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
    affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) (Limits.pullback.fst f g)
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
h : ¬l i = 0
⊢ l i ∈ ↑(s.attach.biUnion sf ∪ s) ∪ ↑(Finset.image (⇑l) l.support)

Tactic:
Finset.coe_image

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
h : ¬l i = 0
⊢ l i ∈ ↑(s.attach.biUnion sf ∪ s) ∪ ⇑l '' ↑l.support
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q✝ Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hZ : IsAffine Z
hg : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) g
⊢ P (f ≫ g)

Tactic:
obtain ⟨hY, hg⟩ := hg

Goal state after:
Q✝ Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hZ : IsAffine Z
hY : IsAffine Y
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P (f ≫ g)