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

Goal state before:
pp: case right
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
x : ↥(∐ f)
⊢ IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)

Tactic:
have ⟨y, hy⟩ := (Scheme.IsLocallyDirected.openCover (Discrete.functor f)).covers x

Goal state after:
case right
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
x : ↥(∐ f)
y :
  ↥((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).X
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
hy :
  ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
this✝ : IsOpenImmersion (Sigma.desc f)
x : ↥S
hx : x ∈ ⊤
this : x ∈ ⨆ i, Scheme.Hom.opensRange (f i)
⊢ ?m.101

Tactic:
simpa only [Opens.iSup_mk, Opens.mem_mk, Set.mem_iUnion] using this

Goal state after:
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 ⋯) =
    D.opensImagePreimageMap i k U ≫
      (D.f k j).c.app (op ((Opens.map (D.ι k).base).obj (⋯.functor.obj U))) ≫
        (D.t j k).c.app ((Opens.map (D.f k j).base).op.obj (op ((Opens.map (D.ι k).base).obj (⋯.functor.obj U)))) ≫
          (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
opensImagePreimageMap_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 ⋯) =
    (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).c.app (op U) ≫
      invApp (pullback.snd (D.f k i) (D.f k j))
          (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 (k, j)).presheaf.map (eqToHom ⋯) ≫
          (D.t j k).c.app ((Opens.map (D.f k j).base).op.obj (op ((Opens.map (D.ι k).base).obj (⋯.functor.obj U)))) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨l, fi, fj, fk, α, z, hα, hα₁, hα₂, e⟩ := this

Goal state after:
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f j k) (D.f j i)).c.app
        (op
          ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
            ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U))) ≫
      (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
        ((TopCat.Presheaf.pushforward C (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).obj
                (pullback (D.f j k) (D.f j i)).presheaf).map
            (eqToHom ⋯) ≫
          (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
            invApp (pullback.fst (D.f j k) (D.f j i))
                ((Opens.map (D.t' j k i).base).1
                  ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 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:
comp_base,

Goal state after:
case e_a
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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f j k) (D.f j i)).c.app
        (op
          ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
            ((Opens.map ((pullback.fst (D.f j i) (D.f j k)).base ≫ (D.t j i).base ≫ (D.f i j).base)).1 U))) ≫
      (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
        ((TopCat.Presheaf.pushforward C (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).obj
                (pullback (D.f j k) (D.f j i)).presheaf).map
            (eqToHom ⋯) ≫
          (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
            invApp (pullback.fst (D.f j k) (D.f j i))
                ((Opens.map (D.t' j k i).base).1
                  ((Opens.map ((pullback.fst (D.f k i) (D.f k j)).base ≫ (D.t k i).base ≫ (D.f i k).base)).1 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.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
⊢ { l //
    l ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt},
          m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).snd = s.snd → m = l }

Tactic:
refine ⟨gluedLift 𝒰 f g s, gluedLift_p1 𝒰 f g s, gluedLift_p2 𝒰 f g s, ?_⟩

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
⊢ ∀ {m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt},
    m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).fst = s.fst →
      m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).snd = s.snd → m = gluedLift 𝒰 f g s
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P f

Tactic:
· refine of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange <| .ulift 𝒰) fun i ↦ ?_
    dsimp
    rw [← IsOpenImmersion.isoOfRangeEq_inv_fac (𝒰.f _) (Scheme.Opens.ι _)
      (congr_arg Opens.carrier (𝒰.f _).opensRange.opensRange_ι.symm), Category.assoc,
      P.cancel_left_of_respectsIso]
    exact hf _

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

Goal state before:
pp: case h₂
P : MorphismProperty Scheme
inst✝¹ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : Y✝ ≅ Z✝
f✝ : X✝ ⟶ Y✝
inst✝ : IsAffine Y✝
⊢ of P f✝ → of P (f✝ ≫ e✝.hom)

Tactic:
apply MorphismProperty.RespectsIso.postcomp

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
this : (s.fst ≫ D.ι i).base = (s.snd ≫ D.ι j).base
⊢ s.fst.base ≫ (forget C).map (D.ι i) ≫ (D.gluedIso (forget C)).hom =
    s.snd.base ≫ (forget C).map (D.ι j) ≫ (D.gluedIso (forget C)).hom

Tactic:
comp_base,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
this : s.fst.base ≫ (D.ι i).base = (s.snd ≫ D.ι j).base
⊢ s.fst.base ≫ (forget C).map (D.ι i) ≫ (D.gluedIso (forget C)).hom =
    s.snd.base ≫ (forget C).map (D.ι j) ≫ (D.gluedIso (forget C)).hom
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : P.RespectsIso
H : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
⊢ P f

Tactic:
have : (f ≫ g) ⁻¹ᵁ g.opensRange = ⊤ := by simp

Goal state after:
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
H : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
this : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
⊢ P f
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsDominant f
hf : IsClosed (Set.range ⇑f)
⊢ Set.range ⇑f = Set.univ

Tactic:
← hf.closure_eq,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsDominant f
hf : IsClosed (Set.range ⇑f)
⊢ closure (Set.range ⇑f) = Set.univ
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case of_basicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS : ⨆ f, Y.basicOpen ↑f = ⊤
hS' : ∀ (r : ↥S), CompactSpace ↥↑(f ⁻¹ᵁ Y.basicOpen ↑r)
⊢ CompactSpace ↥X

Tactic:
rw [← isCompact_univ_iff, ← Opens.coe_top, ← f.preimage_top, ← hS, Scheme.Hom.preimage_iSup,
        Opens.iSup_mk, Opens.coe_mk]

Goal state after:
case of_basicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS : ⨆ f, Y.basicOpen ↑f = ⊤
hS' : ∀ (r : ↥S), CompactSpace ↥↑(f ⁻¹ᵁ Y.basicOpen ↑r)
⊢ IsCompact (⋃ i, ((Opens.map f.base).1 (Y.basicOpen ↑i)).carrier)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case refine_2.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s),
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n i *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
      0
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ n, f ^ n * x = 0

Tactic:
use Finset.univ.sup n

Goal state after:
case h
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s),
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n i *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
      0
this : Finite ↑s
val✝ : Fintype ↑s
⊢ f ^ Finset.univ.sup n * x = 0
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : y * ↑m' = 0
⊢ x = 0

Tactic:
← (IsLocalization.map_units S m).mul_left_inj,

Goal state after:
case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : y * ↑m' = 0
⊢ x * (algebraMap R S) ↑m = 0 * (algebraMap R S) ↑m
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
⊢ I.height + 1 ≤ J.height

Tactic:
J.height_eq_inf_minimalPrimes

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
⊢ I.height + 1 ≤ ⨅ J_1 ∈ J.minimalPrimes, J_1.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal A
⊢ ⨅ J_1 ∈ (comap (algebraMap R A) J).minimalPrimes, J_1.height = J.height

Tactic:
J.height_eq_inf_minimalPrimes

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal A
⊢ ⨅ J_1 ∈ (comap (algebraMap R A) J).minimalPrimes, J_1.height = ⨅ J_1 ∈ J.minimalPrimes, J_1.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
⊢ ¬↑I ⊆ ⋃ K ∈ hS.toFinset, ↑K

Tactic:
refine (Ideal.subset_union_prime ⊥ ⊥ ?_).not.mpr ?_

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
⊢ ∀ i ∈ hS.toFinset, i ≠ ⊥ → i ≠ ⊥ → i.IsPrime

case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
⊢ ¬∃ i ∈ hS.toFinset, I ≤ i
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case ofLocalizationSpanTarget
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))

pp: case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))

pp: case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] f ↦
    P (Spec.map (CommRingCat.ofHom f))

Tactic:
· intro R S _ _ f s hs H
    apply IsZariskiLocalAtSource.of_openCover (Scheme.affineOpenCoverOfSpanRangeEqTop
      (fun i : s ↦ (i : S)) (by simpa)).openCover
    intro i
    simp only [CommRingCat.coe_of, ← Spec.map_comp,
      Scheme.AffineOpenCover.openCover_f, Scheme.affineOpenCoverOfSpanRangeEqTop_f]
    exact H i

Goal state after:
case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))

case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] f ↦
    P (Spec.map (CommRingCat.ofHom f))
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 s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
s : ↑Us
f' : ↑(V s) ⟶ ↑(U.ι ⁻¹ᵁ ↑s) := f ∣_ U.ι ⁻¹ᵁ ↑s
⊢ P ((V s).ι ≫ f ≫ U.ι)

Tactic:
have hf' : P f' := IsZariskiLocalAtTarget.restrict hf _

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
s : ↑Us
f' : ↑(V s) ⟶ ↑(U.ι ⁻¹ᵁ ↑s) := f ∣_ U.ι ⁻¹ᵁ ↑s
hf' : P f'
⊢ P ((V s).ι ≫ f ≫ U.ι)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inr
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
h : U.carrier.Nonempty
⊢ _root_.IsReduced ↑Γ(X, U)

Tactic:
· have : Nonempty U := by simpa
    infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
H : ∃ x x_1, ∃ (_ : IsClosed x) (_ : IsClosed x_1) (_ : Set.univ ⊆ x ∪ x_1), ¬(Set.univ ⊆ x ∨ Set.univ ⊆ x_1)
⊢ False

Tactic:
not_or

Goal state after:
X : Scheme
inst✝ : IsIntegral X
H : ∃ x x_1, ∃ (_ : IsClosed x) (_ : IsClosed x_1) (_ : Set.univ ⊆ x ∪ x_1), ¬Set.univ ⊆ x ∧ ¬Set.univ ⊆ x_1
⊢ False
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a
X : Scheme
I✝ : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this✝¹ : Algebra ↑Γ(X, ↑U) ↑Γ(X, ↑(X.affineBasicOpen f)) := (CommRingCat.Hom.hom F).toAlgebra
this✝ : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, X.basicOpen f)
this : Topology.IsOpenEmbedding ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, ↑U))
hx : x ∈ PrimeSpectrum.vanishingIdeal (closure (⇑(Spec.map F) ⁻¹' Z'))
I : Ideal ↑Γ(X, ↑U)
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus ↑I
⊢ x ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (PrimeSpectrum.vanishingIdeal Z')

Tactic:
← this.isOpenMap.preimage_closure_eq_closure_preimage this.continuous,

Goal state after:
case a
X : Scheme
I✝ : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this✝¹ : Algebra ↑Γ(X, ↑U) ↑Γ(X, ↑(X.affineBasicOpen f)) := (CommRingCat.Hom.hom F).toAlgebra
this✝ : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, X.basicOpen f)
this : Topology.IsOpenEmbedding ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, ↑U))
hx : x ∈ PrimeSpectrum.vanishingIdeal (⇑(Spec.map F) ⁻¹' closure Z')
I : Ideal ↑Γ(X, ↑U)
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus ↑I
⊢ x ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (PrimeSpectrum.vanishingIdeal Z')
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
⊢ ∃ s_1 ∈ Submonoid.powers s, s_1 * x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

Tactic:
suffices ∃ (V : X.Opens) (hV : V = X.basicOpen ((f.app U).hom s)),
        letI := hV.trans_le (X.basicOpen_le _); ((f.app U).hom x |_ V) = 0 by
      obtain ⟨_, rfl, H⟩ := this
      obtain ⟨n, hn⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact
        X (U := f ⁻¹ᵁ U) (QuasiCompact.isCompact_preimage (f := f) _ U.1.2 U.2.isCompact)
        (f.app U x) (f.app U s) H
      exact ⟨_, ⟨n, rfl⟩, by simpa using hn⟩

Goal state after:
case a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
⊢ ∃ V, ∃ (hV : V = X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)), ((CommRingCat.Hom.hom (f.app ↑U)) x |_ V) ⋯ = 0
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
⊢ g.ker ≤ ker (f ≫ g)

Tactic:
refine ofIdeals_mono fun U ↦ ?_

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
U : ↑Z.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (g.app ↑U)) ≤ RingHom.ker (CommRingCat.Hom.hom (app (f ≫ g) ↑U))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
I : Y.IdealSheafData
hI : ∀ (i : 𝒰.I₀), I ≤ ker (𝒰.f i ≫ f)
U : ↑Y.affineOpens
⊢ ∀ (i : 𝒰.I₀), I.ideal U ≤ (ker (𝒰.f i ≫ f)).ideal U

Tactic:
exact fun i ↦ hI i U

Goal state after: