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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
⊢ (pullbackRestrictIsoRestrict f ↑U).inv ≫
      Cover.trans (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        (pullbackRestrictIsoRestrict f ↑V).hom =
    X.homOfLE ⋯

Tactic:
← cancel_mono (Scheme.Opens.ι _)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
⊢ ((pullbackRestrictIsoRestrict f ↑U).inv ≫
        Cover.trans (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
          (pullbackRestrictIsoRestrict f ↑V).hom) ≫
      (f ⁻¹ᵁ ↑V).ι =
    X.homOfLE ⋯ ≫ (f ⁻¹ᵁ ↑V).ι
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case succ
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝² : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝¹ : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝ : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
⊢ ZariskisMainProperty R p

Tactic:
have : Algebra.WeaklyQuasiFiniteAt R (p.under R') := by
      let := Localization.AtPrime.algebraOfLiesOver (p.under R') p
      let e : Localization.AtPrime (p.under R') ≃ₐ[R] Localization.AtPrime p :=
        .ofBijective (IsScalarTower.toAlgHom _ _ _) <| by
          refine Localization.localRingHom_bijective_of_saturated_inf_eq_top _ ?_ _
          rw [← top_le_iff, ← hs, Algebra.adjoin_le_iff]
          intro x hx
          refine ⟨r ^ (s.sup m), pow_mem (by exact ⟨hrp, hrR'⟩) _, Algebra.subset_adjoin ?_⟩
          simp [Set.smul_mem_smul_set hx, ← smul_eq_mul]
      exact .of_algHom_localization _ _ e.symm.toAlgHom e.symm.surjective

Goal state after:
case succ
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝³ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝² : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝¹ : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
⊢ ZariskisMainProperty R p
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
r : R
⊢ (C r).resultant g m n = (-1) ^ (m * n) * g.coeff n ^ m * r ^ n

Tactic:
rw [← zero_add m, resultant_add_left_deg _ _ _ _ _ (by simp), mul_comm n m]
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
this : ↑(ker (toNormalization f)).support = ↑⊥.support
⊢ IsDominant (toNormalization f)

Tactic:
IdealSheafData.support_bot,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
this : ↑(ker (toNormalization f)).support = ↑⊤
⊢ IsDominant (toNormalization f)
Module: Mathlib.RingTheory.Ideal.Quotient.Over

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
f : S →ₐ[R] T
Hf : Function.Surjective ⇑f
P : Ideal R
P' : Ideal S
inst✝¹ : P'.IsPrime
inst✝ : P'.LiesOver P
hkP' : ¬RingHom.ker f.toRingHom ≤ P'
H : (P.primesOver S).Finite
q : Ideal T
left✝ : q.IsPrime
right✝ : q.LiesOver P
⊢ comap f q ∈ P.primesOver S

Tactic:
exact ⟨inferInstance, inferInstanceAs ((q.comap f).LiesOver _)⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := ⋯
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := ⋯
this :
  (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    (algebraMap K L) ((f %ₘ g).leadingCoeff ^ g.natDegree) *
      (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)).prod
⊢ (Multiset.map (fun x ↦ (f %ₘ g).leadingCoeff * eval x r) g.roots).prod =
    (f %ₘ g).leadingCoeff ^ g.natDegree * (Multiset.map (fun x ↦ eval x r) g.roots).prod

Tactic:
simp [hg'.natDegree_eq_card_roots]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case tmul.refine_2.C
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
H₁ : ∀ (i : Fin m), (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)
H₂ : ∀ (i : Fin k), (universalFactorizationMap R n m k hn).IsIntegralElem (1 ⊗ₜ[R] X i)
x : MvPolynomial (Fin m) R
a : R
⊢ (universalFactorizationMap R n m k hn).IsIntegralElem (1 ⊗ₜ[R] C a)

Tactic:
simpa [← algebraMap_eq, ← algebraMap_apply, Algebra.algebraMap_eq_smul_one] using!
          (universalFactorizationMap R n m k hn).isIntegralElem_map (x := .C a)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type (max 0 u_1) := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective ⇑φ
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ φ ((f'.scaleRoots g'.leadingCoeff).resultant g'.integralNormalization f'.natDegree g'.natDegree) =
    φ g'.leadingCoeff ^ (f'.natDegree * (g'.natDegree - 1)) * (map φ f').resultant (map φ g') f'.natDegree g'.natDegree

Tactic:
this f' g' (by simpa [natDegree_eq_natDegree eg]) inferInstance

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type (max 0 u_1) := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective ⇑φ
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ φ (g'.leadingCoeff ^ (f'.natDegree * (g'.natDegree - 1)) * f'.resultant g') =
    φ g'.leadingCoeff ^ (f'.natDegree * (g'.natDegree - 1)) * (map φ f').resultant (map φ g') f'.natDegree g'.natDegree
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst✝ : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H : map (algebraMap R P.ResidueField) ↑p = ↑f * ↑g
Hpq : IsCoprime ↑f ↑g
φ : 𝓡' →ₐ[R] P.ResidueField := (homEquiv P.ResidueField m k hn p).symm ⟨(f, g), ⋯⟩
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
x : 𝓡'
⊢ ↑φ x = e.symm ((IsScalarTower.toAlgHom R 𝓡' Q.ResidueField) x)

Tactic:
by simp [e, φ']

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hUV : V ≤ f ⁻¹ᵁ U
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FiniteType
⊢ ∃ U g,
    Etale g ∧ s ∈ Set.range ⇑g ∧ ∃ V W v, IsCompl V W ∧ IsFinite (V.ι ≫ pullback.snd f g) ∧ (pullback.fst f g) ↑v = x

Tactic:
algebraize [(f.appLE U V hUV).hom]

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hUV : V ≤ f ⁻¹ᵁ U
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FiniteType
algInst✝ : Algebra ↑Γ(S, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑Γ(S, U) ↑Γ(X, V)
⊢ ∃ U g,
    Etale g ∧ s ∈ Set.range ⇑g ∧ ∃ V W v, IsCompl V W ∧ IsFinite (V.ι ≫ pullback.snd f g) ∧ (pullback.fst f g) ↑v = x
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X : C
F : Cᵒᵖ ⥤ CommMonCat
α : (F ⋙ forget CommMonCat).RepresentableBy X
this✝ : MonObj X := MonObj.ofRepresentableBy X (F ⋙ forget₂ CommMonCat MonCat) α
this : μ = α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))
⊢ autoParam
    (α.homEquiv' ((β_ X X).hom ≫ fst X X) * α.homEquiv' ((β_ X X).hom ≫ snd X X) =
      α.homEquiv' (fst X X) * α.homEquiv' (snd X X))
    mul_comm._autoParam

Tactic:
braiding_hom_fst,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X : C
F : Cᵒᵖ ⥤ CommMonCat
α : (F ⋙ forget CommMonCat).RepresentableBy X
this✝ : MonObj X := MonObj.ofRepresentableBy X (F ⋙ forget₂ CommMonCat MonCat) α
this : μ = α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))
⊢ autoParam
    (α.homEquiv' (snd X X) * α.homEquiv' ((β_ X X).hom ≫ snd X X) = α.homEquiv' (fst X X) * α.homEquiv' (snd X X))
    mul_comm._autoParam
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: 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
Heq : toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι = V
⊢ ((pullback f fT).isoOfEq Heq).inv ≫ (toNormalization (pullback.snd f fT) ≫ e.hom) ∣_ opensRange ι =
    (isoOpensRange ι).hom

Tactic:
← cancel_mono (Scheme.Opens.ι _)

Goal state after:
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
Heq : toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι = V
⊢ (((pullback f fT).isoOfEq Heq).inv ≫ (toNormalization (pullback.snd f fT) ≫ e.hom) ∣_ opensRange ι) ≫
      (opensRange ι).ι =
    (isoOpensRange ι).hom ≫ (opensRange ι).ι
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
I : Ideal S
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
t : T
x : ↥(Submodule.restrictScalars R I)
⊢ ∃ a,
    (tensorCotangentHom R T I) a =
      (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
        ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) (t ⊗ₜ[R] x), ⋯⟩

Tactic:
use t ⊗ₜ I.toCotangent x
    apply Ideal.cotangentToQuotientSquare_injective
    simp [-AlgHom.toRingHom_eq_coe, tensorCotangentHom_tmul, Algebra.smul_def,
      ← Ideal.Quotient.mk_algebraMap, ← map_mul]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : (⇑f '' ⇑(f ≫ g) ⁻¹' {s}).Finite
inst✝² : IsProper (f ≫ g)
inst✝¹ : IsSeparated g
inst✝ : LocallyOfFiniteType g
this✝ : IsProper f
this : IsProper (Scheme.Hom.imageι f ≫ g)
⊢ ∃ U, s ∈ U ∧ IsFinite ((Scheme.Hom.imageι f ≫ g) ∣_ U)

Tactic:
refine exists_isFinite_morphismRestrict_of_finite_preimage_singleton _ _ ?_

Goal state after:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : (⇑f '' ⇑(f ≫ g) ⁻¹' {s}).Finite
inst✝² : IsProper (f ≫ g)
inst✝¹ : IsSeparated g
inst✝ : LocallyOfFiniteType g
this✝ : IsProper f
this : IsProper (Scheme.Hom.imageι f ≫ g)
⊢ (⇑(Scheme.Hom.imageι f ≫ g) ⁻¹' {s}).Finite
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]
⊢ (P.tensorCotangentSpace T) (t ⊗ₜ[R] (s ⊗ₜ[P.Ring] x)) =
    t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring] (KaehlerDifferential.map R T P.Ring P.baseChange.Ring) x

Tactic:
simp only [tensorCotangentSpace, LinearEquiv.trans_apply, LinearEquiv.restrictScalars_apply,
    ← mk_apply s x, IsTensorProduct.assocOfMapSMul_symm_tmul]

Goal state after:
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]
⊢ (AlgebraTensorModule.congr (LinearEquiv.refl P.baseChange.Ring (T ⊗[R] S))
        (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring P.baseChange.Ring))
      ((AlgebraTensorModule.cancelBaseChange P.Ring P.baseChange.Ring P.baseChange.Ring (T ⊗[R] S) Ω[P.Ring⁄R]).symm
        (((TensorProduct.mk R T S) t) s ⊗ₜ[P.Ring] x)) =
    t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring] (KaehlerDifferential.map R T P.Ring P.baseChange.Ring) x
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : FormallyUnramified T (T ⊗[R] S)
x✝ : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this : Subsingleton (T ⊗[R] Ω[S⁄R])
⊢ Subsingleton Ω[S⁄R]

Tactic:
exact Module.FaithfullyFlat.lTensor_reflects_triviality R T _

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
x✝ : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
⊢ ∀ (x : T), (TensorProduct.comm R S T).toRingEquiv ((algebraMap T (S ⊗[R] T)) x) = (algebraMap T (T ⊗[R] S)) x

Tactic:
by simp [RingHom.algebraMap_toAlgebra]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
h : IsUnit a
x : R
⊢ ord R (a * x) = ord R x

Tactic:
ord,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R
h : IsUnit a
x : R
⊢ Module.length R (R ⧸ span {a * x}) = ord R x
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
h : IsUnit a
x : R
⊢ Module.length R (R ⧸ span {a * x}) = ord R x

Tactic:
ord,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R
h : IsUnit a
x : R
⊢ Module.length R (R ⧸ span {a * x}) = Module.length R (R ⧸ span {x})
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
h : IsUnit a
x : R
⊢ ord R (x * a) = ord R x

Tactic:
ord,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R
h : IsUnit a
x : R
⊢ Module.length R (R ⧸ span {x * a}) = ord R x
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
h : IsUnit a
x : R
⊢ Module.length R (R ⧸ span {x * a}) = ord R x

Tactic:
ord,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R
h : IsUnit a
x : R
⊢ Module.length R (R ⧸ span {x * a}) = Module.length R (R ⧸ span {x})
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
⊢ IsSimpleModule R (R ⧸ span {ϖ})

Tactic:
have : (Ideal.span {ϖ}).IsMaximal :=
    PrincipalIdealRing.isMaximal_of_irreducible hϖ

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
this : (span {ϖ}).IsMaximal
⊢ IsSimpleModule R (R ⧸ span {ϖ})
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x

Tactic:
by_cases hf : f = 0
  · simp [hf]
  by_cases hg : g = 0
  · simp [hg]
  by_cases! hx : coheight x ≠ 1
  · simp [hx]
  rw [inf_le_iff, ord_le_ord_iff hx hx hf hfg, ord_le_ord_iff hx hx hg hfg]
  exact inf_le_iff.mp <| Ring.ordFrac_add (R := X.presheaf.stalk x) _ _ hfg

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
f : ↑Zs → Set A := fun i ↦ Classical.choose ⋯
H : ⋂ i, zeroLocus 𝒜 (f i) ∈ Set.range (zeroLocus 𝒜)
⊢ ⋂ i, ↑i ∈ Set.range (zeroLocus 𝒜)

Tactic:
convert! H using 2

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
f : ↑Zs → Set A := fun i ↦ Classical.choose ⋯
H : ⋂ i, zeroLocus 𝒜 (f i) ∈ Set.range (zeroLocus 𝒜)
⊢ (fun i ↦ ↑i) = fun i ↦ zeroLocus 𝒜 (f i)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), (GradedRing.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ f ∈ z.asHomogeneousIdeal

Tactic:
← DirectSum.sum_support_decompose 𝒜 f

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), (GradedRing.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) f), ↑(((decompose 𝒜) f) i) ∈ z.asHomogeneousIdeal
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
i : ℕ
hi : (GradedRing.proj 𝒜 i) f ∉ z.asHomogeneousIdeal
⊢ z ∈ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f)

Tactic:
mem_basicOpen

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
i : ℕ
hi : (GradedRing.proj 𝒜 i) f ∉ z.asHomogeneousIdeal
⊢ (GradedRing.proj 𝒜 i) f ∉ z.asHomogeneousIdeal
Module: Mathlib.RingTheory.GradedAlgebra.FiniteType

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
s : S
hs : s ∈ ↑F
⊢ ∑ i ∈ DFinsupp.support ((DirectSum.decompose 𝒜) s), ↑(((DirectSum.decompose 𝒜) s) i) ∈
    ↑(Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ))

Tactic:
exact sum_mem fun n hn ↦ Algebra.subset_adjoin (by simpa using ⟨⟨⟨s, hs⟩, n, hn⟩, rfl⟩)

Goal state after: