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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Nontrivial R₁
inst✝ : Nontrivial R₂
h : IsUnit (1, 0)
⊢ IsUnit 0

Tactic:
simpa using

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Nontrivial R₁
inst✝ : Nontrivial R₂
h : IsUnit (1, 0)
⊢ False
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Nontrivial R₁
inst✝ : Nontrivial R₂
ha : ¬IsUnit (1, 0)
h : IsUnit (0, 1)
⊢ IsUnit 0

Tactic:
simpa using

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Nontrivial R₁
inst✝ : Nontrivial R₂
ha : ¬IsUnit (1, 0)
h : IsUnit (0, 1)
⊢ False
Module: Mathlib.RingTheory.LocalRing.Pullback

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
h : Function.Surjective ⇑g
r : R
⊢ ∃ a, (f.pullbackFst g) a = r

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
h : Function.Surjective ⇑g
r : R
⊢ ∃ x, f r = g x
Module: Mathlib.RingTheory.LocalRing.Pullback

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
h : Function.Surjective ⇑f
s : S
⊢ ∃ a, (f.pullbackSnd g) a = s

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
h : Function.Surjective ⇑f
s : S
⊢ ∃ a, f a = g s
Module: Mathlib.RingTheory.LocalRing.Pullback

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
s : S
hs : s ∈ ker g
⊢ (0, s) ∈ f.pullback g

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
s : S
hs : s ∈ ker g
⊢ 0 = g s
Module: Mathlib.RingTheory.Localization.Rat

Goal state before:
pp: q : ℚ
⊢ IsRelPrime q.num ↑⟨↑q.den, ⋯⟩

Tactic:
simpa using

Goal state after:
q : ℚ
⊢ q.num.natAbs.Coprime q.den
Module: Mathlib.RingTheory.Localization.Rat

Goal state before:
pp: q : ℚ
⊢ (↑(IsFractionRing.den ℤ q)).natAbs = q.den

Tactic:
simpa using

Goal state after:
q : ℚ
⊢ (↑(IsFractionRing.den ℤ q)).natAbs = q.den
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.refine_2
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⸩ × K⸨X⸩
hP : x✝ ∈ {P | Valued.v (P.2 - P.1) < ↑γ}
⊢ (x✝.1.coeff d, x✝.2.coeff d) ∈ S

Tactic:
simpa using

Goal state after:
case h.refine_2
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⸩ × K⸨X⸩
hP : x✝ ∈ {P | Valued.v (P.2 - P.1) < ↑γ}
⊢ (x✝.1.coeff d, x✝.1.coeff d) ∈ S
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✝⁵ : IsDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : IsTorsionFree R S
inst✝² : Algebra R Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
Q Q' : ↑(p.primesOver S)
h :
  { toFun := fun P ↦ ⟨Ideal.map (algebraMap S Sₚ) ↑P, ⋯⟩, invFun := fun Q ↦ ⟨comap (algebraMap S Sₚ) ↑Q, ⋯⟩,
        left_inv := ⋯, right_inv := ⋯ }
      Q ≤
    { toFun := fun P ↦ ⟨Ideal.map (algebraMap S Sₚ) ↑P, ⋯⟩, invFun := fun Q ↦ ⟨comap (algebraMap S Sₚ) ↑Q, ⋯⟩,
        left_inv := ⋯, right_inv := ⋯ }
      Q'
this : (↑Q').IsMaximal
⊢ Q ≤ Q'

Tactic:
simpa using

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✝⁵ : IsDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : IsTorsionFree R S
inst✝² : Algebra R Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
Q Q' : ↑(p.primesOver S)
h :
  { toFun := fun P ↦ ⟨Ideal.map (algebraMap S Sₚ) ↑P, ⋯⟩, invFun := fun Q ↦ ⟨comap (algebraMap S Sₚ) ↑Q, ⋯⟩,
        left_inv := ⋯, right_inv := ⋯ }
      Q ≤
    { toFun := fun P ↦ ⟨Ideal.map (algebraMap S Sₚ) ↑P, ⋯⟩, invFun := fun Q ↦ ⟨comap (algebraMap S Sₚ) ↑Q, ⋯⟩,
        left_inv := ⋯, right_inv := ⋯ }
      Q'
this : (↑Q').IsMaximal
⊢ Q ≤ Q'
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
i : n
S : Type (max u_4 u_3) := MvPolynomial { j // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  (renameEquiv R (Equiv.optionSubtypeNe i).symm).trans (optionEquivLeft R { b // b ≠ i })
he : (↑e.symm).comp Polynomial.CAlgHom = rename Subtype.val
f : S
hf0 : ((↑e.symm).comp Polynomial.CAlgHom).toRingHom f ≠ 0
hif : i ∉ (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f).vars
g : S
hig : i ∉ (((↑e.symm).comp Polynomial.CAlgHom).toRingHom g).vars
h : IsRelPrime (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f) (((↑e.symm).comp Polynomial.CAlgHom).toRingHom g)
⊢ Irreducible
    (e (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f * X i + ((↑e.symm).comp Polynomial.CAlgHom).toRingHom g))

Tactic:
simpa using

Goal state after:
n : Type u_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
i : n
S : Type (max u_4 u_3) := MvPolynomial { j // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  (renameEquiv R (Equiv.optionSubtypeNe i).symm).trans (optionEquivLeft R { b // b ≠ i })
he : (↑e.symm).comp Polynomial.CAlgHom = rename Subtype.val
f : S
hf0 : ((↑e.symm).comp Polynomial.CAlgHom).toRingHom f ≠ 0
hif : i ∉ (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f).vars
g : S
hig : i ∉ (((↑e.symm).comp Polynomial.CAlgHom).toRingHom g).vars
h : IsRelPrime (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f) (((↑e.symm).comp Polynomial.CAlgHom).toRingHom g)
⊢ Irreducible (Polynomial.C f * Polynomial.X + Polynomial.C g)
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
⊢ coeff d f ≠ 0

Tactic:
simpa using

Goal state after:
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
⊢ ¬coeff d f = 0
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
this : ∀ (x : n →₀ ℕ), d ≠ x → x ∈ f.support → i ∉ x.support
⊢ i ∉ ψ.vars

Tactic:
simpa using

Goal state after:
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
this : ∀ (x : n →₀ ℕ), d ≠ x → x ∈ f.support → i ∉ x.support
⊢ ∀ (x : n →₀ ℕ), ¬d = x → ¬coeff x f = 0 → x i = 0
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
⊢ coeff d₂ ψ ≠ 0

Tactic:
simpa using

Goal state after:
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
⊢ ¬coeff d₂ f = 0
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

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
hle : a.totalDegree ≤ b.totalDegree
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ a.totalDegree + b.totalDegree = 1

Tactic:
simpa using

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
hle : a.totalDegree ≤ b.totalDegree
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ a.totalDegree + b.totalDegree = 1
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
simpa using

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

Goal state before:
pp: K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
⊢ ∀ n < d + 1, (PowerSeries.coeff n) (F - ↑((trunc (d + 1)) F)) = 0

Tactic:
simpa using

Goal state after:
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
⊢ ∀ n < d + 1, (PowerSeries.coeff n) F = if n < d + 1 then (PowerSeries.coeff n) F else 0
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hp'
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
r : R
hr : ∀ (i : n →₀ ℕ), r ∣ coeff i (sumSMulX c)
i : n
⊢ r ∣ c i

Tactic:
simpa using

Goal state after:
case hp'
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
r : R
hr : ∀ (i : n →₀ ℕ), r ∣ coeff i (sumSMulX c)
i : n
⊢ r ∣ c i
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ Valued.v (((single 1) 1 ^ s)⁻¹ * (ofPowerSeries ℤ K) F - 1 / (single 1) 1 ^ s * (algebraMap K⟮X⟯ K⸨X⸩) ↑P) < ↑γ

Tactic:
← inv_eq_one_div,

Goal state after:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ Valued.v (((single 1) 1 ^ s)⁻¹ * (ofPowerSeries ℤ K) F - ((single 1) 1 ^ s)⁻¹ * (algebraMap K⟮X⟯ K⸨X⸩) ↑P) < ↑γ
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case isPrimitive
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' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
r : R
hr : ∀ (d : n ⊕ n →₀ ℕ), r ∣ coeff d (sumSMulXSMulY c)
i : n
⊢ r ∣ c i

Tactic:
simpa using

Goal state after:
case isPrimitive
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' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
r : R
hr : ∀ (d : n ⊕ n →₀ ℕ), r ∣ coeff d (sumSMulXSMulY c)
i : n
⊢ r ∣ c i
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

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

Tactic:
simpa using

Goal state after:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ := Fintype.card σ
this : (-1) ^ (k + 1) * ∑ a ∈ antidiagonal k, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = 0
⊢ ∑ a ∈ antidiagonal (Fintype.card σ), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = 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
⊢ Function.support ((expand p hp) φ) ⊆ (fun x ↦ p • x) '' Function.support φ

Tactic:
by
  intro d hd
  have : ∀ i, p ∣ d i := fun _ => by_contra fun hc => hd (coeff_expand_of_not_dvd p hp φ hc)
  let m := d.mapRange (fun n => n / p) (Nat.zero_div p)
  have eq_aux : p • m = d := (Finsupp.ext fun a => Nat.eq_mul_of_div_eq_right (this a) rfl).symm
  rw [Function.mem_support, ← eq_aux, ← coeff_apply (expand p hp φ), coeff_expand_smul,
    coeff_apply] at hd
  exact ⟨m, hd, eq_aux⟩

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
d : σ →₀ ℕ
hd : d ∈ (fun x ↦ p • x) '' Function.support φ
⊢ d ∈ Function.support ((expand p hp) φ)

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := hd

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d n : σ →₀ ℕ
hn₁ : n ∈ Function.support φ
hn₂ : (fun x ↦ p • x) n = d
⊢ d ∈ Function.support ((expand p hp) φ)
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ = 0
⊢ ((expand p hp) φ).order = p • φ.order

Tactic:
simpa using

Goal state after:
case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ = 0
⊢ ⊤ = ↑p * ⊤
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
v : ι → ↥(toModuleCatObj R (↑M) j)
i : ι
⊢ ?m.237

Tactic:
simpa using

Goal state after:
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
v : ι → ↥(toModuleCatObj R (↑M) j)
i : ι
⊢ ?m.237
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
⊢ IsRestricted c 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
⊢ Tendsto (fun t ↦ 0) cofinite (𝓝 0)
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
a : R
⊢ IsRestricted c (C a)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
a : R
⊢ IsRestricted c (C a)
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case pos
σ : 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
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))

Tactic:
obtain ⟨m, hm⟩ : ∃ m, p • m = d := ⟨d.mapRange (fun a ↦ a / p) (by simp),
      by ext i; simp [(Nat.mul_div_cancel' (h i))]⟩
    by_cases h_le : m ≤ n
    · rw [← hm, coeff_trunc', if_pos (nsmul_le_nsmul_right h_le p), coeff_expand_smul,
        MvPolynomial.coeff_expand_smul _ hp, coeff_trunc', if_pos h_le]
    · have not_le : ¬ p • m ≤ p • n := by
        obtain ⟨i, hi⟩ : ∃ i, m i > n i := by
          by_contra! hc
          exact h_le (Finsupp.coe_le_coe.mp hc)
        have : ¬ p • m i ≤ p • n i := by
          simp [Nat.mul_lt_mul_of_pos_left hi (p.ne_zero_iff_zero_lt.mp hp)]
        exact Not.intro fun a ↦ this (a i)
      rw [coeff_trunc', ← hm, if_neg not_le, MvPolynomial.coeff_expand_smul _ hp, coeff_trunc',
        if_neg h_le]

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
⊢ Tendsto (fun t ↦ ‖(coeff t) (-f)‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
⊢ Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c x1| ^ x2) cofinite (𝓝 0)
Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced

Goal state before:
pp: case refine_2
k : Type u_3
A : Type u_4
inst✝² : Field k
inst✝¹ : Ring A
inst✝ : Algebra k A
e : (p : Ideal k) → [inst : p.IsPrime] → AlgebraicClosure k ≃ₐ[k] AlgebraicClosure p.ResidueField :=
  fun p [p.IsPrime] ↦
    have this := ⋯;
    IsAlgClosure.equiv k (AlgebraicClosure k) (AlgebraicClosure p.ResidueField)
h : IsReduced (AlgebraicClosure k ⊗[k] A)
p : Ideal k
hp : p.IsPrime
⊢ IsReduced (AlgebraicClosure p.ResidueField ⊗[k] A)

Tactic:
exact isReduced_of_injective _ (Algebra.TensorProduct.congr (e p).symm AlgEquiv.refl).injective

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced

Goal state before:
pp: k : Type u_3
A : Type u_4
inst✝² : Field k
inst✝¹ : Ring A
inst✝ : Algebra k A
⊢ IsGeometricallyReduced k A ↔ IsReduced (AlgebraicClosure k ⊗[k] A)

Tactic:
let e (p : Ideal k) [p.IsPrime] : AlgebraicClosure k ≃ₐ[k] AlgebraicClosure p.ResidueField :=
    have := p.algEquivResidueFieldOfField.isAlgebraic
    IsAlgClosure.equiv k _ _
  refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨fun p hp ↦ ?_⟩⟩
  · exact isReduced_of_injective _ (Algebra.TensorProduct.congr (e ⊥) AlgEquiv.refl).injective
  · exact isReduced_of_injective _ (Algebra.TensorProduct.congr (e p).symm AlgEquiv.refl).injective

Goal state after: