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

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (pullback.snd f fT) ≅ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) :=
  (normalizationCoprodIso (pullback.snd f fT) H).symm ≪≫
    coprod.mapIso (asIso (toNormalization (V.ι ≫ pullback.snd f fT))).symm
      (Iso.refl (normalization (W.ι ≫ pullback.snd f fT)))
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := coprod.inl
⊢ ι = V.ι ≫ toNormalization (pullback.snd f fT) ≫ e.hom

Tactic:
rw [← Category.assoc, ← Iso.comp_inv_eq]

Goal state after:
case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (pullback.snd f fT) ≅ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) :=
  (normalizationCoprodIso (pullback.snd f fT) H).symm ≪≫
    coprod.mapIso (asIso (toNormalization (V.ι ≫ pullback.snd f fT))).symm
      (Iso.refl (normalization (W.ι ≫ pullback.snd f fT)))
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := coprod.inl
⊢ ι ≫ e.inv = V.ι ≫ toNormalization (pullback.snd f fT)
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (X ^ (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b
hf : (aeval s) f = 0
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Etale R R'
P : Ideal R'
w✝¹ : P.IsPrime
w✝ : P.LiesOver p
a' b' : R'[X]
hP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom (X ^ (m + 1)) =
    Polynomial.map (algebraMap R' P.ResidueField) a'
hb' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom b =
    Polynomial.map (algebraMap R' P.ResidueField) b'
s₀ : ↥(integralClosure R S) := ⟨s, hRs⟩
hfs₀ : (aeval s₀) f = 0
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : (aeval s') f = 0
hs₀'f : (aeval (1 ⊗ₜ[R] s₀)) f = 0
e₀ : R' ⊗[R] ↥(integralClosure R S) := (aeval (1 ⊗ₜ[R] s₀)) (c * a')
he₀ : IsIdempotentElem e₀
e : R' ⊗[R] S := (aeval s') (c * a')
φ : R' ⊗[R] ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S := TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val
he₀e : φ e₀ = e
he : IsIdempotentElem e
P' : ↑(P.primesOver (R' ⊗[R] S)) := (Ideal.fiberIsoOfBijectiveResidueField hP).symm ⟨q, ⋯⟩
this : Algebra (Localization.AtPrime P) (Localization.AtPrime ↑P') := Localization.AtPrime.algebraOfLiesOver P ↑P'
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom ↑P' = q
hs'P' : s' ∉ ↑P'
ha'P' : (aeval s') a' ∉ ↑P'
⊢ (aeval s') (Polynomial.map (algebraMap R R') f) ∈ ↑P'

Tactic:
simp [hs'f]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
x : 𝒰.toPreZeroHypercover.1
this : (⨆ i, V i).ι ''ᵁ opensRange (𝒰.f x) = V x
⊢ MorphismProperty.isomorphisms Scheme (toNormalization f ∣_ (⨆ x, V x).ι ''ᵁ opensRange (𝒰.f x))

Tactic:
convert! hV x

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FaithfullyFlat R T
inst✝ : Module.Finite T (T ⊗[R] M)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Submodule.span T (Set.range s) = ⊤
k : Fin n → ℕ
t : (i : Fin n) → Fin (k i) → T
m : (i : Fin n) → Fin (k i) → M
h : ∀ (i : Fin n), s i = ∑ j, t i j ⊗ₜ[R] m i j
f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M :=
  ((Pi.basisFun R ((i : Fin n) × Fin (k i))).constr R) fun x ↦
    match x with
    | ⟨i, j⟩ => m i j
this : Function.Surjective ⇑((AlgebraTensorModule.lTensor T T) f₀)
⊢ Function.Surjective ⇑f₀

Tactic:
← Module.FaithfullyFlat.lTensor_surjective_iff_surjective _ T

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FaithfullyFlat R T
inst✝ : Module.Finite T (T ⊗[R] M)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Submodule.span T (Set.range s) = ⊤
k : Fin n → ℕ
t : (i : Fin n) → Fin (k i) → T
m : (i : Fin n) → Fin (k i) → M
h : ∀ (i : Fin n), s i = ∑ j, t i j ⊗ₜ[R] m i j
f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M :=
  ((Pi.basisFun R ((i : Fin n) × Fin (k i))).constr R) fun x ↦
    match x with
    | ⟨i, j⟩ => m i j
this : Function.Surjective ⇑((AlgebraTensorModule.lTensor T T) f₀)
⊢ Function.Surjective ⇑(LinearMap.lTensor T f₀)
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
x : ↥↑(f ⁻¹ᵁ V)
H : ¬Scheme.Hom.QuasiFiniteAt f ((f ⁻¹ᵁ V).ι x)
⊢ False

Tactic:
exact x.2 ⟨_, H, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: R S T : Type u_1
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : (algebraMap S (S ⊗[R] T)).Smooth
⊢ (algebraMap R T).Smooth

Tactic:
rw [smooth_algebraMap] at h' ⊢

Goal state after:
R S T : Type u_1
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : Algebra.Smooth S (S ⊗[R] T)
⊢ Algebra.Smooth R T
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
s : S
x : Ω[P.Ring⁄R]
this : x ∈ Submodule.span P.Ring (Set.range ⇑(KaehlerDifferential.D R P.Ring))
⊢ t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring]
      (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring P.baseChange.Ring) (1 ⊗ₜ[P.Ring] x) =
    t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring] (KaehlerDifferential.map R T P.Ring P.baseChange.Ring) x

Tactic:
induction this using Submodule.span_induction with
  | zero => simp
  | add x y _ _ hx hy => simp [tmul_add, hx, hy]
  | mem y hy =>
    obtain ⟨y, rfl⟩ := hy
    simp
  | smul a x _ hx =>
    rw [tmul_smul, ← algebraMap_smul (P.baseChange (T := T)).Ring a, LinearEquiv.map_smul,
      tmul_smul, hx, LinearMap.map_smul, ← algebraMap_smul (P.baseChange (T := T)).Ring a,
      tmul_smul]

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

Goal state before:
pp: X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝¹ : IsNoetherian X
inst✝ : IrreducibleSpace ↥X
this : CategoryTheory.IsIso (X.irreducibleComponentOpen Z).ι
⊢ CategoryTheory.IsIso (X.irreducibleComponentIdeal Z hZ).subschemeι

Tactic:
isIso_subschemeι_iff_eq_bot,

Goal state after:
X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝¹ : IsNoetherian X
inst✝ : IrreducibleSpace ↥X
this : CategoryTheory.IsIso (X.irreducibleComponentOpen Z).ι
⊢ X.irreducibleComponentIdeal Z hZ = ⊥
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
η : 𝟙 a✝ ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
a : B
⊢ leftZigzagIso (ρ_ (𝟙 a)).symm (ρ_ (𝟙 a)) = λ_ (𝟙 a) ≪≫ (ρ_ (𝟙 a)).symm

Tactic:
by ext; simp [bicategoricalIsoComp]

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
s : Finset S
hs : Submodule.span R ↑s = ⊤
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Free R S'
w✝ : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : ↑s ⊆ ↑f.range
⊢ Function.Surjective ⇑f

Tactic:
have := (Submodule.span_le (p := LinearMap.range f.toLinearMap)).mpr hsf

Goal state after:
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
s : Finset S
hs : Submodule.span R ↑s = ⊤
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Free R S'
w✝ : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : ↑s ⊆ ↑f.range
this : Submodule.span R ↑s ≤ f.toLinearMap.range
⊢ Function.Surjective ⇑f
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Finite σ
⊢ ringKrullDim R + ↑(ENat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
rw [ENat.card_eq_coe_natCard]

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Finite σ
⊢ ringKrullDim R + ↑↑(Nat.card σ) ≤ ringKrullDim (MvPolynomial σ R)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
y : ↥(nonZeroDivisors R)
⊢ (ordMonoidWithZeroHom R) ↑y = 0 ↔ ord R ↑y = ⊤

Tactic:
simp only [ordMonoidWithZeroHom, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, SetLike.coe_mem,
    ↓reduceIte]
  generalize ord R y = k
  cases k
  all_goals simp

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K
h1 : x + y ≠ 0
⊢ min ((valuation K (IsDiscreteValuationRing.maximalIdeal R)) x)⁻¹
      ((valuation K (IsDiscreteValuationRing.maximalIdeal R)) y)⁻¹ ≤
    ((valuation K (IsDiscreteValuationRing.maximalIdeal R)) (x + y))⁻¹

Tactic:
grw [Valuation.map_add, min_inv_inv_le]

Goal state after:
case hb
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K
h1 : x + y ≠ 0
⊢ 0 < (valuation K (IsDiscreteValuationRing.maximalIdeal R)) (x + y)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst✝² : SMul α A
inst✝¹ : IsScalarTower α A A
inst✝ : SMulMemClass σ α A
m : α
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ (Setoid.ker (embedding 𝒜 x)) (m • c1) (m • c2)

Tactic:
by
    change Localization.mk _ _ = Localization.mk _ _
    simp only [num_smul, den_smul]
    convert! congr_arg (fun z : at x => m • z) h <;> rw [Localization.smul_mk]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
y1 y2 : HomogeneousLocalization 𝒜 x
⊢ (y1 - y2).val = y1.val - y2.val

Tactic:
rw [sub_eq_add_neg, ← val_neg, ← val_add]; rfl

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ (Quotient.mk'' y ^ n).val = val (Quotient.mk'' y) ^ n

Tactic:
by rw [← mk_pow, val_mk, val_mk, Localization.mk_pow]; rfl

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
⊢ g ^ e * f ^ (2 * e + d) ∈ 𝒜 ((d + e) • (d + e))

Tactic:
by
      convert!
        SetLike.mul_mem_graded (SetLike.pow_mem_graded e hg)
          (SetLike.pow_mem_graded (2 * e + d) hf) using 2
      ring

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

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g✝ : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range fun i ↦ ↑i.snd)

Tactic:
by
  classical
  intro z hz
  rw [← DirectSum.sum_support_decompose 𝒜 z]
  refine Ideal.sum_mem _ fun c hc ↦ if hc0 : c = 0 then ?_ else
    Ideal.subset_span ⟨⟨⟨c, Nat.pos_iff_ne_zero.mpr hc0⟩, _⟩, rfl⟩
  convert! Ideal.zero_mem _
  subst hc0
  exact hz

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case neg
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
H : ¬∑ i, ai i • dv i = n
⊢ mk { deg := n, num := ((decompose 𝒜) (∏ i, v i ^ ai i)) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ } ∈
    Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
convert! zero_mem (Submodule.span (𝒜 0) _)

Goal state after:
case e'_5
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
H : ¬∑ i, ai i • dv i = n
⊢ mk { deg := n, num := ((decompose 𝒜) (∏ i, v i ^ ai i)) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ } = 0
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case neg.zero
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
⊢ mk { deg := n, num := ((decompose 𝒜) 0) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ } ∈
    Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
convert! zero_mem (Submodule.span (𝒜 0) _)

Goal state after:
case e'_5
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
⊢ mk { deg := n, num := ((decompose 𝒜) 0) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ } = 0
Module: Mathlib.RingTheory.LocalRing.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
K : Type u_3
inst✝² : Field K
A✝ : Subring K
P✝ : Ideal ↥A✝
inst✝¹ : P✝.IsPrime
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
⊢ ∀ (y : ↥P.primeCompl), IsUnit (A.subtype ↑y)

Tactic:
by simp [Ideal.primeCompl, not_imp_not]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Integral

Goal state before:
pp: case neg.refine_2
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf : 1 < v x
⊢ ∀ i < f.natDegree, v ((algebraMap O R) (f.coeff i)) * v x ^ i < v x ^ f.natDegree

Tactic:
intro _

Goal state after:
case neg.refine_2
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf : 1 < v x
i✝ : ℕ
⊢ i✝ < f.natDegree → v ((algebraMap O R) (f.coeff i✝)) * v x ^ i✝ < v x ^ f.natDegree
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
⊢ IsPullback X'_to_X f' f Y'_to_Y → Existence f → Existence f'

Tactic:
hP

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
⊢ Existence f → Existence f'
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h.succ
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n✝ : ℕ
hf : f ∈ 𝒜 (n✝ + 1)
hd : 0 < n✝ + 1
this : n = j * (n✝ + 1 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * ((n✝ + 1) * (e + 1)), num := ⟨a * g ^ (j * (n✝ + 1 - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩,
    den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * ((n✝ + 1) * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * (n✝ + 1)), ⋯⟩, den_mem := ⋯ }
⊢ x ^ j * (a * g ^ (j * (n✝ + 1 - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * (n✝ + 1)))) =
    x ^ (j * (e + 1)) * x ^ (j * (n✝ + 1)) * a

Tactic:
· simp only [hx, add_tsub_cancel_right]
    ring

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case mp
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ Existence f✝ → (topologically @SpecializingMap).universally f✝

Tactic:
intro _

Goal state after:
case mp
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
a✝ : Existence f✝
⊢ (topologically @SpecializingMap).universally f✝
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P Q : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT✝ : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : ∃ 𝒰 x, 𝒰.toPresieveOver ≤ T.arrows
⊢ ∃ 𝒰 x,
    𝒰.toPresieveOver ≤
      (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
          (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT✝⟩)).arrows

Tactic:
obtain ⟨𝒰, h, hle⟩ := hT

Goal state after:
P Q : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X)
hT : T ∈ (overGrothendieckTopology P S) ((MorphismProperty.Over.forget Q ⊤ S).obj X)
𝒰 : Cover (precoverage P) ((MorphismProperty.Over.forget Q ⊤ S).obj X).left
h : Cover.Over S 𝒰
hle : 𝒰.toPresieveOver ≤ T.arrows
⊢ ∃ 𝒰 x,
    𝒰.toPresieveOver ≤
      (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
          (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S) ↑⟨T, hT⟩)).arrows
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case intro
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range

Tactic:
have : Nonempty ι := ⟨j⟩

Goal state after:
case intro
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this : Nonempty ι
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range