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

Goal state before:
pp: case e'_5
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
k : ℕ
hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCauchySequence I N
hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤
n : ℕ
d : N
hdmem : d ∈ I ^ (k + n + 1) • ⊤
y yₙ : M
hd : f y = ↑x (k + n + 1) - d
hyₙ : f yₙ - ↑x (k + n) ∈ I ^ (k + n) • ⊤
⊢ ↑x (k + n + 1) - d - f yₙ = ↑x (k + n + 1) - ↑x (k + n) - d - (f yₙ - ↑x (k + n))

pp: case convert_6
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
k : ℕ
hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCauchySequence I N
hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤
n : ℕ
d : N
hdmem : d ∈ I ^ (k + n + 1) • ⊤
y yₙ : M
hd : f y = ↑x (k + n + 1) - d
hyₙ : f yₙ - ↑x (k + n) ∈ I ^ (k + n) • ⊤
⊢ ↑x (k + n + 1) - ↑x (k + n) - d - (f yₙ - ↑x (k + n)) ∈ I ^ (k + n) • ⊤

Tactic:
· abel

Goal state after:
case convert_6
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
k : ℕ
hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCauchySequence I N
hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤
n : ℕ
d : N
hdmem : d ∈ I ^ (k + n + 1) • ⊤
y yₙ : M
hd : f y = ↑x (k + n + 1) - d
hyₙ : f yₙ - ↑x (k + n) ∈ I ^ (k + n) • ⊤
⊢ ↑x (k + n + 1) - ↑x (k + n) - d - (f yₙ - ↑x (k + n)) ∈ I ^ (k + n) • ⊤
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
n : ℕ
⊢ (↑(evalₐ I n)).comp (liftRingHom I f ⋯) = f n

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: S : Type u_5
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ (Ideal.Quotient.mk (I ^ n • ⊤)) ((ofAlgEquiv I).symm x) = (eval I S n) x

Tactic:
nth_rw 2 [← of_ofAlgEquiv_symm I x]

Goal state after:
S : Type u_5
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ (Ideal.Quotient.mk (I ^ n • ⊤)) ((ofAlgEquiv I).symm x) = (eval I S n) ((of I S) ((ofAlgEquiv I).symm x))
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
⊢ g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))

Tactic:
wlog h : m ∈ LinearMap.ker s

Goal state after:
case inr
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
this :
  ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
    [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K]
    [inst_6 : Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K},
    s ∘ₗ f = LinearMap.id →
      Function.Exact ⇑f ⇑g →
        ∀ {κ : Type u_6} {σ : Type u_7} (v : κ ⊕ σ → M),
          Function.Surjective ⇑g →
            (∀ (i : κ), s (v (Sum.inl i)) = 0) →
              LinearIndependent R (⇑s ∘ v ∘ Sum.inr) →
                ⊤ ≤ Submodule.span R (Set.range v) → ∀ m ∈ s.ker, g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))
h : m ∉ s.ker
⊢ g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))

R✝ : Type u_1
M✝ : Type u_2
K✝ : Type u_3
P✝ : Type u_4
inst✝¹³ : Ring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup K✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ K✝
inst✝⁷ : Module R✝ P✝
g✝ : M✝ →ₗ[R✝] P✝
s✝ : M✝ →ₗ[R✝] K✝
κ✝ : Type u_6
σ✝ : Type u_7
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
h : m ∈ s.ker
⊢ g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
this : Fintype σ
⊢ IsUnit ((LinearMap.toMatrix (Pi.basisFun S σ) (Pi.basisFun S σ)) P.aevalDifferential).det

Tactic:
convert! P.jacobian_isUnit
    rw [LinearMap.toMatrix_eq_toMatrix', jacobian_eq_jacobiMatrix_det,
      aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, P.algebraMap_eq]
    simp [RingHom.map_det]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : PreSubmersivePresentation R S ι σ
x : ↥P.ker
i : σ
⊢ (Finsupp.linearEquivFunOnFinite S S σ)
      ((Finsupp.lcomapDomain P.map ⋯)
        (P.cotangentSpaceBasis.repr (1 ⊗ₜ[P.toExtension.Ring] (KaehlerDifferential.D R P.toExtension.Ring) ↑x)))
      i =
    (aeval P.val) ((pderiv (P.map i)) ↑x)

Tactic:
simp only [Generators.toExtension_Ring, Finsupp.lcomapDomain_apply,
    Finsupp.linearEquivFunOnFinite_apply, Finsupp.comapDomain_apply,
    Generators.cotangentSpaceBasis_repr_tmul, one_mul]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: case a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.dblY P * P z ^ 2 + W'.negDblY P * P z ^ 2 - ((eval P) W'.polynomialX ^ 3 + -(eval P) W'.polynomialX ^ 3) = 0

Tactic:
(rw [dblY, negY_eq, dblX_of_Y_eq hP hPz hQz hx hy hy',
    dblZ_of_Y_eq hQz hx hy hy']; ring1)

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

Goal state before:
pp: 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 ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
⊢ ((localizationAway T g).comp P).ker =
    Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker ⊔ Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1}

Tactic:
by
  have : (localizationAway T g).ker = Ideal.map ((localizationAway T g).ofComp P).toAlgHom
      (Ideal.span {MvPolynomial.rename Sum.inr f * MvPolynomial.X (Sum.inl ()) - 1}) := by
    rw [Ideal.map_span, Set.image_singleton, map_sub, map_mul, map_one, ker_localizationAway,
      Hom.toAlgHom_X, toAlgHom_ofComp_rename, h, ofComp_val, Sum.elim_inl]
  rw [ker_comp_eq_sup, Algebra.Generators.map_toComp_ker, this,
    Ideal.comap_map_of_surjective _ (toAlgHom_ofComp_surjective _ P), ← RingHom.ker_eq_comap_bot,
    ← sup_assoc]
  simp

Goal state after:
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✝¹ : FinitePresentation R S
inst✝ : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
hb : Set.range ⇑b ⊆ Set.range ⇑(D R S)
a✝ : Nontrivial S
n : ℕ
P : Generators R S (Fin n)
⊢ IsStandardSmooth R S

Tactic:
choose f' hf' using hb

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
inst✝ : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
a✝ : Nontrivial S
n : ℕ
P : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → a ∈ Set.range ⇑b → S
hf' : ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : a ∈ Set.range ⇑b), (D R S) (f' a_1) = a
⊢ IsStandardSmooth R S
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal ↑Γ(Y, U) := (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
q : Ideal ↑Γ(X, V) := (hV.primeIdealOf ⟨x, hx⟩).asIdeal
this : q.LiesOver p
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)

Tactic:
let := Localization.AtPrime.algebraOfLiesOver p q

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal ↑Γ(Y, U) := (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
q : Ideal ↑Γ(X, V) := (hV.primeIdealOf ⟨x, hx⟩).asIdeal
this✝ : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)
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
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : (aeval a) q₁ = 0
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : F.totalDegree ≤ q₁.totalDegree
⊢ IsUnit q₁ ∨ IsUnit q₂

Tactic:
e,

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : (aeval a) q₁ = 0
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : (q₁ * q₂).totalDegree ≤ q₁.totalDegree
⊢ IsUnit q₁ ∨ IsUnit q₂
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: X✝ X : Scheme
Z Y : X.Etale
f : Z ⟶ Y
⊢ Etale (f.left ≫ Y.hom)

Tactic:
CategoryTheory.Over.w

Goal state after:
X✝ X : Scheme
Z Y : X.Etale
f : Z ⟶ Y
⊢ Etale (Over.hom Z.toComma)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (W'⁄B).addX (⇑f ∘ P) (⇑f ∘ Q) = f ((W'⁄A).addX P Q)

Tactic:
by
  rw [← RingHom.coe_coe, ← map_addX, map_baseChange]

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k ↑s)) K
t : Finset K
hts : ↑t ⊆ ↑s
ht : IsTranscendenceBasis k Subtype.val
⊢ Algebra.IsAlgebraic (↥(adjoin k ↑t)) K

Tactic:
convert! ht.isAlgebraic_field <;> simp

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
M : Submonoid S
inst✝¹ : IsLocalization M T
inst✝ : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
p : R[X]
u : S
s : ↥M
hp : (aeval ((algebraMap S T) x)) p * IsLocalization.mk' T u s = 0
⊢ ∃ a ∈ M, a * ((aeval x) p * u) = 0

Tactic:
simpa [aeval_algebraMap_apply, ← Algebra.smul_def, IsLocalization.smul_mk',
      IsLocalization.mk'_eq_zero_iff] using hp

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

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
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
e : eval₂ (algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (C x * X) p = 0
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
⊢ q.coeff p.natDegree ≠ 0

Tactic:
simp [q, hp]

Goal state after:
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
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
e : eval₂ (algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (C x * X) p = 0
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
⊢ q.coeff p.natDegree = 1

Tactic:
simp [q, hp]

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
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
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
⊢ conductor R x ⊔ Ideal.map (algebraMap R S) I = ⊤

Tactic:
Ideal.eq_top_iff_one

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
hx : 1 ∈ 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
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
⊢ 1 ∈ conductor R x ⊔ Ideal.map (algebraMap R S) I
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective ⇑C

Tactic:
rw [← algebraMap_comp_C, RingHom.coe_comp]

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective (⇑(algebraMap K[X] K⟮X⟯) ∘ ⇑Polynomial.C)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case neg
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
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S
hp : IsAlmostIntegral R[X] (C p)
hn : (C p).natDegree = n
hp' : (C p).natDegree = 0
h : ¬i = 0
⊢ IsAlmostIntegral R 0

Tactic:
· exact (completeIntegralClosure R S).zero_mem

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
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
⊢ p - C p.leadingCoeff * map (algebraMap R S) (X ^ p.natDegree) ∈ completeIntegralClosure R[X] S[X]

Tactic:
refine sub_mem hp (mul_mem ?_ (algebraMap_mem (R := R[X]) _ _))

Goal state after:
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
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
⊢ C p.leadingCoeff ∈ completeIntegralClosure R[X] S[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
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • p.leadingCoeff ^ n ∈ (algebraMap R S).range
⊢ C p.leadingCoeff ∈ completeIntegralClosure R[X] S[X]

Tactic:
refine ⟨C r, by simpa using hr, fun n ↦ ?_⟩

Goal state after:
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
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n✝ : ℕ
IH : ∀ m < n✝, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n✝
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • p.leadingCoeff ^ n ∈ (algebraMap R S).range
n : ℕ
⊢ C r • C p.leadingCoeff ^ n ∈ (algebraMap R[X] S[X]).range
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
⊢ QuasiFinite R (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))

Tactic:
let := Localization.AtPrime.algebraOfLiesOver p q

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
⊢ QuasiFinite R (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case refine_1.refine_1
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ Spec.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))

pp: case refine_1.refine_2
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ (Spec R).fromSpecResidueField x ≫ 𝟙 (Spec R) =
    Spec.map (Spec.residueFieldIso R x).inv ≫ Spec.map (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField))

Tactic:
· simp; rfl

Goal state after:
case refine_1.refine_2
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ (Spec R).fromSpecResidueField x ≫ 𝟙 (Spec R) =
    Spec.map (Spec.residueFieldIso R x).inv ≫ Spec.map (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField))
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : RingHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ ∀ (x y : R⟮X⟯), (↑(map φ hφ)).toFun (x + y) = (↑(map φ hφ)).toFun x + (↑(map φ hφ)).toFun y

Tactic:
rintro ⟨x⟩ ⟨y⟩

Goal state after:
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]
inst✝ : RingHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
x y : FractionRing R[X]
⊢ (↑(map φ hφ)).toFun ({ toFractionRing := x } + { toFractionRing := y }) =
    (↑(map φ hφ)).toFun { toFractionRing := x } + (↑(map φ hφ)).toFun { toFractionRing := y }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ Function.Injective ⇑(liftMonoidWithZeroHom φ hφ')

Tactic:
rintro ⟨x⟩ ⟨y⟩

Goal state after:
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
x y : FractionRing R[X]
⊢ (liftMonoidWithZeroHom φ hφ') { toFractionRing := x } = (liftMonoidWithZeroHom φ hφ') { toFractionRing := y } →
    { toFractionRing := x } = { toFractionRing := y }