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

Goal state before:
pp: 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
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
hπ : ∀ (x : S), π (g • x) = π x
x : ↑(f.rootSet S)
hx : g • x ≠ x
⊢ π (g • ↑x) = π ↑x

Tactic:
by simp [hπ]

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

Goal state before:
pp: 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 = ⊤
⊢ Function.Surjective ⇑(MulAction.toPermHom G ↑(f.rootSet S))

Tactic:
apply surjective_of_isSwap_of_isPretransitive'
      (⋃ m : MaximalSpectrum S, m.asIdeal.inertia G)
  · intro σ hσ
    obtain ⟨m, hm⟩ := Set.mem_iUnion.mp hσ
    exact hf.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia m.asIdeal (h m) σ hm
  · simpa [Subgroup.closure_iUnion]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ Function.support ((expand p hp) φ) ⊆ (fun x ↦ p • x) '' Function.support φ

Tactic:
by
  rw [expand, MvPowerSeries.support_expand]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ Function.support ((expand p hp) φ) = (fun x ↦ p • x) '' Function.support φ

Tactic:
by
  rw [expand, MvPowerSeries.support_expand]

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

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
u : S ⊗[R] N
P : Submodule R S
hu : u ∈ (rTensor N P.subtype).range
s : Finset S
hs : span R ↑s = P
this : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
⊢ u ∈ (rTensor N (Algebra.adjoin R ↑s).val.toLinearMap).range

Tactic:
rw [← subtype_comp_inclusion P _ this, rTensor_comp] at hu

Goal state after:
case right
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
u : S ⊗[R] N
P : Submodule R S
s : Finset S
hs : span R ↑s = P
this : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
hu : u ∈ (rTensor N (Subalgebra.toSubmodule (Algebra.adjoin R ↑s)).subtype ∘ₗ rTensor N (inclusion this)).range
⊢ u ∈ (rTensor N (Algebra.adjoin R ↑s).val.toLinearMap).range
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h✝ : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
this : (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (rTensor N (inclusion hP₁_le)) u₁ = (rTensor N (inclusion hP₁_le)) u'₁
s : Finset S
hs : span R ↑s = P'₁
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'

Tactic:
let ⟨w, hw⟩ := hA

Goal state after:
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h✝ : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
this : (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (rTensor N (inclusion hP₁_le)) u₁ = (rTensor N (inclusion hP₁_le)) u'₁
s : Finset S
hs : span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
f' q' : A⟦X⟧
r' : A[X]
H : f.IsWeierstrassDivisionAt g q r I
H' : f'.IsWeierstrassDivisionAt g q' r' I
⊢ g * q + ↑r + (g * q' + ↑r') = g * (q + q') + (↑r + ↑r')

Tactic:
ring

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

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
hj' : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A'.val
h✝ :
  (rTensor N (A ⊔ A').val.toLinearMap) ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t) =
    (rTensor N (A ⊔ A').val.toLinearMap) ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (rTensor N (Subalgebra.inclusion hB_le).toLinearMap) ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t) =
    (rTensor N (Subalgebra.inclusion hB_le).toLinearMap) ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t')
⊢ (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t = (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t'

Tactic:
simpa only [← rTensor_comp, ← comp_apply] using! h

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
⊢ f - g * q' = f - g * q + g * (q - q')

Tactic:
ring

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
⊢ X ^ n * s₁ + ↑s₀ + -((X ^ n * 1 + ↑((trunc n) g) * ↑⋯.unit⁻¹) * s₁) = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹

Tactic:
ring

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
inst✝ : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
hi : ¬i < ((map (Ideal.Quotient.mk I)) g).order.toNat
k : ℕ
⊢ f - g * H.div f = f - g * H.seq f k - g * (H.div f - H.seq f k)

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
R' : Type u_2
inst✝¹ : CommRing R'
e : R ≃+* R'
inst✝ : IsRegularRing R
this : IsNoetherianRing R'
p : Ideal R'
hp : p.IsPrime
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
exact IsRegularLocalRing.of_ringEquiv <| IsLocalization.ringEquivOfRingEquiv
    (Localization.AtPrime (p.comap e)) (Localization.AtPrime p) e (e.map_primeCompl_comap_eq p)

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
⊢ IsRegularRing R

Tactic:
by
  rw [isRegularRing_iff]
  intro p hp
  by_cases eqbot : p = ⊥
  · let : Field (Localization.AtPrime p) := IsField.toField <| by
      simp [isField_iff_maximalIdeal_eq, ← Localization.AtPrime.map_eq_maximalIdeal, eqbot]
    infer_instance
  · have := IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain
      R eqbot (Localization.AtPrime p)
    infer_instance

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : p = q
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)

pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)

Tactic:
· have ht1 : (maximalIdeal R).height ≤ p.height := by simpa [eq]
    have : Ideal.span ((algebraMap R (Localization.AtPrime p)) '' (maximalIdeal R).generators) =
      maximalIdeal (Localization.AtPrime p) := by
      rw [IsScalarTower.algebraMap_eq R R[X] (Localization.AtPrime p), RingHom.coe_comp,
        Set.image_comp, ← Ideal.map_span, ← Ideal.map_span]
      simp only [Ideal.span, (maximalIdeal R).span_generators, algebraMap_eq, q, ← eq,
        Localization.AtPrime.map_eq_maximalIdeal]
    simp only [← maximalIdeal_height_eq_ringKrullDim, ← IsLocalization.height_under p.primeCompl,
      IsLocalization.AtPrime.under_maximalIdeal _ p, ge_iff_le]
    apply le_trans _ (WithBot.coe_le_coe.mpr ht1)
    simp only [maximalIdeal_height_eq_ringKrullDim, ← reg, Nat.cast_le, ← this,
      ← Submodule.FG.generators_ncard fg']
    exact (Submodule.spanFinrank_span_le_ncard_of_finite (fg.image _)).trans (Set.ncard_image_le fg)

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)
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
⊢ (coeff j)
      (X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
        mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) ∈
    I

Tactic:
coeff_X_pow_mul',

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
⊢ (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
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: case hpq
R : Type u
inst✝⁸ : CommSemiring R
M : Type u_1
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := ⋯
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := ⋯
j : Fin s.card → Fin s'.card := ⋯
eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M := ⋯
ha' : π R M T ⟨s', p'⟩ = (rTensor M h.toLinearMap) t
⊢ (rTensor M (h'.comp (φ R s).rangeRestrict).toLinearMap) p = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'

Tactic:
simp only [p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
    congr
    ext n
    simp only [AlgHom.coe_comp, Function.comp_apply, coe_codRestrict,
      Subalgebra.coe_val, rename_X, h', j]
    simp only [φ, aeval_X, Equiv.symm_apply_apply]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q q' : A⟦X⟧
r r' : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hr' : r'.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = g * q' + ↑r' - ↑r
⊢ g * q' + ↑r' - ↑r - g * q' = ↑r' - ↑r

Tactic:
ring

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a✝ : A
f✝ f'✝ : A⟦X⟧
inst✝ : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
a : A⟦X⟧
ha : a * g + f' = g * H.div f + ↑(H.mod f)
hf1 : (H.mod f).degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hf2 : f = g * H.div f + ↑(H.mod f)
hf'1 : (H.mod f').degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hf'2 : f' = g * H.div f' + ↑(H.mod f')
⊢ H.mod f = H.mod f'

Tactic:
hf'2,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a✝ : A
f✝ f'✝ : A⟦X⟧
inst✝ : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
a : A⟦X⟧
ha : a * g + (g * H.div f' + ↑(H.mod f')) = g * H.div f + ↑(H.mod f)
hf1 : (H.mod f).degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hf2 : f = g * H.div f + ↑(H.mod f)
hf'1 : (H.mod f').degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hf'2 : f' = g * H.div f' + ↑(H.mod f')
⊢ H.mod f = H.mod f'
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
h✝ : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
f : A[X]
⊢ f /ₘ g * g = f - (f - g * (f /ₘ g))

Tactic:
ring

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
g' : A⟦X⟧
f' : A[X]
h' : A⟦X⟧
H' : g'.IsWeierstrassFactorizationAt f' h' I
⊢ ↑f * h * (↑f' * h') = ↑f * ↑f' * (h * h')

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N✝ : Type u_3
S : Type u_4
inst✝¹⁰ : CommSemiring R₀
inst✝⁹ : Ring R
inst✝⁸ : Algebra R₀ R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N✝
inst✝² : Module R S
inst✝¹ : IsSimpleModule R S
ι : Type u_5
inst✝ : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : ⨆ i, N i = ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : Module.End R M
x : M
⊢ ((fun f ↦ ↑(ind.linearEquiv iSup_top) ∘ₗ DFinsupp.mapRange.linearMap f ∘ₗ ↑(ind.linearEquiv iSup_top).symm)
        ((fun f i ↦ LinearMap.restrict f ⋯) f))
      x =
    f x

Tactic:
by
    exact Submodule.iSup_induction _ (motive := (_ = f ·)) (iSup_top ▸ Submodule.mem_top (x := x))
      (fun i x h ↦ by simp [ind.linearEquiv_symm_apply _ h]) (by simp)
      fun _ _ h₁ h₂ ↦ by simpa only [map_add] using congr($h₁ + $h₂)

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
h : x ∈ (PrimeSpectrum.comap C { asIdeal := Ideal.map C x✝.asIdeal, isPrime := ⋯ }).asIdeal
⊢ x ∈ x✝.asIdeal

Tactic:
rw [← @coeff_C_zero R x _]

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
h : x ∈ (PrimeSpectrum.comap C { asIdeal := Ideal.map C x✝.asIdeal, isPrime := ⋯ }).asIdeal
⊢ (C x).coeff 0 ∈ x✝.asIdeal
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
      (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
          a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun v ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
      (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
      (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
          a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
        nthRemainder p n bs (truncateFun (n + 1) a₂))

Tactic:
ring

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

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ ↑p ^ (n + 1) * X (0, n + 1) *
        ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
          (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
      (↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        (↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1)) +
          (↑p ^ (n + 1) * X (1, n + 1) *
              ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1)))))

Tactic:
ring

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
            ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
          ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
        (remainder p n - wittPolyProdRemainder p (n + 1)) +
      ↑p ^ (n + 1) * (↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    ↑p ^ (n + 1) * (X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) +
      (↑p ^ (n + 1) * (X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))

Tactic:
ring

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars ⊆
    univ ×ˢ range (n + 1)

Tactic:
apply mul_polyOfInterest_vars

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
x y : 𝕎 k
⊢ (x * y).coeff (n + 1) =
    x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
      ((x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1))

Tactic:
ring

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inr.refine_1
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
s : Set α
hs : s ⊆ Function.fixedPoints f
hs₀ : s.Nonempty
x✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
⊢ IsLUB (f '' s) a

pp: case inr.refine_2
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
a : α
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y

Tactic:
· rwa [image_congr hs, image_id']

Goal state after:
case inr.refine_2
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
a : α
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case inr
A : Type u_1
T : ↥(tree A)
x y : List A
h : ∃ z ∈ subAt T x, y = x ++ z
h' : x.length ≤ y.length
⊢ y ∈ ↑T

Tactic:
obtain ⟨_, h, rfl⟩ := h

Goal state after:
case inr
A : Type u_1
T : ↥(tree A)
x w✝ : List A
h : w✝ ∈ subAt T x
h' : x.length ≤ (x ++ w✝).length
⊢ x ++ w✝ ∈ ↑T
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x : List A
⊢ subAt (pullSub T x) x = T

Tactic:
by
  ext y; simp

Goal state after: