mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ I.height ≤ J.height

Tactic:
by
  simp only [I.height_eq_inf_minimalPrimes, J.height_eq_inf_minimalPrimes]
  refine le_iInf₂ (fun p hp ↦ ?_)
  have := hp.isPrime
  obtain ⟨q, hq, e⟩ := Ideal.exists_minimalPrimes_le (h.trans hp.le)
  have := hq.isPrime
  exact (iInf₂_le q hq).trans (Ideal.height_mono_of_isPrime e)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
hI : I.height = 0
p : Ideal R
w✝ : p.IsPrime
hIp : I ≤ p
hp0 : p = ⊥
⊢ I = ⊥

Tactic:
exact bot_unique (hIp.trans_eq hp0)

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

Goal state before:
pp: X : Scheme
J : X.IdealSheafData
i : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen✝ :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (i U) = i (X.affineBasicOpen f)
s : Set ↥X
hs : s = ⋂ U, X.zeroLocus ↑(i U)
h :
  { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝, supportSet := s,
        supportSet_eq_iInter_zeroLocus := hs }.ideal =
    J.ideal
⊢ { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝, supportSet := s, supportSet_eq_iInter_zeroLocus := hs } = J

Tactic:
obtain ⟨j, _, t, ht⟩ := J

Goal state after:
X : Scheme
i : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen✝¹ :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (i U) = i (X.affineBasicOpen f)
s : Set ↥X
hs : s = ⋂ U, X.zeroLocus ↑(i U)
j : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen✝ :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (j U) = j (X.affineBasicOpen f)
t : Set ↥X
ht : t = ⋂ U, X.zeroLocus ↑(j U)
h :
  { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
        supportSet_eq_iInter_zeroLocus := hs }.ideal =
    { ideal := j, map_ideal_basicOpen := map_ideal_basicOpen✝, supportSet := t,
        supportSet_eq_iInter_zeroLocus := ht }.ideal
⊢ { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s, supportSet_eq_iInter_zeroLocus := hs } =
    { ideal := j, map_ideal_basicOpen := map_ideal_basicOpen✝, supportSet := t, supportSet_eq_iInter_zeroLocus := ht }
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case refine_1.mp.inl
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS✝ : IsClosed S
hT✝ : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
x : ↥X
hS : x ∈ ↑{ carrier := Sᶜ, is_open' := ⋯ }
hT : x ∈ ↑{ carrier := Tᶜ, is_open' := ⋯ }
h : x ∈ S
⊢ x ∈ ↑⊥

pp: case refine_1.mp.inr
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS✝ : IsClosed S
hT✝ : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
x : ↥X
hS : x ∈ ↑{ carrier := Sᶜ, is_open' := ⋯ }
hT : x ∈ ↑{ carrier := Tᶜ, is_open' := ⋯ }
h : x ∈ T
⊢ x ∈ ↑⊥

Tactic:
exacts [hS h, hT h]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Subtype.val ⁻¹' (X.zeroLocus ↑(I.ideal U))ᶜ = (Subtype.val ⁻¹' I.supportSet)ᶜ

Tactic:
simp only [Set.preimage_compl, compl_inj_iff]

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Subtype.val ⁻¹' X.zeroLocus ↑(I.ideal U) = Subtype.val ⁻¹' I.supportSet
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫ (↑U).ι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯

Tactic:
Category.assoc

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv ≫ (↑U).ι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: X Y : Scheme
⊢ RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] x ↦ Function.Bijective ⇑x

Tactic:
RingHom.toMorphismProperty_respectsIso_iff

Goal state after:
X Y : Scheme
⊢ (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] x ↦ Function.Bijective ⇑x).RespectsIso
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫
      Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫
        (IsAffineOpen.isoSpec ⋯).inv =
    (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫ X.homOfLE h

Tactic:
Category.assoc

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫
      Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫
        (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
⊢ (Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯ ≫ Y.residue ((ConcreteCategory.hom f.base) ↑x)) ≫
      CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f ↑x))) =
    f.c.app (op V) ≫ X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯ ≫ X.residue ↑x

Tactic:
Category.assoc

Goal state after:
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
⊢ Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯ ≫
      Y.residue ((ConcreteCategory.hom f.base) ↑x) ≫
        CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f ↑x))) =
    f.c.app (op V) ≫ X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯ ≫ X.residue ↑x
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
X : Scheme
x : ↥X
f : X.presheaf.stalk x ⟶ CommRingCat.of K
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
⊢ Spec.map (descResidueField f) ≫ X.fromSpecResidueField x = Spec.map f ≫ X.fromSpecStalk x

Tactic:
simp [fromSpecResidueField, ← Spec.map_comp_assoc]

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

Goal state before:
pp: X Y✝ Z Y : Scheme
f g : (Over Y)ᵒᵖ
hfg : f ⟶ g
⊢ Hom.ker (Opposite.unop f).hom ≤ Hom.ker (Opposite.unop g).hom

Tactic:
simpa only [Functor.id_obj, Functor.const_obj_obj,
    OrderDual.toDual_le_toDual, ← Over.w hfg.unop] using hfg.unop.left.le_ker_comp f.unop.hom

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

Goal state before:
pp: case right
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
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ Q) (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen r)))

Tactic:
dsimp only
      rw [morphismRestrict_appTop, CommRingCat.hom_comp, hPi.cancel_right_isIso]
      -- Not sure why the `show` fixes the following `rw` complaining about "motive is incorrect"
      change Q (Scheme.Hom.app f ((Y.basicOpen r).ι ''ᵁ ⊤)).hom
      rw [Scheme.Opens.ι_image_top]
      rw [(isAffineOpen_top Y).app_basicOpen_eq_away_map f (isAffineOpen_top X),
        CommRingCat.hom_comp, hPi.cancel_right_isIso, ← Scheme.Hom.appTop]
      dsimp only [Opens.map_top]
      apply hQl
      exact hf

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
S' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)
n : ℕ
hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ ↑A.toSubsemiring
hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)
a : ↥M
ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)
⊢ ↑a * ↑(y ^ n) * x = x' * ↑a

Tactic:
SubmonoidClass.coe_pow,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
S' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)
n : ℕ
hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ ↑A.toSubsemiring
hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)
a : ↥M
ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)
⊢ ↑a * ↑y ^ n * x = x' * ↑a
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Set S
hs : Ideal.span s = ⊤
h : ∀ x ∈ s, FiniteType R (Localization.Away x)
⊢ FiniteType R S

Tactic:
obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
h : ∀ x ∈ s✝, FiniteType R (Localization.Away x)
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
⊢ FiniteType R S
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
e : CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) ≅ Γ(I.subscheme, I.subschemeι ⁻¹ᵁ ↑U) :=
  (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).symm ≪≫
    (Hom.appIso (I.subschemeCover.f U) ⊤).symm ≪≫ Functor.mapIso I.subscheme.presheaf (eqToIso ⋯).op
⊢ RingHom.ker (e.commRingCatIsoToRingEquiv.toRingHom.comp (Ideal.Quotient.mk (I.ideal U))) = I.ideal U

Tactic:
rw [RingHom.ker_equiv_comp, Ideal.mk_ker]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Set R
hs : Ideal.span s = ⊤
h : ∀ i ∈ s, FiniteType (Localization.Away i) (Localization.Away i ⊗[R] S)
⊢ FiniteType R S

Tactic:
obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set R
hs✝ : Ideal.span s✝ = ⊤
h : ∀ i ∈ s✝, FiniteType (Localization.Away i) (Localization.Away i ⊗[R] S)
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
⊢ FiniteType R S
Module: Mathlib.RingTheory.RingHom.FiniteType

Goal state before:
pp: R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), ((algebraMap S (Localization.Away ↑r)).comp f).FiniteType
algInst✝ : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
⊢ Algebra.FiniteType R (Localization.Away r)

Tactic:
simp_rw [RingHom.FiniteType] at H

Goal state after:
R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), Algebra.FiniteType R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
⊢ Algebra.FiniteType R (Localization.Away r)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
x : ↥X
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
have h := (f ≫ g).stalkMap_surjective x
    simp_rw [Scheme.Hom.stalkMap_comp] at h
    exact Function.Surjective.of_comp h

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

Goal state before:
pp: X Y Z : Scheme
f✝ f : X ⟶ Y
inst✝ : IsImmersion f
⊢ Set.range ⇑f ⊆ Set.range ⇑(coborderRange f).ι

Tactic:
simpa using! subset_coborder

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
this✝ : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Scheme.Hom.liftCoborder f)
⊢ Set.range ⇑f ⊆ Set.range ⇑(Scheme.Hom.coborderRange f).ι

Tactic:
simpa using! subset_coborder

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

Goal state before:
pp: case inst.refine_2
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
i : Y ⟶ Z
f : X ⟶ Y
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
⊢ IsLocallyClosed Set.univ

Tactic:
exact isOpen_univ.isLocallyClosed

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Set S
hs : Ideal.span s = ⊤
h : ∀ i ∈ s, FinitePresentation R (Localization.Away i)
⊢ FinitePresentation R S

Tactic:
obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
h : ∀ i ∈ s✝, FinitePresentation R (Localization.Away i)
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
⊢ FinitePresentation R S
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
S : ConstructibleSetData R
x✝¹ : BasicConstructibleSetData R
x✝ : x✝¹ ∈ ↑S
⊢ IsConstructible (zeroLocus {x✝¹.f})ᶜ

Tactic:
exact (isRetrocompact_zeroLocus_compl (Set.finite_singleton _)).isConstructible
      (isClosed_zeroLocus _).isOpen_compl

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

Goal state before:
pp: 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
⊢ 1 * Module.finrank R A = Module.finrank R A

Tactic:
one_mul

Goal state after:
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
⊢ Module.finrank R A = Module.finrank R A
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case neg.inr
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
he0 : ¬e = { val := 0 }
h✝ : Nontrivial R
⊢ P R e

Tactic:
simp only [InductionObj.ext_iff, funext_iff, Pi.zero_apply, not_forall] at he0

Goal state after:
case neg.inr
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
⊢ P R e
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
⊢ IsSeparated (terminal.from X)

Tactic:
← terminal.comp_from X.toSpecΓ

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
⊢ IsSeparated (X.toSpecΓ ≫ terminal.from (Spec Γ(X, ⊤)))
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
this : IsIso (Hom.imageι X.toSpecΓ)
⊢ IsOpenImmersion X.toSpecΓ

Tactic:
← X.toSpecΓ.toImage_imageι

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
this : IsIso (Hom.imageι X.toSpecΓ)
⊢ IsOpenImmersion (Hom.toImage X.toSpecΓ ≫ Hom.imageι X.toSpecΓ)
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
⊢ X.IsGermInjective

Tactic:
suffices ∀ (R : CommRingCat.{u}) (_ : IsNoetherianRing R), (Spec R).IsGermInjective by
    refine @Scheme.IsGermInjective.of_openCover _ (X.affineOpenCover.openCover) (fun i ↦ this _ ?_)
    exact isLocallyNoetherian_Spec.mp
      (isLocallyNoetherian_of_isOpenImmersion (X.affineOpenCover.f i))

Goal state after:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst✝ : IsLocallyNoetherian X
⊢ ∀ (R : CommRingCat), IsNoetherianRing ↑R → (Spec R).IsGermInjective
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
⊢ (Hom.isoImage (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι
          ((TopologicalSpace.Opens.map (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv.base).obj
            ((TopologicalSpace.Opens.map (f.hom ∣_ g.domain).base).obj
              ((TopologicalSpace.Opens.map g.hom.base).obj h.domain)))).inv ≫
      ((Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ∣_ (f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain ≫
          f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain) ≫
        h.hom =
    (X₁.isoOfEq ⋯).hom ≫
      (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
        (↑f.domain).homOfLE ⋯ ≫
          (Hom.isoImage (f.hom ⁻¹ᵁ g.domain).ι ((f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
            f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom

Tactic:
Category.assoc

Goal state after:
case H
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
⊢ (Hom.isoImage (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι
          ((TopologicalSpace.Opens.map (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv.base).obj
            ((TopologicalSpace.Opens.map (f.hom ∣_ g.domain).base).obj
              ((TopologicalSpace.Opens.map g.hom.base).obj h.domain)))).inv ≫
      (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ∣_ (f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain ≫
        f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom =
    (X₁.isoOfEq ⋯).hom ≫
      (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
        (↑f.domain).homOfLE ⋯ ≫
          (Hom.isoImage (f.hom ⁻¹ᵁ g.domain).ι ((f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
            f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : (𝒰.functorOfLocallyDirected ⋙ forget).obj i
xj : (𝒰.functorOfLocallyDirected ⋙ forget).obj j
hxij :
  (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map fi)) xi =
    (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map fj)) xj
⊢ ∃ l fli flj x,
    (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map fli)) x = xi ∧
      (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map flj)) x = xj

Tactic:
simp only [Functor.comp_obj, functorOfLocallyDirected_obj, forget_obj, Functor.comp_map,
      functorOfLocallyDirected_map, forget_map, ConcreteCategory.hom_ofHom,
      TypeCat.Fun.coe_mk] at hxij

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : (𝒰.functorOfLocallyDirected ⋙ forget).obj i
xj : (𝒰.functorOfLocallyDirected ⋙ forget).obj j
hxij : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ ∃ l fli flj x,
    (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map fli)) x = xi ∧
      (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map flj)) x = xj
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: ⊢ @UniversallyInjective =
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x ↦ Injective x).universally

Tactic:
ext X Y f; rw [universallyInjective_iff]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
⊢ (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f

Tactic:
intro ⟨h_inj, hf⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
h_inj : Injective ⇑f
hf : ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable
⊢ ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f