mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ y ∈ s, y ≠ x → c y = 0
⊢ (x, x) ∈ s ×ˢ s

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[G] →ₐc[R] R[H]
g₁ g₂ : G
⊢ mapDomainOfBialgHomFun f (g₁ * g₂) = mapDomainOfBialgHomFun f g₁ * mapDomainOfBialgHomFun f g₂

Tactic:
refine single_left_injective (R := R) one_ne_zero ?_
    simp only [single_mapDomainOfBialgHomFun_one]
    rw [← mul_one (1 : R), ← single_mul_single, ← single_mul_single, map_mul]
    simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case h
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
e : ↥T → ℕ
g : ↥T → ↥S
hg : ∀ (a : ↥T), g a • ↑a ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * ↑(∏ a, g a)) • m = 0
⊢ 0 ∈ ⊥

Tactic:
mem_bot

Goal state after:
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
r : R
rs : List R
⊢ map (r • ⊤).mkQ (Ideal.ofList rs • ⊤) = Ideal.ofList rs • ⊤

Tactic:
by rw [map_smul'', map_top, range_mkQ]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case pos
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ ha : a ∈ I
⊢ hI'.dpow n a = hI.dpow n a

pp: case neg
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ : a ∈ I
ha : a ∉ I
⊢ hI'.dpow n a = hI.dpow n a

Tactic:
· refine hI.dpow_comp_from_gens hI' (f := RingHom.id A) hS ?_ ?_ a ha
    · intro s hs
      simp only [RingHom.id_apply, hS]
      exact subset_span hs
    · intro m b hb
      simpa only [RingHom.id_apply] using (hdp b hb)

Goal state after:
case neg
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ : a ∈ I
ha : a ∉ I
⊢ hI'.dpow n a = hI.dpow n a
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ torsionBy R M b = a • ⊤ ⊓ torsionBy R M b

Tactic:
rw [← (isSMulRegular_on_quot_iff_lsmul_comap_eq _ _).mp hb]

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ torsionBy R M b = comap ((lsmul R M) b) (a • ⊤) ⊓ torsionBy R M b
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S
hSI : span S ≤ I
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ {j : A}, j ∈ span S → hI.dpow n j ∈ span S

Tactic:
intro m hm z hz

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S
hSI : span S ≤ I
m : ℕ
hm : m ≠ 0
z : A
hz : z ∈ span S
⊢ hI.dpow m z ∈ span S
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x✝ : ℕ
hn : x✝ ≠ 0
x : A
hx : x ∈ ⊥
⊢ 0 ∈ ⊥

Tactic:
mem_bot

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x✝ : ℕ
hn : x✝ ≠ 0
x : A
hx : x ∈ ⊥
⊢ 0 = 0
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⨅ s ∈ insert ⊤ S, s.carrier = I ⊓ sInf (val '' Set.range fun a ↦ ⨅ (_ : a ∈ S), ⟨a.carrier, ⋯⟩)

Tactic:
sInf_image,

Goal state after:
case refine_2
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⨅ s ∈ insert ⊤ S, s.carrier = I ⊓ ⨅ a ∈ Set.range fun a ↦ ⨅ (_ : a ∈ S), ⟨a.carrier, ⋯⟩, ↑a
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R✝ : Type u
S✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
inst✝³ : Algebra R✝ S✝
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (IsScalarTower.toAlgHom P.Ring (Generators.self P.Ring S).toExtension.Ring S).comp
      (ofId P.Ring (Generators.self P.Ring S).toExtension.Ring) =
    (IsScalarTower.toAlgHom P.Ring S S).comp (IsScalarTower.toAlgHom P.Ring P.extendScalars.Ring S)

Tactic:
by ext

Goal state after:
Module: Mathlib.RingTheory.Flat.LocallyFree

Goal state before:
pp: case inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
h✝ : Subsingleton R
⊢ ∃ a ∉ p, Free (Localization.Away a) (LocalizedModule.Away a M)

Tactic:
use 1, Ideal.IsPrime.one_notMem ‹_›

Goal state after:
case right
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
h✝ : Subsingleton R
⊢ Free (Localization.Away 1) (LocalizedModule.Away 1 M)
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ∑ᶠ (n : ℕ), ((powerSeriesFamily x f).coeff 0) n = constantCoeff f

Tactic:
finsum_eq_single (fun n => ((powerSeriesFamily x f).coeff 0) n) 0,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ((powerSeriesFamily x f).coeff 0) 0 = constantCoeff f

Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ∀ (x_1 : ℕ), x_1 ≠ 0 → ((powerSeriesFamily x f).coeff 0) x_1 = 0
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
g : Γ
⊢ (s.mul t).hsum.coeff g = ∑ x ∈ antidiagonal ⋯ ⋯ g, s.hsum.coeff x.1 • t.hsum.coeff x.2

Tactic:
mul_eq_smul

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
g : Γ
⊢ (s.smul t).hsum.coeff g = ∑ x ∈ antidiagonal ⋯ ⋯ g, s.hsum.coeff x.1 • t.hsum.coeff x.2
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
⊢ (s.mul t).hsum = s.hsum • t.hsum

Tactic:
mul_eq_smul

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
⊢ (s.smul t).hsum = s.hsum • t.hsum
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
⊢ {a | ((fun n ↦ x ^ n) a).coeff g ≠ 0}.Finite

Tactic:
by_cases h0 : x = 0

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : x = 0
⊢ {a | ((fun n ↦ x ^ n) a).coeff g ≠ 0}.Finite

case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
⊢ {a | ((fun n ↦ x ^ n) a).coeff g ≠ 0}.Finite
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∑ a ∈ Finset.range (((taylor (c n)) f).natDegree + 2),
      ((taylor (c n)) f).coeff a * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ a ∈
    I ^ (n + 1 + 1)

pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∀ (n_1 : ℕ), 0 * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ n_1 = 0

Tactic:
←
          Finset.sum_range_add_sum_Ico _ (Nat.le_add_left _ _)

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∑ k ∈ Finset.range 2, ((taylor (c n)) f).coeff k * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k +
      ∑ k ∈ Finset.Ico 2 (((taylor (c n)) f).natDegree + 2),
        ((taylor (c n)) f).coeff k * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k ∈
    I ^ (n + 1 + 1)

R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∀ (n_1 : ℕ), 0 * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ n_1 = 0
Module: Mathlib.Topology.Algebra.ClopenNhdofOne

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : g ∈ sInf {N | IsOpen ↑N ∧ ↑H ≤ N}
hg_not : g ∉ ↑H
U : Set G := (g • ↑H)ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : ↑N ⊆ U
NH : Subgroup G := ↑N.toOpenSubgroup ⊔ ↑H
⊢ g ∉ NH

Tactic:
by_contra hg'

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : g ∈ sInf {N | IsOpen ↑N ∧ ↑H ≤ N}
hg_not : g ∉ ↑H
U : Set G := (g • ↑H)ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : ↑N ⊆ U
NH : Subgroup G := ↑N.toOpenSubgroup ⊔ ↑H
hg' : g ∈ NH
⊢ False
Module: Mathlib.RingTheory.KrullDimension.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
x✝ : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
hn : ¬IsField R
h✝ : ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
this : ¬ringKrullDim R ≤ 0
h : ringKrullDim R ≤ ↑1
⊢ ringKrullDim R = 1

Tactic:
exact le_antisymm h (Order.succ_le_of_lt (lt_of_not_ge this))

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
⊢ IsClosed (support R M)

Tactic:
support_eq_zeroLocus

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
⊢ IsClosed (PrimeSpectrum.zeroLocus ↑(annihilator R M))
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
⊢ p.height ≤ (map (Quotient.mk I) p).height + ↑(Submodule.spanFinrank I)

Tactic:
have : Set.SurjOn (Ideal.Quotient.mk I) p s := by
    refine Set.SurjOn.mono subset_rfl hsp' fun x hx ↦ ?_
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    exact ⟨x, by simpa [hrp, sup_of_le_left, p'] using hx⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this✝ : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
⊢ p.height ≤ (map (Quotient.mk I) p).height + ↑(Submodule.spanFinrank I)
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: case of_equiv
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
ι : Type u_2
inst✝ : Finite ι
α✝ β✝ : Type u_2
e : α✝ ≃ β✝
H : ringKrullDim (MvPolynomial α✝ R) = ringKrullDim R + ↑(Nat.card α✝)
⊢ ringKrullDim (MvPolynomial β✝ R) = ringKrullDim R + ↑(Nat.card β✝)

Tactic:
convert! ← H using 1
    · exact ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv
    · rw [Nat.card_congr e]

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
h : x ∈ (annihilator R M).jacobson
a✝ : Nontrivial M
p : LTSeries ↑(support R M)
this :
  ∀ (p : LTSeries ↑(support R M)), x ∈ (↑(RelSeries.last p)).asIdeal → ↑p.length ≤ supportDim R (QuotSMulTop x M) + 1
hxp : x ∉ (↑(RelSeries.last p)).asIdeal
⊢ ↑p.length ≤ supportDim R (QuotSMulTop x M) + 1

pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
h : x ∈ (annihilator R M).jacobson
a✝ : Nontrivial M
p : LTSeries ↑(support R M)
hxp : x ∈ (↑(RelSeries.last p)).asIdeal
⊢ ↑p.length ≤ supportDim R (QuotSMulTop x M) + 1

Tactic:
· obtain ⟨p, hle, hm⟩ := exists_ltSeries_support_isMaximal_last_of_ltSeries_support p
    have hj : (annihilator R M).jacobson ≤ p.last.1.1 :=
      sInf_le ⟨mem_support_iff_of_finite.mp p.last.2, inferInstance⟩
    exact (Nat.cast_le.mpr hle).trans <| this _ (hj h)

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
h : x ∈ (annihilator R M).jacobson
a✝ : Nontrivial M
p : LTSeries ↑(support R M)
hxp : x ∈ (↑(RelSeries.last p)).asIdeal
⊢ ↑p.length ≤ supportDim R (QuotSMulTop x M) + 1
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
⊢ False

Tactic:
Int.dvd_add_left this

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
⊢ False
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⸨X⸩
hn : ↑n = order f
⊢ (ofPowerSeries ℤ R) (PowerSeries.X ^ n * f.powerSeriesPart) = f

Tactic:
simp only [map_mul, map_pow, ofPowerSeries_X, single_pow, nsmul_eq_mul, mul_one, one_pow, hn,
    single_order_mul_powerSeriesPart]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case ofNat
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ Valued.v ((single ↑s) 1) = exp (-↑s)

Tactic:
← HahnSeries.ofPowerSeries_X_pow,

Goal state after:
case ofNat
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ Valued.v ((ofPowerSeries ℤ K) (PowerSeries.X ^ s)) = exp (-↑s)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case negSucc
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ Valued.v ((single ↑s.succ) 1) = (exp ↑s.succ)⁻¹

Tactic:
← HahnSeries.ofPowerSeries_X_pow,

Goal state after:
case negSucc
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ Valued.v ((ofPowerSeries ℤ K) (PowerSeries.X ^ s.succ)) = (exp ↑s.succ)⁻¹
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = ↑s
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-D + ↑s)

Tactic:
by_cases! hDs : D - s ≤ 0

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = ↑s
hDs : D - ↑s ≤ 0
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-D + ↑s)

case neg
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = ↑s
hDs : 0 < D - ↑s
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-D + ↑s)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ

Tactic:
obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (Int.neg_nonpos_of_nonneg ord_nonpos)
    obtain ⟨P, hP⟩ := exists_Polynomial_intValuation_lt (PowerSeries.X ^ s * F) γ
    use P
    rw [← X_order_mul_powerSeriesPart (neg_inj.1 hs).symm, ← RatFunc.coe_coe,
      ← PowerSeries.coe_sub, ← coe_algebraMap, adicValued_apply, valuation_of_algebraMap]
    exact hP

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case right.inr.ind
R : Type u_3
inst✝ : CommRing R
n : ℕ
t : Lex (Fin n →₀ ℕ)
ih :
  ∀ y < t,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
he : supDegree (⇑toLex) p = t
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range

Tactic:
| _ t ih
   => 

Goal state after:
case right.inr.ind
R : Type u_3
inst✝ : CommRing R
n : ℕ
t : Lex (Fin n →₀ ℕ)
ih :
  ∀ y < t,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
he : supDegree (⇑toLex) p = t
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range