mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
r : R
⊢ (RatFunc.mk ((algebraMap R K[X]) r) 1).toFractionRing = (algebraMap R (FractionRing K[X])) r

Tactic:
mk_one'

Goal state after:
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
r : R
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) ((algebraMap R K[X]) r) }.toFractionRing =
    (algebraMap R (FractionRing K[X])) r
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ (toFractionRingRingEquiv K).symm = (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) K⟮X⟯).toRingEquiv

Tactic:
ext x

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : FractionRing K[X]
⊢ (toFractionRingRingEquiv K).symm x = (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) K⟮X⟯).toRingEquiv x
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case e'_1
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X : Scheme} {x : ↥X} (R : CommRingCat) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    (∃ S, X = Spec S) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := ⋯
⊢ QuasiFiniteAt f ((X.affineCover.f i) x) ↔ QuasiFiniteAt (ι ≫ f) x

Tactic:
exact quasiFiniteAt_comp_iff_of_isOpenImmersion.symm

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case neg
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
hf : ¬Module.Finite k⟮X⟯ K⟮X⟯
⊢ Module.finrank k⟮X⟯ K⟮X⟯ = Module.finrank k K

Tactic:
· have hf' : ¬ Module.Finite k K := by
      rwa [← Module.rank_lt_aleph0_iff, ← rank_ratFunc_ratFunc, Module.rank_lt_aleph0_iff]
    rw [Module.finrank_of_not_finite hf, Module.finrank_of_not_finite hf']

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

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
P : StandardEtalePair R
S : Type u_1
x✝¹ : CommRing S
x✝ : Algebra R S
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
⊢ ∃! a, ↑a - x ∈ I

Tactic:
obtain ⟨ε, ⟨hεI, hε⟩, H⟩ := P.existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot I hI _ hx

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
P : StandardEtalePair R
S : Type u_1
x✝¹ : CommRing S
x✝ : Algebra R S
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
ε : S
H : ∀ (y : S), (fun ε ↦ ε ∈ I ∧ P.HasMap (x + ε)) y → y = ε
hεI : ε ∈ I
hε : P.HasMap (x + ε)
⊢ ∃! a, ↑a - x ∈ I
Module: Mathlib.RingTheory.Etale.StandardEtale

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
P : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : f₁ P.x = f₂ P.x
this : f₁.comp ↑P.equivRing.symm = f₂.comp ↑P.equivRing.symm
⊢ f₁ = f₂

Tactic:
ext x

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
P : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : f₁ P.x = f₂ P.x
this : f₁.comp ↑P.equivRing.symm = f₂.comp ↑P.equivRing.symm
x : S
⊢ f₁ x = f₂ x
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case e_5
R : Type u_1
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Q.LiesOver P
inst✝² : IsUnramifiedAt R Q
x : S
p : R[X]
inst✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
hp₂ : R[x] = ⊤
Q' : Ideal (P.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S P) ⟨Q, ⋯⟩).asIdeal
this✝⁴ : Q'.LiesOver Q
this✝³ : Q'.LiesOver P
this✝² : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver Q Q'
this✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver P Q'
this✝ : IsUnramifiedAt P.ResidueField Q'
this : Function.Surjective ⇑(aeval (1 ⊗ₜ[R] x))
r : IsLocalRing.ResidueField (Localization.AtPrime P)
⊢ algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P)) (IsLocalRing.ResidueField (Localization.AtPrime Q')) =
    algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P)) (IsLocalRing.ResidueField (Localization.AtPrime Q'))

Tactic:
ext x

Goal state after:
case e_5
R : Type u_1
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Q.LiesOver P
inst✝² : IsUnramifiedAt R Q
x✝ : S
p : R[X]
inst✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (aeval (1 ⊗ₜ[R] x✝)).toRingHom
hp₂ : R[x✝] = ⊤
Q' : Ideal (P.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S P) ⟨Q, ⋯⟩).asIdeal
this✝⁴ : Q'.LiesOver Q
this✝³ : Q'.LiesOver P
this✝² : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver Q Q'
this✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver P Q'
this✝ : IsUnramifiedAt P.ResidueField Q'
this : Function.Surjective ⇑(aeval (1 ⊗ₜ[R] x✝))
r : IsLocalRing.ResidueField (Localization.AtPrime P)
x : R
⊢ ((algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
            (IsLocalRing.ResidueField (Localization.AtPrime Q'))).comp
        (algebraMap R P.ResidueField))
      x =
    ((algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
            (IsLocalRing.ResidueField (Localization.AtPrime Q'))).comp
        (algebraMap R P.ResidueField))
      x
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
s : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
this✝ :
  ∀ (r : ↑s),
    IsLocalizedModule.Away (↑r)
      (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
φ : (r : ↑s) → ↥(integralClosure S (S ⊗[R] B)) →ₐ[S] ↥(integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B)) :=
  fun r ↦
    ((Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R B)).comp
          (integralClosure S (S ⊗[R] B)).val).codRestrict
      (Subalgebra.restrictScalars S (integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B))) ⋯
this : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (φ r).toLinearMap
r : ↑s
⊢ (IsLocalizedModule.map (Submonoid.powers ↑r)
          (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
          (φ r).toLinearMap)
        (toIntegralClosure R S B).toLinearMap ∘ₗ
      (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap =
    ↑S (toIntegralClosure R (Sᵣ r) B).toLinearMap ∘ₗ
      (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap

Tactic:
ext x

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
s : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
this✝ :
  ∀ (r : ↑s),
    IsLocalizedModule.Away (↑r)
      (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
φ : (r : ↑s) → ↥(integralClosure S (S ⊗[R] B)) →ₐ[S] ↥(integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B)) := ⋯
this : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (φ r).toLinearMap
r : ↑s
x : ↥(integralClosure R B)
⊢ ↑(((AlgebraTensorModule.curry
            ((IsLocalizedModule.map (Submonoid.powers ↑r)
                  (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
                  (φ r).toLinearMap)
                (toIntegralClosure R S B).toLinearMap ∘ₗ
              (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap))
          1)
        x) =
    ↑(((AlgebraTensorModule.curry
            (↑S (toIntegralClosure R (Sᵣ r) B).toLinearMap ∘ₗ
              (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap))
          1)
        x)
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_4
x : MvPolynomial σ R ⊗[R] B
hx : x ∈ integralClosure (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)
e₀ : MvPolynomial σ R ⊗[R] B ≃ₐ[R] MvPolynomial σ B :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) B).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R B))
e₁ : MvPolynomial σ R ⊗[R] ↥(integralClosure R B) ≃ₐ[R] MvPolynomial σ ↥(integralClosure R B) :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) ↥(integralClosure R B)).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R ↥(integralClosure R B)))
e : MvPolynomial σ R ⊗[R] B ≃ₐ[MvPolynomial σ R] MvPolynomial σ B :=
  let __RingEquiv := e₀.toRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : ∀ (n : σ →₀ ℕ), IsIntegral R (MvPolynomial.coeff n (e x))
y : MvPolynomial σ ↥(integralClosure R B)
hy : (MvPolynomial.map (integralClosure R B).val.toRingHom) y = e x
⊢ ∃ a, (toIntegralClosure R (MvPolynomial σ R) B) a = ⟨x, hx⟩

Tactic:
refine ⟨e₁.symm y, Subtype.ext <| e.injective (.trans ?_ hy)⟩

Goal state after:
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_4
x : MvPolynomial σ R ⊗[R] B
hx : x ∈ integralClosure (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)
e₀ : MvPolynomial σ R ⊗[R] B ≃ₐ[R] MvPolynomial σ B :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) B).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R B))
e₁ : MvPolynomial σ R ⊗[R] ↥(integralClosure R B) ≃ₐ[R] MvPolynomial σ ↥(integralClosure R B) :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) ↥(integralClosure R B)).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R ↥(integralClosure R B)))
e : MvPolynomial σ R ⊗[R] B ≃ₐ[MvPolynomial σ R] MvPolynomial σ B :=
  let __RingEquiv := e₀.toRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : ∀ (n : σ →₀ ℕ), IsIntegral R (MvPolynomial.coeff n (e x))
y : MvPolynomial σ ↥(integralClosure R B)
hy : (MvPolynomial.map (integralClosure R B).val.toRingHom) y = e x
⊢ e ↑((toIntegralClosure R (MvPolynomial σ R) B) (e₁.symm y)) = (MvPolynomial.map (integralClosure R B).val.toRingHom) y
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsStandardEtale R S
Sₛ : Type u_4
inst✝⁴ : CommRing Sₛ
inst✝³ : Algebra S Sₛ
inst✝² : Algebra R Sₛ
inst✝¹ : IsScalarTower R S Sₛ
s : S
inst✝ : IsLocalization.Away s Sₛ
⊢ IsStandardEtale R Sₛ

Tactic:
have P : StandardEtalePresentation R S := IsStandardEtale.nonempty_standardEtalePresentation.some
  obtain ⟨p, n, hp⟩ := P.exists_mul_aeval_x_g_pow_eq_aeval_x s
  let P' : StandardEtalePair R := ⟨P.f, P.monic_f, p * P.g, have ⟨p₁, p₂, m, e⟩ := P.cond;
    ⟨p₁ * p ^ m, p₂ * p ^ m, m, by linear_combination e * p ^ m⟩⟩
  let S' := Localization.Away (AdjoinRoot.mk P.f P.g)
  let e : S ≃ₐ[R] S' := P.equivRing.trans P.P.equivAwayAdjoinRoot
  have := IsLocalization.Away.mul S' (Localization.Away (algebraMap _ S' (AdjoinRoot.mk P.f p)))
    (AdjoinRoot.mk P.f P.g) (.mk _ p)
  rw [← map_mul] at this
  have H : Submonoid.map e.symm.toRingEquiv.toMonoidHom (.powers
      (algebraMap _ S' (AdjoinRoot.mk P.f p))) = .powers (aeval P.x p) := by
    have : ((e.symm.toAlgHom.comp (IsScalarTower.toAlgHom R _ S')).comp (AdjoinRoot.mkₐ P.f)) =
      aeval P.x := by ext; simp [e, StandardEtalePair.equivAwayAdjoinRoot]
    rw [Submonoid.map_powers]
    exact congr(Submonoid.powers ($this p))
  have : IsLocalization.Away (aeval P.x p) Sₛ :=
    IsLocalization.Away.of_associated (r := s) ⟨(P.hasMap.2.pow n).unit, hp⟩
  let e₁ : P'.Ring ≃ₐ[R]
      Localization.Away (algebraMap _ S' (AdjoinRoot.mk P.f p)) :=
    P'.equivAwayAdjoinRoot.trans ((IsLocalization.algEquiv (.powers (AdjoinRoot.mk P.f (p * P.g)))
      (Localization.Away (AdjoinRoot.mk P.f (p * P.g))) _).restrictScalars R)
  let e₂ : Localization.Away (algebraMap _ S' (AdjoinRoot.mk P.f p)) ≃ₐ[R] Sₛ :=
    { __ := IsLocalization.ringEquivOfRingEquiv _ _ _ H,
      commutes' r := by
        simp [IsScalarTower.algebraMap_apply R S' (Localization.Away _),
          - AlgEquiv.symm_toRingEquiv, IsScalarTower.algebraMap_eq R S Sₛ] }
  exact .of_equiv (e₁.trans e₂)

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case hb
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) := ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := ⋯
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
⊢ (AlgHom.restrictScalars R (AlgHom.restrictScalars R (toIntegralClosure R S B))).comp
      Algebra.TensorProduct.includeRight =
    (AlgHom.restrictScalars R
          ↑(AlgEquiv.restrictScalars R
              (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
                (S ⊗[R] ↥(integralClosure R B)) ↥(integralClosure S (S ⊗[R] B))))).comp
      Algebra.TensorProduct.includeRight

Tactic:
ext x

Goal state after:
case hb
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) := ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := ⋯
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
x : ↥(integralClosure R B)
⊢ ↑(((AlgHom.restrictScalars R (AlgHom.restrictScalars R (toIntegralClosure R S B))).comp
          Algebra.TensorProduct.includeRight)
        x) =
    ↑(((AlgHom.restrictScalars R
              ↑(AlgEquiv.restrictScalars R
                  (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
                    (S ⊗[R] ↥(integralClosure R B)) ↥(integralClosure S (S ⊗[R] B))))).comp
          Algebra.TensorProduct.includeRight)
        x)
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
⊢ a ∈ Algebra.adjoin S ↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B))

Tactic:
have 𝓟 := Classical.ofNonempty (α := StandardEtalePresentation R S)

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
⊢ a ∈ Algebra.adjoin S ↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B))
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case inr
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : FiniteType R S
inst✝ : IsUnramifiedAt R Q
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
    [inst_3 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q],
    Unramified R S → ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H : ¬Unramified R S
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨s, hsQ, hs⟩ := exists_formallyUnramified_of_isUnramifiedAt (R := R) Q
    have hQ : (Ideal.map (algebraMap S (Localization.Away s)) Q).IsPrime :=
      IsLocalization.isPrime_of_isPrime_disjoint (.powers s) _ _ ‹_› (by simp [Set.disjoint_iff,
        Set.ext_iff, Submonoid.mem_powers_iff, mt (‹Q.IsPrime›.mem_of_pow_mem _) hsQ])
    have inst : Unramified R (Localization.Away s) := {}
    obtain ⟨f, hf, H⟩ := this (R := R)
      (Q.map (algebraMap _ (Localization.Away s))) inferInstance
    obtain ⟨f, t, rfl⟩ := IsLocalization.exists_mk'_eq (.powers s) f
    refine ⟨s * f, ?_, ?_⟩
    · simpa [IsLocalization.mk'_mem_map_algebraMap_iff, Submonoid.mem_powers_iff,
        Ideal.IsPrime.mul_mem_left_iff, hsQ, (mt (‹Q.IsPrime›.mem_of_pow_mem _) hsQ)] using hf
    obtain ⟨P, φ, hφ⟩ : HasStandardEtaleSurjectionOn R (algebraMap S (Localization.Away s) f) :=
      H.of_dvd ⟨algebraMap _ _ t.1, by simp⟩
    exact .mk _ hφ

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✝² : IsReduced S
x✝ : S
hx' : (aeval x✝).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
left✝ : IsDomain S
right✝ : FaithfulSMul R S
this✝ : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra (↥R') L := adjoin ↥R' ↑(algebraMap S L).range
x : S
⊢ (IsScalarTower.toAlgHom R S L) x ∈ Subalgebra.restrictScalars R S'

Tactic:
by
    simpa using show algebraMap S L x ∈ S' from Algebra.subset_adjoin ⟨x, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U V : (TopologicalSpace.Opens ↥Y)ᵒᵖ
i : U ⟶ V
⊢ Y.presheaf.map i ≫
      CommRingCat.ofHom
        (algebraMap ↑Γ(Y, Opposite.unop V) ↥(integralClosure ↑Γ(Y, Opposite.unop V) ↑Γ(X, f ⁻¹ᵁ Opposite.unop V))) =
    CommRingCat.ofHom
        (algebraMap ↑Γ(Y, Opposite.unop U) ↥(integralClosure ↑Γ(Y, Opposite.unop U) ↑Γ(X, f ⁻¹ᵁ Opposite.unop U))) ≫
      (normalizationDiagram f).map i

Tactic:
ext x

Goal state after:
X Y : Scheme
f : X ⟶ Y
U V : (TopologicalSpace.Opens ↥Y)ᵒᵖ
i : U ⟶ V
x : ↑(Y.presheaf.obj U)
⊢ (CommRingCat.Hom.hom
        (Y.presheaf.map i ≫
          CommRingCat.ofHom
            (algebraMap ↑Γ(Y, Opposite.unop V) ↥(integralClosure ↑Γ(Y, Opposite.unop V) ↑Γ(X, f ⁻¹ᵁ Opposite.unop V)))))
      x =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (algebraMap ↑Γ(Y, Opposite.unop U) ↥(integralClosure ↑Γ(Y, Opposite.unop U) ↑Γ(X, f ⁻¹ᵁ Opposite.unop U))) ≫
          (normalizationDiagram f).map i))
      x
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
n : ℕ
r : R
hg : g.natDegree ≤ n
⊢ (X + C r).resultant g 1 n = (X - -C r).resultant g 1 n

Tactic:
sub_neg_eq_add

Goal state after:
R : Type u_1
inst✝ : CommRing R
g : R[X]
n : ℕ
r : R
hg : g.natDegree ≤ n
⊢ (X + C r).resultant g 1 n = (X + C r).resultant g 1 n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
m : ℕ
r : R
hf : f.natDegree ≤ m
⊢ f.resultant (X + C r) m 1 = f.resultant (X - -C r) m 1

Tactic:
sub_neg_eq_add

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
m : ℕ
r : R
hf : f.natDegree ≤ m
⊢ f.resultant (X + C r) m 1 = f.resultant (X + C r) m 1
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] := 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) ((f %ₘ g).leadingCoeff ^ g.natDegree))⁻¹ *
      (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.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) ((f %ₘ g).leadingCoeff ^ g.natDegree) ≠ 0

Tactic:
by simp [hr₀]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
⊢ pullback.snd (fromNormalization f) g ⁻¹ᵁ V =
    pullback.snd (fromNormalization f) g ⁻¹ᵁ g ⁻¹ᵁ U ⊓ pullback.snd (fromNormalization f) g ⁻¹ᵁ V

Tactic:
← Scheme.Hom.preimage_inf,

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
⊢ pullback.snd (fromNormalization f) g ⁻¹ᵁ V = pullback.snd (fromNormalization f) g ⁻¹ᵁ (g ⁻¹ᵁ U ⊓ V)