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

Goal state before:
pp: case pos
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : q = 0
⊢ { toFractionRing := 0 } = c • RatFunc.mk p 0

Tactic:
mk_zero,

Goal state after:
case pos
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : q = 0
⊢ { toFractionRing := 0 } = c • { toFractionRing := 0 }
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case mp
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
V : X.Opens
hV : IsAffineOpen V
f : ⟨V, hV⟩ ⟶ U
⊢ (Sieve.generate (U.presieveOfSections s)).arrows f → ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨V, hV⟩

pp: case mpr
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
V : X.Opens
hV : IsAffineOpen V
f : ⟨V, hV⟩ ⟶ U
⊢ (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨V, hV⟩) → (Sieve.generate (U.presieveOfSections s)).arrows f

Tactic:
· rintro ⟨⟨W, hW⟩, ⟨f₁, hf₁⟩, -, ⟨f₂, hf₂s, rfl⟩, rfl⟩
    subst hf₁
    obtain ⟨f₃, hf₃⟩ := U.2.basicOpen_basicOpen_is_basicOpen f₂ f₁
    refine ⟨f₂, hf₂s, f₃, ?_⟩
    rw [X.basicOpen_mul, hf₃, inf_eq_right]
    exact X.basicOpen_le _

Goal state after:
case mpr
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
V : X.Opens
hV : IsAffineOpen V
f : ⟨V, hV⟩ ⟶ U
⊢ (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨V, hV⟩) → (Sieve.generate (U.presieveOfSections s)).arrows f
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: 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]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
x y : R⟮X⟯
⊢ (x * y).liftOn (fun p q ↦ φ p / φ q) ⋯ = x.liftOn (fun p q ↦ φ p / φ q) ⋯ * y.liftOn (fun p q ↦ φ p / φ q) ⋯

Tactic:
obtain ⟨x⟩ := x
    obtain ⟨y⟩ := y
    cases x using Localization.induction_on
    cases y using Localization.induction_on
    rw [← ofFractionRing_mul, Localization.mk_mul]
    simp only [liftOn_ofFractionRing_mk, div_mul_div_comm, map_mul, Submonoid.coe_mul]

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X},
    (∃ R, Y = Spec R) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy : (Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x) = f ((pullback.fst f (Y.affineCover.f i)) x)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
⊢ QuasiFiniteAt f ((pullback.fst f (Y.affineCover.f i)) x) ↔ IsOpen {⟨(pullback.fst f (Y.affineCover.f i)) x, ⋯⟩}

Tactic:
convert! this (f := pullback.snd f ι) (x := x) ⟨_, rfl⟩ using 1

Goal state after:
case e'_1
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X},
    (∃ R, Y = Spec R) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy : (Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x) = f ((pullback.fst f (Y.affineCover.f i)) x)
ι : Y.affineCover.X i ⟶ Y := ⋯
⊢ QuasiFiniteAt f ((pullback.fst f (Y.affineCover.f i)) x) ↔ QuasiFiniteAt (pullback.snd f ι) x

case e'_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X},
    (∃ R, Y = Spec R) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy : (Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x) = f ((pullback.fst f (Y.affineCover.f i)) x)
ι : Y.affineCover.X i ⟶ Y := ⋯
⊢ IsOpen {⟨(pullback.fst f (Y.affineCover.f i)) x, ⋯⟩} ↔ IsOpen {⟨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
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this✝ : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := φ.toAlgebra
this : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
⊢ Function.Bijective ⇑(toIntegralClosure R S B)

Tactic:
have : IsScalarTower (integralClosure R B) (integralClosure S (S ⊗[R] B)) (S ⊗[R] B) :=
    .of_algebraMap_eq' rfl

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
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this✝¹ : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := φ.toAlgebra
this✝ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
⊢ Function.Bijective ⇑(toIntegralClosure R S B)
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
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
hx' : Function.Surjective ⇑(aeval x)
p : R[X]
hpI : p ∈ I
hp :
  Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬m ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
⊢ minpoly R x ∈ I

Tactic:
simp [I]

Goal state after:
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 := Ideal.under R Q
this✝⁴ : p.IsPrime
this✝³ : Module p.ResidueField (p.Fiber S) := leftModule
this✝² : SMul p.ResidueField (p.Fiber S) := this✝³.toSMul
this✝¹ : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : Q.ResidueField
hx : p.ResidueField⟮x⟯ = ⊤
⊢ ∃ x, x ≠ 0 ∧ p.ResidueField[x] = ⊤

Tactic:
rw [IntermediateField.adjoin_eq_top_iff] at hx

Goal state after:
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 := Ideal.under R Q
this✝⁴ : p.IsPrime
this✝³ : Module p.ResidueField (p.Fiber S) := leftModule
this✝² : SMul p.ResidueField (p.Fiber S) := this✝³.toSMul
this✝¹ : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : Q.ResidueField
hx : p.ResidueField[x] = ⊤
⊢ ∃ x, x ≠ 0 ∧ p.ResidueField[x] = ⊤
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
p : Ideal S
r : S
hr : r ∈ integralClosure R S
hrp : r ∉ p
⊢ Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom ⟨r, ⋯⟩) ↔
    ∀ (x : S), ∃ m, IsIntegral R (r ^ m * x)

Tactic:
rw [Function.Bijective, and_iff_right
    (by exact IsLocalization.map_injective_of_injective _ _ _ Subtype.val_injective),
    Localization.awayMap_surjective_iff]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal S
r : S
hr : r ∈ integralClosure R S
hrp : r ∉ p
⊢ (∀ (a : S), ∃ b m, (integralClosure R S).val.toRingHom b = (integralClosure R S).val.toRingHom ⟨r, ⋯⟩ ^ m * a) ↔
    ∀ (x : S), ∃ m, IsIntegral R (r ^ m * 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[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
g : S'[X]
hg :
  Polynomial.map (algebraMap S S') (derivative f * y) -
      (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum =
    Polynomial.map (algebraMap S S') f * g
⊢ (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum.natDegree <
    (Polynomial.map (algebraMap S S') f).natDegree

Tactic:
rw [hf.natDegree_map, ← Nat.le_sub_one_iff_lt (Ne.bot_lt hfd)]

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[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
g : S'[X]
hg :
  Polynomial.map (algebraMap S S') (derivative f * y) -
      (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum =
    Polynomial.map (algebraMap S S') f * g
⊢ (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum.natDegree ≤
    f.natDegree - 1
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
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e✝ : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e✝.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e✝.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
this : Module.Finite R (AdjoinRoot 𝓟.f)
e : AdjoinRoot 𝓟.f →ₐ[R] AdjoinRoot 𝓟'.f := AdjoinRoot.mapAlgHom (Algebra.ofId R B) 𝓟.f 𝓟'.f ⋯
⊢ (AdjoinRoot.mk 𝓟'.f).comp (mapRingHom (algebraMap R B)) = e.comp (AdjoinRoot.mk 𝓟.f)

Tactic:
ext <;> simp [e]

Goal state after:
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
s : S
hsQ : s ∉ Q
hs : FormallyUnramified R (Localization.Away s)
hQ : (Ideal.map (algebraMap S (Localization.Away s)) Q).IsPrime
inst : Unramified R (Localization.Away s)
f : S
t : ↥(Submonoid.powers s)
hf : IsLocalization.mk' (Localization.Away s) f t ∉ Ideal.map (algebraMap S (Localization.Away s)) Q
H : HasStandardEtaleSurjectionOn R (IsLocalization.mk' (Localization.Away s) f t)
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
refine ⟨s * f, ?_, ?_⟩

Goal state after:
case inr.refine_1
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
s : S
hsQ : s ∉ Q
hs : FormallyUnramified R (Localization.Away s)
hQ : (Ideal.map (algebraMap S (Localization.Away s)) Q).IsPrime
inst : Unramified R (Localization.Away s)
f : S
t : ↥(Submonoid.powers s)
hf : IsLocalization.mk' (Localization.Away s) f t ∉ Ideal.map (algebraMap S (Localization.Away s)) Q
H : HasStandardEtaleSurjectionOn R (IsLocalization.mk' (Localization.Away s) f t)
⊢ s * f ∉ Q

case inr.refine_2
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
s : S
hsQ : s ∉ Q
hs : FormallyUnramified R (Localization.Away s)
hQ : (Ideal.map (algebraMap S (Localization.Away s)) Q).IsPrime
inst : Unramified R (Localization.Away s)
f : S
t : ↥(Submonoid.powers s)
hf : IsLocalization.mk' (Localization.Away s) f t ∉ Ideal.map (algebraMap S (Localization.Away s)) Q
H : HasStandardEtaleSurjectionOn R (IsLocalization.mk' (Localization.Away s) f t)
⊢ HasStandardEtaleSurjectionOn R (s * f)
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
this✝¹ : Algebra.IsIntegral R R'
this✝ : FaithfulSMul R' K
this : FaithfulSMul R R'
⊢ False

Tactic:
have : FaithfulSMul R' L := .trans _ 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'
this✝¹ : FaithfulSMul R' K
this✝ : FaithfulSMul R R'
this : FaithfulSMul R' L
⊢ False
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
⊢ ↑(LinearEquiv.det (taylorLinearEquiv r n)) = ↑1

Tactic:
by rw [LinearEquiv.coe_det, det_taylorLinearEquiv_toLinearMap, Units.val_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : R[X]
m : ℕ
i j✝ : Fin (0 + m)
j : Fin m
⊢ (if ↑i ∈ Icc (↑j) (↑j + 0) then f.coeff (↑i - ↑j) else 0) = Matrix.diagonal (fun x ↦ f.coeff 0) i (Fin.natAdd 0 j)

Tactic:
Matrix.diagonal_apply

Goal state after:
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m : ℕ
i j✝ : Fin (0 + m)
j : Fin m
⊢ (if ↑i ∈ Icc (↑j) (↑j + 0) then f.coeff (↑i - ↑j) else 0) = if i = Fin.natAdd 0 j then f.coeff 0 else 0
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case pos.refine_3
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
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∈ p
a : R
ha : (ofId R S).toRingHom a = f.leadingCoeff • x
⊢ (algebraMap R S) ((f.eraseLead + C a * X ^ m).coeff n) ∉ p

Tactic:
· suffices algebraMap R S (f.coeff n) + algebraMap R S (if n = m then a else 0) ∉ p by
        simpa [eraseLead_coeff, show n ≠ f.natDegree by rintro rfl; exact hfn (by simpa)]
      rwa [Ideal.add_mem_iff_left]
      split_ifs
      · convert p.mul_mem_right x Hfp
        simpa [Algebra.smul_def] using! ha
      · simp

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

Goal state before:
pp: case succ.inl.left
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ : Fin (m + n)
j₂ : Fin m
IH : ↑(Fin.castAdd n j₂) ≤ m → (M ↑(Fin.castAdd n j₂)).det = M₂.det
hi : ↑j₂ + 1 ≤ m
⊢ Fin.addCases
        (fun j₁_1 ↦
          if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) + (f * (monomial k) r).coeff (↑j₁ - ↑j₁_1) else 0)
        (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.castAdd n j₂) -
      r *
        Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
          (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0)
          ⟨↑(Fin.castAdd n j₂) + (k + m), ⋯⟩ =
    Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
      (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.castAdd n j₂)

Tactic:
have : Fin.mk (n := m + n) (↑j₂ + (k + m)) (by lia) = .natAdd m ⟨j₂ + k, by lia⟩ :=
            Fin.ext (by simp; lia)

Goal state after:
case succ.inl.left
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ : Fin (m + n)
j₂ : Fin m
IH : ↑(Fin.castAdd n j₂) ≤ m → (M ↑(Fin.castAdd n j₂)).det = M₂.det
hi : ↑j₂ + 1 ≤ m
this : ⟨↑j₂ + (k + m), ⋯⟩ = Fin.natAdd m ⟨↑j₂ + k, ⋯⟩
⊢ Fin.addCases
        (fun j₁_1 ↦
          if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) + (f * (monomial k) r).coeff (↑j₁ - ↑j₁_1) else 0)
        (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.castAdd n j₂) -
      r *
        Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
          (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0)
          ⟨↑(Fin.castAdd n j₂) + (k + m), ⋯⟩ =
    Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
      (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.castAdd n j₂)