mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
⊢ W'.addX P Q * (P z * Q z) ^ 2 +
        ((2 * Q x * P z * Q z ^ 3 - P x * Q z ^ 4) * 0 + (Q x * P z ^ 4 - 2 * P x * P z ^ 3 * Q z) * 0) -
      (((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                  W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                W'.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
              P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
            Q x * P z * (P x * Q z - Q x * P z) ^ 2) *
          (P x * Q z - Q x * P z) +
        ((2 * Q x * P z * Q z ^ 3 - P x * Q z ^ 4) *
            (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
              (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3)) +
          (Q x * P z ^ 4 - 2 * P x * P z ^ 3 * Q z) *
            (Q y ^ 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 2 -
              (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z + W'.a₄ * Q x * Q z ^ 2 + W'.a₆ * Q z ^ 3)))) =
    0

Tactic:
rw [addX]

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
⊢ (-P x * Q y ^ 2 * P z + Q x * P y ^ 2 * Q z - 2 * P x * P y * Q y * Q z + 2 * Q x * P y * Q y * P z -
                                  W'.a₁ * P x ^ 2 * Q y * Q z +
                                W'.a₁ * Q x ^ 2 * P y * P z +
                              W'.a₂ * P x ^ 2 * Q x * Q z -
                            W'.a₂ * P x * Q x ^ 2 * P z -
                          W'.a₃ * P x * P y * Q z ^ 2 +
                        W'.a₃ * Q x * Q y * P z ^ 2 -
                      2 * W'.a₃ * P x * Q y * P z * Q z +
                    2 * W'.a₃ * Q x * P y * P z * Q z +
                  W'.a₄ * P x ^ 2 * Q z ^ 2 -
                W'.a₄ * Q x ^ 2 * P z ^ 2 +
              3 * W'.a₆ * P x * P z * Q z ^ 2 -
            3 * W'.a₆ * Q x * P z ^ 2 * Q z) *
          (P z * Q z) ^ 2 +
        ((2 * Q x * P z * Q z ^ 3 - P x * Q z ^ 4) * 0 + (Q x * P z ^ 4 - 2 * P x * P z ^ 3 * Q z) * 0) -
      (((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                  W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                W'.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
              P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
            Q x * P z * (P x * Q z - Q x * P z) ^ 2) *
          (P x * Q z - Q x * P z) +
        ((2 * Q x * P z * Q z ^ 3 - P x * Q z ^ 4) *
            (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
              (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3)) +
          (Q x * P z ^ 4 - 2 * P x * P z ^ 3 * Q z) *
            (Q y ^ 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 2 -
              (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z + W'.a₄ * Q x * Q z ^ 2 + W'.a₆ * Q z ^ 3)))) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.addX P P = 0

Tactic:
rw [addX]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -P x * P y ^ 2 * P z + P x * P y ^ 2 * P z - 2 * P x * P y * P y * P z + 2 * P x * P y * P y * P z -
                            W'.a₁ * P x ^ 2 * P y * P z +
                          W'.a₁ * P x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * P x * P z -
                      W'.a₂ * P x * P x ^ 2 * P z -
                    W'.a₃ * P x * P y * P z ^ 2 +
                  W'.a₃ * P x * P y * P z ^ 2 -
                2 * W'.a₃ * P x * P y * P z * P z +
              2 * W'.a₃ * P x * P y * P z * P z +
            W'.a₄ * P x ^ 2 * P z ^ 2 -
          W'.a₄ * P x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * P z ^ 2 -
      3 * W'.a₆ * P x * P z ^ 2 * P z =
    0
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).OpenCover :=
  fun j ↦ ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).affineCover
⊢ IsOpenImmersion (pullback.diagonal f)

Tactic:
apply IsZariskiLocalAtTarget.of_range_subset_iSup _
      (Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange f 𝒰Y 𝒰X)

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := ⋯
𝒰X : (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).OpenCover := ⋯
⊢ ∀ (i : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) × (𝒰X i).I₀),
    IsOpenImmersion
      (pullback.diagonal f ∣_ Scheme.Hom.opensRange ((Scheme.Pullback.diagonalCover f 𝒰Y 𝒰X).f ⟨i.fst, (i.snd, i.snd)⟩))
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.addX 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]
          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]

Tactic:
← addY_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.addX P Q, W.addZ P Q * ![W.addX P Q / W.addZ P Q, W.addY P Q / W.addZ P Q, 1] y,
      W.addZ P Q * ![W.addX P Q / W.addZ P Q, W.addY P Q / W.addZ P Q, 1] z]
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g], Q f → P (pullback.fst f g) → P g
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hf : Q f
hfst : P fst
this : HasPullback f g
⊢ P g

Tactic:
apply H hf

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g], Q f → P (pullback.fst f g) → P g
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hf : Q f
hfst : P fst
this : HasPullback f g
⊢ P (pullback.fst f g)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: ⊢ CodescendsAlong (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) fun {R S} [CommRing R] [CommRing S] ↦
    FaithfullyFlat

Tactic:
apply CodescendsAlong.mk _ injective_respectsIso
  introv h H
  rw [faithfullyFlat_algebraMap_iff] at h
  exact h.injective_of_tensorProduct H

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [inst : HasPushout f g], Q f → P (pushout.inl f g) → P g
A X Y Z : C
f : A ⟶ X
g : A ⟶ Y
inl : X ⟶ Z
inr : Y ⟶ Z
h : IsPushout f g inl inr
hf : Q f
hfst : P inl
this : HasPushout f g
⊢ P g

Tactic:
apply H hf

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [inst : HasPushout f g], Q f → P (pushout.inl f g) → P g
A X Y Z : C
f : A ⟶ X
g : A ⟶ Y
inl : X ⟶ Z
inr : Y ⟶ Z
h : IsPushout f g inl inr
hf : Q f
hfst : P inl
this : HasPushout f g
⊢ P (pushout.inl f g)
Module: Mathlib.RingTheory.RingHom.QuasiFinite

Goal state before:
pp: ⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite

Tactic:
by
  refine .mk respectsIso ?_
  introv H
  rw [quasiFinite_algebraMap] at H ⊢
  infer_instance

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: 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
a : R
ha : a ∈ I
⊢ l a * (algebraMap R S) a * (algebraMap R S) p ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
mul_assoc,

Goal state after:
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
a : R
ha : a ∈ I
⊢ l a * ((algebraMap R S) a * (algebraMap R S) p) ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: 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
a : R
ha : a ∈ I
⊢ (algebraMap R S) a * (algebraMap R S) p * l a ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
mul_assoc,

Goal state after:
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
a : R
ha : a ∈ I
⊢ (algebraMap R S) a * ((algebraMap R S) p * l a) ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case inr.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
e :
  ∑ b ∈ Finset.range (p.natDegree + 1),
      ((algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (p.coeff b) * (C x * X) ^ b).coeff
        p.natDegree =
    0
i : ℕ
hi : i ≤ p.natDegree
⊢ (algebraMap R S) ((↑(p.coeff i)).coeff (p.natDegree - i)) * x ^ i =
    ((algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (p.coeff i) * (C x * X) ^ i).coeff p.natDegree

Tactic:
rw [mul_pow, mul_left_comm, ← map_pow, coeff_C_mul, coeff_mul_X_pow', if_pos hi, mul_comm]

Goal state after:
case inr.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
e :
  ∑ b ∈ Finset.range (p.natDegree + 1),
      ((algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (p.coeff b) * (C x * X) ^ b).coeff
        p.natDegree =
    0
i : ℕ
hi : i ≤ p.natDegree
⊢ x ^ i * (algebraMap R S) ((↑(p.coeff i)).coeff (p.natDegree - i)) =
    x ^ i * ((algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (p.coeff i)).coeff (p.natDegree - i)
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
s : S
inst✝ : IsNoetherianRing R
H' : R⁰ ≤ Submonoid.comap (algebraMap R S) S⁰
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • s ^ n ∈ (algebraMap R S).range
n : ℕ
⊢ (fun x ↦ s ^ x) n ∈
    ↑(Submodule.comap (IsScalarTower.toAlgHom R S (Localization.Away ((algebraMap R S) r))).toLinearMap
        (R ∙ Localization.Away.invSelf ((algebraMap R S) r)))

Tactic:
obtain ⟨a, ha⟩ := hr' n

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
s : S
inst✝ : IsNoetherianRing R
H' : R⁰ ≤ Submonoid.comap (algebraMap R S) S⁰
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • s ^ n ∈ (algebraMap R S).range
n : ℕ
a : R
ha : (algebraMap R S) a = r • s ^ n
⊢ (fun x ↦ s ^ x) n ∈
    ↑(Submodule.comap (IsScalarTower.toAlgHom R S (Localization.Away ((algebraMap R S) r))).toLinearMap
        (R ∙ Localization.Away.invSelf ((algebraMap R S) r)))
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case empty
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : ι → S[X]
H : ∀ i ∈ ∅, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)
j : ℕ
⊢ IsIntegral R ((∅.prod p).coeff j)

Tactic:
simp [coeff_one, apply_ite, isIntegral_zero, isIntegral_one]

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

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
hp' : p.natDegree = 0
⊢ IsAlmostIntegral R (p.coeff i)

Tactic:
obtain ⟨p, rfl⟩ := natDegree_eq_zero.mp hp'
    simp only [coeff_C]
    split_ifs with h
    · simpa using H hp
    · exact (completeIntegralClosure R S).zero_mem

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
⊢ p - (monomial p.natDegree) p.leadingCoeff ∈ completeIntegralClosure R[X] S[X]

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
⊢ p - C p.leadingCoeff * X ^ p.natDegree ∈ completeIntegralClosure R[X] S[X]
Module: Mathlib.RingTheory.QuasiFinite.Polynomial

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
inst✝ : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_1 : P.IsPrime],
    Algebra.WeaklyQuasiFiniteAt R P → IsField R → False
hR : ¬IsField R
p : Ideal R := Ideal.under R P
Q : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber R[X])
hQ :
  (PrimeSpectrum.preimageEquivFiber R R[X] { asIdeal := p, isPrime := ⋯ }).symm Q =
    ⟨{ asIdeal := P, isPrime := inst✝ }, ⋯⟩
⊢ False

Tactic:
have inst : Algebra.WeaklyQuasiFiniteAt p.ResidueField Q.asIdeal :=
      .baseChange P Q.asIdeal congr($(hQ.symm).1.1)

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
inst✝ : P.IsPrime
H : Algebra.WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R[X]) [inst_1 : P.IsPrime],
    Algebra.WeaklyQuasiFiniteAt R P → IsField R → False
hR : ¬IsField R
p : Ideal R := Ideal.under R P
Q : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber R[X])
hQ :
  (PrimeSpectrum.preimageEquivFiber R R[X] { asIdeal := p, isPrime := ⋯ }).symm Q =
    ⟨{ asIdeal := P, isPrime := inst✝ }, ⋯⟩
inst : Algebra.WeaklyQuasiFiniteAt p.ResidueField Q.asIdeal
⊢ False
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
p : K[X]
⊢ ((algebraMap K[X] K⟮X⟯) p).denom = 1

Tactic:
convert! denom_div p one_ne_zero

Goal state after:
case e'_2
K : Type u
inst✝ : Field K
p : K[X]
⊢ (algebraMap K[X] K⟮X⟯) p = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) 1

case e'_3
K : Type u
inst✝ : Field K
p : K[X]
⊢ 1 = C (1 / gcd p 1).leadingCoeff⁻¹ * (1 / gcd p 1)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
h : x.num = 0
⊢ x = 0

Tactic:
rw [← num_div_denom x, h, map_zero, zero_div]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p * (algebraMap K[X] K⟮X⟯) x.denom ↔
    (algebraMap K[X] K⟮X⟯) x.num * ((algebraMap K[X] K⟮X⟯) x.denom)⁻¹ * (algebraMap K[X] K⟮X⟯) q =
      (algebraMap K[X] K⟮X⟯) p

Tactic:
mul_assoc,

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p * (algebraMap K[X] K⟮X⟯) x.denom ↔
    (algebraMap K[X] K⟮X⟯) x.num * (((algebraMap K[X] K⟮X⟯) x.denom)⁻¹ * (algebraMap K[X] K⟮X⟯) q) =
      (algebraMap K[X] K⟮X⟯) p
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
P : StandardEtalePresentation R S
p : R[X]
⊢ (MvPolynomial.aeval P.toPresentation.val) ((Bivariate.equivMvPolynomial R) (C p)) = (aeval P.x) p

Tactic:
change (((MvPolynomial.aeval _).comp (Bivariate.equivMvPolynomial R).toAlgHom).comp CAlgHom) _ = _

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePresentation R S
p : R[X]
⊢ (((MvPolynomial.aeval P.toPresentation.val).comp ↑(Bivariate.equivMvPolynomial R)).comp CAlgHom) p = (aeval P.x) p
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
T : Type u_4
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
H : Function.Bijective ⇑(toIntegralClosure R S B)
H' : Function.Bijective ⇑(toIntegralClosure S T (S ⊗[R] B))
e : T ⊗[R] ↥(integralClosure R B) ≃ₐ[T] ↥(integralClosure T (T ⊗[R] B)) := ⋯
x✝ : ↥(integralClosure R B)
⊢ ↑(((AlgHom.restrictScalars R (toIntegralClosure R T B)).comp Algebra.TensorProduct.includeRight) x✝) =
    ↑(((AlgHom.restrictScalars R ↑e).comp Algebra.TensorProduct.includeRight) x✝)

Tactic:
simp [e, toIntegralClosure]

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
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'
⊢ False

Tactic:
have := (FaithfulSMul.algebraMap_injective R K).isDomain

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
⊢ False
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 S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)

Tactic:
obtain ⟨g₀, hg, H⟩ := IsEtaleAt.exists_isStandardEtale (R := (MvPolynomial (Fin n) R))
    (S := (Localization.Away f)) (p.map (algebraMap _ _))

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H✝ : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg✝ : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
g₀ : Localization.Away f
hg : g₀ ∉ Ideal.map (algebraMap S (Localization.Away f)) p
H : IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away g₀)
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)