mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⨆ f, X.basicOpen ↑f = U ↔ ⇑hU.fromSpec ⁻¹' (⨆ f, X.basicOpen ↑f).carrier = ⇑hU.fromSpec ⁻¹' U.carrier

pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑hU.fromSpec ⁻¹' (⨆ f, X.basicOpen ↑f).carrier = ⇑hU.fromSpec ⁻¹' U.carrier ↔
    ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ

Tactic:
· refine ⟨fun h => by rw [h], ?_⟩
      intro h
      apply_fun Set.image hU.fromSpec at h
      rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.range_fromSpec]
        at h
      simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h
      ext1
      refine Set.Subset.antisymm ?_ h
      simp only [Set.iUnion_subset_iff, SetCoe.forall, Opens.coe_iSup]
      intro x _
      exact X.basicOpen_le x

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑hU.fromSpec ⁻¹' (⨆ f, X.basicOpen ↑f).carrier = ⇑hU.fromSpec ⁻¹' U.carrier ↔
    ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
x : ↥X
hx : x ∈ ↑V
⊢ x ∈ ⨆ f_1, X.basicOpen ↑f_1

Tactic:
iSup_range',

Goal state after:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
x : ↥X
hx : x ∈ ↑V
⊢ x ∈ ⨆ i, X.basicOpen (f i)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).c.app (op U) ≫
      (D.t' j k i).c.app
          (op (unop (op ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 (unop (op U)))))) ≫
        invApp (pullback.fst (D.f j k) (D.f j i))
            ((Opens.map (D.t' j k i).base).1
              (unop (op ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 (unop (op U)))))) ≫
          (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
            ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
              (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
← PresheafedSpace.comp_c_app_assoc

Goal state after:
case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).c.app (op U) ≫
      invApp (pullback.fst (D.f j k) (D.f j i))
          ((Opens.map (D.t' j k i).base).1
            (unop (op ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 (unop (op U)))))) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
          ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case hprecomp
P : AffineTargetMorphismProperty
h₁ : ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], P f → P (e.hom ≫ f)
h₂ : ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], P f → P (f ≫ e.hom)
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z), P.toProperty f → P.toProperty (e.hom ≫ f)

Tactic:
rintro X Y Z e f ⟨a, h⟩; exact ⟨a, h₁ e f h⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ pullback.snd fWX (𝒰.f i) ≫ 𝒰.f i ≫ fXZ = (pullback.fst fWX (𝒰.f i) ≫ fWY) ≫ fYZ

Tactic:
simp [← h]

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := ⋯
⊢ Q (pullback.snd f (𝟙 Y)) ↔ Q f

Tactic:
rw [← Category.comp_id (pullback.snd _ _), ← pullback.condition,
    Q.cancel_left_of_respectsIso]

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

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
⊢ P.diagonal.toProperty.RespectsIso

Tactic:
delta AffineTargetMorphismProperty.diagonal

Goal state after:
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
⊢ (toProperty fun {X x} f x_1 ↦
      ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
        [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ f)).RespectsIso
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : DenseRange ⇑(f ≫ g)
inst✝ : IsOpenImmersion g
⊢ DenseRange ⇑f

Tactic:
DenseRange

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : Dense (Set.range ⇑(f ≫ g))
inst✝ : IsOpenImmersion g
⊢ Dense (Set.range ⇑f)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case mp
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
    ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

Tactic:
intro ⟨s, hsone, hs⟩
    obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hsone
    exact ⟨s', h₂, fun t ht ↦ hs t (h₁ ht)⟩

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f ↔
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
            P ((algebraMap S Sₜ).comp f)

Tactic:
rw [locally_iff_finite P f]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
⊢ (∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)) ↔
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
            P ((algebraMap S Sₜ).comp f)
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
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
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)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (e a) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (e a)) e ⋯
⊢ P ((algebraMap T (Localization.Away (e a))).comp (e.toRingHom.comp f))

Tactic:
have : (algebraMap T (Localization.Away (e a))).comp e.toRingHom =
          e'.toRingHom.comp (algebraMap S (Localization.Away a)) := by
        ext x
        simp [e']

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
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
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)
a : S
ha : a ∈ s
e' : Localization.Away a ≃+* Localization.Away (e a) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (e a)) e ⋯
this :
  (algebraMap T (Localization.Away (e a))).comp e.toRingHom = e'.toRingHom.comp (algebraMap S (Localization.Away a))
⊢ P ((algebraMap T (Localization.Away (e a))).comp (e.toRingHom.comp f))
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (IsLocalization.map (Localization.Away (f ↑r)) f ⋯)
      (IsLocalization.mk' (Localization.Away ↑r) b ⟨(fun x ↦ ↑r ^ x) n, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) x
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range

Tactic:
IsLocalization.map_mk',

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  IsLocalization.mk' (Localization.Away (f ↑r)) (f b) ⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩ =
    (algebraMap S (Localization.Away (f ↑r))) x
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range
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)
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))

Tactic:
simp only [this, a']

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 ((Localization.awayMap g' ↑a).comp ((algebraMap S (Localization.Away ↑a)).comp f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y) {ι : Type u} (U : ι → Opens X),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P (f ∘ Subtype.val))
⊢ IsZariskiLocalAtSource (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P)

Tactic:
refine topologically_isZariskiLocalAtSource P ?_ (fun f hf _ U hU hf' ↦ (hP f U hU hf).mpr hf')
  introv hf hs
  refine (hP f (![⊤, U] ∘ Equiv.ulift) ?_ hf).mp hs ⟨1⟩
  rw [IsOpenCover, ← top_le_iff]
  exact le_iSup (![⊤, U] ∘ Equiv.ulift) ⟨0⟩

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

Goal state before:
pp: case hb'
X : Scheme
U : Set ↥X
⊢ ∀ (i : ↑X.affineOpens), IsCompact ↑↑i

Tactic:
· exact fun i => i.2.isCompact

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

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ AffineTargetMorphismProperty.diagonal (fun X x x_1 x_2 ↦ CompactSpace ↥X) f ↔ QuasiSeparatedSpace ↥X

Tactic:
delta AffineTargetMorphismProperty.diagonal

Goal state after:
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯) ↔
    QuasiSeparatedSpace ↥X
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
x : ↑Γ(X, X.basicOpen f)
⊢ ∃ n y, (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x

Tactic:
have := (hU.isLocalization_basicOpen f).1.2

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
x : ↑Γ(X, X.basicOpen f)
this :
  ∀ (z : ↑Γ(X, X.basicOpen f)),
    ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1
⊢ ∃ n y, (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case refine_2
R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃p : Ideal R⦄, p.IsPrime → ↑p.height ≤ n
p : PrimeSpectrum R
⊢ ↑(Order.height p) ≤ n

Tactic:
specialize h p.2

Goal state after:
case refine_2
R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
p : PrimeSpectrum R
h : ↑p.asIdeal.height ≤ n
⊢ ↑(Order.height p) ≤ n
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
h1 : p.height = 1
x : R
hx : x ∈ p
hxp : Prime x
⊢ p = span {x}

Tactic:
have : (span {x}).IsPrime := by simp [span_singleton_prime hxp.ne_zero, hxp]
  have : p.FiniteHeight := by simp [p.finiteHeight_iff, h1]
  by_contra! hne
  apply hxp.ne_zero
  rw [← span_singleton_eq_bot, ← height_eq_zero_iff_eq_bot, ← Order.lt_one_iff, ← h1]
  refine height_strict_mono_of_isPrime_of_isPrime (lt_of_le_of_ne ?_ hne.symm)
  simp only [p.span_singleton_le_iff_mem, hx]

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

Goal state before:
pp: case mp
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H✝ : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
H : Set.range ⇑(Spec.map φ) = Set.range ⇑(Spec.map f)
⊢ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

Tactic:
let i : S ≅ .of _ := (Scheme.Spec.preimageIso
      (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop

Goal state after:
case mp
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H✝ : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
H : Set.range ⇑(Spec.map φ) = Set.range ⇑(Spec.map f)
i : S ≅ CommRingCat.of (↑R ⧸ Ideal.span {e}) :=
  (Scheme.Spec.preimageIso (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
⊢ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}
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
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
⊢ P f ↔ ∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
by
  have := respects_isOpenImmersion (P := P)
    (RingHom.locally_stableUnderCompositionWithLocalizationAwaySource hQ)
  refine ⟨fun hf x ↦ ?_,
      fun hf ↦ (IsZariskiLocalAtSource.iff_exists_resLE (P := P)).mpr <| fun x ↦ ?_⟩
  · 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 _
  · obtain ⟨U, V, hxV, e, hf⟩ := hf x
    use U, V, hxV, e
    simp only [iff_of_isAffine (P := P), Scheme.Hom.appLE, homOfLE_leOfHom] at hf ⊢
    have : (toMorphismProperty (Locally Q)).RespectsIso := toMorphismProperty_respectsIso_iff.mp <|
      (isLocal_ringHomProperty P).respectsIso
    exact (MorphismProperty.arrow_mk_iso_iff (toMorphismProperty (Locally Q))
      (arrowResLEAppIso f U V e)).mpr (locally_of hQi _ hf)

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

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
⊢ (I ⊔ J).radical = (I.radical ⊔ J.radical).radical

Tactic:
ext U : 2
  exact (Ideal.radical_sup (I.ideal U) (J.ideal U))

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

Goal state before:
pp: case refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑U ∩ ↑(X.basicOpen ↑i))

pp: case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑V ∩ ↑(X.basicOpen ↑i))

Tactic:
· rw [← Opens.coe_inf, ← X.basicOpen_res _ (homOfLE le_top).op]
    exact (U.2.basicOpen _).isCompact

Goal state after:
case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑V ∩ ↑(X.basicOpen ↑i))
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ IsEmpty ↥(pullback f g) → Disjoint (Set.range ⇑f) (Set.range ⇑g)

Tactic:
rw [Set.disjoint_iff_forall_ne]

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ IsEmpty ↥(pullback f g) → ∀ ⦃a : ↥S⦄, a ∈ Set.range ⇑f → ∀ ⦃b : ↥S⦄, b ∈ Set.range ⇑g → a ≠ b
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

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

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.toSpecΓ ⁻¹ᵁ ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩)

pp: case refine_4
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ IsIso (Scheme.Hom.appTop (X.toSpecΓ ∣_ ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩))

Tactic:
· rw [PrimeSpectrum.iSup_basicOpen_eq_top_iff, Subtype.range_coe_subtype, Set.ofPred_mem_eq, hs]

Goal state after:
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.toSpecΓ ⁻¹ᵁ ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩)

case refine_4
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ IsIso (Scheme.Hom.appTop (X.toSpecΓ ∣_ ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩))