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

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

pp: case neg
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
· rw [toAffine_of_Z_ne_zero hP hPz, toAffine_of_Z_ne_zero hQ hQz, Affine.Point.add_of_Y_eq
            ((X_eq_iff hPz hQz).mp hxy.left) ((Y_eq_iff' hPz hQz).mp hxy.right)]
        by_cases hy : P y * Q z = Q y * P z
        · rw [add_of_Y_eq hP.left hPz hQz hxy.left hy hxy.right,
            toAffine_smul _ <| isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, toAffine_zero]
        · rw [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy,
            toAffine_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy, toAffine_zero]

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q
Module: Mathlib.RingTheory.RingHom.Smooth

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ f.Smooth

Tactic:
rw [RingHom.smooth_def]
  exact ⟨.of_bijective hf, .of_bijective hf⟩

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

Goal state before:
pp: R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
⊢ ∃ r ∈ s, x ∈ PrimeSpectrum.basicOpen r

Tactic:
by
    simpa using (PrimeSpectrum.iSup_basicOpen_eq_top_iff'.mpr hs).ge
      (TopologicalSpace.Opens.mem_top x)

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

Goal state before:
pp: case e'_1
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
this : LocalizedModule (Submonoid.powers f) (H1Cotangent R A) ≃ₗ[A] H1Cotangent R (Localization.Away f)
⊢ Subsingleton (H1Cotangent R (Localization.Away f)) ↔ Subsingleton (LocalizedModule.Away f (H1Cotangent R A))

Tactic:
rw [this.subsingleton_congr]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
r : R
x✝ : S
y✝ : Ω[A⁄R]
⊢ x✝ ⊗ₜ[R] ((algebraMap R A) r • y✝) = r • x✝ ⊗ₜ[R] y✝

Tactic:
algebraMap_smul,

Goal state after:
case tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
r : R
x✝ : S
y✝ : Ω[A⁄R]
⊢ x✝ ⊗ₜ[R] (r • y✝) = r • x✝ ⊗ₜ[R] y✝
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (D S (S ⊗[R] A)) (s ⊗ₜ[R] a) = (algebraMap S (S ⊗[R] A)) s • (D S (S ⊗[R] A)) (1 ⊗ₜ[R] a)

Tactic:
algebraMap_smul,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (D S (S ⊗[R] A)) (s ⊗ₜ[R] a) = s • (D S (S ⊗[R] A)) (1 ⊗ₜ[R] a)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (D S (A ⊗[R] S)) (a ⊗ₜ[R] s) = (algebraMap S (A ⊗[R] S)) s • (D S (A ⊗[R] S)) (a ⊗ₜ[R] 1)

Tactic:
algebraMap_smul,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (D S (A ⊗[R] S)) (a ⊗ₜ[R] s) = s • (D S (A ⊗[R] S)) (a ⊗ₜ[R] 1)
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R ⧸ I • ⊤
b₁ b₂ : R
h✝ : b₁ ≈ b₂
a✝ : M
h : b₁ - b₂ ∈ I
⊢ (b₁ - b₂) • Quotient.mk'' a✝ = 0

Tactic:
Submodule.Quotient.mk''_eq_mk,

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R ⧸ I • ⊤
b₁ b₂ : R
h✝ : b₁ ≈ b₂
a✝ : M
h : b₁ - b₂ ∈ I
⊢ (b₁ - b₂) • Submodule.Quotient.mk a✝ = 0
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
ι : Type u_4
inst✝ : Finite ι
⊢ Function.Bijective ⇑(ofTensorProduct I (ι → R))

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
ι : Type u_4
inst✝ : Finite ι
val✝ : Fintype ι
⊢ Function.Bijective ⇑(ofTensorProduct I (ι → R))
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Smooth R S
f : (p : Ideal S) → [inst : p.IsPrime] → [IsSmoothAt R p] → S
hf₁ : ∀ (p : Ideal S) [inst : p.IsPrime] [inst_1 : IsSmoothAt R p], f p ∉ p
hf₂ : ∀ (p : Ideal S) [inst : p.IsPrime] [inst_1 : IsSmoothAt R p], IsStandardSmooth R (Localization.Away (f p))
⊢ ∀ x ∈ Set.range fun p ↦ f p.asIdeal, IsStandardSmooth R (Localization.Away x)

Tactic:
by
    simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]; intro; apply hf₂

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

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
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
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : P.σ g ^ n * ↑x ∈ P.ker ^ 2
⊢ (algebraMap P.Ring S) (P.σ g ^ n) • Extension.Cotangent.mk x = 0

Tactic:
algebraMap_smul,

Goal state after:
case h
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
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
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : P.σ g ^ n * ↑x ∈ P.ker ^ 2
⊢ P.σ g ^ n • Extension.Cotangent.mk x = 0
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: case h₂
n : ℕ
⊢ ∀ ⦃R S T : Type u_2⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    IsStandardSmoothOfRelativeDimension n (algebraMap R T) →
      IsStandardSmoothOfRelativeDimension n (algebraMap S (S ⊗[R] T))

Tactic:
introv h
    replace h : Algebra.IsStandardSmoothOfRelativeDimension n R T := by
      rw [RingHom.IsStandardSmoothOfRelativeDimension] at h
      convert! h; ext; simp_rw [Algebra.smul_def]; rfl
    suffices Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T) by
      rw [RingHom.IsStandardSmoothOfRelativeDimension]
      convert! this; ext; simp_rw [Algebra.smul_def]; rfl
    infer_instance

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

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ f.Smooth ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f

Tactic:
by
  refine ⟨fun hf ↦ hf.locally_isStandardSmooth, fun hf ↦ ?_⟩
  rw [← locally_iff_of_localizationSpanTarget Smooth.propertyIsLocal.respectsIso
    Smooth.ofLocalizationSpanTarget]
  exact locally_of_locally (fun hf ↦ hf.smooth) hf

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis k fun x ↦ a ↑x
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (F.toPolynomialAdjoinImageCompl a i)
⊢ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)

Tactic:
have := (AlgebraicIndepOn.aevalEquiv (s := {i}ᶜ) Hi.1).uniqueFactorizationMonoid inferInstance

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis k fun x ↦ a ↑x
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (F.toPolynomialAdjoinImageCompl a i)
this : UniqueFactorizationMonoid ↥(Algebra.adjoin k (a '' {i}ᶜ))
⊢ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
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 : S[X]
hp : (aeval x) p * t = 0
⊢ map (algebraMap S T) p * C t = 0

Tactic:
obtain ⟨p, rfl⟩ := map_surjective _ H p

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
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
⊢ map (algebraMap S T) (map (algebraMap R S) p) * C t = 0
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this✝ : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
this : Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p) ≤ p
P : Ideal SQ
hP : P.IsPrime
e : Ideal.comap (algebraMap R SQ) P = p
⊢ Ideal.under S P ≤ Q

Tactic:
exact (Ideal.comap_mono (IsLocalRing.le_maximalIdeal_of_isPrime P)).trans_eq
      Localization.AtPrime.under_maximalIdeal

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

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q
⊢ (RatFunc.mk p q).liftOn' f H = f p q

Tactic:
rw [RatFunc.liftOn', RatFunc.liftOn_mk _ _ _ f0]

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q
⊢ ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'
Module: Mathlib.RingTheory.Conductor

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
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
⊢ Function.Surjective ⇑f

Tactic:
refine Ideal.Quotient.lift_surjective_of_surjective _ _ fun y => ?_

Goal state after:
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
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
⊢ ∃ a, ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) a = y
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 : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
x✝ : ℕ
hn : p.natDegree = x✝
⊢ IsAlmostIntegral R (p.coeff i)

Tactic:
induction hn : p.natDegree using Nat.strong_induction_on generalizing p with

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

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
f : R[X] →ₐ[R] S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
algInst✝ : Algebra R[X] S := f.toAlgebra
e : Ideal.map C (Ideal.under R P) = Ideal.comap (↑f) P
this✝³ : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime (Ideal.under R[X] P)) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) (Ideal.under R[X] P)
this✝² : Algebra (Localization.AtPrime (Ideal.under R[X] P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R[X] P) P
this✝¹ : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
this✝ : Module.Finite (Ideal.under R P).ResidueField P.ResidueField
this : Module.Finite (Ideal.under R P).ResidueField (Ideal.under R[X] P).ResidueField
⊢ False

Tactic:
have : Module.Finite (P.under R).ResidueField (RatFunc (P.under R).ResidueField) :=
    .of_surjective (residueFieldMapCAlgEquiv _ (P.under _) e.symm).toLinearMap
      (residueFieldMapCAlgEquiv _ (P.under _) e.symm).surjective

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
algInst✝ : Algebra R[X] S := f.toAlgebra
e : Ideal.map C (Ideal.under R P) = Ideal.comap (↑f) P
this✝⁴ : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime (Ideal.under R[X] P)) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) (Ideal.under R[X] P)
this✝³ : Algebra (Localization.AtPrime (Ideal.under R[X] P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R[X] P) P
this✝² : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
this✝¹ : Module.Finite (Ideal.under R P).ResidueField P.ResidueField
this✝ : Module.Finite (Ideal.under R P).ResidueField (Ideal.under R[X] P).ResidueField
this : Module.Finite (Ideal.under R P).ResidueField (RatFunc (Ideal.under R P).ResidueField)
⊢ False
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 S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
φ : A ⊗[R] S →ₐ[A] (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₁ : Function.Surjective ⇑φ
hφ₂ : RingHom.ker φ.toRingHom = Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)
hφ₃ :
  φ.comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p)))
this : (Ideal.map φ.toRingHom q).IsPrime
⊢ p = Ideal.comap (φ.comp TensorProduct.includeRight.toRingHom) (Ideal.map φ.toRingHom q)

Tactic:
← Ideal.comap_comap,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
φ : A ⊗[R] S →ₐ[A] (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₁ : Function.Surjective ⇑φ
hφ₂ : RingHom.ker φ.toRingHom = Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)
hφ₃ :
  φ.comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p)))
this : (Ideal.map φ.toRingHom q).IsPrime
⊢ p = Ideal.comap TensorProduct.includeRight.toRingHom (Ideal.comap φ.toRingHom (Ideal.map φ.toRingHom 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)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
this : Function.Surjective ⇑φ₃
⊢ QuasiFinite R (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))

Tactic:
have inst : QuasiFiniteAt R Q := .trans _ p.ResidueField _

Goal state after:
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)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
this : Function.Surjective ⇑φ₃
inst : QuasiFiniteAt R Q
⊢ QuasiFinite R (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H.H
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₀⁰
y✝¹ y✝ : R[X] × ↥R[X]⁰
⊢ { toFractionRing := Localization.mk (y✝¹.1 * y✝.1) (y✝¹.2 * y✝.2) }.liftOn (fun p q ↦ φ p / φ q) ⋯ =
    { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 }.liftOn (fun p q ↦ φ p / φ q) ⋯ *
      { toFractionRing := Localization.mk y✝.1 y✝.2 }.liftOn (fun p q ↦ φ p / φ q) ⋯

Tactic:
simp only [liftOn_ofFractionRing_mk, div_mul_div_comm, map_mul, Submonoid.coe_mul]

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePresentation R S
x : Localization.Away ((AdjoinRoot.mk P.f) P.g)
⊢ ∃ p n, (P.equivRing.trans P.equivAwayAdjoinRoot).symm x * (aeval P.x) P.g ^ n = (aeval P.x) p

Tactic:
obtain ⟨⟨p, ⟨_, n, rfl⟩⟩, e⟩ := IsLocalization.surj (.powers (AdjoinRoot.mk P.f P.g)) x

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePresentation R S
x : Localization.Away ((AdjoinRoot.mk P.f) P.g)
p : AdjoinRoot P.f
n : ℕ
e :
  x *
      (algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g)))
        ↑(p, ⟨(fun x ↦ (AdjoinRoot.mk P.f) P.g ^ x) n, ⋯⟩).2 =
    (algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g)))
      (p, ⟨(fun x ↦ (AdjoinRoot.mk P.f) P.g ^ x) n, ⋯⟩).1
⊢ ∃ p n, (P.equivRing.trans P.equivAwayAdjoinRoot).symm x * (aeval P.x) P.g ^ n = (aeval P.x) p