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

Goal state before:
pp: case inl
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (Scheme.Cover.pullbackHom (coprodOpenCover X' Y') (coprod.map f g) (Sum.inl PUnit.unit))

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso P
      (isPullback_inl_inl_coprodMap f g).flip.isoPullback.hom]
    convert! hf
    simp [Scheme.Cover.pullbackHom, coprodOpenCover]

Goal state after:
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 : PullbackCone f✝ g✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
      (𝒰.f i) ⋯ ⋯ =
    (pullbackSymmetry
          (pullback.snd f
            (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))
          (pullback.snd g
            (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))).hom ≫
      (limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv ≫
        pullback.map
            (pullback.snd f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
              𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst)
            g
            (pullback.fst f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
              f)
            g
            (𝟙
              (pullback f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst)))
            (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫
          pullback.map
            (pullback.fst f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
              f)
            g f g
            (pullback.fst f
              (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))
            (𝟙 Y) (𝟙 Z) ⋯ ⋯

Tactic:
ext : 1 <;>
  · simp only [limit.lift_π, PullbackCone.mk_π_app, Equiv.trans_apply, Category.assoc,
    limit.lift_π_assoc, cospan_left, Category.comp_id,
      limit.isoLimitCone_inv_π_assoc, PullbackCone.π_app_left, IsPullback.cone_fst,
      pullbackSymmetry_hom_comp_snd_assoc, limit.isoLimitCone_inv_π,
      PullbackCone.π_app_right, IsPullback.cone_snd, pullbackSymmetry_hom_comp_fst_assoc]
    rfl

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)
h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) := ⋯
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
⊢ ∀ (i : 𝒱.toPreZeroHypercover.1), Q (Scheme.Cover.pullbackHom 𝒱 (pullback.diagonal f) i)

Tactic:
rintro ⟨i, j, k⟩

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)
h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀
j k : (𝒰' i).I₀
⊢ Q (Scheme.Cover.pullbackHom 𝒱 (pullback.diagonal f) ⟨i, (j, k)⟩)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ pullback.map (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯)
        ((𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.snd f (𝟙 Y))
        ((𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.snd f (𝟙 Y)) (𝟙 (𝒰.X i.1)) (𝟙 (𝒰.X i.2)) (pullback.snd f (𝟙 Y))
        ⋯ ⋯ ≫
      (pullback.congrHom ⋯ ⋯).hom =
    (asIso
          (pullback.map (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.1) (𝒰.f i.2)
            (𝟙 (𝒰.X i.1)) (𝟙 (𝒰.X i.2)) (pullback.fst f (𝟙 Y)) ⋯ ⋯)).hom ≫
      pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f

Tactic:
cat_disch

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ pullback.map ((𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.snd f (𝟙 Y))
        ((𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.snd f (𝟙 Y)) f f
        ((𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.fst f (𝟙 Y))
        ((𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.fst f (𝟙 Y)) (𝟙 Y) ⋯ ⋯ ≫
      (Iso.refl (pullback.diagonalObj f)).hom =
    (pullback.congrHom ⋯ ⋯).hom ≫ pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯

Tactic:
cat_disch

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

Goal state before:
pp: P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
⊢ IsZariskiLocalAtTarget P.universally

Tactic:
apply IsZariskiLocalAtTarget.mk'
  · exact fun {X Y} f U => P.universally.of_isPullback
      (isPullback_morphismRestrict f U).flip
  · intro X Y f ι U hU H X' Y' i₁ i₂ f' h
    apply hP₂ _ (fun i ↦ i₂ ⁻¹ᵁ U i)
    · simp only [IsOpenCover, ← top_le_iff] at hU ⊢
      rintro x -
      simpa using @hU (i₂ x) trivial
    · rintro i
      refine H _ ((X'.isoOfEq ?_).hom ≫ i₁ ∣_ _) (i₂ ∣_ _) _ ?_
      · exact congr($(h.1.1) ⁻¹ᵁ U i)
      · rw [← (isPullback_morphismRestrict f _).paste_vert_iff]
        · simp only [Category.assoc, morphismRestrict_ι, Scheme.isoOfEq_hom_ι_assoc]
          exact (isPullback_morphismRestrict f' (i₂ ⁻¹ᵁ U i)).paste_vert h
        · rw [← cancel_mono (Scheme.Opens.ι _)]
          simp [morphismRestrict_ι_assoc, h.1.1]

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

Goal state before:
pp: case of_basicOpenCover
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
U : ↑X.affineOpens
r : ↑↑s
hs' :
  ∀ (r : ↥s) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ Y.basicOpen ↑r),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen ↑r) (↑V) e))
this :
  P
    (CommRingCat.Hom.hom
      (Scheme.Hom.appLE f (Y.basicOpen ↑r) ↑⟨X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r), ⋯⟩ ⋯))
⊢ P (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)

Tactic:
IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2,

Goal state after:
case of_basicOpenCover
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
U : ↑X.affineOpens
r : ↑↑s
hs' :
  ∀ (r : ↥s) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ Y.basicOpen ↑r),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen ↑r) (↑V) e))
this :
  P
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen ↑r))))
          (↑(X.presheaf.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)))))
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)))
⊢ P (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsQuasiSeparated ↑U
this : QuasiSeparatedSpace ↥↑U
⊢ IsQuasiSeparated ↑(f ⁻¹ᵁ U)

Tactic:
exact (isQuasiSeparated_iff_quasiSeparatedSpace _ (f ⁻¹ᵁ U).2).mpr
    (quasiSeparatedSpace_of_quasiSeparated (f ∣_ U))

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ : Y.Opens
U₂ : ↑Y.affineOpens
V₁ : X.Opens
V₂ : ↑X.affineOpens
hx₁ : x ∈ V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ U₁.carrier
r : ↑Γ(Y, ↑U₂)
hBr : Y.basicOpen r ≤ U₁
hBfx : ↑⟨f x, hfx₁⟩ ∈ Y.basicOpen r
s : ↑Γ(X, ↑V₂)
hBs : X.basicOpen s ≤ V₁
hBx : ↑⟨x, hx₁⟩ ∈ X.basicOpen s
r' : ↑Γ(Y, ↑⟨Y.basicOpen r, ⋯⟩)
s' : ↑Γ(X, ↑⟨X.basicOpen s, ⋯⟩)
hBx' : x ∈ X.basicOpen s'
e' : X.basicOpen s' ≤ f ⁻¹ᵁ Y.basicOpen r'
hf' : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen s') e'))
⊢ ∃ U' V',
    ∃ (_ : ↑U' ≤ U₁) (_ : ↑V' ≤ V₁) (_ : x ∈ ↑V') (e : ↑V' ≤ f ⁻¹ᵁ ↑U'),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U') (↑V') e))

Tactic:
exact ⟨⟨Y.basicOpen r', (U₂.2.basicOpen _).basicOpen _⟩,
    ⟨X.basicOpen s', (V₂.2.basicOpen _).basicOpen _⟩, le_trans (Y.basicOpen_le _) hBr,
    le_trans (X.basicOpen_le _) hBs, hBx', e', hf'⟩

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

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

Tactic:
rw [hf]

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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ (1 |_ X.basicOpen f) ⋯ = 0

Tactic:
rw [← TopCat.Presheaf.restrict_restrict e bot_le]

Goal state after:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
e : X.basicOpen f ≤ ⊥
⊢ ((1 |_ ⊥) ⋯ |_ X.basicOpen f) e = 0
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ p.primeHeight = p.height

Tactic:
have := hp.isPrime

Goal state after:
R : Type u_1
inst✝ : CommRing R
I p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
⊢ p.primeHeight = p.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
⊢ ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height

Tactic:
have := hp.isPrime

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this : p.IsPrime
⊢ ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case refine_2
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.181).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.240).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
hs : ↑S ∩ ↑↑U = ⋃ i ∈ s, ↑↑i
⊢ ∃ n y,
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x

Tactic:
have := hs'.to_subtype

Goal state after:
case refine_2
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.181).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.240).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
hs : ↑S ∩ ↑↑U = ⋃ i ∈ s, ↑↑i
this : Finite ↑s
⊢ ∃ n y,
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≠ ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
⊢ ↑I.height ≤ ringKrullDim R

Tactic:
rw [I.height_eq_inf_minimalPrimes]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≠ ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
⊢ ↑(⨅ J ∈ I.minimalPrimes, J.height) ≤ ringKrullDim R
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : FiniteRingKrullDim R
inst✝¹ : IsLocalRing R
inst✝ : (IsLocalRing.maximalIdeal R).IsPrime
⊢ ↑(IsLocalRing.maximalIdeal R).height = ringKrullDim R

Tactic:
exact IsLocalRing.maximalIdeal_height_eq_ringKrullDim

Goal state after:
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 p : Ideal A
hp : p ∈ J.minimalPrimes
⊢ (comap (algebraMap R A) p).height = p.height

Tactic:
have := hp.isPrime

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 p : Ideal A
hp : p ∈ J.minimalPrimes
this : p.IsPrime
⊢ (comap (algebraMap R A) p).height = p.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: 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

pp: 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

Tactic:
· rintro K hK - -
        rw [Set.Finite.mem_toFinset] at hK
        exact hK.1.isPrime

Goal state after:
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.RingTheory.Ideal.Height

Goal state before:
pp: 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
K : Ideal R
hK : K ∈ S
e : I ≤ K
this : ↑(r + 1) ≤ K.height
⊢ False

Tactic:
rw [hK.2, ← not_lt] at this

Goal state after:
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
K : Ideal R
hK : K ∈ S
e : I ≤ K
this : ¬↑r < ↑(r + 1)
⊢ False
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case succ.refine_3
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
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
⊢ ↑(r + 1) ≤ p.primeHeight

Tactic:
have := hp.isPrime

Goal state after:
case succ.refine_3
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
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this : p.IsPrime
⊢ ↑(r + 1) ≤ p.primeHeight
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : f x ∈ U
right✝ : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑V)) Sₜ] [IsLocalization.Away t Sₜ],
            Q ((algebraMap (↑Γ(X, ↑V)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)))
s : Finset ↑Γ(X, ↑⟨V, hV⟩)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑⟨V, hV⟩)) Sₜ] [IsLocalization.Away t Sₜ],
      Q ((algebraMap (↑Γ(X, ↑⟨V, hV⟩)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑⟨U, hU⟩) (↑⟨V, hV⟩) e)))
hs : ⨆ i ∈ ↑s, X.basicOpen i = ↑⟨V, hV⟩
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
have : x ∈ (⨆ i ∈ s, X.basicOpen i) := hs.symm ▸ hx

Goal state after:
case refine_1
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this✝ : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : f x ∈ U
right✝ : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑V)) Sₜ] [IsLocalization.Away t Sₜ],
            Q ((algebraMap (↑Γ(X, ↑V)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)))
s : Finset ↑Γ(X, ↑⟨V, hV⟩)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑⟨V, hV⟩)) Sₜ] [IsLocalization.Away t Sₜ],
      Q ((algebraMap (↑Γ(X, ↑⟨V, hV⟩)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑⟨U, hU⟩) (↑⟨V, hV⟩) e)))
hs : ⨆ i ∈ ↑s, X.basicOpen i = ↑⟨V, hV⟩
this : x ∈ ⨆ i ∈ s, X.basicOpen i
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
f : ↑Γ(X, ↑U)
hV : V = X.affineBasicOpen f
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) = I.ideal V

Tactic:
subst hV

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) = I.ideal (X.affineBasicOpen f)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.map i.op))

Tactic:
injective_iff_map_eq_zero

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
⊢ ∀ (a : ↑Γ(X, V)), (ConcreteCategory.hom (X.presheaf.map i.op)) a = 0 → a = 0
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ ∀ ⦃b : X.IdealSheafData⦄, I ≤ b → b.support ≤ I.support

Tactic:
J

Goal state after:
X : Scheme
I J : X.IdealSheafData
⊢ I ≤ J → J.support ≤ I.support
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: 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)))
H : ((CommRingCat.Hom.hom (f.app ↑U)) x |_ X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)) ⋯ = 0
n : ℕ
hn : (ConcreteCategory.hom (f.app ↑U)) s ^ n * (ConcreteCategory.hom (f.app ↑U)) x = 0
⊢ (fun x ↦ s ^ x) n * x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

Tactic:
by simpa using hn

Goal state after: