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

Goal state before:
pp: k : Type u_1
R : Type u_2
inst✝⁴ : Field k
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsFiniteSplit k R
p : Ideal R
inst✝ : p.IsPrime
⊢ Function.Bijective ⇑(algebraMap k (R ⧸ p))

Tactic:
obtain ⟨n, ⟨e⟩⟩ := nonempty_algEquiv_fun k R
  let p' : Ideal (Fin n → k) := p.comap e.symm
  obtain ⟨i, q, hq⟩ := PrimeSpectrum.exists_comap_evalRingHom_eq ⟨p', inferInstance⟩
  obtain rfl : q = ⊥ := Subsingleton.elim _ _
  let g : (R ⧸ p) ≃ₐ[k] k :=
    (quotientEquivAlg _ p' e <| comap_symm e.toRingEquiv).trans <|
    (quotientEquivAlgOfEq k congr($(hq).asIdeal).symm).trans <|
    quotientKerAlgEquivOfSurjective (f := Pi.evalAlgHom k (fun _ ↦ k) i)
      (Function.surjective_eval _)
  simpa [← g.symm.toAlgHom.comp_algebraMap] using g.symm.bijective

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: case h
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Subsingleton R
this : IsFiniteSplit R S
⊢ IsFiniteSplit R (R ⊗[R] S)

Tactic:
exact .of_algEquiv (TensorProduct.lid R S).symm

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst✝¹² : DecidableEq ι
inst✝¹¹ : AddMonoid ι
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : 𝒜 →ₐᵍ[R] fun x ↦ Submodule.restrictScalars R (ℬ x)
i✝ : ι
x : S ⊗[R] ↥(𝒜 i✝)
hx : ↑((toBaseChange S (𝒜 i✝)) x) ∈ baseChange S (𝒜 i✝)
⊢ ((AlgHom.liftEquiv R S A B) ↑f).toRingHom ↑((toBaseChange S (𝒜 i✝)) x) ∈ ℬ i✝

Tactic:
induction x with
        | zero => simp
        | add => simp_all [add_mem]
        | tmul r x => simpa using smul_mem _ _ <| by exact f.map_mem x.2

Goal state after:
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
this :
  ∀ (g₁ g₂ : MvPowerSeries (Fin 3) R),
    ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] = fun i ↦ (MvPowerSeries.map f) (![g₁, g₂] i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← map_subst .X_X,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
this :
  ∀ (g₁ g₂ : MvPowerSeries (Fin 3) R),
    ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] = fun i ↦ (MvPowerSeries.map f) (![g₁, g₂] i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case refine_2
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal g ⋯
hgh : gh ∉ (fun a ↦ a) '' ↑(VAddAntidiagonal g ⋯)
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

Tactic:
· simp only [Set.image_id', mem_coe, mem_vaddAntidiagonal, mem_support, ne_eq, not_and] at hgh
    by_cases h : s.hsum.coeff gh.1 = 0
    · exact smul_eq_zero_of_left h (t.hsum.coeff gh.2)
    · simp_all

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f g : R⟦σ →₀ ℕ⟧
⊢ (f * g).coeff = f.coeff * g.coeff

Tactic:
ext n
    classical
      change (f * g).coeff n = _
      simp_rw [coeff_mul]
      refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
        sum_filter_ne_zero _
      ext m
      simp only [and_congr_left_iff, Finset.mem_antidiagonal, mem_filter, mem_support,
        HasAntidiagonal.mem_antidiagonal]
      rintro h
      rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv (antipode R) * toConv LinearMap.id).ofConv ∘ₗ f.toLinearMap =
    (toConv (f.toLinearMap ∘ₗ antipode R) * toConv f.toLinearMap).ofConv

Tactic:
rw [convMul_comp_coalgHom_distrib, hS]; rfl

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv LinearMap.id * toConv (antipode R)).ofConv ∘ₗ f.toLinearMap =
    (toConv f.toLinearMap * toConv (f.toLinearMap ∘ₗ antipode R)).ofConv

Tactic:
rw [convMul_comp_coalgHom_distrib, hS]; rfl

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
⊢ c m ≡ c (m + k) [SMOD I ^ m]

Tactic:
induction k with

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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : c m ≡ c (m + k) [SMOD I ^ m]
⊢ c m ≡ c (m + (k + 1)) [SMOD I ^ m]
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
⊢ a = b

Tactic:
by
  obtain ⟨c, _⟩ := exists_mul_sq_add_linear_part_eq_eval_add f a (b - a)
  have hc : (c * (b - a) + eval a (derivative f)) * (b - a) = 0 := by grind
  suffices (c * (b - a) + eval a (derivative f)) ∉ maximalIdeal R by
    rw [notMem_maximalIdeal, isUnit_iff_exists] at this
    grind
  by_contra!
  replace this := (maximalIdeal R).add_mem this ((maximalIdeal R).mul_mem_left c h)
  ring_nf at this
  contradiction

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Finset R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
hn : s.card ≤ n + 1
w✝ : IsLocalRing R
hp : maximalIdeal R ∈ (span ↑s).minimalPrimes
this : (maximalIdeal R).IsPrime
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
⊢ ∃ x s', x ∉ s' ∧ s = insert x s' ∧ x ∉ q

Tactic:
have : ¬(s : Set R) ⊆ q := by
          rw [← span_le]
          exact fun e ↦ lt_irrefl _ ((hp.2 ⟨hq, e⟩ hpq.le).trans_lt hpq)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Finset R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
hn : s.card ≤ n + 1
w✝ : IsLocalRing R
hp : maximalIdeal R ∈ (span ↑s).minimalPrimes
this✝ : (maximalIdeal R).IsPrime
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
this : ¬↑s ⊆ ↑q
⊢ ∃ x s', x ∉ s' ∧ s = insert x s' ∧ x ∉ q
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
⊢ ↑I.height ≤ Submodule.spanRank I

Tactic:
by
  trans ↑I.spanRank.toENat
  · exact_mod_cast I.height_le_spanRank_toENat hI
  · exact I.spanRank.ofENat_toENat_le

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
q : LTSeries ↑(support R M)
m : Ideal R
hmm : m.IsMaximal
hm : (↑(RelSeries.last q)).asIdeal ≤ m
hlt : (↑(RelSeries.last q)).asIdeal < m
⊢ ∃ p, q.length ≤ p.length ∧ (↑(RelSeries.last p)).asIdeal.IsMaximal

Tactic:
use q.snoc ⟨⟨m, inferInstance⟩, mem_support_mono hm q.last.2⟩ hlt

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
q : LTSeries ↑(support R M)
m : Ideal R
hmm : m.IsMaximal
hm : (↑(RelSeries.last q)).asIdeal ≤ m
hlt : (↑(RelSeries.last q)).asIdeal < m
⊢ q.length ≤ (RelSeries.snoc q ⟨{ asIdeal := m, isPrime := ⋯ }, ⋯⟩ hlt).length ∧
    (↑(RelSeries.snoc q ⟨{ asIdeal := m, isPrime := ⋯ }, ⋯⟩ hlt).last).asIdeal.IsMaximal
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
q : Submodule R M
hqt : q ∈ ↑t
x : M
hxt : x ∈ (t.erase q).inf id
hxq : x ∉ q
⊢ (fun J ↦ (J.colon Set.univ).radical) q ∈ N.associatedPrimes

Tactic:
use (ht.primary hqt).isPrime_radical_colon, x

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
q : Submodule R M
hqt : q ∈ ↑t
x : M
hxt : x ∈ (t.erase q).inf id
hxq : x ∉ q
⊢ (fun J ↦ (J.colon Set.univ).radical) q = (N.colon {x}).radical
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro.mk
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
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
b : ↥Zx
hb : ↑b ∉ Zx
⊢ False

Tactic:
exact hb b.2

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
M : ModuleCat R
⊢ injectiveDimension (M.localizedModule S) ≤ injectiveDimension M

Tactic:
have aux (n : ℕ) : injectiveDimension M ≤ n → injectiveDimension (M.localizedModule S) ≤ n := by
    simp only [injectiveDimension_le_iff]
    intro h
    exact M.localizedModule_hasInjectiveDimensionLE n S
  refine le_of_forall_ge (fun N ↦ ?_)
  induction N with
  | bot =>
    simp only [le_bot_iff, injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    intro _
    apply LocalizedModule.instSubsingleton _
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R✝ : Type u_1
R : Type u_2
V : Type u_3
inst✝² : AddCommGroup V
inst✝¹ : Semiring R
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
x : ℤ
h : x ∈ Function.support fun n ↦ Ring.choose (n + ↑k) k • f.coeff (n + ↑k)
⊢ order f - ↑k ≤ x

Tactic:
contrapose! h

Goal state after:
R✝ : Type u_1
R : Type u_2
V : Type u_3
inst✝² : AddCommGroup V
inst✝¹ : Semiring R
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
x : ℤ
h : x < order f - ↑k
⊢ x ∉ Function.support fun n ↦ Ring.choose (n + ↑k) k • f.coeff (n + ↑k)
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

Tactic:
contrapose! h

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

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
inst✝¹⁴ : p.IsPrime
Rₚ : Type u_3
inst✝¹³ : CommRing Rₚ
inst✝¹² : Algebra R Rₚ
inst✝¹¹ : IsLocalization.AtPrime Rₚ p
inst✝¹⁰ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra S Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝⁵ : Algebra R Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
inst✝² : p.IsMaximal
inst✝¹ : P.IsMaximal
inst✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
⊢ (maximalIdeal Rₚ).inertiaDeg' (Ideal.map (algebraMap S Sₚ) P) = p.inertiaDeg' P

Tactic:
rw [inertiaDeg'_algebraMap, inertiaDeg'_algebraMap]
  refine Algebra.finrank_eq_of_equiv_equiv (equivQuotMaximalIdeal p Rₚ).symm
    (equivQuotientMapOfIsMaximal p Sₚ P).symm ?_
  ext x
  exact algebraMap_equivQuotMaximalIdeal_symm_apply p Rₚ Sₚ P x

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

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
inst✝¹² : p.IsPrime
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
⊢ (Ideal.map (algebraMap S Sₚ) P).ramificationIdx Rₚ = P.ramificationIdx R

Tactic:
rw [ramificationIdx_eq (maximalIdeal Rₚ) (P.map (algebraMap S Sₚ)), ramificationIdx_eq p P]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsPrime
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
⊢ (length (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))
        (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P) ⧸
          Ideal.map (algebraMap Rₚ (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))) (maximalIdeal Rₚ))).toNat =
    (length (Localization.AtPrime P)
        (Localization.AtPrime P ⧸ Ideal.map (algebraMap R (Localization.AtPrime P)) p)).toNat
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.refine_1
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
x : K⸨X⸩
hx : Valued.v x = ↑γ
this : Valued.v.restrict x ≠ 0
⊢ {P |
      Valued.v.restrict (P.2 - P.1) <
        (MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x} ∈
    uniformity K⸨X⸩

Tactic:
exact (Valued.hasBasis_uniformity K⸨X⸩ ℤᵐ⁰).mem_of_mem
      (i := Units.mk0 (Valued.v.restrict x) this) (by tauto)

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
⊢ UniformContinuous fun f ↦ f.coeff d

Tactic:
by
  refine uniformContinuous_iff_eventually.mpr fun S hS ↦ eventually_iff_exists_mem.mpr ?_
  let γ : (ℤᵐ⁰)ˣ := Units.mk0 (exp (-(d + 1))) coe_ne_zero
  use {P | Valued.v (P.snd - P.fst) < ↑γ}
  refine ⟨?_, fun _ hP ↦ ?_⟩
  · obtain ⟨x, hx⟩ := LaurentSeries.valuation_surjective K γ
    have : Valued.v.restrict x ≠ 0 := fun h ↦ NeZero.ne γ.1 <|
      hx ▸ MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff.1 h
    rw [← hx]
    nth_rw 2 [← Valuation.coe_ofClass]
    rw [← MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀]
    simp_rw [← Valued.v.restrict_lt_iff_lt_embedding]
    exact (Valued.hasBasis_uniformity K⸨X⸩ ℤᵐ⁰).mem_of_mem
      (i := Units.mk0 (Valued.v.restrict x) this) (by tauto)
  · simpa [eq_coeff_of_valuation_sub_lt K hP.le (lt_add_one _)] using mem_uniformity_of_eq hS rfl

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

Goal state before:
pp: R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
⊢ supDegree (⇑toLex) (esymm (Fin m) R (i + 1)) = toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x_1 ↦ 1) ∧
    Monic (⇑toLex) (esymm (Fin m) R (i + 1))

Tactic:
have := supDegree_leadingCoeff_sum_eq (D := toLex) (s := univ.powersetCard (i + 1))
    (i := Iic (⟨i, him⟩ : Fin m)) ?_ (f := fun s ↦ monomial (∑ j ∈ s, fun₀ | j => 1) (1 : R)) ?_

Goal state after:
case refine_3
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
this :
  supDegree (⇑toLex) (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1)) 1) =
      supDegree (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 1)) 1) ∧
    leadingCoeff (⇑toLex) (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1)) 1) =
      leadingCoeff (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 1)) 1)
⊢ supDegree (⇑toLex) (esymm (Fin m) R (i + 1)) = toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x_1 ↦ 1) ∧
    Monic (⇑toLex) (esymm (Fin m) R (i + 1))

case refine_1
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
⊢ Iic ⟨i, him⟩ ∈ powersetCard (i + 1) univ

case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
⊢ ∀ j ∈ powersetCard (i + 1) univ,
    j ≠ Iic ⟨i, him⟩ →
      supDegree (⇑toLex) ((monomial (∑ j ∈ j, fun₀ | j => 1)) 1) <
        supDegree (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 1)) 1)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : 1 < η
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

pp: case neg
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : η ≤ 1
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

Tactic:
· use 0
    simpa using (intValuation_le_one (PowerSeries.idealX K) F).trans_lt h_neg

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : η ≤ 1
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : unzero ⋯ ≤ 1
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

Tactic:
← Multiplicative.toAdd_le,

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ Multiplicative.toAdd 1
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
⊢ Irreducible (sumSMulXSMulY c)

Tactic:
let ι : n ↪ ((n ⊕ n) →₀ ℕ) :=
    ⟨fun i ↦ .single (.inl i) 1 + .single (.inr i) 1,
     fun i j ↦ by simp +contextual [Finsupp.ext_iff, Finsupp.single_apply, ite_eq_iff']⟩

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
⊢ Irreducible (sumSMulXSMulY c)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
hp : IsSymmetric 0
⊢ Antitone ⇑(ofLex ⊥)

Tactic:
bot_eq_zero (α := Lex (σ →₀ ℕ))

Goal state after:
case inl
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
hp : IsSymmetric 0
⊢ Antitone ⇑(ofLex 0)
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ m i
⊢ (coeff m) ((expand p hp) φ) = 0

Tactic:
contrapose! h

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : (coeff m) ((expand p hp) φ) ≠ 0
⊢ p ∣ m i
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* N
r : M
n : ℕ
⊢ f (((powMulEquiv M p).trans (powMulEquiv M p ^ n)).symm r ^ p) = (fun n ↦ f ((powMulEquiv M (p ^ n)).symm r)) n

Tactic:
MulEquiv.symm_trans_apply,

Goal state after:
M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* N
r : M
n : ℕ
⊢ f ((powMulEquiv M p).symm ((powMulEquiv M p ^ n).symm r) ^ p) = (fun n ↦ f ((powMulEquiv M (p ^ n)).symm r)) n