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

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
P : Presieve U
⊢ U.presieveOfSections (sectionsOfPresieve P) = P

Tactic:
refine funext₂ fun ⟨V, hV⟩ ⟨f, hf⟩ ↦ eq_iff_iff.mpr ⟨?_, ?_⟩
  · rintro ⟨_, H, rfl⟩
    exact H
  · intro H
    obtain rfl : _ = V := hf
    exact ⟨_, H, rfl⟩

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyQuasiFinite f
x : ↥X
⊢ QuasiFiniteAt f x

Tactic:
refine HasRingHomProperty.stalkMap ?_ ‹_› x
  introv hf
  algebraize [f]
  refine .of_comp (g := algebraMap R _) ?_
  convert!
    RingHom.quasiFinite_algebraMap.mpr
      (inferInstance : Algebra.QuasiFinite R (Localization.AtPrime J))
  ext; simp; rfl

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ ∃ q, q ≠ 0 ∧ x⁻¹ = (algebraMap K[X] K⟮X⟯) x.denom / (algebraMap K[X] K⟮X⟯) q

Tactic:
refine ⟨x.num, num_ne_zero hx, ?_⟩

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x⁻¹ = (algebraMap K[X] K⟮X⟯) x.denom / (algebraMap K[X] K⟮X⟯) x.num
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
hx' : Function.Surjective ⇑(aeval x)
⊢ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker (aeval x).toRingHom) =
    RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom

Tactic:
let I := RingHom.ker (aeval (R := R) x).toRingHom

Goal state after:
R : Type u_1
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
hx' : Function.Surjective ⇑(aeval x)
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
⊢ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker (aeval x).toRingHom) =
    RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
Module: Mathlib.RingTheory.Etale.StandardEtale

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
P : StandardEtalePair R
⊢ (algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f}))
      ((aeval X) P.f) =
    0

Tactic:
IsScalarTower.algebraMap_apply _ (Localization.Away P.g) (_ ⧸ _),

Goal state after:
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
P : StandardEtalePair R
⊢ (algebraMap (Localization.Away P.g)
        (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f}))
      ((algebraMap R[X] (Localization.Away P.g)) ((aeval X) P.f)) =
    0
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_2
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
⊢ IsUnit
    ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f}))
      ((aeval X) P.g))

Tactic:
IsScalarTower.algebraMap_apply _ (Localization.Away P.g) (_ ⧸ _),

Goal state after:
case refine_2
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
⊢ IsUnit
    ((algebraMap (Localization.Away P.g)
        (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f}))
      ((algebraMap R[X] (Localization.Away P.g)) ((aeval X) P.g)))
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
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
let I := RingHom.ker (aeval (R := R) x).toRingHom

Goal state after:
case inr
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[(algebraMap S St) (φ X)]
this✝² : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝¹ : Algebra (↥R₂) St := R₂.toAlgebra
this✝ : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h✝ : Nontrivial ↥R₁
⊢ (algebraMap S St) (φ X) ∈ ↑(integralClosure (↥R₁) St)

Tactic:
SetLike.mem_coe,

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[(algebraMap S St) (φ X)]
this✝² : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝¹ : Algebra (↥R₂) St := R₂.toAlgebra
this✝ : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h✝ : Nontrivial ↥R₁
⊢ (algebraMap S St) (φ X) ∈ integralClosure (↥R₁) St
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[(algebraMap S St) (φ X)]
this✝² : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝¹ : Algebra (↥R₂) St := R₂.toAlgebra
this✝ : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h✝ : Nontrivial ↥R₁
⊢ (algebraMap S St) (φ X) ∈ integralClosure (↥R₁) St

Tactic:
mem_integralClosure_iff

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[(algebraMap S St) (φ X)]
this✝² : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝¹ : Algebra (↥R₂) St := R₂.toAlgebra
this✝ : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h✝ : Nontrivial ↥R₁
⊢ IsIntegral (↥R₁) ((algebraMap S St) (φ X))
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: 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✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := ⋯
this✝⁵ : p.IsPrime
this✝⁴ : Module p.ResidueField (p.Fiber S) := ⋯
this✝³ : SMul p.ResidueField (p.Fiber S) := ⋯
this✝² : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := ⋯
this✝¹ : Module.Finite p.ResidueField (p.Fiber S) := ⋯
this✝ : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := ⋯
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField := ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
hsQ' : (algebraMap R Q.ResidueField) s ≠ 0
hrQ' : φ r = 1
e' : (algebraMap R Q.ResidueField) s * φ x = (algebraMap S Q.ResidueField) t
Q' : Ideal S
left✝ : Q'.IsPrime
right✝ : Q'.LiesOver (Ideal.under R Q)
H✝ : Q' ≠ Q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime Q') := ⋯
hsQ'' : (algebraMap R Q'.ResidueField) s ≠ 0
φ' : p.Fiber S →ₐ[p.ResidueField] Q'.ResidueField := ⋯
H : φ' r = 0
⊢ (algebraMap S Q'.ResidueField) t = φ' (1 ⊗ₜ[R] t)

Tactic:
simp [φ']

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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this : IsScalarTower R R[X] S
n : S → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Submodule.span R[X] ↑s = ⊤
x : S
⊢ p.leadingCoeff ^ s.sup n • t * x ∈ Subalgebra.map φ R[ X]

Tactic:
adjoin_X,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this : IsScalarTower R R[X] S
n : S → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Submodule.span R[X] ↑s = ⊤
x : S
⊢ p.leadingCoeff ^ s.sup n • t * x ∈ Subalgebra.map φ ⊤
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
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 : R[X] →ₐ[R] S
H : integralClosure R S = ⊥
hf : ¬conductor R (f X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
this : Algebra (Localization.AtPrime (Ideal.under (↥f.range) p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥f.range) p) p
e : Localization.AtPrime (Ideal.under (↥f.range) p) ≃ₐ[R] Localization.AtPrime p :=
  AlgEquiv.ofBijective
    (IsScalarTower.toAlgHom R (Localization.AtPrime (Ideal.under (↥f.range) p)) (Localization.AtPrime p)) ⋯
⊢ WeaklyQuasiFiniteAt R (Ideal.under (↥f.range) p)

Tactic:
exact .of_algHom_localization _ _ e.symm.toAlgHom e.symm.surjective

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: 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 : Algebra (Localization.AtPrime (Ideal.under (↥R') p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R') p) p
e : Localization.AtPrime (Ideal.under (↥R') p) ≃ₐ[R] Localization.AtPrime p :=
  AlgEquiv.ofBijective (IsScalarTower.toAlgHom R (Localization.AtPrime (Ideal.under (↥R') p)) (Localization.AtPrime p))
    ⋯
⊢ WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)

Tactic:
exact .of_algHom_localization _ _ e.symm.toAlgHom e.symm.surjective

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
⊢ IsDominant (toNormalization f)

Tactic:
by
  have := congr(($(f.ker_toNormalization).support : Set f.normalization))
  rw [IdealSheafData.support_bot, Scheme.Hom.support_ker, TopologicalSpace.Closeds.coe_top] at this
  exact ⟨dense_iff_closure_eq.mpr this⟩

Goal state after:
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
⊢ comap f '' P.primesOver T ⊆ P.primesOver S

pp: case refine_2
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
⊢ P' ∉ comap f '' P.primesOver T

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

Goal state after:
case refine_2
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
⊢ P' ∉ comap f '' P.primesOver T
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.e_a.e_f
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
this :
  (Multiset.map (fun x ↦ eval x f) g.roots).prod =
    (f %ₘ g).leadingCoeff ^ g.natDegree * (Multiset.map (fun x ↦ eval x r) g.roots).prod
x : K
⊢ (aeval ((algebraMap K L) x)) r = (algebraMap K L) (eval x r)

Tactic:
exact aeval_algebraMap_apply _ _ _

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

Goal state before:
pp: case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)

Tactic:
rw [this, ← mul_assoc, ← pow_add, add_comm, ← Nat.mul_add_one, Nat.sub_add_cancel (by lia)]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
G H X : C
inst✝² : GrpObj G
inst✝¹ : GrpObj H
f : X ⟶ G
g : G ⟶ H
inst✝ : IsMonHom g
⊢ f⁻¹ ≫ g = (f ≫ g)⁻¹

Tactic:
by
  simp [Hom.inv_def]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: case e'_2
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝¹⁰ : Nonempty ↥G.left
this✝⁹ : IsProper (G ⊗ G).hom
this✝⁸ : JacobsonSpace ↥(G ⊗ G).left
this✝⁷ : Surjective G.hom
this✝⁶ : IsProper (Over.Hom.left (fst G G))
this✝⁵ : Surjective (Over.Hom.left (fst G G))
this✝⁴ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝³ : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝² : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝¹ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this✝ : IsProper (Over.Hom.left γ)
H✝¹ :
  ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H✝ : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
H : ∀ (x : ↥U), (⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ)).Finite
y : ↥(G ⊗ G).left
hyU : y ∈ ↑(Over.Hom.left (fst G G) ⁻¹ᵁ U)
hy : IsClosed {y}
hx : IsClosed {(Over.Hom.left (fst G G)) y}
x : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ G := Over.homMk (pointOfClosedPoint G.hom ((Over.Hom.left (fst G G)) y) hx) ⋯
xe : ↥(G ⊗ G).left := (Over.Hom.left (fst G G ≫ (ρ_ G).inv ≫ G ◁ η)) y
this : (Over.Hom.left γ) y = xe
⊢ (Over.Hom.left (GrpObj.commutator G)) y = (Over.Hom.left (snd G G)) ((Over.Hom.left γ) y)

Tactic:
simp [γ, ← Scheme.Hom.comp_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsProper f
inst✝ : LocallyQuasiFinite f
⊢ IsFinite f

Tactic:
have : IsIso f.toNormalization :=
    (isIso_iff_isOpenImmersion_and_surjective _).mpr ⟨inferInstance, inferInstance⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsProper f
inst✝ : LocallyQuasiFinite f
this : IsIso (Scheme.Hom.toNormalization f)
⊢ IsFinite f
Module: Mathlib.RingTheory.Finiteness.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✝ : FinitePresentation T (T ⊗[R] S)
this : ∃ n f, Function.Surjective ⇑f
⊢ FinitePresentation R S

Tactic:
obtain ⟨n, f, hf⟩ := this

Goal state after:
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✝ : FinitePresentation T (T ⊗[R] S)
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ FinitePresentation R S
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
x : S ⊗[P.Ring] Ω[P.Ring⁄R]
⊢ (P.tensorCotangentSpace T) (t ⊗ₜ[R] x) = t • (CotangentSpace.map (toBaseChange T)) x

Tactic:
induction x with
  | zero => rw [tmul_zero, LinearEquiv.map_zero, LinearMap.map_zero, smul_zero]
  | add x y hx hy => rw [tmul_add, LinearEquiv.map_add, LinearMap.map_add, smul_add, hx, hy]
  | tmul s y =>
  simp [tensorCotangentSpace_tmul_tmul, CotangentSpace.map_tmul_eq_tmul_map,
    smul_tmul', Algebra.smul_def, RingHom.algebraMap_toAlgebra]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Smooth

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
H : (↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f))ᶜ
hxc : x ∈ closedPoints ↥G
y : ↥G
hyc : y ∈ closedPoints ↥G
x' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨x, hxc⟩) ⋯
y' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨y, hyc⟩) ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
hα : x' ≫ α.hom = y'
hα' : (Over.Hom.left α.hom) x = y
hy : (Over.Hom.left α.hom) x ∈ Scheme.Hom.smoothLocus f
⊢ False

Tactic:
← α.hom.left.mem_preimage,

Goal state after:
K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
H : (↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f))ᶜ
hxc : x ∈ closedPoints ↥G
y : ↥G
hyc : y ∈ closedPoints ↥G
x' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨x, hxc⟩) ⋯
y' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨y, hyc⟩) ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
hα : x' ≫ α.hom = y'
hα' : (Over.Hom.left α.hom) x = y
hy : x ∈ Over.Hom.left α.hom ⁻¹ᵁ Scheme.Hom.smoothLocus f
⊢ False
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
i j : WalkingSpan
t : i ⟶ j
⊢ IsOpenImmersion ((span f g).map t).left

Tactic:
obtain (a | (a | a)) := t

Goal state after:
case id
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
i : WalkingSpan
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i)).left

case init.left
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left)).left

case init.right
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right)).left
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f], finrank f = 1 → (∃ S, X = Spec S) → IsIso f
hX : ¬∃ S, X = Spec S
⊢ IsIso f

pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
hX : ∃ S, X = Spec S
⊢ IsIso f

Tactic:
· have _ : IsAffine X := isAffine_of_isAffineHom f
    rw [← isIso_comp_left_iff X.isoSpec.inv]
    refine this _ _ ?_ ⟨_, rfl⟩
    rw [finrank_comp_left_of_isIso, h]

Goal state after:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
hX : ∃ S, X = Spec S
⊢ IsIso f