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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) := CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Hom.app (IsAffineOpen.isoSpec ⋯).inv ⊤ ≫ (ΓSpecIso Γ(X, ↑U)).hom ≫ φ = X.presheaf.map (eqToHom ⋯).op ≫ φ

Tactic:
rw [← Scheme.Hom.appTop, U.2.isoSpec_inv_appTop, Category.assoc, Iso.inv_hom_id_assoc]

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) := CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ (↑U).topIso.hom ≫ φ = X.presheaf.map (eqToHom ⋯).op ≫ φ
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
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
wlog h : IsAffine X ∧ IsAffine Y generalizing X Y f

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
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f → ∀ (x : ↥X), IsAffine X ∧ IsAffine Y → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

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✝
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
h : IsAffine X ∧ IsAffine Y
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
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
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this✝ :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f →
      ∀ (x : ↥X),
        IsAffine X → IsAffine Y → (∃ R S, Y = Spec R ∧ X = Spec S) → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ R S, Y = Spec R ∧ X = Spec S
this : Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv (X.isoSpec.hom x))))
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
have heq : (X.isoSpec.inv (X.isoSpec.hom x)) = x := by simp

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
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this✝ :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f →
      ∀ (x : ↥X),
        IsAffine X → IsAffine Y → (∃ R S, Y = Spec R ∧ X = Spec S) → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ R S, Y = Spec R ∧ X = Spec S
this : Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv (X.isoSpec.hom x))))
heq : X.isoSpec.inv (X.isoSpec.hom x) = x
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ Spec.map (Triplet.tensorCongr ⋯).hom ≫ T.SpecTensorTo = T.SpecTensorTo

Tactic:
simp only [Triplet.tensorCongr_refl, Iso.refl_hom, Spec.map_id, Category.id_comp]

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

Goal state before:
pp: case h₀
X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)

Tactic:
rw [← cancel_mono (glueDataObjι _ _)]

Goal state after:
case h₀
X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ (I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫ I.glueDataObjι i =
    (𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫ I.glueDataObjι i
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
          (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯ ≫
        pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯) =
    (pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
        I.glueDataT i j) ≫
      pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)

Tactic:
rw [← cancel_mono (glueDataObjι _ _)]

Goal state after:
case h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ ((pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
            (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯ ≫
          pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
            (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) ≫
        pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)) ≫
      I.glueDataObjι (j, i).1 =
    ((pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
            (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
          I.glueDataT i j) ≫
        pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)) ≫
      I.glueDataObjι (j, i).1
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mp.left
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
t : ↥(pullback f g)
⊢ (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) t ∈ ⇑(pullback.fst f' g') ⁻¹' Set.range ⇑i₁

Tactic:
use pullback.fst f g t

Goal state after:
case h
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
t : ↥(pullback f g)
⊢ i₁ ((pullback.fst f g) t) = (pullback.fst f' g') ((pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) t)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case hs₂
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
⊢ ∀ i ∈ ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) '' ↑s, IsAffineOpen (X.basicOpen i)

Tactic:
rintro - ⟨r, hr, rfl⟩

Goal state after:
case hs₂
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
r : ↑Γ(Y, ⊤)
hr : r ∈ ↑s
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) r))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

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

Tactic:
rw [← cancel_mono (glueDataObjι _ _)]

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

Goal state before:
pp: X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥U
hx : f x ∈ W
⊢ i ((coprodMk ↑(f ⁻¹ᵁ W) ↑(g ⁻¹ᵁ W)) (Sum.inl ⟨x, hx⟩)) = (coprodMk U V) (Sum.inl x)

Tactic:
by simp [i, ← Scheme.Hom.comp_apply]

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

Goal state before:
pp: X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥V
hx : g x ∈ W
⊢ i ((coprodMk ↑(f ⁻¹ᵁ W) ↑(g ⁻¹ᵁ W)) (Sum.inr ⟨x, hx⟩)) = (coprodMk U V) (Sum.inr x)

Tactic:
by simp [i, ← Scheme.Hom.comp_apply]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ ⊥.subschemeι ≫ Hom.toImage (𝟙 X) ≫ IdealSheafData.inclusion ⋯ = 𝟙 ⊥.subscheme

Tactic:
simp [← cancel_mono (IdealSheafData.subschemeι _)]

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

Goal state before:
pp: X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
x : ↥Y
hx : g x ∈ Set.range ⇑(X.affineCover.f i)
⊢ False

Tactic:
apply hxU

Goal state after:
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
x : ↥Y
hx : g x ∈ Set.range ⇑(X.affineCover.f i)
⊢ Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
inst✝ : Algebra.FinitePresentation R S
⊢ IsOpenMap (comap (algebraMap R S))

Tactic:
rw [isBasis_basic_opens.isOpenMap_iff]
  rintro _ ⟨_, ⟨f, rfl⟩, rfl⟩
  exact isOpen_of_stableUnderGeneralization_of_isConstructible
    ((basicOpen f).2.stableUnderGeneralization.image
      (Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap.mp ‹_›))
    (isConstructible_comap_image (RingHom.finitePresentation_algebraMap.mpr ‹_›)
      isConstructible_basicOpen)

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

Goal state before:
pp: case neg
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
⊢ IsClosedImmersion (Scheme.Cover.pullbackHom X.affineCover g i)

Tactic:
· have : IsEmpty ((X.affineCover.pullback₁ g).X i) := by
        apply Scheme.isEmpty_pullback
        rw [← Set.subset_compl_iff_disjoint_left]
        rintro _ hx ⟨x, rfl⟩
        apply hxU
        rintro _ ⟨y, rfl⟩
        exact Subsingleton.elim x y ▸ hx
      infer_instance

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inr.mpr.inr.inr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi✝ : i ≠ ((LinearMap.mul R A) f).charpoly.natDegree
hi : ((LinearMap.mul R A) f).charpoly.natDegree < i
⊢ (Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f))).coeff i =
    (X ^ ((LinearMap.mul R A) f).charpoly.natDegree).coeff i

Tactic:
simp [hi.ne', coeff_eq_zero_of_natDegree_lt hi]

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

Goal state before:
pp: R S : CommRingCat
s : Set ↥(Spec S)
hs : IsLocallyConstructible s
φ : R ⟶ S
hf : (CommRingCat.Hom.hom φ).FinitePresentation
inst✝ : QuasiCompact (Spec.map φ)
⊢ IsLocallyConstructible (⇑(Spec.map φ) '' s)

Tactic:
exact (PrimeSpectrum.isConstructible_comap_image hf hs.isConstructible).isLocallyConstructible

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

Goal state before:
pp: P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
y : Spec (of K) ⟶ Y
Z : Scheme
⊢ ∀ (fst : Z ⟶ X) (snd : Z ⟶ Spec (of K)), IsPullback fst snd f y → P Z

Tactic:
fst

Goal state after:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
y : Spec (of K) ⟶ Y
Z : Scheme
fst : Z ⟶ X
⊢ ∀ (snd : Z ⟶ Spec (of K)), IsPullback fst snd f y → P Z
Module: Mathlib.AlgebraicGeometry.Geometrically.Integral

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝² : GeometricallyIntegral f
inst✝¹ : Subsingleton ↥S
inst✝ : IsIntegral S
⊢ IrreducibleSpace ↥X ∧ IsReduced X

Tactic:
refine ⟨GeometricallyIrreducible.irreducibleSpace_of_subsingleton f,
    GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian f⟩

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
hf : IsPullback f' i₁ i₂ f
hf' : IsClosedImmersion f'
⊢ topologically (@IsClosedMap) f'

Tactic:
exact f'.isClosedEmbedding.isClosedMap

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝⁴ : Subsingleton ↥X
inst✝³ : IsReduced X
inst✝² : JacobsonSpace ↥Y
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [Subsingleton ↥X] [IsReduced X] [JacobsonSpace ↥Y],
    (∃ S, Y = Spec S) → (IsFinite f ↔ LocallyOfFiniteType f)
hY : ¬∃ S, Y = Spec S
inst✝¹ :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    Subsingleton ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
inst✝ :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    IsReduced ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
inst : ∀ (i : Y.affineCover.I₀), JacobsonSpace ↥(Y.affineCover.X i)
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    ∀ (i : Y.affineCover.toPreZeroHypercover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
exact forall_congr' fun i ↦ this ⟨_, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
k : J
f : x.fst ⟶ k
f' : y.fst ⟶ k
h : (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map f')) y.snd
⊢ Relation.EqvGen F.ColimitTypeRel x y

Tactic:
apply Relation.EqvGen.trans (y := ⟨k, F.map f' y.2⟩)

Goal state after:
case mpr.a
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
k : J
f : x.fst ⟶ k
f' : y.fst ⟶ k
h : (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map f')) y.snd
⊢ Relation.EqvGen F.ColimitTypeRel x ⟨k, (ConcreteCategory.hom (F.map f')) y.snd⟩

case mpr.a
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
k : J
f : x.fst ⟶ k
f' : y.fst ⟶ k
h : (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map f')) y.snd
⊢ Relation.EqvGen F.ColimitTypeRel ⟨k, (ConcreteCategory.hom (F.map f')) y.snd⟩ y
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Lattice Y
inst✝ : Zero Y
⊢ ∀ (a : locallyFinsuppWithin U Y), a ≤ a

Tactic:
simp [le_def]

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ 0 ≤ max (f₁ x) 0 + max (f₂ x) 0

Tactic:
simp [add_nonneg]

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ 0 ≤ max (-f₁ x) 0 + max (-f₂ x) 0

Tactic:
simp [add_nonneg]

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
⊢ max (-(n • f x)) 0 = n • max (-f x) 0

Tactic:
by_cases h : -f x < 0

Goal state after:
case pos
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
h : -f x < 0
⊢ max (-(n • f x)) 0 = n • max (-f x) 0

case neg
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
h : ¬-f x < 0
⊢ max (-(n • f x)) 0 = n • max (-f x) 0
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
⊢ ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0

Tactic:
choose f hf using fun x ↦ (hJ x).mp

Goal state after:
X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
⊢ ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this✝ : IsAffine ↑V
this :
  ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
⊢ Scheme.Hom.resLE f V U ⋯ = Scheme.Hom.resLE g V U ⋯

Tactic:
← cancel_mono V.toScheme.isoSpec.hom

Goal state after:
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this✝ : IsAffine ↑V
this :
  ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
⊢ Scheme.Hom.resLE f V U ⋯ ≫ (↑V).isoSpec.hom = Scheme.Hom.resLE g V U ⋯ ≫ (↑V).isoSpec.hom
Module: Mathlib.AlgebraicGeometry.Birational.Birational

Goal state before:
pp: X U S : Scheme
f : U ⟶ X
inst✝¹ : IsOpenImmersion f
inst✝ : IsDominant f
sX : X ⟶ S
sU : U ⟶ S
hf : f ≫ sX = sU
⊢ PartialIso.IsOver sU sX (partialIso f)

Tactic:
simp [PartialIso.IsOver, hf]

Goal state after: