mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
hJ✝ : J ≤ P.ker
hJ : P.ker ≤ J ⊔ P.ker • P.ker
g : P.Ring
hgmem : g - 1 ∈ P.ker
hg : g • P.ker ≤ J
D : Aux P b₀ := { f := f, hf := hf, g := g, hgmem := hgmem, hg := hg }
⊢ ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
exact ⟨D.pres, D.basis, D.pres_val_comp_inr, D.basis_apply⟩

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

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
⊢ Subsingleton (KaehlerDifferential.ideal R S).Cotangent

Tactic:
exact inferInstanceAs <| Subsingleton Ω[S⁄R]

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
⊢ False

Tactic:
classical
  replace H (ι : Type u_3) (_ : Fintype ι) (v : ι → K) (hv : LinearIndependent k v) :
      LinearIndependent k (v · ^ p) := by
    simpa only [Finset.coe_image, Finset.coe_univ, Set.image_univ, linearIndepOn_range_iff
      hv.injective] using! H (Finset.univ.image v) (by simpa using! hv.linearIndepOn_id)
  have := mt (H F.support inferInstance (fun s ↦ aeval a (monomial (σ' s) (1 : k)))) (by
    simp_rw [← map_pow, monomial_pow, ← hσ'', one_pow, not_linearIndependent_iff]
    refine ⟨.univ, (F.coeff ·), ?_, by simpa [MvPolynomial.eq_zero_iff] using! hF0⟩
    simp only [← map_smul, ← map_sum, Finset.univ_eq_attach, smul_eq_mul, mul_one]
    rw [F.support.sum_attach (fun i ↦ monomial i (F.coeff i)), support_sum_monomial_coeff, hFa])
  simp only [LinearIndependent, injective_iff_map_eq_zero, not_forall] at this
  obtain ⟨F', hF', hF'0⟩ := this
  let F'' : MvPolynomial ι k := .ofCoeff <| F'.mapDomain fun s ↦ σ' s.1
  have hF''0 : F'' ≠ 0 := ne_of_ne_of_eq (AddMonoidAlgebra.ofCoeff_eq_zero.ne.2 <|
    (Finsupp.mapDomain_injective fun s t h ↦ Subtype.ext
    (Finsupp.ext fun i ↦ by rw [hσ' _ s.2, hσ' _ t.2, h])).ne hF'0) (by simp)
  have hF'' : aeval a F'' = 0 := by
    have : (aeval a).toLinearMap ∘ₗ (AddMonoidAlgebra.coeffLinearEquiv _).symm.toLinearMap ∘ₗ
      Finsupp.lmapDomain k k (fun s : F.support ↦ σ' s) =
        (Finsupp.linearCombination k fun s : F.support ↦ aeval a (monomial (σ' s) (1 : k))) := by
      ext v; simp [monomial]
    simp only [← hF', F'', ← this]; rfl
  suffices hpm : p * F''.totalDegree ≤ F.totalDegree by
    have hF''0' : F''.totalDegree ≠ 0 := by
      contrapose hF''0
      rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, aeval_C, map_eq_zero] at hF''
      rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, hF'', map_zero]
    replace this := hpm.trans ((HF F'' hF''0 hF'').trans_eq (one_mul _).symm)
    exact hp.one_lt.not_ge ((mul_le_mul_iff_of_pos_right hF''0'.bot_lt).mp this)
  rw [totalDegree, Finset.mul_sup₀, Finset.sup_le_iff]
  intro σ hσ
  obtain ⟨σ, hσ₂, rfl⟩ := Finset.mem_image.mp (Finsupp.mapDomain_support hσ)
  refine le_trans ?_ (Finset.le_sup σ.2)
  conv_rhs => rw [hσ' _ σ.2, Finsupp.sum_smul_index (fun _ ↦ rfl), ← Finsupp.mul_sum]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
hZ : IsUnit (W.addZ P Q)
⊢ ![W.addX P Q, W.addY P Q, W.addZ P Q] =
    ![W.addZ P Q *
        ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          x,
      W.addZ P Q *
        ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          y,
      W.addZ P Q *
        ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          z]

Tactic:
← addX_of_Z_ne_zero hP hQ hPz hQz hx,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
hZ : IsUnit (W.addZ P Q)
⊢ ![W.addX P Q, W.addY P Q, W.addZ P Q] =
    ![W.addZ P Q *
        ![W.addX P Q / W.addZ P Q,
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          x,
      W.addZ P Q *
        ![W.addX P Q / W.addZ P Q,
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          y,
      W.addZ P Q *
        ![W.addX P Q / W.addZ P Q,
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          z]
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain S
inst✝³ : FaithfulSMul R S
inst✝² : Algebra.IsIntegral R S
inst✝¹ : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
⊢ ∀ (Q : Ideal S) [Q.IsPrime], p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
Q

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain S
inst✝³ : FaithfulSMul R S
inst✝² : Algebra.IsIntegral R S
inst✝¹ : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
Q : Ideal S
⊢ ∀ [Q.IsPrime], p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
⊢ ∀ (n : ℕ), 1 • (algebraMap R S) r ^ n ∈ (algebraMap R S).range

Tactic:
by simp [← map_pow]

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z
lem :
  ∀ {a : R},
    a ∈ I →
      l a • (algebraMap R S) a * (algebraMap R S) p ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
⊢ ∀ x_1 ∈ l.support,
    (fun a c ↦ c • (algebraMap R S) a * (algebraMap R S) p) x_1 (l x_1) ∈
      ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
· intro y hy
    exact lem ((Finsupp.mem_supported _ l).mp H hy)

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

Goal state before:
pp: case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
pq p'q' : R[X] × ↥R[X]⁰
⊢ ({ toFractionRing := Localization.mk pq.1 pq.2 } * { toFractionRing := Localization.mk p'q'.1 p'q'.2 }).liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := Localization.mk pq.1 pq.2 }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      { toFractionRing := Localization.mk p'q'.1 p'q'.2 }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯

Tactic:
| _ p'q'
     => 

Goal state after:
case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
pq p'q' : R[X] × ↥R[X]⁰
⊢ ({ toFractionRing := Localization.mk pq.1 pq.2 } * { toFractionRing := Localization.mk p'q'.1 p'q'.2 }).liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := Localization.mk pq.1 pq.2 }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      { toFractionRing := Localization.mk p'q'.1 p'q'.2 }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ ∃ p, x + y = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) (x.denom * y.denom)

Tactic:
refine ⟨x.num * y.denom + x.denom * y.num, ?_⟩

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ x + y = (algebraMap K[X] K⟮X⟯) (x.num * y.denom + x.denom * y.num) / (algebraMap K[X] K⟮X⟯) (x.denom * y.denom)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ Associated x⁻¹.num x.denom

Tactic:
apply associated_of_dvd_dvd (num_inv_dvd hx)

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x.denom ∣ x⁻¹.num
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)
ε : S
H : ∀ (y : S), (fun ε ↦ ε ∈ I ∧ P.HasMap (x + ε)) y → y = ε
hεI : ε ∈ I
hε : P.HasMap (x + ε)
⊢ ∃! a, ↑a - x ∈ I

Tactic:
exact ⟨⟨x + ε, hε⟩, by simpa, fun y hy ↦
    Subtype.ext (sub_eq_iff_eq_add'.mp (H _ ⟨hy, by simpa using y.2⟩))⟩

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
⊢ P.Ring ≃ₐ[R] Localization.Away ((AdjoinRoot.mk P.f) P.g)

Tactic:
by
  refine .ofAlgHom (P.lift (algebraMap (AdjoinRoot P.f) _ (.root P.f)) ⟨?_, ?_⟩)
    (IsLocalization.Away.liftAlgHom (AdjoinRoot.mk P.f P.g)
      (f := AdjoinRoot.liftAlgHom _ _ P.X P.hasMap_X.1) P.hasMap_X.2) ?_ ?_
  · rw [aeval_algebraMap_apply, AdjoinRoot.aeval_eq, AdjoinRoot.mk_self, map_zero]
  · rw [aeval_algebraMap_apply, AdjoinRoot.aeval_eq]
    exact IsLocalization.Away.algebraMap_isUnit ..
  · ext; simp [Algebra.algHom]
  · ext; simp

Goal state after:
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
𝓟 : StandardEtalePresentation R S
e : S ≃ₐ[R] Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g) := 𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst✝ : Algebra (AdjoinRoot 𝓟.f) S :=
  ((↑e.symm).comp (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f) (Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g)))).toAlgebra
this : IsLocalization (Submonoid.powers ((AdjoinRoot.mk 𝓟.f) 𝓟.g)) S
m : ℕ
hm :
  ∀ (k : ℕ),
    IsIntegral (AdjoinRoot 𝓟.f)
      ((algebraMap (AdjoinRoot 𝓟.f) (S ⊗[R] B)) ((AdjoinRoot.mk 𝓟.f) 𝓟.g ^ k) *
        ⟨(fun x ↦ (AdjoinRoot.mk 𝓟.f) 𝓟.g ^ x) m, ⋯⟩ • a)
⊢ ∃ n, ∀ (m : ℕ), IsIntegral R ((aeval 𝓟.x) 𝓟.g ^ (n + m) • a)

Tactic:
simp only [Submonoid.smul_def, ← @IsScalarTower.algebraMap_smul (AdjoinRoot 𝓟.f) S,
      ← map_pow, ← Algebra.smul_def, ← mul_smul, ← map_mul, ← pow_add, add_comm _ m] at hm

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
e : S ≃ₐ[R] Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g) := 𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst✝ : Algebra (AdjoinRoot 𝓟.f) S :=
  ((↑e.symm).comp (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f) (Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g)))).toAlgebra
this : IsLocalization (Submonoid.powers ((AdjoinRoot.mk 𝓟.f) 𝓟.g)) S
m : ℕ
hm : ∀ (k : ℕ), IsIntegral (AdjoinRoot 𝓟.f) ((algebraMap (AdjoinRoot 𝓟.f) S) ((AdjoinRoot.mk 𝓟.f) (𝓟.g ^ (m + k))) • a)
⊢ ∃ n, ∀ (m : ℕ), IsIntegral R ((aeval 𝓟.x) 𝓟.g ^ (n + m) • a)
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
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝ : IsDomain S'
this : IsDomain R
⊢ False

Tactic:
have : Algebra.IsIntegral R R' := IsIntegralClosure.isIntegral_algebra _ K

Goal state after:
R : Type u_1
S : Type u_2
inst✝²⁸ : CommRing R
inst✝²⁷ : CommRing S
inst✝²⁶ : Algebra R S
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝¹ : IsDomain S'
this✝ : IsDomain R
this : Algebra.IsIntegral R R'
⊢ False
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case zero
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 0) R →ₐ[R] S
hf : f.Finite
⊢ ZariskisMainProperty R p

Tactic:
have : Module.Finite R S := by
      rw [← RingHom.finite_algebraMap]
      convert! RingHom.Finite.comp hf (RingHom.Finite.of_surjective _ (MvPolynomial.C_surjective _))
      exact f.comp_algebraMap.symm

Goal state after:
case zero
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 0) R →ₐ[R] S
hf : f.Finite
this : Module.Finite R S
⊢ ZariskisMainProperty R p
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (-1) ^ (↑(Fin.last ((m + 1).add n)) + ↑(Fin.castAdd (n + 1) (Fin.last m))) *
        f.sylvester g (m + 1) (n + 1) (Fin.last ((m + 1).add n)) (Fin.castAdd (n + 1) (Fin.last m)) *
      ((f.sylvester g (m + 1) (n + 1)).submatrix (Fin.last ((m + 1).add n)).succAbove
          (Fin.castAdd (n + 1) (Fin.last m)).succAbove).det =
    (-1) ^ (n + 1) * g.coeff (n + 1) * f.resultant g m (n + 1)

Tactic:
rw [resultant, ← Matrix.det_reindex_self (finCongr (show (m + 1).add n = m + (n + 1) by grind))]
    simp only [Nat.add_eq, Nat.succ_eq_add_one, Fin.val_last, Fin.val_castAdd, Fin.succAbove_last,
      Matrix.reindex_apply, finCongr_symm, Matrix.submatrix_submatrix]
    congr 2
    · trans (-1) ^ (2 * m + (n + 1))
      · congr 1; lia
      · simp [pow_add]
    · simp only [sylvester, Set.mem_Icc, Matrix.of_apply, Fin.val_last, Fin.addCases_left]
      rw [if_pos (by lia)]
      simp [add_assoc, add_comm 1]
    · ext i j
      simp only [sylvester, Set.mem_Icc, Matrix.submatrix_apply, Function.comp_apply,
        finCongr_apply, Matrix.of_apply, Fin.val_castSucc, Fin.val_cast]
      induction j using Fin.addCases with
      | left j =>
        have : ((Fin.last m).castAdd (n + 1)).succAbove ((j.castAdd (n + 1)).cast (by grind)) =
          j.castSucc.castAdd (n + 1) := by ext; simp [Fin.succAbove, Fin.lt_def]
        simp [this]
      | right j =>
        have : ((Fin.last m).castAdd (n + 1)).succAbove ((j.natAdd m).cast (by grind)) =
          j.natAdd _ := by ext; simp [Fin.succAbove, Fin.lt_def, add_right_comm]
        simp only [ite_and, this, Fin.addCases_right]
        split_ifs with h₁ h₂ h₃ h₃ <;> try lia
        exact coeff_eq_zero_of_natDegree_lt (by lia)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case refine_2.e_a
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U V : (directedCover Y).I₀
i✝ : U ⟶ V
i : ↑(CommRingCat.of ↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ ↑V))))
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑V) (f ⁻¹ᵁ toOpens V) ⋯)).codRestrict
              (integralClosure ↑Γ(Y, toOpens V) ↑Γ(X, f ⁻¹ᵁ toOpens V)) ⋯) ≫
          (normalizationDiagram f).map ((toOpensFunctor Y).map i✝).op))
      i =
    (CommRingCat.Hom.hom
        (T.presheaf.map (homOfLE ⋯).op ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure ↑Γ(Y, toOpens U) ↑Γ(X, f ⁻¹ᵁ toOpens U)) ⋯)))
      i

Tactic:
apply Subtype.ext

Goal state after:
case refine_2.e_a
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U V : (directedCover Y).I₀
i✝ : U ⟶ V
i : ↑(CommRingCat.of ↑(T.presheaf.1 (Opposite.op (f₂ ⁻¹ᵁ ↑V))))
⊢ ↑((CommRingCat.Hom.hom
          (CommRingCat.ofHom
              ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑V) (f ⁻¹ᵁ toOpens V) ⋯)).codRestrict
                (integralClosure ↑Γ(Y, toOpens V) ↑Γ(X, f ⁻¹ᵁ toOpens V)) ⋯) ≫
            (normalizationDiagram f).map ((toOpensFunctor Y).map i✝).op))
        i) =
    ↑((CommRingCat.Hom.hom
          (T.presheaf.map (homOfLE ⋯).op ≫
            CommRingCat.ofHom
              ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
                (integralClosure ↑Γ(Y, toOpens U) ↑Γ(X, f ⁻¹ᵁ toOpens U)) ⋯)))
        i)
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 : QuasiFiniteAt R q.asIdeal
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) ≃ₜ PrimeSpectrum (p.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S p
⊢ IsOpen {⟨q, ⋯⟩}

Tactic:
rw [← e.isOpen_image, Set.image_singleton]

Goal state after:
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 : QuasiFiniteAt R q.asIdeal
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) ≃ₜ PrimeSpectrum (p.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S p
⊢ IsOpen {e ⟨q, ⋯⟩}
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 : ℕ
p : MonicDegreeEq S n
g : S →ₐ[R] T
⊢ (mapEquivMonic R T n).symm (p.map ↑g) = g.comp ((mapEquivMonic R S n).symm p)

Tactic:
by
  obtain ⟨f, rfl⟩ := (mapEquivMonic R S n).surjective p
  exact (mapEquivMonic R T n).symm_apply_eq.mpr (by simp [coe_mapEquivMonic_comp'])

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫ f =
    coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)) ≫
      coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))

Tactic:
apply coprod.hom_ext <;> simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫
      toNormalization f ≫
        normalizationDesc f
            ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
              coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
            (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ ≫
          coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
            (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) =
    (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫ toNormalization f ≫ 𝟙 (normalization f)

Tactic:
apply coprod.hom_ext <;> simp

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

Goal state before:
pp: case injective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Injective ⇑φ
f : R[X]
IH : (map φ f).resultant (map φ f) = 0 ^ (map φ f).natDegree
⊢ φ (f.resultant f) = φ (0 ^ f.natDegree)

Tactic:
simpa only [resultant_map_map, natDegree_map_eq_of_injective hφ, map_zero, map_pow] using IH

Goal state after: