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

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
t : S
inst✝ : IsLocalization.Away t T
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)
⊢ Ideal.map (algebraMap S T) ⊤ = ⊤

Tactic:
Ideal.map_top

Goal state after:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
t : S
inst✝ : IsLocalization.Away t T
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)
⊢ ⊤ = ⊤
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_1
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)
⊢ Ideal.map (algebraMap S S') ⊤ = ⊤

Tactic:
Ideal.map_top

Goal state after:
case refine_1
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)
⊢ ⊤ = ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P
    ((CommRingCat.Hom.hom
          (Scheme.Hom.appTop
            (PreservesPullback.iso AffineScheme.forgetToScheme (AffineScheme.ofHom f) (AffineScheme.ofHom g)).inv)).comp
      (CommRingCat.Hom.hom
        (Scheme.Hom.appTop
          (AffineScheme.forgetToScheme.map (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g))))))

Tactic:
hP'.cancel_right_isIso,

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P
    (CommRingCat.Hom.hom
      (Scheme.Hom.appTop
        (AffineScheme.forgetToScheme.map (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)))))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
this :
  (pullback.fst (Scheme.Hom.appTop (AffineScheme.ofHom f).hom).op
          (Scheme.Hom.appTop (AffineScheme.ofHom g).hom).op).unop ≫
      (PreservesPullback.iso (AffineScheme.forgetToScheme.op ⋙ Scheme.Γ).rightOp (AffineScheme.ofHom f)
            (AffineScheme.ofHom g)).hom.unop =
    Scheme.Hom.appTop (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)).hom
⊢ P
    ((CommRingCat.Hom.hom
          (PreservesPullback.iso (AffineScheme.forgetToScheme.op ⋙ Scheme.Γ).rightOp (AffineScheme.ofHom f)
                (AffineScheme.ofHom g)).hom.unop).comp
      (CommRingCat.Hom.hom
        (pullback.fst (Scheme.Hom.appTop (AffineScheme.ofHom f).hom).op
            (Scheme.Hom.appTop (AffineScheme.ofHom g).hom).op).unop))

Tactic:
hP'.cancel_right_isIso,

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
this :
  (pullback.fst (Scheme.Hom.appTop (AffineScheme.ofHom f).hom).op
          (Scheme.Hom.appTop (AffineScheme.ofHom g).hom).op).unop ≫
      (PreservesPullback.iso (AffineScheme.forgetToScheme.op ⋙ Scheme.Γ).rightOp (AffineScheme.ofHom f)
            (AffineScheme.ofHom g)).hom.unop =
    Scheme.Hom.appTop (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)).hom
⊢ P
    (CommRingCat.Hom.hom
      (pullback.fst (Scheme.Hom.appTop (AffineScheme.ofHom f).hom).op
          (Scheme.Hom.appTop (AffineScheme.ofHom g).hom).op).unop)
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: 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
⊢ ∀ (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y) (iS : Spec R ⟶ S)
    (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))

Tactic:
f'

Goal state after:
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
f' : Spec A ⟶ Spec R
⊢ ∀ (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y) (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f)
    (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) 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)
Mₐ : (a : ↑s) → Submonoid (Localization.Away ↑a) :=
  fun a ↦ Submonoid.map (algebraMap S (Localization.Away ↑a)) (Submonoid.map f M)
Sₐ : ↑s → Type u := fun a ↦ Localization (Mₐ a)
hM : ∀ (a : ↑s), Submonoid.map ((algebraMap S (Localization.Away ↑a)).comp f) M = Mₐ a
this✝² : ∀ (a : ↑s), IsLocalization (Submonoid.map ((algebraMap S (Localization.Away ↑a)).comp f) M) (Sₐ a)
this✝¹ : ∀ (a : ↑s), IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f M)) (Sₐ 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)
⊢ Ideal.map (algebraMap S S') ⊤ = ⊤

Tactic:
Ideal.map_top

Goal state after:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) 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)
Mₐ : (a : ↑s) → Submonoid (Localization.Away ↑a) :=
  fun a ↦ Submonoid.map (algebraMap S (Localization.Away ↑a)) (Submonoid.map f M)
Sₐ : ↑s → Type u := fun a ↦ Localization (Mₐ a)
hM : ∀ (a : ↑s), Submonoid.map ((algebraMap S (Localization.Away ↑a)).comp f) M = Mₐ a
this✝² : ∀ (a : ↑s), IsLocalization (Submonoid.map ((algebraMap S (Localization.Away ↑a)).comp f) M) (Sₐ a)
this✝¹ : ∀ (a : ↑s), IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f M)) (Sₐ 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)
⊢ ⊤ = ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top
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 := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
intro X Y f ι U hU hf x
    have hy : x ∈ iSup U := by rw [hU]; trivial
    obtain ⟨i, hi⟩ := Opens.mem_iSup.mp hy
    rw [← hP.cancel_right_isIso _ ((U i).ι.stalkMap ⟨x, hi⟩)]
    simpa [Scheme.Hom.stalkMap_comp] using hf i ⟨x, hi⟩

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
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
introv R hf
  obtain ⟨s, hsone, hs⟩ := hf
  rw [locally_iff_exists hPl.away.respectsIso]
  let Mₐ (a : s) : Submonoid (Localization.Away a.val) :=
    (M.map f).map (algebraMap S (Localization.Away a.val))
  let Sₐ (a : s) := Localization (Mₐ a)
  have hM (a : s) : M.map ((algebraMap S (Localization.Away a.val)).comp f) = Mₐ a :=
    (M.map_map _ _).symm
  have (a : s) :
      IsLocalization (M.map ((algebraMap S (Localization.Away a.val)).comp f)) (Sₐ a) := by
    rw [hM]
    infer_instance
  have (a : s) :
      IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away a.val) (M.map f)) (Sₐ a) :=
    inferInstanceAs <| IsLocalization (Mₐ a) (Sₐ a)
  let (a : s) : Algebra S' (Sₐ a) :=
    (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away a.val))
      (M.map f).le_comap_map).toAlgebra
  have (a : s) : IsScalarTower S S' (Sₐ a) :=
    IsScalarTower.of_algebraMap_eq' (IsLocalization.map_comp (M.map f).le_comap_map).symm
  refine ⟨s, fun a ↦ algebraMap S S' a.val, ?_, Sₐ,
      inferInstance, inferInstance, fun a ↦ ?_, fun a ↦ ?_⟩
  · rw [← Set.image_eq_range, ← Ideal.map_span, hsone, Ideal.map_top]
  · convert!
    IsLocalization.commutes (T := Sₐ a) (M₁ := M.map f) (S₁ := S') (S₂ := Localization.Away a.val)
      (M₂ := Submonoid.powers a.val)
    simp [Algebra.algebraMapSubmonoid]
  · rw [algebraMap_toAlgebra, IsLocalization.map_comp_map]
    apply hPl
    exact hs a.val a.property

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↥Y
a✝ : IsOpen U
hU' : IsCompact U
⊢ IsCompact (⇑f ⁻¹' U)

Tactic:
convert! hU'.image (inv f.base).hom.continuous_toFun using 1

Goal state after:
case e'_3
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↥Y
a✝ : IsOpen U
hU' : IsCompact U
⊢ ⇑f ⁻¹' U = (TopCat.Hom.hom (inv f.base)).toFun '' U
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mpr.refine_2.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S✝ : X.Opens
x✝¹ : IsCompact S✝.carrier
V : ↑X.affineOpens
S : X.Opens
x✝ : IsCompact S.carrier
W : ↑X.affineOpens
hW : IsCompact (S.carrier ∩ ↑↑V)
⊢ IsCompact (S.carrier ∩ ↑↑V ∪ ↑↑W ∩ ↑↑V)

Tactic:
apply hW.union

Goal state after:
case mpr.refine_2.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S✝ : X.Opens
x✝¹ : IsCompact S✝.carrier
V : ↑X.affineOpens
S : X.Opens
x✝ : IsCompact S.carrier
W : ↑X.affineOpens
hW : IsCompact (S.carrier ∩ ↑↑V)
⊢ IsCompact (↑↑W ∩ ↑↑V)
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
⊢ Set.range ⇑f ⊆ Set.range ⇑U.ι

Tactic:
by simp [hf]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
e : R ≃+* S
I : Ideal S
⊢ (comap e I).height = I.height

Tactic:
refine (Equiv.iInf_congr e.idealComapOrderIso fun J ↦ (Equiv.iInf_congr ?_ fun h ↦ ?_).symm).symm

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
e : R ≃+* S
I J : Ideal S
⊢ J ∈ I.minimalPrimes ≃ ↑e.idealComapOrderIso J ∈ (comap e I).minimalPrimes

case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
e : R ≃+* S
I J : Ideal S
h : J ∈ I.minimalPrimes
⊢ (↑e.idealComapOrderIso J).primeHeight = J.primeHeight
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case refine_1
R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
h : ∀ (i : PrimeSpectrum R), ↑(Order.height i) ≤ n
p : Ideal R
hp : p.IsPrime
⊢ ↑p.primeHeight ≤ n

Tactic:
exact h ⟨p, hp⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ↑(⨆ I, ⨆ (_ : I ≠ ⊤), I.height) = ringKrullDim R

Tactic:
by
  apply le_antisymm
  · rw [WithBot.coe_iSup ⟨⊤, fun _ _ => le_top⟩]
    refine iSup_le fun I => ?_
    by_cases h : I = ⊤
    · simp [h, ringKrullDim_nonneg_of_nontrivial]
    · simp [h, height_le_ringKrullDim_of_ne_top]
  · refine iSup_le fun p => WithBot.coe_le_coe.mpr (le_trans (b := p.last.asIdeal.height) ?_ ?_)
    · rw [height_eq_primeHeight]
      apply le_trans (b := ⨆ (_ : p.last ≤ p.last), ↑p.length)
      · exact le_iSup (fun _ => (↑p.length : ℕ∞)) le_rfl
      · exact le_iSup (fun p' => (⨆ _, p'.length : ℕ∞)) p
    · apply le_trans (b := ⨆ (_ : (p.last).asIdeal ≠ ⊤), p.last.asIdeal.height)
      · exact le_iSup_of_le p.last.isPrime.ne_top' le_rfl
      · exact le_iSup (fun I => ⨆ _, I.height) p.last.asIdeal

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.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
⊢ P (f ≫ g)

Tactic:
wlog hZ : IsAffine Z generalizing X Y Z
    · rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
      intro U
      rw [morphismRestrict_comp]
      exact this _ _ (IsZariskiLocalAtTarget.restrict hf _)
        (IsZariskiLocalAtTarget.restrict hg _) U.2
    wlog hY : IsAffine Y generalizing X Y
    · rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (Y.affineCover.pullback₁ f)]
      intro i
      rw [← Scheme.Cover.pullbackHom_map_assoc]
      exact this _ _ (IsZariskiLocalAtTarget.of_isPullback (.of_hasPullback _ _) hf)
        (comp_of_isOpenImmersion _ _ _ hg) inferInstance
    wlog hX : IsAffine X generalizing X
    · rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) X.affineCover]
      intro i
      rw [← Category.assoc]
      exact this _ (comp_of_isOpenImmersion _ _ _ hf) inferInstance
    rw [iff_of_isAffine (P := P)] at hf hg ⊢
    exact hP _ _ hg hf

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↥X
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this :
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (X.basicOpen g) x ⋯))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (X.basicOpen g) x ⋯))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal V))
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)

Tactic:
simp only [Ideal.map_map, ← CommRingCat.hom_comp, affineBasicOpen_coe, X.presheaf.germ_res]
    at this ⊢

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↥X
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this :
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x ⋯)) (I.ideal U) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑V) x ⋯)) (I.ideal V)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op ≫ X.presheaf.germ (↑U) x hxU)) (I.ideal V) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
⊢ Antitone support

Tactic:
intro I J h
  rw [← SetLike.coe_subset_coe, I.coe_support_eq_eq_iInter_zeroLocus,
    J.coe_support_eq_eq_iInter_zeroLocus]
  exact Set.iInter_mono fun U ↦ X.zeroLocus_mono (h U)

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

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

Tactic:
isomorphisms.iff

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

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

Tactic:
ext U : 2
  simp only [radical_ideal, ideal_mul, Pi.mul_apply, Ideal.radical_mul, ideal_inf, Pi.inf_apply]

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

Goal state before:
pp: case inr.refine_1
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
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme},
    IsAffine Y →
      ∀ {X : Scheme} {f : X ⟶ Y},
        (∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) →
          IsAffine X → (∃ R S, Y = Spec R ∧ X = Spec S) → P f
hXY : ¬∃ R S, Y = Spec R ∧ X = Spec S
x : ↥(Spec Γ(X, ⊤))
⊢ Q
    ((CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv x))).comp
      (CommRingCat.Hom.hom (Scheme.Hom.stalkMap Y.isoSpec.hom (f (X.isoSpec.inv x)))))

Tactic:
hQi.cancel_left_isIso

Goal state after:
case inr.refine_1
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
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme},
    IsAffine Y →
      ∀ {X : Scheme} {f : X ⟶ Y},
        (∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) →
          IsAffine X → (∃ R S, Y = Spec R ∧ X = Spec S) → P f
hXY : ¬∃ R S, Y = Spec R ∧ X = Spec S
x : ↥(Spec Γ(X, ⊤))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv x)))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(IsAffineOpen.fromSpec ⋯) '' ⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑I.support =
    ⇑(IsAffineOpen.fromSpec ⋯) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
rw [Set.image_preimage_eq_inter_range, IsAffineOpen.range_fromSpec,
    IsAffineOpen.fromSpec_image_zeroLocus, coe_support_inter]

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

Goal state before:
pp: case hs
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ Ideal.map (CommRingCat.Hom.hom U.topIso.inv) ⊤ = ⊤

Tactic:
Ideal.map_top

Goal state after:
case hs
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ ⊤ = ⊤