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 : Y.AffineZariskiSite
r : ↑Γ(Y, ↑U)
this✝³ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝² : Algebra ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (app f ↑(U.basicOpen r))).toAlgebra
this✝¹ : Algebra ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
  ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this : IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))) r)
    ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r))

Tactic:
let : Algebra ↑Γ(Y, U.1) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
    (f.appLE _ _ (f.preimage_mono (Y.basicOpen_le _))).hom.toAlgebra

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.AffineZariskiSite
r : ↑Γ(Y, ↑U)
this✝⁴ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝³ : Algebra ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (app f ↑(U.basicOpen r))).toAlgebra
this✝² : Algebra ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
  ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this✝¹ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this✝ : IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (appLE f (↑U) (f ⁻¹ᵁ Y.basicOpen r) ⋯)).toAlgebra
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))) r)
    ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r))
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
this :
  (pullbackRestrictIsoRestrict f ↑U).inv ≫
      Cover.trans (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        (pullbackRestrictIsoRestrict f ↑V).hom =
    X.homOfLE ⋯
⊢ (f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑V) ↑Γ(X, f ⁻¹ᵁ ↑V)).val ≫ X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (normalizationGlueData f).functor V =
    (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫
        colimit.ι (normalizationGlueData f).functor U

Tactic:
← colimit.w f.normalizationGlueData.functor i

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
this :
  (pullbackRestrictIsoRestrict f ↑U).inv ≫
      Cover.trans (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        (pullbackRestrictIsoRestrict f ↑V).hom =
    X.homOfLE ⋯
⊢ (f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑V) ↑Γ(X, f ⁻¹ᵁ ↑V)).val ≫ X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (normalizationGlueData f).functor V =
    (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫
        (normalizationGlueData f).functor.map i ≫ colimit.ι (normalizationGlueData f).functor V
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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
x : K
hx : x ∈ g.roots
⊢ (x, x).1 ∈ (g * r).roots ∧ (x, x).2 ∈ g.roots

Tactic:
simp_all [hg.ne_zero]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
q : PrimeSpectrum S
H : IsOpen {⟨q, ⋯⟩}
⊢ QuasiFiniteAt R q.asIdeal

Tactic:
by
  let p := q.comap (algebraMap R S)
  let e := PrimeSpectrum.preimageHomeomorphFiber R S p
  suffices Algebra.QuasiFiniteAt p.asIdeal.ResidueField (e ⟨q, rfl⟩).asIdeal from
    .of_quasiFiniteAt_residueField _ q.asIdeal (e ⟨q, rfl⟩).asIdeal
      congr($(e.symm_apply_apply ⟨q, rfl⟩).1.asIdeal)
  refine .of_isOpen_singleton _ ?_
  rwa [← Set.image_singleton, e.isOpen_image]

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

Goal state before:
pp: case neg
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] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
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
⊢ (algebraMap K L) ((-1) ^ (g.natDegree * (f.natDegree - r.natDegree))) *
        (algebraMap K L) (g.coeff g.natDegree ^ (f.natDegree - r.natDegree)) *
      ((algebraMap K L) ((-1) ^ (r.natDegree * g.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)) =
    (algebraMap K L) (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod

Tactic:
map_sub_roots_sprod_eq_prod_map_eval _ _ hf hf',

Goal state after:
case neg
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] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
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
⊢ (algebraMap K L) ((-1) ^ (g.natDegree * (f.natDegree - r.natDegree))) *
        (algebraMap K L) (g.coeff g.natDegree ^ (f.natDegree - r.natDegree)) *
      ((algebraMap K L) ((-1) ^ (r.natDegree * g.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)) =
    (algebraMap K L) ((-1) ^ (g.roots.card * f.roots.card) * (Multiset.map (fun x ↦ eval x f) g.roots).prod)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
⊢ ∀ b ∈ Finset.antidiagonal ↑j,
    b ≠ (↑j - ↑i, ↑i) →
      (if b.2 < k then
          if h : b.1 < m then if b.2 = ↑i then X (Sum.inl ⟨b.1, h⟩) else 0 else if b.1 = m ∧ b.2 = ↑i then 1 else 0
        else 0) =
        0

pp: case inr.h₁
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
⊢ (↑j - ↑i, ↑i) ∉ Finset.antidiagonal ↑j →
    (if (↑j - ↑i, ↑i).2 < k then
        if h : (↑j - ↑i, ↑i).1 < m then if (↑j - ↑i, ↑i).2 = ↑i then X (Sum.inl ⟨(↑j - ↑i, ↑i).1, h⟩) else 0
        else if (↑j - ↑i, ↑i).1 = m ∧ (↑j - ↑i, ↑i).2 = ↑i then 1 else 0
      else 0) =
      0

Tactic:
· simp only [Finset.mem_antidiagonal, ne_eq, ite_eq_right_iff, Prod.forall, Prod.mk.injEq]
      intro a b _ _ _
      simp [show b ≠ i by lia]

Goal state after:
case inr.h₁
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
⊢ (↑j - ↑i, ↑i) ∉ Finset.antidiagonal ↑j →
    (if (↑j - ↑i, ↑i).2 < k then
        if h : (↑j - ↑i, ↑i).1 < m then if (↑j - ↑i, ↑i).2 = ↑i then X (Sum.inl ⟨(↑j - ↑i, ↑i).1, h⟩) else 0
        else if (↑j - ↑i, ↑i).1 = m ∧ (↑j - ↑i, ↑i).2 = ↑i then 1 else 0
      else 0) =
      0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]), p.Splits → P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
    Function.Injective ⇑φ → ∀ (p : R[X]), P (map φ p) → P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
    Function.Surjective ⇑φ → ∀ (p : S[X]), (∀ (q : R[X]), P q) → P p
R : Type u
inst✝ : CommRing R
p : R[X]
hR✝ : IsDomain R
hR : IsField R
this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]), IsDomain R → IsField R → p.Splits → P p
hp : ¬p.Splits
inst : Field R := hR.toField
⊢ P p

Tactic:
exact injective _ _ _ (algebraMap R p.SplittingField).injective _
      (this _ inferInstance (Field.toIsField _) (SplittingField.splits _))

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

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
H : IsCoprime 0 g
⊢ ∃ n, resultant 0 g ∣ leadingCoeff 0 ^ n

pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
· simp only [isCoprime_zero_left, isUnit_iff] at H
    aesop

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
H : IsCoprime 0 g
⊢ resultant 0 g ≠ 0

pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
⊢ f.resultant g ≠ 0

Tactic:
· simp only [isCoprime_zero_left, isUnit_iff] at H
    aesop

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
⊢ f.resultant g ≠ 0
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: 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
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this✝ : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) S := Algebra.compHom S ((MvPolynomial.mapEquivMonic R R n).symm p).toRingHom
⊢ (fun q ↦
        Algebra.TensorProduct.lift (Algebra.ofId R S)
          (let __RingHom :=
            (↑((MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn (p.map (algebraMap R S))).symm
                  q)).toRingHom;
          { toRingHom := __RingHom, commutes' := ⋯ })
          ⋯)
      ((fun f ↦ ⟨((factor₁ m k hn p).map ↑f, (factor₂ m k hn p).map ↑f), ⋯⟩) f) =
    f

Tactic:
have : IsScalarTower (MvPolynomial (Fin n) R) R S := .of_algebraMap_eq' rfl

Goal state after:
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
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝² : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this✝¹ : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
this✝ : Algebra (MvPolynomial (Fin n) R) S := Algebra.compHom S ((MvPolynomial.mapEquivMonic R R n).symm p).toRingHom
this : IsScalarTower (MvPolynomial (Fin n) R) R S
⊢ (fun q ↦
        Algebra.TensorProduct.lift (Algebra.ofId R S)
          (let __RingHom :=
            (↑((MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn (p.map (algebraMap R S))).symm
                  q)).toRingHom;
          { toRingHom := __RingHom, commutes' := ⋯ })
          ⋯)
      ((fun f ↦ ⟨((factor₁ m k hn p).map ↑f, (factor₂ m k hn p).map ↑f), ⋯⟩) f) =
    f
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
a b : B
f g h i : a ⟶ b
inst✝ : BicategoricalCoherence g h
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
θ : h ⟶ i
θ' : h ≅ i
ih_θ : θ'.hom = θ
⊢ (η' ≪⊗≫ θ').hom = η ⊗≫ θ

Tactic:
by
  simp [ih_η, ih_θ, bicategoricalIsoComp, bicategoricalComp]

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

Goal state before:
pp: case insert
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
a : S
s : Finset S
has : a ∉ s
IH : ∃ S' x x_1, ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, ↑s ⊆ ↑f.range
⊢ ∃ S' x x_1,
    ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, ↑(insert a s) ⊆ ↑f.range

Tactic:
obtain ⟨S', _, _, _, _, _, f, hsf⟩ := IH

Goal state after:
case insert
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
a : S
s : Finset S
has : a ∉ 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
⊢ ∃ S' x x_1,
    ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, ↑(insert a s) ⊆ ↑f.range
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: case insert
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
a : S
s : Finset S
has : a ∉ 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
ha : IsIntegral R a
this : Module.Finite S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
⊢ ∃ S' x x_1,
    ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, ↑(insert a s) ⊆ ↑f.range

Tactic:
have := ((minpoly.monic ha).map (algebraMap R S')).free_adjoinRoot

Goal state after:
case insert
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
a : S
s : Finset S
has : a ∉ 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
ha : IsIntegral R a
this✝ : Module.Finite S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
this : Free S' (AdjoinRoot (Polynomial.map (algebraMap R S') (minpoly R a)))
⊢ ∃ S' x x_1,
    ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, ↑(insert a s) ⊆ ↑f.range
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑f
h1 : g.Finite
h2 : g.Flat
x : PrimeSpectrum S
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.Finite S T
algebraizeInst✝ : Module.Flat S T
this✝ : Module.Finite R T
this : Module.Flat R T
⊢ (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x

Tactic:
have : Algebra.IsPushout R T S T := .of_bijective_left _ _ hg

Goal state after:
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑f
h1 : g.Finite
h2 : g.Flat
x : PrimeSpectrum S
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.Finite S T
algebraizeInst✝ : Module.Flat S T
this✝¹ : Module.Finite R T
this✝ : Module.Flat R T
this : Algebra.IsPushout R T S T
⊢ (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X S Y : Scheme
f : X ⟶ Y
g : Y ⟶ S
inst✝² : IsIso f
inst✝¹ : Flat g
inst✝ : IsFinite g
⊢ finrank (f ≫ g) = finrank g

Tactic:
ext z
  let e : pullback (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z)) ≅
      pullback g (S.affineOpenCover.f (S.affineOpenCover.idx z)) :=
    (pullbackRightPullbackFstIso g (S.affineOpenCover.f (S.affineOpenCover.idx z)) f).symm ≪≫
      asIso (pullback.snd f (pullback.fst g (S.affineOpenCover.f _)))
  have : e.hom ≫ pullback.snd _ _ = pullback.snd _ _ := by simp [e]
  rw [finrank, finrank, ← this, IsAffine.finrank_comp_left_of_isIso]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
⊢ ord R (-x) = ord R x

Tactic:
simp [ord_eq_of_associated (x := -x) (y := x) (by simp)]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsNoetherianRing R
inst✝³ : KrullDimLE 1 R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : x ≠ 0
m : ℕ
hm : ↑m = ord R x
⊢ 1 ≤ (ordMonoidWithZeroHom R) x

Tactic:
ordMonoidWithZeroHom_eq_coe _ (by simpa) hm.symm,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsNoetherianRing R
inst✝³ : KrullDimLE 1 R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : x ≠ 0
m : ℕ
hm : ↑m = ord R x
⊢ 1 ≤ ↑(Multiplicative.ofAdd ↑m)
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✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ Localization.mk ↑(-c1).num ⟨↑(-c1).den, ⋯⟩ = Localization.mk ↑(-c2).num ⟨↑(-c2).den, ⋯⟩

Tactic:
simp only [num_neg, den_neg, ← Localization.neg_mk]

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝² : CommRing A
inst✝¹ : SetLike σ A
inst✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ -Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = -Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
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
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k + k) • m),
    (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) * num z)

Tactic:
rw [← smul_eq_mul, add_smul,
    DirectSum.degree_eq_of_mem_mem 𝒜 (SetLike.pow_mem_graded _ hf) (hk.symm ▸ z.den_mem_deg) hfk]

Goal state after:
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
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k) • m + deg z),
    (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) • num z)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
U : (Spec R).Opens
f : ↑R
hf : U ≤ PrimeSpectrum.basicOpen f
⊢ IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, U))) f)

Tactic:
rw [Module.End.isUnit_iff]
  have : ⇑((algebraMap R (Module.End ↑R ↑Γ(M, U))) f) =
      algebraMap (Γ(Spec R, U)) (Module.End Γ(Spec R, U) Γ(M, U))
        (((Spec R).presheaf.map (homOfLE hf).op) <| algebraMap R _ f) :=
    rfl
  rw [this, ← Module.End.isUnit_iff]
  exact ((IsLocalization.Away.algebraMap_isUnit _).map _).map _

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

Goal state before:
pp: A B C σ τ ψ : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
p : ↥(Proj ℬ)
x : ↑((Proj 𝒜).presheaf.stalk ((ConcreteCategory.hom (sheafedSpaceMap f hf).hom.base) p))
this : IsLocalHom (CommRingCat.Hom.hom (stalkIso ℬ p).inv)
hx :
  IsUnit
    ((localRingHom f ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal p.asHomogeneousIdeal.toIdeal ⋯)
      ((CommRingCat.Hom.hom (stalkIso 𝒜 ((ProjectiveSpectrum.comap f hf) p)).hom) x))
⊢ IsUnit x

Tactic:
replace hx := IsLocalHom.map_nonunit _ hx

Goal state after:
A B C σ τ ψ : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
p : ↥(Proj ℬ)
x : ↑((Proj 𝒜).presheaf.stalk ((ConcreteCategory.hom (sheafedSpaceMap f hf).hom.base) p))
this : IsLocalHom (CommRingCat.Hom.hom (stalkIso ℬ p).inv)
hx : IsUnit ((CommRingCat.Hom.hom (stalkIso 𝒜 ((ProjectiveSpectrum.comap f hf) p)).hom) x)
⊢ IsUnit x