mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x y : AdicCompletion I R
⊢ ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) (x + y)) ∘ₗ of I M =
    ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) x) ∘ₗ of I M +
      ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) y) ∘ₗ of I M

Tactic:
apply LinearMap.ext

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x y : AdicCompletion I R
⊢ ∀ (x_1 : M),
    (↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) (x + y)) ∘ₗ of I M) x_1 =
      (↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) x) ∘ₗ of I M +
          ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) y) ∘ₗ of I M)
        x_1
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
r x : AdicCompletion I R
⊢ ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) (r • x)) ∘ₗ of I M =
    (RingHom.id (AdicCompletion I R)) r • ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) x) ∘ₗ of I M

Tactic:
apply LinearMap.ext

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
r x : AdicCompletion I R
⊢ ∀ (x_1 : M),
    (↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) (r • x)) ∘ₗ of I M) x_1 =
      ((RingHom.id (AdicCompletion I R)) r •
          ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) x) ∘ₗ of I M)
        x_1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.negDblY P * P z ^ 2 =
    -(eval P) W'.polynomialX *
        ((eval P) W'.polynomialX ^ 2 - W'.a₁ * (eval P) W'.polynomialX * P z * (P y - W'.negY P) -
              W'.a₂ * P z ^ 2 * (P y - W'.negY P) ^ 2 -
            2 * P x * P z * (P y - W'.negY P) ^ 2 -
          P x * P z * (P y - W'.negY P) ^ 2) +
      P y * P z ^ 2 * (P y - W'.negY P) ^ 3

Tactic:
by
  linear_combination (norm := (rw [negDblY, eval_polynomialX, negY]; ring1))
    -9 * (P y ^ 2 * P z + 2 * W'.a₁ * P x * P y * P z - 3 * P x ^ 3 - 3 * W'.a₂ * P x ^ 2 * P z)
      * (equation_iff _).mp hP

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case e_6.h0
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ (Presentation.naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) ⋯).σ 0 = 0

Tactic:
rw [Presentation.naive, Generators.naive_σ]
    simp

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

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : P.RespectsIso
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
φ : R ⟶ S
ψ : R ⟶ T
h : P' (Spec.map ψ)
hf : P (pullback.fst (Spec.map ψ) (Spec.map φ))
⊢ P (Spec.map φ)

Tactic:
algebraize [φ.hom, ψ.hom]

Goal state after:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : P.RespectsIso
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
φ : R ⟶ S
ψ : R ⟶ T
h : P' (Spec.map ψ)
hf : P (pullback.fst (Spec.map ψ) (Spec.map φ))
algInst✝¹ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑T := (CommRingCat.Hom.hom ψ).toAlgebra
⊢ P (Spec.map φ)
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : P.RespectsIso
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
φ : R ⟶ S
ψ : R ⟶ T
h : P' (Spec.map ψ)
algInst✝¹ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑T := (CommRingCat.Hom.hom ψ).toAlgebra
hf :
  P (pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑T))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))))
⊢ Q (algebraMap (↑T) (↑T ⊗[↑R] ↑S))

Tactic:
← pullbackSpecIso_hom_fst R T S,

Goal state after:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : P.RespectsIso
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
φ : R ⟶ S
ψ : R ⟶ T
h : P' (Spec.map ψ)
algInst✝¹ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑T := (CommRingCat.Hom.hom ψ).toAlgebra
hf : P ((pullbackSpecIso ↑R ↑T ↑S).hom ≫ Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom))
⊢ Q (algebraMap (↑T) (↑T ⊗[↑R] ↑S))
Module: Mathlib.RingTheory.RingHom.QuasiFinite

Goal state before:
pp: R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite) ((algebraMap S (Localization.Away ↑r)).comp f✝)
algInst✝ : Algebra R S := f✝.toAlgebra
P : Ideal R
x✝ : P.IsPrime
this✝ : ∀ (r : ↥s), Module.Finite P.ResidueField (P.Fiber (Localization.Away ↑r))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away ↑r) :=
  fun r ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away ↑r))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away ↑r) := AlgHom.pi φ
this : IsNoetherian P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away ↑r))
a : P.Fiber S
ha : f a = 0
⊢ a = 0

Tactic:
apply eq_zero_of_localization _ fun J hJ ↦ ?_

Goal state after:
R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite) ((algebraMap S (Localization.Away ↑r)).comp f✝)
algInst✝ : Algebra R S := f✝.toAlgebra
P : Ideal R
x✝ : P.IsPrime
this✝ : ∀ (r : ↥s), Module.Finite P.ResidueField (P.Fiber (Localization.Away ↑r))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away ↑r) :=
  fun r ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away ↑r))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away ↑r) := AlgHom.pi φ
this : IsNoetherian P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away ↑r))
a : P.Fiber S
ha : f a = 0
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
⊢ (algebraMap (P.Fiber S) (Localization.AtPrime J)) a = 0
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
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
s : R
t : ↥M
H : IsIntegral R (IsLocalization.mk' S s t)
⊢ IsAlmostIntegral R (IsLocalization.mk' S s t)

Tactic:
exact H.isAlmostIntegral_of_exists_smul_mem_range ⟨t, hM t.2, by simp⟩

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 : IsIntegral R s
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
⊢ IsAlmostIntegral R s

Tactic:
obtain ⟨s, t, rfl⟩ := IsLocalization.exists_mk'_eq M s
  exact H.isAlmostIntegral_of_exists_smul_mem_range ⟨t, hM t.2, by simp⟩

Goal state after:
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
i : ℕ
hi : i ∈ Finset.range (p.natDegree + 1) \ {p.natDegree}
⊢ v ((aeval w) ((monomial i) (p.coeff i))) < v ((aeval w) ((monomial p.natDegree) (p.coeff p.natDegree)))

Tactic:
simp only [Finset.mem_sdiff, Finset.mem_range, Nat.lt_add_one_iff, Finset.mem_singleton,
    ← lt_iff_le_and_ne] at hi

Goal state after:
Γ : 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
i : ℕ
hi : i < p.natDegree
⊢ v ((aeval w) ((monomial i) (p.coeff i))) < v ((aeval w) ((monomial p.natDegree) (p.coeff p.natDegree)))
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
s : Finset ι
p : ι → S[X]
H : ∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)
j : ℕ
⊢ IsIntegral R ((s.prod p).coeff j)

Tactic:
induction s using Finset.induction generalizing j with

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : v RatFunc.X ≤ 1
p : K[X]
i : ℕ
h0 : p.coeff i = 0
⊢ i ∈ Finset.range (p.natDegree + 1) → v ((algebraMap K[X] K⟮X⟯) ((monomial i) (p.coeff i))) ≤ 1

pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : v RatFunc.X ≤ 1
p : K[X]
i : ℕ
h0 : ¬p.coeff i = 0
⊢ i ∈ Finset.range (p.natDegree + 1) → v ((algebraMap K[X] K⟮X⟯) ((monomial i) (p.coeff i))) ≤ 1

Tactic:
· simp_all

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : v RatFunc.X ≤ 1
p : K[X]
i : ℕ
h0 : ¬p.coeff i = 0
⊢ i ∈ Finset.range (p.natDegree + 1) → v ((algebraMap K[X] K⟮X⟯) ((monomial i) (p.coeff i))) ≤ 1
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
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S},
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f →
      ∀ (n : σ →₀ ℕ), Finite σ → IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial (↥f.vars) S
hg : (rename Subtype.val) g = f
n : ↥f.vars →₀ ℕ
⊢ (((rename Subtype.val).comp (algebraMap (MvPolynomial (↥f.vars) R) (MvPolynomial (↥f.vars) S))).comp
        (killCompl ⋯).toRingHom).IsIntegralElem
    ((rename Subtype.val).toRingHom g)

Tactic:
simp only [AlgHom.toRingHom_eq_coe, algebraMap_def, RingHom.coe_coe, hg]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S},
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f →
      ∀ (n : σ →₀ ℕ), Finite σ → IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial (↥f.vars) S
hg : (rename Subtype.val) g = f
n : ↥f.vars →₀ ℕ
⊢ (((↑(rename Subtype.val)).comp (map (algebraMap R S))).comp ↑(killCompl ⋯)).IsIntegralElem f
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: S : Type u_2
inst✝⁴ : CommRing S
q : Ideal S
inst✝³ : q.IsPrime
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : WeaklyQuasiFiniteAt K q
H : QuasiFinite K (Localization.AtPrime q ⧸ Ideal.map (algebraMap K (Localization.AtPrime q)) (Ideal.under K q))
⊢ Module.Finite K (Localization.AtPrime q)

Tactic:
← Ideal.over_def q ⊥,

Goal state after:
S : Type u_2
inst✝⁴ : CommRing S
q : Ideal S
inst✝³ : q.IsPrime
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : WeaklyQuasiFiniteAt K q
H : QuasiFinite K (Localization.AtPrime q ⧸ Ideal.map (algebraMap K (Localization.AtPrime q)) ⊥)
⊢ Module.Finite K (Localization.AtPrime q)
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 : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
φ₁ : p.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
y : p.Fiber S
hy : y ∈ Q.primeCompl
r : R
hrp : r ∉ p
s : S
H : r • y = 1 ⊗ₜ[R] s
this✝ : s ∉ q
this : IsUnit ((algebraMap Sq (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ((algebraMap S Sq) ↑⟨s, this✝⟩))
⊢ IsUnit (φ₂ (1 ⊗ₜ[R] s))

Tactic:
simpa [φ₂, ← IsScalarTower.algebraMap_apply] using this

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

Goal state before:
pp: X : Scheme
⊢ ∀ (U : X.Opens), Sieve.coverByImage (toOpensFunctor X) U ∈ (Opens.grothendieckTopology ↥X) U

Tactic:
by
    intro U x hx
    obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open hx U.2
    exact ⟨V, homOfLE hVU, ⟨⟨V, hV⟩, 𝟙 _, homOfLE hVU, rfl⟩, hxV⟩

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

Goal state before:
pp: case refine_2
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
H : P { down := { down := ⋯ } }
⊢ U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } }

Tactic:
obtain rfl : _ = V := hf

Goal state after:
case refine_2
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
f : ↑Γ(X, U.toOpens)
hV : IsAffineOpen (X.basicOpen f)
x✝ : ⟨X.basicOpen f, hV⟩ ⟶ U
H : P { down := { down := ⋯ } }
⊢ U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : CommRing K
x✝¹ x✝ : K⟮X⟯
toFractionRing✝¹ toFractionRing✝ : FractionRing K[X]
⊢ ({ toFractionRing := toFractionRing✝¹ } + { toFractionRing := toFractionRing✝ }).toFractionRing =
    { toFractionRing := toFractionRing✝¹ }.toFractionRing + { toFractionRing := toFractionRing✝ }.toFractionRing

Tactic:
by simp [← ofFractionRing_add]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
F : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ⇑φ
⊢ Function.Injective ⇑(map φ hφ)

Tactic:
rintro ⟨x⟩ ⟨y⟩ h
  induction x using Localization.induction_on
  induction y using Localization.induction_on
  simpa only [map_apply_ofFractionRing_mk, ofFractionRing_injective.eq_iff,
    Localization.mk_eq_mk_iff, Localization.r_iff_exists, mul_cancel_left_coe_nonZeroDivisors,
    exists_const, ← map_mul, hf.eq_iff] using h

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

Goal state before:
pp: case refine_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
φ : 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'))
a : S'
ham : a ∈ m
⊢ 0 ∈ Multiset.map (eval a) (Multiset.map (fun x ↦ X - C x) m)

Tactic:
· simpa using ⟨a, ham, by simp⟩

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] = ⊤
hx0 : x = 0
⊢ p.ResidueField[1] = ⊤

Tactic:
simpa [p, hx0] using hx

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
p : Ideal S
r : S
hrp : r ∉ p
H : ∀ (x : S), ∃ m, IsIntegral R (r ^ m * x)
n : ℕ
hn : IsIntegral R (r ^ n * r)
⊢ IsIntegral R r

Tactic:
← pow_succ

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
hrp : r ∉ p
H : ∀ (x : S), ∃ m, IsIntegral R (r ^ m * x)
n : ℕ
hn : IsIntegral R (r ^ (n + 1))
⊢ IsIntegral R r
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: 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
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := (conductor R (f X)).radical
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
⊢ (aeval ((Ideal.Quotient.mk (conductor R (f X)).radical) (f X))).Finite

Tactic:
convert! (RingHom.Finite.of_surjective _ (Ideal.Quotient.mk_surjective (I := J))).comp hf
      using 1

Goal state after:
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
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := (conductor R (f X)).radical
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
⊢ (aeval ((Ideal.Quotient.mk (conductor R (f X)).radical) (f X))).toRingHom = (Ideal.Quotient.mk J).comp f.toRingHom
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
n : ℕ
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg : natDegree 0 ≤ n
⊢ f.resultant 0 f.natDegree n = (Multiset.map (fun x ↦ eval x 0) f.roots).prod

Tactic:
by_cases hf' : f.natDegree = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
n : ℕ
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg : natDegree 0 ≤ n
hf' : f.natDegree = 0
⊢ f.resultant 0 f.natDegree n = (Multiset.map (fun x ↦ eval x 0) f.roots).prod

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
n : ℕ
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg : natDegree 0 ≤ n
hf' : ¬f.natDegree = 0
⊢ f.resultant 0 f.natDegree n = (Multiset.map (fun x ↦ eval x 0) f.roots).prod
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.injective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Injective ⇑φ
f : R[X]
IH :
  ∀ (g : S[X]) (r : S),
    map φ f ≠ 0 →
      g ≠ 0 →
        ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
          r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  ((map φ f).scaleRoots (φ r)).resultant ((map φ g).scaleRoots (φ r)) (map φ f).natDegree (map φ g).natDegree =
    φ r ^ ((map φ f).natDegree * (map φ g).natDegree) * (map φ f).resultant (map φ g)
⊢ φ ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) =
    φ (r ^ (f.natDegree * g.natDegree) * f.resultant g)

Tactic:
← map_scaleRoots,

Goal state after:
case inr.inr.injective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Injective ⇑φ
f : R[X]
IH :
  ∀ (g : S[X]) (r : S),
    map φ f ≠ 0 →
      g ≠ 0 →
        ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
          r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  (map φ (f.scaleRoots r)).resultant ((map φ g).scaleRoots (φ r)) (map φ f).natDegree (map φ g).natDegree =
    φ r ^ ((map φ f).natDegree * (map φ g).natDegree) * (map φ f).resultant (map φ g)
⊢ φ ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) =
    φ (r ^ (f.natDegree * g.natDegree) * f.resultant g)

case inr.inr.injective.h
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Injective ⇑φ
f : R[X]
IH :
  ∀ (g : S[X]) (r : S),
    map φ f ≠ 0 →
      g ≠ 0 →
        ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
          r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  ((map φ f).scaleRoots (φ r)).resultant ((map φ g).scaleRoots (φ r)) (map φ f).natDegree (map φ g).natDegree =
    φ r ^ ((map φ f).natDegree * (map φ g).natDegree) * (map φ f).resultant (map φ g)
⊢ φ f.leadingCoeff ≠ 0