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

Goal state before:
pp: case pos.refine_2
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
i : (_ : ℕ) × ℕ × ℕ
his : i ∉ (fun x ↦ ⟨x.1 + x.2, x⟩) '' ↑⋯.toFinset
hisc :
  ∀ (j k : ℕ), ⟨j + k, (j, k)⟩ = i → (PowerSeries.coeff k) b • (PowerSeries.coeff j) a • (x ^ j * x ^ k).coeff g = 0
hi : i.fst ∈ image (fun i ↦ i.1 + i.2) ⋯.toFinset ∧ i.snd.1 + i.snd.2 = i.fst
⊢ ((PowerSeries.coeff i.snd.2) b * (PowerSeries.coeff i.snd.1) a) • (x ^ i.fst).coeff g = 0

Tactic:
← hi.2,

Goal state after:
case pos.refine_2
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
i : (_ : ℕ) × ℕ × ℕ
his : i ∉ (fun x ↦ ⟨x.1 + x.2, x⟩) '' ↑⋯.toFinset
hisc :
  ∀ (j k : ℕ), ⟨j + k, (j, k)⟩ = i → (PowerSeries.coeff k) b • (PowerSeries.coeff j) a • (x ^ j * x ^ k).coeff g = 0
hi : i.fst ∈ image (fun i ↦ i.1 + i.2) ⋯.toFinset ∧ i.snd.1 + i.snd.2 = i.fst
⊢ ((PowerSeries.coeff i.snd.2) b * (PowerSeries.coeff i.snd.1) a) • (x ^ (i.snd.1 + i.snd.2)).coeff g = 0
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
a : α
ha : ↑g = (s a).orderTop
hg : ∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g'
hna : ∀ (b : α), b ≠ a → (s b).coeff g = 0
hs : s.hsum ≠ 0
this : ⋯.min ⋯ = g
⊢ s.hsum.leadingCoeff = (s a).coeff g

Tactic:
simp only [leadingCoeff_of_ne_zero hs, coeff_hsum, untop_orderTop_of_ne_zero hs, this]

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
a : α
ha : ↑g = (s a).orderTop
hg : ∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g'
hna : ∀ (b : α), b ≠ a → (s b).coeff g = 0
hs : s.hsum ≠ 0
this : ⋯.min ⋯ = g
⊢ ∑ᶠ (i : α), (s i).coeff g = (s a).coeff g
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ subst (fun x ↦ subst ![PowerSeries.X, 0] F.toPowerSeries) (![PowerSeries.X, 0] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [← PowerSeries.subst_def, PowerSeries.subst_X this]

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

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ subst (fun x ↦ subst ![0, PowerSeries.X] F.toPowerSeries) (![0, PowerSeries.X] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![0, subst ![0, PowerSeries.X] F.toPowerSeries] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [← PowerSeries.subst_def, PowerSeries.subst_X this]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ PowerSeries.subst f (subst ![0, PowerSeries.X] F.toPowerSeries) = f

Tactic:
by
      simp [zeroX_eq_X, PowerSeries.subst_X hf]

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

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
b : β
g : Γ
h : g ∈ (if h : b ∈ Set.range ⇑f then s (Classical.choose h) else 0).support
hb : b ∈ Set.range ⇑f
⊢ g ∈ ⋃ a, (s a).support

Tactic:
rw [dif_pos hb] at h
      exact Set.mem_iUnion.2 ⟨Classical.choose hb, h⟩

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
a : α
⊢ (s.embDomain f) (f a) = s a

Tactic:
rw [embDomain_apply, dif_pos (Set.mem_range_self a)]

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
a : α
⊢ s (Classical.choose ⋯) = s a
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
⊢ maximalIdeal R ≤ ⊥.jacobson

Tactic:
rw [Ideal.jacobson, le_sInf_iff]

Goal state after:
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
⊢ ∀ b ∈ {J | ⊥ ≤ J ∧ J.IsMaximal}, maximalIdeal R ≤ b
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
a : Γ
r : R
hr : r ≠ 0
⊢ ((single a) r)⁻¹ = (single (-a)) r⁻¹

Tactic:
simp [inv_def, hr]

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case refine_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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : ∀ (n : ℕ), c n ≡ a [SMOD I ^ n • ⊤]
n : ℕ
⊢ Polynomial.eval a f ≡ 0 [SMOD I ^ n • ⊤]

Tactic:
specialize ha n

Goal state after:
case refine_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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
n : ℕ
ha : c n ≡ a [SMOD I ^ n • ⊤]
⊢ Polynomial.eval a f ≡ 0 [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case hIN
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → qs n = qs m
⊢ (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
      (map (algebraMap R (Localization.AtPrime q)) q ^ n) ≤
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)) (map f q ^ (n + 1))

Tactic:
refine Submodule.le_of_le_smul_of_le_jacobson_bot (I := I) (IsNoetherian.noetherian _) ?_ ?_

Goal state after:
case hIN.refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → qs n = qs m
⊢ I ≤ ⊥.jacobson

case hIN.refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → qs n = qs m
⊢ (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
      (map (algebraMap R (Localization.AtPrime q)) q ^ n) ≤
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)) (map f q ^ (n + 1)) ⊔
      I •
        (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
          (map (algebraMap R (Localization.AtPrime q)) q ^ n)
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 : Ring.KrullDimLE 1 R
⊢ ringKrullDim R = 1

Tactic:
rw [Ring.krullDimLE_iff] at h

Goal state after:
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
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: case h
P : ProfiniteGrp.{u}
U : Set ↑(limit P.diagram).toProfinite.toTop
s : Set ((j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux P.diagram
uDefaultSpec : spc ∈ s
J : Finset (OpenNormalSubgroup ↑P.toProfinite.toTop)
fJ : (a : OpenNormalSubgroup ↑P.toProfinite.toTop) → Set ↑(P.diagram.obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ spc a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑P.toProfinite.toTop := ⨅ j, ↑(↑j).toOpenSubgroup
hM : M.Normal
hMOpen : IsOpen ↑M
m : OpenNormalSubgroup ↑P.toProfinite.toTop := { toSubgroup := M, isOpen' := hMOpen, isNormal' := ⋯ }
origin : ↑P.toProfinite.toTop
horigin : (QuotientGroup.mk' M) origin = spc m
a : OpenNormalSubgroup ↑P.toProfinite.toTop
a_in_J : a ∈ ↑J
M_to_Na : m ⟶ a := ⋯.hom
⊢ (ConcreteCategory.hom (P.toFiniteQuotientFunctor.map M_to_Na)) (spc m) ∈ fJ a

Tactic:
exact Set.mem_of_eq_of_mem (hspc M_to_Na) (hJ1 a a_in_J).2

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
s : Set R
p : Ideal R
inst✝ : p.IsPrime
hrm : s ⊆ ↑p
⊢ span s ≤ p

Tactic:
rwa [span_le]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : R
reg : IsSMulRegular R x
hx : x ∈ maximalIdeal R
⊢ x ∈ Ring.jacobson R

Tactic:
ringJacobson_eq_maximalIdeal R

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : R
reg : IsSMulRegular R x
hx : x ∈ maximalIdeal R
⊢ x ∈ maximalIdeal R
Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
⊢ Injective Rₛ Mₛ

Tactic:
by
  have MB : Baer R M := Baer.of_injective ‹_›
  simp only [← Baer.iff_injective, Module.Baer.iff_surjective] at MB ⊢
  intro Iₛ g
  obtain ⟨I, rfl⟩ : ∃ I, .localized' Rₛ S (Algebra.linearMap R Rₛ) I = Iₛ :=
    ⟨Iₛ.comap (algebraMap R Rₛ), by simp [Ideal.localized'_eq_map, IsLocalization.map_under S]⟩
  have : FinitePresentation R I := finitePresentation_of_finite R I
  obtain ⟨⟨g', a⟩, e : a.1 • g = _⟩ := surj S (mapExtendScalars S (I.toLocalized' _ _ _) f Rₛ) g
  obtain ⟨g', rfl⟩ := MB I g'
  refine ⟨IsLocalization.mk' Rₛ 1 a • mapExtendScalars S (Algebra.linearMap _ _) f _ g', ?_⟩
  apply ((Module.End.isUnit_iff _).mp ((IsLocalization.map_units Rₛ a).map
    (algebraMap _ (Module.End Rₛ _)))).1
  simp_rw [algebraMap_end_apply, map_smul, ← mul_smul, algebraMap_smul, IsLocalization.mk'_spec', e]
  apply LinearMap.restrictScalars_injective R
  refine IsLocalizedModule.linearMap_ext S (I.toLocalized' Rₛ S (Algebra.linearMap R Rₛ)) f ?_
  ext
  simp [-Algebra.linearMap_apply]

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

Goal state before:
pp: case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization S)
n : ℕ
ih : ∀ (M : ModuleCat R) [HasInjectiveDimensionLE M n], HasInjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat R
inst✝ : HasInjectiveDimensionLE M (n + 1)
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)

Tactic:
have ei : EnoughInjectives (ModuleCat.{v} R) := inferInstance

Goal state after:
case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization S)
n : ℕ
ih : ∀ (M : ModuleCat R) [HasInjectiveDimensionLE M n], HasInjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat R
inst✝ : HasInjectiveDimensionLE M (n + 1)
ei : EnoughInjectives (ModuleCat R)
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
⊢ HasInjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)

Tactic:
have ei : EnoughInjectives (ModuleCat.{v} R) := inferInstance

Goal state after:
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
ei : EnoughInjectives (ModuleCat R)
⊢ HasInjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: 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β_gen : Function.Surjective ⇑(aeval β)
p : R[X]
⊢ (aeval ((residue S) β)) (map (residue R) p) = (residue S) ((aeval β) p)

Tactic:
by
      rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl p β]

Goal state after:
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:
· contrapose!
    simp only [ne_eq]
    intro h
    rw [PowerSeries.ext_iff, not_forall]
    use 0
    simpa

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 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)

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
hDs : 0 < D - ↑s
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-D + ↑s)

Tactic:
· apply le_trans ((PowerSeries.idealX K).valuation_le_one F)
        rw [← log_le_iff_le_exp one_ne_zero, log_one]
        lia

Goal state after:
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.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : d i = 1
disjoint : (↑f.support).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀) (coeff d f)
ψ : MvPolynomial n R := f - φ * X i
hf : f = φ * X i + ψ
hφ : φ * X i = (monomial d) (coeff d f)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
q : MvPolynomial n R
m : n →₀ ℕ
b : R
hm : m ≤ d₀
hb : b ∣ coeff d f
hpφ : (monomial m) b ∣ φ
hq : ψ = (monomial m) b * q
d₂ : n →₀ ℕ
hd₂ : d₂ ∈ f.support
H : d₂ ≠ d
aux : m ≤ d₂ ∧ ¬b * coeff (d₂ - m) q = 0
⊢ m = 0

Tactic:
simpa using disjoint hd₂ hd H (Finsupp.support_mono aux.1)
        ((Finsupp.support_mono hm).trans (d.support.erase_subset i))

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

Goal state before:
pp: case right.inl
R : Type u_3
inst✝ : CommRing R
n : ℕ
hp : 0 ∈ symmetricSubalgebra (Fin n) R
⊢ ⟨0, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range

Tactic:
exact Subalgebra.zero_mem _

Goal state after:
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
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
h : ∀ (i : σ), p ∣ d i
⊢ p • Finsupp.mapRange (fun a ↦ a / p) ⋯ d = d

Tactic:
by ext i; simp [(Nat.mul_div_cancel' (h i))]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
⊢ (coeff n) ((expand p hp) ↑φ) = MvPolynomial.coeff n ((MvPolynomial.expand p) φ)

Tactic:
by_cases! h : ∀ i, p ∣ n i

Goal state after:
case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ n i
⊢ (coeff n) ((expand p hp) ↑φ) = MvPolynomial.coeff n ((MvPolynomial.expand p) φ)

case neg
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∃ i, ¬p ∣ n i
⊢ (coeff n) ((expand p hp) ↑φ) = MvPolynomial.coeff n ((MvPolynomial.expand p) φ)
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ n i
⊢ p • Finsupp.mapRange (fun a ↦ a / p) ⋯ n = n

Tactic:
by ext i; simp [(Nat.mul_div_cancel' (h i))]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
⊢ p • Finsupp.mapRange (fun a ↦ a / p) ⋯ d = d

Tactic:
by ext i; simp [(Nat.mul_div_cancel' (h i))]

Goal state after:
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
i✝ : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
v : ι → ↑X
i : ι
⊢ r • (ModuleCat.Hom.hom f) (v i) =
    ((algebraMap R₀ (Matrix ι ι R)) r • (LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f)) v) i

Tactic:
simp [Matrix.algebraMap_matrix_apply]

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

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
⊢ psum σ R k =
    (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ antidiagonal k with a.1 ∈ Set.Ioo 0 k, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2

Tactic:
by
  simp only [Set.Ioo, Set.mem_ofPred_eq, and_comm]
  have hesymm := mul_esymm_eq_sum σ R k
  rw [← (sum_filter_add_sum_filter_not {a ∈ antidiagonal k | a.fst < k}
    (fun a ↦ 0 < a.fst) (fun a ↦ (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd))] at hesymm
  have sub_both_sides := congrArg (· - (-1 : MvPolynomial σ R) ^ (k + 1) *
    ∑ a ∈ {a ∈ antidiagonal k | a.fst < k} with 0 < a.fst,
    (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd) hesymm
  simp only [left_distrib, add_sub_cancel_left] at sub_both_sides
  have sub_both_sides := congrArg ((-1 : MvPolynomial σ R) ^ (k + 1) * ·) sub_both_sides
  simp only [mul_sub_left_distrib, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k + 1, rfl⟩, one_mul,
    filter_filter (fun a : ℕ × ℕ ↦ a.fst < k) (fun a ↦ ¬0 < a.fst)]
    at sub_both_sides
  have : {a ∈ antidiagonal k | a.fst < k ∧ ¬0 < a.fst} = {(0, k)} := by
    ext a
    rw [mem_filter, mem_antidiagonal, mem_singleton]
    refine ⟨?_, by rintro rfl; lia⟩
    rintro ⟨ha, ⟨_, ha0⟩⟩
    rw [← ha, Nat.eq_zero_of_not_pos ha0, zero_add, ← Nat.eq_zero_of_not_pos ha0]
  rw [this, sum_singleton] at sub_both_sides
  simp only [_root_.pow_zero, esymm_zero, mul_one, one_mul, filter_filter] at sub_both_sides
  exact sub_both_sides.symm

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
this : g.symm.toRingEquiv.toRingHom.comp ↑g = RingHom.id (MvPolynomial (Fin (n + 1)) k)
⊢ Ideal.map (T f) I = Ideal.map (↑(T f)) I

Tactic:
Ideal.map_coe

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
this : g.symm.toRingEquiv.toRingHom.comp ↑g = RingHom.id (MvPolynomial (Fin (n + 1)) k)
⊢ Ideal.map (T f) I = Ideal.map (T f) I
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
⊢ Ideal.map (T f).symm.toRingEquiv.toRingHom (Ideal.map (T f) I) = Ideal.map (↑(T f).symm) (Ideal.map (T f) I)

Tactic:
Ideal.map_coe

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
⊢ Ideal.map (T f).symm.toRingEquiv.toRingHom (Ideal.map (T f) I) = Ideal.map (T f).symm (Ideal.map (T f) I)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_1.le_succ_of_le
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m k✝ : ℕ
hle : n ≤ k✝
xk : R
⊢ R

Tactic:
choose x hx using h xk

Goal state after:
case refine_1.le_succ_of_le
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x✝ : R
m k✝ : ℕ
hle : n ≤ k✝
xk x : R
hx : (frobenius R p) x = xk
⊢ R