mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case zero.refine_1
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : Projective M
p : MaximalSpectrum R
⊢ Projective (M.localizedModule p.asIdeal.primeCompl)

pp: case zero.refine_2
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (m : MaximalSpectrum R), Projective (M.localizedModule m.asIdeal.primeCompl)
⊢ Projective M

Tactic:
·

Goal state after:
case zero.refine_1
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : Projective M
p : MaximalSpectrum R
⊢ Projective (M.localizedModule p.asIdeal.primeCompl)
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case zero.refine_2
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (m : MaximalSpectrum R), Projective (M.localizedModule m.asIdeal.primeCompl)
⊢ Projective M

Tactic:
·

Goal state after:
case zero.refine_2
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (m : MaximalSpectrum R), Projective (M.localizedModule m.asIdeal.primeCompl)
⊢ Projective M
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
⊢ (ResidueField R)[(residue S) β] = ⊤ → R[β] = ⊤

pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
⊢ R[β] = ⊤ → (ResidueField R)[(residue S) β] = ⊤

Tactic:
·

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
⊢ (ResidueField R)[(residue S) β] = ⊤ → R[β] = ⊤
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case mp.refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : Function.Surjective ⇑(aeval ((residue S) β))
s : S
a✝ : s ∈ ⊤
q : R[X]
hp : (aeval ((residue S) β)) (map (residue R) q) = (residue S) s
⊢ (aeval β) q ∈ Subalgebra.toSubmodule R[β]

pp: case mp.refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : Function.Surjective ⇑(aeval ((residue S) β))
s : S
a✝ : s ∈ ⊤
q : R[X]
hp : (aeval ((residue S) β)) (map (residue R) q) = (residue S) s
⊢ s - (aeval β) q ∈ Submodule.restrictScalars R (Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
·

Goal state after:
case mp.refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : Function.Surjective ⇑(aeval ((residue S) β))
s : S
a✝ : s ∈ ⊤
q : R[X]
hp : (aeval ((residue S) β)) (map (residue R) q) = (residue S) s
⊢ (aeval β) q ∈ Subalgebra.toSubmodule R[β]
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case mp.refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : Function.Surjective ⇑(aeval ((residue S) β))
s : S
a✝ : s ∈ ⊤
q : R[X]
hp : (aeval ((residue S) β)) (map (residue R) q) = (residue S) s
⊢ s - (aeval β) q ∈ Submodule.restrictScalars R (Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
·

Goal state after:
case mp.refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : Function.Surjective ⇑(aeval ((residue S) β))
s : S
a✝ : s ∈ ⊤
q : R[X]
hp : (aeval ((residue S) β)) (map (residue R) q) = (residue S) s
⊢ s - (aeval β) q ∈ Submodule.restrictScalars R (Ideal.map (algebraMap R S) (maximalIdeal R))
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
⊢ R[β] = ⊤ → (ResidueField R)[(residue S) β] = ⊤

Tactic:
·

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
⊢ R[β] = ⊤ → (ResidueField R)[(residue S) β] = ⊤
Module: Mathlib.RingTheory.LocalRing.Etale

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
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
this : Module.Free R S
e : (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) ≃ₗ[R ⧸ maximalIdeal R] S ⧸ maximalIdeal S
⊢ Module.finrank R S = Module.finrank (ResidueField R) (ResidueField S)

pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
this : Module.Free R S
⊢ ∀ (c : R ⧸ maximalIdeal R) (x : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)),
    (Ideal.quotEquivOfEq ⋯).toAddEquiv (c • x) = c • (Ideal.quotEquivOfEq ⋯).toAddEquiv x

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
this : Module.Free R S
e : (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) ≃ₗ[R ⧸ maximalIdeal R] S ⧸ maximalIdeal S
⊢ Module.finrank R S = Module.finrank (ResidueField R) (ResidueField S)
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
this : Module.Free R S
⊢ ∀ (c : R ⧸ maximalIdeal R) (x : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)),
    (Ideal.quotEquivOfEq ⋯).toAddEquiv (c • x) = c • (Ideal.quotEquivOfEq ⋯).toAddEquiv x

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
this : Module.Free R S
⊢ ∀ (c : R ⧸ maximalIdeal R) (x : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)),
    (Ideal.quotEquivOfEq ⋯).toAddEquiv (c • x) = c • (Ideal.quotEquivOfEq ⋯).toAddEquiv x
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
β : S
hadj : R[β] = ⊤
h : (minpoly R β).Monic
⊢ (aeval ((residue S) β)) (map (residue R) (minpoly R β)) = 0

pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
β : S
hadj : R[β] = ⊤
h : (minpoly R β).Monic
⊢ (map (residue R) (minpoly R β)).natDegree ≤ (minpoly (ResidueField R) ((residue S) β)).natDegree

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
β : S
hadj : R[β] = ⊤
h : (minpoly R β).Monic
⊢ (aeval ((residue S) β)) (map (residue R) (minpoly R β)) = 0
Module: Mathlib.RingTheory.LocalRing.Etale

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
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
β : S
hadj : R[β] = ⊤
h : (minpoly R β).Monic
⊢ (map (residue R) (minpoly R β)).natDegree ≤ (minpoly (ResidueField R) ((residue S) β)).natDegree

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
β : S
hadj : R[β] = ⊤
h : (minpoly R β).Monic
⊢ (map (residue R) (minpoly R β)).natDegree ≤ (minpoly (ResidueField R) ((residue S) β)).natDegree
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
n : ℤ
x : V
m : ℤ
h : m = n
⊢ Ring.choose (m + ↑k) k • ((single (n + ↑k)) x).coeff (m + ↑k) = ((single n) (Ring.choose (n + ↑k) k • x)).coeff m

pp: case neg
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
n : ℤ
x : V
m : ℤ
h : ¬m = n
⊢ Ring.choose (m + ↑k) k • ((single (n + ↑k)) x).coeff (m + ↑k) = ((single n) (Ring.choose (n + ↑k) k • x)).coeff m

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
n : ℤ
x : V
m : ℤ
h : m = n
⊢ Ring.choose (m + ↑k) k • ((single (n + ↑k)) x).coeff (m + ↑k) = ((single n) (Ring.choose (n + ↑k) k • x)).coeff m
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
n : ℤ
x : V
m : ℤ
h : ¬m = n
⊢ Ring.choose (m + ↑k) k • ((single (n + ↑k)) x).coeff (m + ↑k) = ((single n) (Ring.choose (n + ↑k) k • x)).coeff m

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
n : ℤ
x : V
m : ℤ
h : ¬m = n
⊢ Ring.choose (m + ↑k) k • ((single (n + ↑k)) x).coeff (m + ↑k) = ((single n) (Ring.choose (n + ↑k) k • x)).coeff m
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((hasseDeriv R k) ((hasseDeriv R l) f)).coeff n = ((k + l).choose k • ((hasseDeriv R (k + l)) f).coeff) n

Tactic:
simp only [hasseDeriv_coeff, Pi.smul_apply, Nat.cast_add]

Goal state after:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ Ring.choose (n + ↑k) k • Ring.choose (n + ↑k + ↑l) l • f.coeff (n + ↑k + ↑l) =
    (k + l).choose k • Ring.choose (n + (↑k + ↑l)) (k + l) • f.coeff (n + (↑k + ↑l))
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Square

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ maximalIdeal R ^ 2 < maximalIdeal R ↔ ¬maximalIdeal R ^ 2 = maximalIdeal R

pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ ¬maximalIdeal R ^ 2 = maximalIdeal R ↔ ¬IsField R

Tactic:
·

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ maximalIdeal R ^ 2 < maximalIdeal R ↔ ¬maximalIdeal R ^ 2 = maximalIdeal R
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Square

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ ¬maximalIdeal R ^ 2 = maximalIdeal R ↔ ¬IsField R

Tactic:
·

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ ¬maximalIdeal R ^ 2 = maximalIdeal R ↔ ¬IsField R
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
tfae_1_to_2 : ¬IsLocalRing R → Nontrivial (MaximalSpectrum R)
tfae_2_to_3 : Nontrivial (MaximalSpectrum R) → ∃ m₁ m₂, m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂
tfae_3_to_1 : (∃ m₁ m₂, m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂) → ¬IsLocalRing R
⊢ [¬IsLocalRing R, Nontrivial (MaximalSpectrum R), ∃ m₁ m₂, m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂].TFAE

Tactic:
tfae_finish

Goal state after:
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
s : (j : OpenNormalSubgroup G) → (stabilizerHomSurjectiveAuxFunctor P Q σ).obj j
hs : s ∈ (stabilizerHomSurjectiveAuxFunctor P Q σ).sections
a : ↑(ProfiniteGrp.of G).toProfinite.toTop :=
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv) ⟨fun N ↦ ↑↑(s N), ⋯⟩
this : ∀ (N : OpenNormalSubgroup G), ↑a = ↑↑(s N)
⊢ (stabilizerHom Q P G) ⟨a, ⋯⟩ = σ

Tactic:
·

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
s : (j : OpenNormalSubgroup G) → (stabilizerHomSurjectiveAuxFunctor P Q σ).obj j
hs : s ∈ (stabilizerHomSurjectiveAuxFunctor P Q σ).sections
a : ↑(ProfiniteGrp.of G).toProfinite.toTop :=
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv) ⟨fun N ↦ ↑↑(s N), ⋯⟩
this : ∀ (N : OpenNormalSubgroup G), ↑a = ↑↑(s N)
⊢ (stabilizerHom Q P G) ⟨a, ⋯⟩ = σ
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x.powerSeriesPart = 0 → x = 0

pp: case mpr
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x = 0 → x.powerSeriesPart = 0

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x.powerSeriesPart = 0 → x = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x = 0 → x.powerSeriesPart = 0

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x = 0 → x.powerSeriesPart = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x = 0 → x.powerSeriesPart = 0

Tactic:
· rintro rfl
    simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : order x ≤ n
⊢ ((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff n

pp: case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ ((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff n

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : order x ≤ n
⊢ ((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff n
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ ((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff n

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ ((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff n
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ 0 = x.coeff n

pp: case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ n - order x ∉ Set.range ⇑Nat.castOrderEmbedding

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ 0 = x.coeff n
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ n - order x ∉ Set.range ⇑Nat.castOrderEmbedding

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ n - order x ∉ Set.range ⇑Nat.castOrderEmbedding
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (single ↑n) 1 * (single (-↑n)) 1 = 1

pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (single (-↑n)) 1 * (single ↑n) 1 = 1

pp: case refine_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ↑{ val := (single ↑n) 1, inv := (single (-↑n)) 1, val_inv := ?refine_1, inv_val := ?refine_2 } =
    (algebraMap R⟦X⟧ R⸨X⸩) ↑⟨(fun x ↦ PowerSeries.X ^ x) n, ⋯⟩

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (single ↑n) 1 * (single (-↑n)) 1 = 1
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (single (-↑n)) 1 * (single ↑n) 1 = 1

pp: case refine_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ↑{ val := (single ↑n) 1, inv := (single (-↑n)) 1, val_inv := ⋯, inv_val := ?refine_2 } =
    (algebraMap R⟦X⟧ R⸨X⸩) ↑⟨(fun x ↦ PowerSeries.X ^ x) n, ⋯⟩

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (single (-↑n)) 1 * (single ↑n) 1 = 1
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ↑{ val := (single ↑n) 1, inv := (single (-↑n)) 1, val_inv := ⋯, inv_val := ⋯ } =
    (algebraMap R⟦X⟧ R⸨X⸩) ↑⟨(fun x ↦ PowerSeries.X ^ x) n, ⋯⟩

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ↑{ val := (single ↑n) 1, inv := (single (-↑n)) 1, val_inv := ⋯, inv_val := ⋯ } =
    (algebraMap R⟦X⟧ R⸨X⸩) ↑⟨(fun x ↦ PowerSeries.X ^ x) n, ⋯⟩
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
z : R⸨X⸩
h : 0 ≤ order z
⊢ ∃ x, z * (algebraMap R⟦X⟧ R⸨X⸩) ↑x.2 = (algebraMap R⟦X⟧ R⸨X⸩) x.1

pp: case neg
R : Type u_1
inst✝ : CommRing R
z : R⸨X⸩
h : order z < 0
⊢ ∃ x, z * (algebraMap R⟦X⟧ R⸨X⸩) ↑x.2 = (algebraMap R⟦X⟧ R⸨X⸩) x.1

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
z : R⸨X⸩
h : 0 ≤ order z
⊢ ∃ x, z * (algebraMap R⟦X⟧ R⸨X⸩) ↑x.2 = (algebraMap R⟦X⟧ R⸨X⸩) x.1
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
z : R⸨X⸩
h : order z < 0
⊢ ∃ x, z * (algebraMap R⟦X⟧ R⸨X⸩) ↑x.2 = (algebraMap R⟦X⟧ R⸨X⸩) x.1

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
z : R⸨X⸩
h : order z < 0
⊢ ∃ x, z * (algebraMap R⟦X⟧ R⸨X⸩) ↑x.2 = (algebraMap R⟦X⟧ R⸨X⸩) x.1
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case ofNat
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ ((ofPowerSeries ℤ R) f).coeff (Int.ofNat a✝) = if Int.ofNat a✝ < 0 then 0 else (coeff (Int.ofNat a✝).natAbs) f

pp: case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ ((ofPowerSeries ℤ R) f).coeff (Int.negSucc a✝) = if Int.negSucc a✝ < 0 then 0 else (coeff (Int.negSucc a✝).natAbs) f

Tactic:
·

Goal state after:
case ofNat
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ ((ofPowerSeries ℤ R) f).coeff (Int.ofNat a✝) = if Int.ofNat a✝ < 0 then 0 else (coeff (Int.ofNat a✝).natAbs) f
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ ((ofPowerSeries ℤ R) f).coeff (Int.negSucc a✝) = if Int.negSucc a✝ < 0 then 0 else (coeff (Int.negSucc a✝).natAbs) f

Tactic:
·

Goal state after:
case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ ((ofPowerSeries ℤ R) f).coeff (Int.negSucc a✝) = if Int.negSucc a✝ < 0 then 0 else (coeff (Int.negSucc a✝).natAbs) f
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
P : K[X]
hP : P = 0
⊢ (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P

pp: case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P

Tactic:
·

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
P : K[X]
hP : P = 0
⊢ (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
P : K[X]
hP : P = 0
⊢ (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P

pp: case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P

Tactic:
· rw [hP, Valuation.map_zero, Polynomial.coe_zero, Valuation.map_zero]

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ Multiset.count (Ideal.span {Polynomial.X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    Multiset.count (idealX K).asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {↑P}))

Tactic:
convert! (normalized_count_X_eq_of_coe hP).symm

Goal state after:
case e'_2
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ Multiset.count (Ideal.span {Polynomial.X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    Multiset.count Polynomial.X (UniqueFactorizationMonoid.normalizedFactors P)

case e'_3
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ Multiset.count (idealX K).asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {↑P})) =
    Multiset.count X (UniqueFactorizationMonoid.normalizedFactors ↑P)