mathlib-initiative/mathlib-tactics huggingface dataset:
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)
hz' : z ∈ Submodule.span S (⇑(algebraMap R S) '' ↑I)
⊢ (algebraMap R S) p * z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
Finsupp.mem_span_image_iff_linearCombination

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)
hz' : ∃ l ∈ Finsupp.supported S S ↑I, (Finsupp.linearCombination S ⇑(algebraMap R S)) l = z
⊢ (algebraMap R S) p * z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case algebraMap
R : Type u_3
inst✝ : CommRing R
I : Ideal R
P : R[X]
r : R
i : ℕ
⊢ ((algebraMap R R[X]) r).coeff i ∈ I ^ i

Tactic:
| algebraMap r =>

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
H : Function.Surjective ⇑(algebraMap R S)
t : T
p : R[X]
hp : (aeval x) (map (algebraMap R S) p) * t = 0
⊢ (aeval x) p * t = 0

Tactic:
simpa using hp

Goal state after:
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:
mul_pow,

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
⊢ (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 ^ i * X ^ i)).coeff
      p.natDegree
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
a b : S
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • a ^ n ∈ (algebraMap R S).range
s : R
hs : s ∈ R⁰
hs' : ∀ (n : ℕ), s • b ^ n ∈ (algebraMap R S).range
n : ℕ
⊢ (r * s) • (a * b) ^ n ∈ (algebraMap R S).range

Tactic:
mul_pow,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
a b : S
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • a ^ n ∈ (algebraMap R S).range
s : R
hs : s ∈ R⁰
hs' : ∀ (n : ℕ), s • b ^ n ∈ (algebraMap R S).range
n : ℕ
⊢ (r * s) • (a ^ n * b ^ n) ∈ (algebraMap R S).range
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : x ∈ Ideal.map (algebraMap R S) I
⊢ ∃ p, p.Monic ∧ (aeval x) p = 0 ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)

Tactic:
by
  let A : Subalgebra R R[X] := Algebra.adjoin R { C r * X | r ∈ I }
  let := Polynomial.algebra R S
  refine exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral ?_
  induction hx using Submodule.span_induction with
  | zero => simp [isIntegral_zero]
  | add x y _ _ hx hy => simpa [add_mul] using hx.add hy
  | mem x h =>
    obtain ⟨x, hx, rfl⟩ := h
    simpa using isIntegral_algebraMap (R := A) (A := S[X])
      (x := ⟨C x * X, Algebra.subset_adjoin ⟨x, hx, rfl⟩⟩)
  | smul a x _ hx =>
    simp only [smul_eq_mul, map_mul, mul_assoc]
    refine .mul ?_ hx
    exact ((Algebra.IsIntegral.isIntegral (R := R) a).map (IsScalarTower.toAlgHom R S _)).tower_top

Goal state after:
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
H : IsAlmostIntegral R s
inst✝ : IsNoetherianRing R
H' : R⁰ ≤ Submonoid.comap (algebraMap R S) S⁰
⊢ IsIntegral R s

Tactic:
by
  obtain ⟨r, hr, hr'⟩ := H
  let f : Algebra.adjoin R {s} →ₗ[R]
      Submodule.span R {Localization.Away.invSelf (algebraMap R S r)} :=
    (IsScalarTower.toAlgHom R S (Localization.Away (algebraMap R S r))).toLinearMap.restrict
      (p := (Algebra.adjoin R {s}).toSubmodule) <| by
    change (Algebra.adjoin R {s}).toSubmodule ≤ (Submodule.span _ _).comap _
    rw [Algebra.adjoin_eq_span, ← Submonoid.powers_eq_closure, Submodule.span_le]
    rintro _ ⟨n, rfl⟩
    obtain ⟨a, ha⟩ := hr' n
    refine Submodule.mem_span_singleton.mpr ⟨a, ?_⟩
    suffices algebraMap _ _ (s ^ n) * algebraMap _ _ ((algebraMap R S) r) *
        Localization.Away.invSelf ((algebraMap R S) r) = algebraMap S _ (s ^ n) by
      simpa [Algebra.smul_def, IsScalarTower.algebraMap_apply R S (Localization.Away _),
        ha, mul_assoc, mul_left_comm] using this
    simp [mul_assoc, Localization.Away.invSelf, Localization.mk_eq_mk']
  have : Function.Injective f := by
    have : Function.Injective (algebraMap S (Localization.Away (algebraMap R S r))) := by
      apply IsLocalization.injective (M := .powers (algebraMap R S r))
      exact Submonoid.powers_le.mpr (H' hr)
    exact fun x y e ↦ Subtype.ext (this congr($e))
  have : (Algebra.adjoin R {s}).toSubmodule.FG := by
    rw [← Module.Finite.iff_fg]
    exact .of_injective f this
  exact .of_mem_of_fg _ this _ (Algebra.self_mem_adjoin_singleton R s)

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

Goal state before:
pp: K : Type u
inst✝ : CommRing K
P : Sort v
n : K[X]
d : ↥K[X]⁰
f : K[X] → K[X] → P
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
⊢ { toFractionRing := Localization.mk n d }.liftOn f H = f n ↑d

Tactic:
rw [RatFunc.liftOn]

Goal state after:
K : Type u
inst✝ : CommRing K
P : Sort v
n : K[X]
d : ↥K[X]⁰
f : K[X] → K[X] → P
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
⊢ Localization.liftOn { toFractionRing := Localization.mk n d }.toFractionRing (fun p q ↦ f p ↑q) ⋯ = f n ↑d
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
r : K
x : K⟮X⟯
⊢ r • x = C r * x

Tactic:
rw [Algebra.smul_def, algebraMap_eq_C]

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
p : R[X]
q : S[X]
hp : p.Monic
hq : q.Monic
H : q ∣ map (algebraMap R S) p
i : ℕ
a✝ : Nontrivial S
T : Type u_2
w✝⁴ : CommRing T
w✝³ : Algebra S T
w✝² : Module.Finite S T
w✝¹ : Module.Free S T
w✝ : Nontrivial T
hqT : (map (algebraMap S T) q).Splits
algInst✝ : Algebra R T := ((algebraMap S T).comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
⊢ IsIntegral R ((map (algebraMap S T) q).coeff i)

Tactic:
refine Polynomial.isIntegral_coeff_of_factors _ (by simp [hq.map, isIntegral_one]) hqT ?_ i

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R[X]
q : S[X]
hp : p.Monic
hq : q.Monic
H : q ∣ map (algebraMap R S) p
i : ℕ
a✝ : Nontrivial S
T : Type u_2
w✝⁴ : CommRing T
w✝³ : Algebra S T
w✝² : Module.Finite S T
w✝¹ : Module.Free S T
w✝ : Nontrivial T
hqT : (map (algebraMap S T) q).Splits
algInst✝ : Algebra R T := ((algebraMap S T).comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
⊢ ∀ (x : T), (map (algebraMap S T) q).IsRoot x → IsIntegral R x
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
p✝ : S[X]
hp✝ : IsAlmostIntegral R[X] p✝
i : ℕ
q : S[X]
p : R[X]
hp : p ∈ R[X]⁰
hp' : ∀ (n : ℕ), p • q ^ n ∈ (algebraMap R[X] S[X]).range
⊢ p.leadingCoeff ∈ R⁰

Tactic:
simpa using hp

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

Goal state before:
pp: case e'_5
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
⊢ ((isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom.comp (algebraMap R S)).comp
      (isEmptyAlgEquiv R PEmpty.{w + 1}).toRingEquiv.toRingHom =
    algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)

Tactic:
ext r m

Goal state after:
case e'_5.hC
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
r : R
m : PEmpty.{w + 1} →₀ ℕ
⊢ coeff m
      (((((isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom.comp (algebraMap R S)).comp
              (isEmptyAlgEquiv R PEmpty.{w + 1}).toRingEquiv.toRingHom).comp
          C)
        r) =
    coeff m (((algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).comp C) r)

case e'_5.hX
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
r : PEmpty.{w + 1}
m : PEmpty.{w + 1} →₀ ℕ
⊢ coeff m
      ((((isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom.comp (algebraMap R S)).comp
          (isEmptyAlgEquiv R PEmpty.{w + 1}).toRingEquiv.toRingHom)
        (X r)) =
    coeff m ((algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)) (X r))
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : WeaklyQuasiFiniteAt R Q
this✝¹ : (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P).IsPrime
this✝ :
  Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P =
    Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) Q
this :
  P ⊔ Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) ⊥ =
    Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q)))
      (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) Q)
⊢ P = Q

Tactic:
simp [Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.map_comap_le] at this

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : WeaklyQuasiFiniteAt R Q
this✝¹ : (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P).IsPrime
this✝ :
  Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P =
    Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) Q
this : P ⊔ Ideal.map (algebraMap R S) (Ideal.under R Q) = Q
⊢ P = Q
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U V : X.AffineZariskiSite
⊢ ∀ (f : (toOpensFunctor X).obj U ⟶ (toOpensFunctor X).obj V),
    Sieve.functorPushforward (toOpensFunctor X) ((toOpensFunctor X).imageSieve f) ∈
      (Opens.grothendieckTopology ↥X) ((toOpensFunctor X).obj U)

Tactic:
h

Goal state after:
X : Scheme
U V : X.AffineZariskiSite
h : (toOpensFunctor X).obj U ⟶ (toOpensFunctor X).obj V
⊢ Sieve.functorPushforward (toOpensFunctor X) ((toOpensFunctor X).imageSieve h) ∈
    (Opens.grothendieckTopology ↥X) ((toOpensFunctor X).obj U)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: 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]
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

Tactic:
let : SMulZeroClass R (FractionRing K[X]) := inferInstance

Goal state after:
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
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p q : K[X]
⊢ (map φ hφ) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) =
    (algebraMap R[X] R⟮X⟯) (φ p) / (algebraMap R[X] R⟮X⟯) (φ q)

Tactic:
rcases eq_or_ne q 0 with (rfl | hq)

Goal state after:
case inl
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
⊢ (map φ hφ) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) 0) =
    (algebraMap R[X] R⟮X⟯) (φ p) / (algebraMap R[X] R⟮X⟯) (φ 0)

case inr
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p q : K[X]
hq : q ≠ 0
⊢ (map φ hφ) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) =
    (algebraMap R[X] R⟮X⟯) (φ p) / (algebraMap R[X] R⟮X⟯) (φ q)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p q : K[X]
⊢ (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) = φ p / φ q

Tactic:
rcases eq_or_ne q 0 with (rfl | hq)

Goal state after:
case inl
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p : K[X]
⊢ (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) 0) = φ p / φ 0

case inr
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p q : K[X]
hq : q ≠ 0
⊢ (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) = φ p / φ q
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ IsUnit ((aeval (x + (aeval x) P.f * -b)) P.g)

Tactic:
← IsNilpotent.isUnit_quotient_mk_iff (I := I) ⟨2, hI⟩,

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ IsUnit ((Ideal.Quotient.mk I) ((aeval (x + (aeval x) P.f * -b)) P.g))
Module: Mathlib.RingTheory.Etale.StandardEtale

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
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
ε' : S
hε'I : ε' ∈ I
hε' : (aeval x) P.f + (aeval x) (derivative P.f) * ε' = 0
hε'' : IsUnit ((aeval (x + ε')) P.g)
⊢ ε' = (aeval x) P.f * -b

Tactic:
have : ε * ε' = 0 := ((pow_two _).symm.trans hI).le (Ideal.mul_mem_mul hεI hε'I)

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝¹ : (aeval x) P.f ^ 2 = 0
this✝ : (aeval x) P.f * ε = 0
ε' : S
hε'I : ε' ∈ I
hε' : (aeval x) P.f + (aeval x) (derivative P.f) * ε' = 0
hε'' : IsUnit ((aeval (x + ε')) P.g)
this : ε * ε' = 0
⊢ ε' = (aeval x) P.f * -b
Module: Mathlib.FieldTheory.RatFunc.Basic

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

Tactic:
rw [inv_div]

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✝ : StandardEtalePresentation R S
P : StandardEtalePair R
⊢ Function.Bijective ⇑(P.lift P.X ⋯)

Tactic:
by simpa [StandardEtalePair.lift_X_left] using Function.bijective_id

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

Goal state before:
pp: case inr
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}
y : B
hy : IsIntegral R y
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝ : Algebra S B := (φ.comp C).toAlgebra
⊢ ∃ g, φ (derivative f) * y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)

Tactic:
have := (algebraMap S B).domain_nontrivial

Goal state after:
case inr
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}
y : B
hy : IsIntegral R y
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
⊢ ∃ g, φ (derivative f) * y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)
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
⊢ ∃ t ∉ Q,
    (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧
      (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤

Tactic:
let p := Q.under R

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
⊢ ∃ t ∉ Q,
    (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧
      (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
p : Ideal T
inst✝ : p.IsPrime
h₁ : ZariskisMainProperty R (Ideal.under S p)
r : S
⊢ Submonoid.powers ((algebraMap S T) r) ≤ ⊥.toSubmonoid

Tactic:
simp [Submonoid.powers_le]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case smul
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
a : R[X]
x : S
hx : x ∈ Submodule.span R[X] ↑s
IH : p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
⊢ p.leadingCoeff ^ s.sup n • a • (t * x) ∈ φ.range

Tactic:
smul_comm,

Goal state after:
case smul
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
a : R[X]
x : S
hx : x ∈ Submodule.span R[X] ↑s
IH : p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
⊢ a • p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range