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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalIso R S
⊢ IsLocalIso T (T ⊗[R] S)

Tactic:
rw [iff_span_isStandardOpenImmersion_eq_top, _root_.eq_top_iff,
    ← Ideal.map_top Algebra.TensorProduct.includeRight, ← span_isStandardOpenImmersion_eq_top R S,
    Ideal.map_le_iff_le_comap, Ideal.span_le]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalIso R S
⊢ {g | IsStandardOpenImmersion R (Localization.Away g)} ⊆
    ↑(Ideal.comap TensorProduct.includeRight (Ideal.span {g | IsStandardOpenImmersion T (Localization.Away g)}))
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

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

Tactic:
have aux (n : ℕ) : projectiveDimension M ≤ n → projectiveDimension (M.localizedModule S) ≤ n := by
    simp only [projectiveDimension_le_iff]
    intro h
    exact ModuleCat.localizedModule_hasProjectiveDimensionLE n S M

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n → projectiveDimension (M.localizedModule S) ≤ ↑n
⊢ projectiveDimension (M.localizedModule S) ≤ projectiveDimension M
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

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

Tactic:
by
  have aux (n : ℕ) : projectiveDimension M ≤ n → projectiveDimension (M.localizedModule S) ≤ n := by
    simp only [projectiveDimension_le_iff]
    intro h
    exact ModuleCat.localizedModule_hasProjectiveDimensionLE n S M
  refine le_of_forall_ge (fun N ↦ ?_)
  induction N with
  | bot =>
    simp only [le_bot_iff, projectiveDimension_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.Invariant.Profinite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
P✝ : Ideal A
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
N : OpenNormalSubgroup G
⊢ Nonempty ((stabilizerHomSurjectiveAuxFunctor P Q σ).obj N)

Tactic:
have : IsScalarTower (A ⧸ P) (FixedPoints.subalgebra A B N.1.1 ⧸
    Q.under (FixedPoints.subalgebra A B N.1.1)) (B ⧸ Q) := IsScalarTower.of_algebraMap_eq
    (Quotient.ind fun x ↦ rfl)

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
P✝ : Ideal A
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
N : OpenNormalSubgroup G
this :
  IsScalarTower (A ⧸ P)
    (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
      Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
    (B ⧸ Q)
⊢ Nonempty ((stabilizerHomSurjectiveAuxFunctor P Q σ).obj N)
Module: Mathlib.RingTheory.LocalProperties.Semilocal

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
inst✝ : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing (Rₚ P)
this✝¹ : IsNoetherianRing R
this✝ : IsIntegrallyClosed R
this : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
dedekind : IsDedekindDomain R
⊢ IsPrincipalIdealRing R

Tactic:
have hp_finite : {P : Ideal R | P.IsMaximal}.Finite := by
    rw [← MaximalSpectrum.range_asIdeal]
    exact Set.finite_range MaximalSpectrum.asIdeal

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
inst✝ : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing (Rₚ P)
this✝¹ : IsNoetherianRing R
this✝ : IsIntegrallyClosed R
this : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
dedekind : IsDedekindDomain R
hp_finite : {P | P.IsMaximal}.Finite
⊢ IsPrincipalIdealRing R
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case refine_4
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h✝ : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
r : R
p : MvPolynomial σ R
x✝ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h : ∑ i, w i • (X i * (pderiv i) p) = n • p
⊢ ∑ i, w i • (X i * (pderiv i) (r • p)) = n • r • p

Tactic:
(pderiv _).map_smul,

Goal state after:
case refine_4
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h✝ : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
r : R
p : MvPolynomial σ R
x✝ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h : ∑ i, w i • (X i * (pderiv i) p) = n • p
⊢ ∑ x, w x • (X x * r • (pderiv x) p) = n • r • p
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := max ℓ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
this : (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < D, coeff hℱ d = f.coeff d

Tactic:
exact ℱ.sets_of_superset this <| intersec₂.trans intersec₁

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

Goal state before:
pp: case refine_2.ht
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this✝ : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
j : Fin n
hj : m ≤ ↑j
⊢ ((if hi : ↑j < m then s ⟨↑j, hi⟩ else 0) - if hi : ↑j + 1 < m then s ⟨↑j + 1, hi⟩ else 0) = 0

Tactic:
dif_neg hj.not_gt,

Goal state after:
case refine_2.ht
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this✝ : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
j : Fin n
hj : m ≤ ↑j
⊢ (0 - if hi : ↑j + 1 < m then s ⟨↑j + 1, hi⟩ else 0) = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
x : K⸨X⸩
hx : Valued.v x = 0
⊢ ∃ f, Valued.v f = Valued.v x

pp: case neg
K : Type u_2
inst✝ : Field K
x : K⸨X⸩
hx : ¬Valued.v x = 0
⊢ ∃ f, Valued.v f = Valued.v x

Tactic:
· use 0
    simp [hx]

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
x : K⸨X⸩
hx : ¬Valued.v x = 0
⊢ ∃ f, Valued.v f = Valued.v x
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
⊢ expand 1 ⋯ = AlgHom.id R (MvPowerSeries σ R)

Tactic:
ext1 i

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
i : MvPowerSeries σ R
⊢ (expand 1 ⋯) i = (AlgHom.id R (MvPowerSeries σ R)) i
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
τ : Type u_2
S : Type u_4
inst✝ : CommRing S
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ S
hf : HasSubst f
⊢ (expand p hp).comp (substAlgHom hf) = substAlgHom ⋯

Tactic:
ext1 i

Goal state after:
σ : Type u_1
τ : Type u_2
S : Type u_4
inst✝ : CommRing S
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ S
hf : HasSubst f
i : MvPowerSeries σ S
⊢ ((expand p hp).comp (substAlgHom hf)) i = (substAlgHom ⋯) i
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
q : ℕ
hq : q ≠ 0
⊢ expand (p * q) ⋯ = (expand p hp).comp (expand q hq)

Tactic:
ext1 i

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
q : ℕ
hq : q ≠ 0
i : MvPowerSeries σ R
⊢ (expand (p * q) ⋯) i = ((expand p hp).comp (expand q hq)) i
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
⊢ ratfuncAdicComplPkg.compare (LaurentSeriesPkg K)
      { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm RatFunc.X) }.toCompletion =
    (LaurentSeriesPkg K).coe (WithVal.toVal (polynomialValuationX K) RatFunc.X)

Tactic:
← compare_coe

Goal state after:
K : Type u_2
inst✝ : Field K
⊢ ratfuncAdicComplPkg.compare (LaurentSeriesPkg K)
      { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm RatFunc.X) }.toCompletion =
    AbstractCompletion.compare ?pkg (LaurentSeriesPkg K)
      (AbstractCompletion.coe ?pkg (WithVal.toVal (polynomialValuationX K) RatFunc.X))

case pkg
K : Type u_2
inst✝ : Field K
⊢ AbstractCompletion.{?u.24, u_2} (WithVal (polynomialValuationX K))
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 this

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.right
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) ⁻¹' {t | Valued.v t < γ} ⊆
    ⇑Valued.v ⁻¹' S

Tactic:
refine Set.Subset.trans (fun a _ ↦ ?_) (Set.preimage_mono γ_le)

Goal state after:
case h.right
K : Type u_2
inst✝ : Field K
a✝ : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a✝ = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
a : K⟮X⟯
x✝ : a ∈ (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) ⁻¹' {t | Valued.v t < γ}
⊢ a ∈ ⇑Valued.v ⁻¹' Set.Iio γ
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
f g : M → S
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
this :
  ∀ {C : M → ℝ},
    (∀ (a b : M), C (a + b) = C a * C b) →
      Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0) →
        Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0) →
          0 ≤ C → Tendsto (fun a ↦ ‖∑ p ∈ antidiagonal a, f p.1 * g p.2‖ * C a) cofinite (𝓝 0)
hC' : ¬0 ≤ C
⊢ Tendsto (fun i ↦ ‖f i‖ * |C| i) cofinite (𝓝 0)

Tactic:
simpa using hf.norm

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
F : K⟦X⟧
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F) ∈ adicCompletionIntegers K⟮X⟯ (idealX K)

Tactic:
rw [mem_adicCompletionIntegers, valuation_compare, val_le_one_iff_eq_coe]

Goal state after:
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
⊢ ∃ F_1, (ofPowerSeries ℤ K) F_1 = (ofPowerSeries ℤ K) F
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case refine_2
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ∀ (y : ℕ → MvPolynomial (idx × ℕ) ℚ),
    (fun φ ↦ ∀ (n : ℕ), (bind₁ φ) (W_ ℚ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ) y →
      y = wittStructureRat p Φ

Tactic:
intro φ H
    funext n
    rw [show φ n = bind₁ φ (bind₁ (W_ ℚ) (xInTermsOfW p ℚ n)) by
        rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]]
    rw [bind₁_bind₁]
    exact eval₂Hom_congr (RingHom.ext_rat _ _) (funext H) rfl

Goal state after:
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n i : ℕ
⊢ ↑p ^ (i + 1) * x.verschiebungFun.coeff (i + 1) ^ p ^ (n + 1 - (i + 1)) = ↑p * (↑p ^ i * x.coeff i ^ p ^ (n - i))

Tactic:
simp only [pow_succ', verschiebungFun_coeff_succ, Nat.succ_sub_succ_eq_sub, mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
⊢ Function.Injective ⇑verschiebung

Tactic:
by
  rw [injective_iff_map_eq_zero]
  intro w h
  ext n
  rw [← verschiebung_coeff_succ, h]
  simp only [zero_coeff]

Goal state after:
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
i : ℕ
⊢ (x * ↑p).coeff (i + 1) = x.coeff i ^ p

Tactic:
by
  rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_succ]

Goal state after:
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff (Fin.last ↑i) ((f (↑i + 1)) s) = TruncatedWittVector.coeff i ((f n) s)

Tactic:
rw [← f_compat (i + 1) n i.is_lt, RingHom.comp_apply, TruncatedWittVector.coeff_truncate]

Goal state after:
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff (Fin.castLE ⋯ (Fin.last ↑i)) ((f n) s) = TruncatedWittVector.coeff i ((f n) s)
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
S : Finset α
x : α → 𝕎 R
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ S ∧ (x r).coeff n ≠ 0}
n : ℕ
⊢ (∑ s ∈ S, x s).coeff n = ∑ s ∈ S, (x s).coeff n

Tactic:
classical
  induction S using Finset.induction generalizing n with
  | empty =>
    simp
  | insert a S' ha hind =>
    have : (∀ (n : ℕ), Subsingleton {r | r ∈ S' ∧ (x r).coeff n ≠ 0}) := by
      refine fun n ↦ ⟨fun b c ↦ ?_⟩
      ext
      exact congrArg (fun x ↦ x.1) <|
          (h n).allEq ⟨b.1, S'.subset_insert a b.2.1, b.2.2⟩ ⟨c.1, S'.subset_insert a c.2.1, c.2.2⟩
    replace hind := hind this
    simp only [ha, not_false_eq_true, Finset.sum_insert]
    have : ∀ (n : ℕ), (x a).coeff n = 0 ∨ (∑ s ∈ S', x s).coeff n = 0 := by
      simp only [hind]
      by_contra! ⟨m, hma, hmS'⟩
      have := Finset.sum_eq_zero.mt hmS'
      push Not at this
      choose b hb hb' using this
      have : a = b :=
        congrArg (fun x ↦ x.1) <|
          (h m).allEq ⟨a, S'.mem_insert_self a, hma⟩ ⟨b, S'.mem_insert_of_mem hb, hb'⟩
      exact ha (this ▸ hb)
    rw [coeff_add_of_disjoint n _ _ this, hind n]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m n : ℕ
⊢ (dickson 1 1 m).comp (dickson 1 1 n) = (dickson 1 1 n).comp (dickson 1 1 m)

Tactic:
← dickson_one_one_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
m n : ℕ
⊢ dickson 1 1 (m * n) = (dickson 1 1 n).comp (dickson 1 1 m)
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
⊢ p.hilbertPoly d = 0

Tactic:
rcases exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp 1 with ⟨q, hq1, hq2⟩
    have heq : p = q * (-1) ^ p.rootMultiplicity 1 * (1 - X) ^ p.rootMultiplicity 1 := by
      simp only [mul_assoc, ← mul_pow, neg_mul, one_mul, neg_sub]
      exact hq1.trans (mul_comm _ _)
    rw [heq, ← zero_add d, ← Nat.sub_add_cancel hdp, pow_add (1 - X), ← mul_assoc,
      hilbertPoly_mul_one_sub_pow_add, hilbertPoly]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
⊢ Irreducible (X ^ n - X - 1)

Tactic:
by_cases hn0 : n = 0
  · rw [hn0, pow_zero, sub_sub, add_comm, ← sub_sub, sub_self, zero_sub]
    exact Associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X
  have hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩
  have hp : (X ^ n - X - 1 : ℤ[X]) = trinomial 0 1 n (-1) (-1) 1 := by
    simp only [trinomial, C_neg, C_1]; ring
  rw [hp]
  apply IsUnitTrinomial.irreducible_of_coprime' ⟨0, 1, n, zero_lt_one, hn, -1, -1, 1, rfl⟩
  rintro z ⟨h1, h2⟩
  apply X_pow_sub_X_sub_one_irreducible_aux (n := n) z
  rw [trinomial_mirror zero_lt_one hn (-1 : ℤˣ).ne_zero (1 : ℤˣ).ne_zero] at h2
  simp_rw [trinomial, aeval_add, aeval_mul, aeval_X_pow, aeval_C,
    Units.val_neg, Units.val_one, map_neg, map_one] at h1 h2
  replace h1 : z ^ n = z + 1 := by linear_combination h1
  replace h2 := mul_eq_zero_of_left h2 z
  rw [add_mul, add_mul, add_zero, mul_assoc (-1 : ℂ), ← pow_succ, Nat.sub_add_cancel hn.le] at h2
  rw [h1] at h2 ⊢
  exact ⟨rfl, by linear_combination -h2⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
this : C a * X ^ 2 + C b * X + C c = C a * (X - C x1) * (X - C x2)
⊢ (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}

Tactic:
by
      have h1 : C a * (X - C x1) ≠ 0 := mul_ne_zero (by simpa) (Polynomial.X_sub_C_ne_zero _)
      have h2 : C a * (X - C x1) * (X - C x2) ≠ 0 := mul_ne_zero h1 (Polynomial.X_sub_C_ne_zero _)
      simp [this, Polynomial.roots_mul h2, Polynomial.roots_mul h1]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
hp : (f.rootSet S).ncard ≤ 1
g : G
hg : g ∈ Ideal.inertia G p
hfp : map (algebraMap R (S ⧸ p)) f = 0
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap

Tactic:
Set.ncard_le_one_iff_subsingleton,

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
hp : (f.rootSet S).Subsingleton
g : G
hg : g ∈ Ideal.inertia G p
hfp : map (algebraMap R (S ⧸ p)) f = 0
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: case hS1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
f : R[X]
hf : (map (algebraMap R S) f).Splits
inst✝ : MulAction.IsPretransitive G ↑(f.rootSet S)
h : ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ m.asIdeal)).ncard + 1
hG : ⨆ m, Ideal.inertia G m.asIdeal = ⊤
⊢ ∀ σ ∈ ⋃ m, ↑(Ideal.inertia G m.asIdeal),
    (MulAction.toPermHom G ↑(f.rootSet S)) σ = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) σ).IsSwap

Tactic:
intro σ hσ

Goal state after:
case hS1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
f : R[X]
hf : (map (algebraMap R S) f).Splits
inst✝ : MulAction.IsPretransitive G ↑(f.rootSet S)
h : ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ m.asIdeal)).ncard + 1
hG : ⨆ m, Ideal.inertia G m.asIdeal = ⊤
σ : G
hσ : σ ∈ ⋃ m, ↑(Ideal.inertia G m.asIdeal)
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) σ = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) σ).IsSwap
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
q : ℕ
hq : q ≠ 0
⊢ expand (p * q) ⋯ = (expand p hp).comp (expand q hq)

Tactic:
ext1 i

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
q : ℕ
hq : q ≠ 0
i : R⟦X⟧
⊢ (expand (p * q) ⋯) i = ((expand p hp).comp (expand q hq)) i
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
R' : Type u_2
inst✝ : CommRing R'
e : R ≃+* R'
⊢ IsRegularLocalRing R'

Tactic:
have := e.isLocalRing
  have := isNoetherianRing_of_ringEquiv R e
  rwa [isRegularLocalRing_iff, ← ringKrullDim_eq_of_ringEquiv e, ← map_ringEquiv_maximalIdeal e,
    Ideal.spanFinrank_map_eq_of_ringEquiv, ← isRegularLocalRing_iff]

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

Goal state before:
pp: case inl
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq :
  ((X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
          mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
        ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g)) *
      q =
    ↑r
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
j : ℕ
hj : j ≤ i
⊢ (if ((map (Ideal.Quotient.mk I)) g).order.toNat ≤ j then
      (coeff (j - ((map (Ideal.Quotient.mk I)) g).order.toNat))
        (mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g)
    else 0) ∈
    I

Tactic:
if_neg (lt_of_le_of_lt hj hi).not_ge,

Goal state after:
case inl
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq :
  ((X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
          mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
        ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g)) *
      q =
    ↑r
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
j : ℕ
hj : j ≤ i
⊢ 0 ∈ I