mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : S
f : S →ₐ[R] T
hf : Function.Injective ⇑f
h : IsStronglyTranscendental R (f x)
u : S
p : R[X]
hp : (aeval x) p * u = 0
this : map (↑f) (map (algebraMap R S) p) * map (↑f) (C u) = 0
⊢ map (algebraMap R S) p * C u = 0

Tactic:
← Polynomial.map_mul,

Goal state after:
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
x : S
f : S →ₐ[R] T
hf : Function.Injective ⇑f
h : IsStronglyTranscendental R (f x)
u : S
p : R[X]
hp : (aeval x) p * u = 0
this : map (↑f) (map (algebraMap R S) p * C u) = 0
⊢ map (algebraMap R S) p * C u = 0
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case add
R : Type u_3
inst✝ : CommRing R
I : Ideal R
P x y : R[X]
hx : x ∈ Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}
hy : y ∈ Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}
a✝¹ : ∀ (i : ℕ), x.coeff i ∈ I ^ i
a✝ : ∀ (i : ℕ), y.coeff i ∈ I ^ i
i : ℕ
⊢ (x + y).coeff i ∈ I ^ i

Tactic:
aesop

Goal state after:
Module: Mathlib.RingTheory.RingHom.QuasiFinite

Goal state before:
pp: R : Type u_6
S : Type u_7
T : Type u_8
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
hf : f.IsIntegral
g : S →+* T
hg✝ : g.IsStandardOpenImmersion
hg : (g.comp f).FiniteType
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝² : Algebra.IsIntegral R S
algebraizeInst✝¹ : Algebra.IsStandardOpenImmersion S T
algebraizeInst✝ : Algebra.FiniteType R T
s : S
hs : IsLocalization.Away s T
⊢ (g.comp f).QuasiFinite

Tactic:
exact Algebra.QuasiFinite.of_isIntegral_of_finiteType s

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
⊢ (algebraMap R ↥R[x]) a * ⟨l a * (algebraMap R S) p, ⋯⟩ ∈ ↑(Ideal.map (algebraMap R ↥R[x]) I) ∧
    (algebraMap (↥R[x]) S) ((algebraMap R ↥R[x]) a * ⟨l a * (algebraMap R S) p, ⋯⟩) =
      (algebraMap R S) a * ((algebraMap R S) p * l a)

pp: case h
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) p ∈ R[x]

Tactic:
case h =>
      rw [mul_comm]
      exact mem_conductor_iff.mp (Ideal.mem_comap.mp hp) _

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 ↥R[x]) a * ⟨l a * (algebraMap R S) p, ⋯⟩ ∈ ↑(Ideal.map (algebraMap R ↥R[x]) I) ∧
    (algebraMap (↥R[x]) S) ((algebraMap R ↥R[x]) a * ⟨l a * (algebraMap R S) p, ⋯⟩) =
      (algebraMap R S) a * ((algebraMap R S) p * l a)
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
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)
⊢ (l.sum fun a c ↦ c • (algebraMap R S) a * (algebraMap R S) p) ∈
    ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
refine Finset.sum_induction _ (fun u => u ∈ algebraMap R<x> S '' I.map (algebraMap R R<x>))
      (fun a b => ?_) ?_ ?_

Goal state after:
case refine_1
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)
a b : S
⊢ a ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I) →
    b ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I) →
      a + b ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

case refine_2
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)
⊢ 0 ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

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)
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommSemiring A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
v : Valuation B Γ
hv : Valuation.IsTrivialOn A v
w : B
hpos : 1 < v w
p : A[X]
hp : p ≠ 0
⊢ v ((aeval w) p) = v w ^ p.natDegree

Tactic:
rw [← valuation_aeval_monomial_eq_valuation_pow _ _ (leadingCoeff_ne_zero.mpr hp)]
  nth_rw 1 [as_sum_range p, map_sum]
  apply Valuation.map_sum_eq_of_lt _ (by simp)
  intro i hi
  simp only [Finset.mem_sdiff, Finset.mem_range, Nat.lt_add_one_iff, Finset.mem_singleton,
    ← lt_iff_le_and_ne] at hi
  simp only [← C_mul_X_pow_eq_monomial, map_mul, aeval_C, map_pow, aeval_X, coeff_natDegree]
  by_cases h0 : (p.coeff i) = 0
  · simp [hv.eq_one p.leadingCoeff (leadingCoeff_ne_zero.mpr hp),
      h0, pow_pos (lt_of_le_of_lt zero_le_one hpos) p.natDegree]
  · simp [hv.eq_one p.leadingCoeff (leadingCoeff_ne_zero.mpr hp),
      hv.eq_one _ h0, pow_lt_pow_right₀ hpos hi]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : ι → S[X]
a : ι
s : Finset ι
has : a ∉ s
IH : (∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) → ∀ (j : ℕ), IsIntegral R ((s.prod p).coeff j)
H : ∀ i ∈ insert a s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)
j : ℕ
i : ℕ × ℕ
hi : i ∈ Finset.antidiagonal j
x✝¹ : ι
x✝ : x✝¹ ∈ s
⊢ x✝¹ ∈ insert a s

Tactic:
aesop

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))
x : T
hx : (map (algebraMap S T) q).IsRoot x
⊢ eval₂ (algebraMap R T) x p = 0

Tactic:
by simpa using! aeval_eq_zero_of_dvd_aeval_eq_zero (x := x) H (by simp_all)

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
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
n : ℕ
r : R[X]
hr : map (algebraMap R S) r = map (algebraMap R S) p * q ^ n
h : ¬(algebraMap R S) p.leadingCoeff * q.leadingCoeff ^ n = 0
⊢ q.leadingCoeff ^ n ≠ 0

Tactic:
aesop

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

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
p : Ideal R
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : QuasiFiniteAt R q
⊢ WeaklyQuasiFiniteAt R q

Tactic:
rw [weaklyQuasiFiniteAt_iff]
  exact .of_surjective_algHom (Ideal.Quotient.mkₐ _ _) Ideal.Quotient.mk_surjective

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 σ
α β : Type w
e : α ≃ β
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial β S
H : (algebraMap (MvPolynomial β R) (MvPolynomial β S)).IsIntegralElem f
n : β →₀ ℕ
⊢ ((rename ⇑e).comp (algebraMap (MvPolynomial α R) (MvPolynomial α S))).comp (rename ⇑e.symm).toRingHom =
    algebraMap (MvPolynomial β R) (MvPolynomial β S)

Tactic:
aesop

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

Goal state before:
pp: case e'_6
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
α β : Type w
e : α ≃ β
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial β S
H : (algebraMap (MvPolynomial β R) (MvPolynomial β S)).IsIntegralElem f
n : β →₀ ℕ
⊢ (rename ⇑e).toRingHom ((rename ⇑e.symm) f) = f

Tactic:
aesop

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
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
⊢ constantCoeff = (isEmptyAlgEquiv S PEmpty.{?u.342 + 1}).toRingEquiv.toRingHom

Tactic:
aesop

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

Goal state before:
pp: case e'_6
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
this : constantCoeff = (isEmptyAlgEquiv S PEmpty.{?u.342 + 1}).toRingEquiv.toRingHom
⊢ (isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom (coeff 0 f) = f

Tactic:
simpa [-EmbeddingLike.apply_eq_iff_eq, -isEmptyAlgEquiv_apply] using!
        congr((isEmptyAlgEquiv S PEmpty.{w + 1}).symm ($this f))

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

Goal state before:
pp: 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 σ
α : Type w
inst✝ : Fintype α
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial (Option α) S
H : (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f
n : Option α →₀ ℕ
i : R
m : Option α →₀ ℕ
⊢ coeff m
      (((((optionEquivLeft S α).symm.toRingEquiv.toRingHom.comp
                  (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S)))).comp
              (optionEquivLeft R α).toRingEquiv.toRingHom).comp
          C)
        i) =
    coeff m (((algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).comp C) i)

Tactic:
aesop

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

Goal state before:
pp: case e'_5.hX.none
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst✝ : Fintype α
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial (Option α) S
H : (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f
n m : Option α →₀ ℕ
⊢ coeff m
      ((((optionEquivLeft S α).symm.toRingEquiv.toRingHom.comp
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S)))).comp
          (optionEquivLeft R α).toRingEquiv.toRingHom)
        (X none)) =
    coeff m ((algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)) (X none))

Tactic:
aesop

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

Goal state before:
pp: case e'_5.hX.some
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst✝ : Fintype α
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial (Option α) S
H : (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f
n m : Option α →₀ ℕ
val✝ : α
⊢ coeff m
      ((((optionEquivLeft S α).symm.toRingEquiv.toRingHom.comp
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S)))).comp
          (optionEquivLeft R α).toRingEquiv.toRingHom)
        (X (some val✝))) =
    coeff m ((algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)) (X (some val✝)))

Tactic:
aesop

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

Goal state before:
pp: case e'_6
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst✝ : Fintype α
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial (Option α) S
H : (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f
n : Option α →₀ ℕ
⊢ (optionEquivLeft S α).symm.toRingEquiv.toRingHom ((optionEquivLeft S α) f) = f

Tactic:
aesop

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
I : Ideal R
inst✝⁵ : I.IsPrime
J : Ideal R[X]
inst✝⁴ : J.IsPrime
inst✝³ : J.LiesOver I
inst✝² : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra I J
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
p : Ideal R
inst✝ : p.IsPrime
this :
  (AlgHom.restrictScalars R (aeval (1 ⊗ₜ[R] f X))).comp (mapAlgHom (Algebra.ofId R p.ResidueField)) =
    Algebra.TensorProduct.includeRight.comp f
x✝ : R[X]
⊢ x✝ ∈ RingHom.ker ↑f → x✝ ∈ RingHom.ker (Algebra.TensorProduct.includeRight.comp f)

Tactic:
aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1) → ∃ V f, S.arrows f ∧ x ∈ V.toOpens

Tactic:
rintro ⟨V, f, ⟨W, g, h, hg, rfl⟩, hxV⟩

Goal state after:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
V : TopologicalSpace.Opens ↥X
hxV : x ∈ V
W : X.AffineZariskiSite
g : W ⟶ U
h : V ⟶ (toOpensFunctor X).obj W
hg : S.arrows g
⊢ ∃ V f, S.arrows f ∧ x ∈ V.toOpens
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U).ι) x
⊢ ∃ k hki hkj y, (pullback.lift (X.homOfLE ⋯) (X.homOfLE ⋯) ⋯) y = x

Tactic:
have haU : a ∈ U.1 := (pullback.fst U.1.ι V.1.ι x).2

Goal state after:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U).ι) x
haU : a ∈ ↑U
⊢ ∃ k hki hkj y, (pullback.lift (X.homOfLE ⋯) (X.homOfLE ⋯) ⋯) y = x
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).numDenom =
    (C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q), C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))

Tactic:
numDenom,

Goal state after:
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).liftOn'
      (fun p q ↦
        if q = 0 then (0, 1)
        else
          have r := gcd p q;
          (C (q / r).leadingCoeff⁻¹ * (p / r), C (q / r).leadingCoeff⁻¹ * (q / r)))
      ⋯ =
    (C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q), C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))
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 : 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 : derivative P.f * p₁ + P.f * p₂ = P.g ^ n
⊢ ∃! ε, ε ∈ I ∧ P.HasMap (x + ε)

Tactic:
apply_fun aeval x at e

Goal state after:
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 * p₁ + P.f * p₂) = (aeval x) (P.g ^ n)
⊢ ∃! ε, ε ∈ I ∧ P.HasMap (x + ε)
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f g : S
H : HasStandardEtaleSurjectionOn R f
h : f ∣ g
⊢ HasStandardEtaleSurjectionOn R g

Tactic:
obtain ⟨P, φ, hsurj⟩ := H
  obtain ⟨g, rfl⟩ := h
  obtain ⟨a, ha⟩ := hsurj (algebraMap _ _ g)
  have : IsLocalization.Away (f * g) (Localization.Away (φ a)) :=
    ha ▸ .mul' (Localization.Away f) _ _ _
  have : IsStandardEtale R (Localization.Away a) := .of_isLocalizationAway a
  exact .mk _ (IsLocalization.Away.mapₐ_surjective_of_surjective
    (Aₚ := Localization.Away a) (Bₚ := Localization.Away (φ a)) a hsurj)

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 := { f := X, monic_f := ⋯, g := 1, cond := ⋯ }
this : P.X = 0
⊢ (aeval 0) P.f = 0

Tactic:
simp [P]

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 := { f := X, monic_f := ⋯, g := 1, cond := ⋯ }
this : P.X = 0
⊢ IsUnit ((aeval 0) P.g)

Tactic:
simp [P]

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, x ≠ 0 ∧ p.ResidueField[x] = ⊤

Tactic:
obtain ⟨x, hx⟩ := Field.exists_primitive_element p.ResidueField Q.ResidueField

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.Smooth.IntegralClosure

Goal state before:
pp: case e'_2
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, ⋯⟩)))
hfg : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)
heg :
  ∀ (g : R[X]),
    e (1 ⊗ₜ[R] (aeval 𝓟.x) g) =
      (algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)))
        ((AdjoinRoot.mk 𝓟'.f) (Polynomial.map (algebraMap R B) g))
k : ℕ
⊢ e (1 ⊗ₜ[R] ((aeval 𝓟.x) 𝓟.g ^ k)) = e (1 ⊗ₜ[R] (aeval 𝓟.x) 𝓟.g) ^ k

Tactic:
simp [← map_pow, 𝓟', StandardEtalePresentation.baseChange]

Goal state after: