mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ coeff ?m.126 ((rename ⇑(Equiv.swap i j)) p) ≠ 0

pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ σ →₀ ℕ

Tactic:
coeff_rename_mapDomain _ (Equiv.injective _)

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ coeff ?d p ≠ 0

case d
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ σ →₀ ℕ
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case neg
σ : 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
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))

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

Goal state after:
case neg
σ : 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
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
not_le : ¬p • m ≤ p • n
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
i : Fin n
⊢ (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ).leadingCoeff ≠ 0

Tactic:
simp [add_comm, leadingCoeff_X_pow_add_C]

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

Goal state before:
pp: case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ constantCoeff (xInTermsOfW p R n) = 0

Tactic:
| ind n IH =>

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ constantCoeff (xInTermsOfW p R n) = 0
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
i : ℕ
⊢ i.unaryCast.ghostFun = ↑i

Tactic:
induction i

Goal state after:
case zero
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
⊢ (Nat.unaryCast 0).ghostFun = ↑0

case succ
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n✝ : ℕ
a✝ : n✝.unaryCast.ghostFun = ↑n✝
⊢ (n✝ + 1).unaryCast.ghostFun = ↑(n✝ + 1)
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
this : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung (x * frobenius y)
⊢ verschiebung (x * frobenius y) = verschiebung x * y

Tactic:
have : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung x * y :=
    IsPoly₂.comp (hh := mulIsPoly₂) (hf := verschiebung_isPoly) (hg := idIsPolyI' p)

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
this✝ : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung (x * frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung x * y
⊢ verschiebung (x * frobenius y) = verschiebung x * y
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < v ↑p
⊢ 1 / ↑p + 1 / ↑p ≤ 1

Tactic:
← add_div,

Goal state after:
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < v ↑p
⊢ (1 + 1) / ↑p ≤ 1
Module: Mathlib.RingTheory.WittVector.Domain

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ k, x.coeff k ≠ 0

Tactic:
by_contra! hall

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), x.coeff k = 0
⊢ False
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝ : CommRing R
x y : TruncatedWittVector p n R
h : x.out = y.out
i : Fin n
⊢ coeff i x = coeff i y

Tactic:
WittVector.ext_iff

Goal state after:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x y : TruncatedWittVector p n R
h : ∀ (n_1 : ℕ), x.out.coeff n_1 = y.out.coeff n_1
i : Fin n
⊢ coeff i x = coeff i y
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n : ℕ
⊢ hermite (n + 1) = X * hermite n - derivative (hermite n)

Tactic:
hermite

Goal state after:
n : ℕ
⊢ X * hermite n - derivative (hermite n) = X * hermite n - derivative (hermite n)
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
hc : f.leadingCoeff = (a * b).coeff f.natDegree
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))

Tactic:
rw [hm, coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j ↦ a.coeff i * b.coeff j,
    Finset.sum_range_succ, ← sub_eq_iff_eq_add, Nat.sub_self] at hc

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
hc : 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Ring R
x : R
this : (aeval x) ((-1) ^ n * (shiftedLegendre n).comp (1 - X)) = (aeval x) (shiftedLegendre n)
⊢ (aeval x) (shiftedLegendre n) = (-1) ^ n * (aeval (1 - x)) (shiftedLegendre n)

Tactic:
simpa [aeval_comp] using this.symm

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 ≤ (↑∅).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:
Finset.coe_empty,

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).ncard ≤ ∅.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
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: τ : Type u_1
S : Type u_3
inst✝ : CommRing S
p : ℕ
hp : p ≠ 0
f : MvPowerSeries τ S
hf : HasSubst f
φ : S⟦X⟧
⊢ (MvPowerSeries.expand p hp) (MvPowerSeries.subst (fun x ↦ f) φ) = subst ((MvPowerSeries.expand p hp) f) φ

Tactic:
MvPowerSeries.expand_subst _ hp (HasSubst.const hf) (φ := φ),

Goal state after:
τ : Type u_1
S : Type u_3
inst✝ : CommRing S
p : ℕ
hp : p ≠ 0
f : MvPowerSeries τ S
hf : HasSubst f
φ : S⟦X⟧
⊢ MvPowerSeries.subst (fun i ↦ (MvPowerSeries.expand p hp) f) φ = subst ((MvPowerSeries.expand p hp) f) φ
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ Int.negSucc n • f = -(↑n.succ • f)

Tactic:
by
    simp_rw [HSMul.hSMul, SMul.smul]
    ext S _ _ m
    rw [neg_def]
    simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_smul,
      add_def_apply, smul_def_apply, Nat.succ_eq_add_one, Int.cast_add, Int.cast_natCast,
      Int.cast_one, one_smul, add_def, smul_def, Pi.smul_apply, Pi.add_apply, smul_add,
      smul_smul, neg_mul, one_mul]
    rw [add_comm]

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ f : M →ₚₗ[R] N
S : Type u
x✝¹ : CommSemiring S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ -1 • f.toFun' S m + f.toFun' S m = 0

Tactic:
← _root_.one_smul (M := R) (b := f.toFun' S m)

Goal state after:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ f : M →ₚₗ[R] N
S : Type u
x✝¹ : CommSemiring S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ -1 • f.toFun' S m + 1 • f.toFun' S m = 0
Module: Mathlib.RingTheory.Regular.Flat

Goal state before:
pp: case cons
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Flat R S
x : R
tail✝ : List R
ih :
  ∀ {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : Module R M] [inst_2 : AddCommGroup N]
    [inst_3 : Module R N] [inst_4 : Module S N] [inst_5 : IsScalarTower R S N] {f : M →ₗ[R] N},
    IsBaseChange S f → IsWeaklyRegular M tail✝ → IsWeaklyRegular N (List.map (⇑(algebraMap R S)) tail✝)
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
reg : IsSMulRegular M x ∧ IsWeaklyRegular (QuotSMulTop x M) tail✝
e : TensorProduct R S (QuotSMulTop x M) ≃ₗ[S] QuotSMulTop ((algebraMap R S) x) N
⊢ IsSMulRegular N ((algebraMap R S) x) ∧
    IsWeaklyRegular (QuotSMulTop ((algebraMap R S) x) N) (List.map (⇑(algebraMap R S)) tail✝)

Tactic:
have hg : IsBaseChange S <|
        e.toLinearMap.restrictScalars R ∘ₗ TensorProduct.mk R S (QuotSMulTop x M) 1 :=
      IsBaseChange.of_equiv e (fun _ ↦ by simp)

Goal state after:
case cons
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Flat R S
x : R
tail✝ : List R
ih :
  ∀ {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : Module R M] [inst_2 : AddCommGroup N]
    [inst_3 : Module R N] [inst_4 : Module S N] [inst_5 : IsScalarTower R S N] {f : M →ₗ[R] N},
    IsBaseChange S f → IsWeaklyRegular M tail✝ → IsWeaklyRegular N (List.map (⇑(algebraMap R S)) tail✝)
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
reg : IsSMulRegular M x ∧ IsWeaklyRegular (QuotSMulTop x M) tail✝
e : TensorProduct R S (QuotSMulTop x M) ≃ₗ[S] QuotSMulTop ((algebraMap R S) x) N
hg : IsBaseChange S (↑R ↑e ∘ₗ (TensorProduct.mk R S (QuotSMulTop x M)) 1)
⊢ IsSMulRegular N ((algebraMap R S) x) ∧
    IsWeaklyRegular (QuotSMulTop ((algebraMap R S) x) N) (List.map (⇑(algebraMap R S)) tail✝)
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⁻¹
⊢ s + -(g * s₁ * ↑⋯.unit⁻¹) = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹

Tactic:
mul_right_comm

Goal state after:
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⁻¹
⊢ s + -(g * ↑⋯.unit⁻¹ * s₁) = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case succ
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
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
heq :
  X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat * q =
    ↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)
i : ℕ
⊢ (coeff i) q ∈ I ^ (k + 1)

Tactic:
← coeff_X_pow_mul _ (g.map (Ideal.Quotient.mk I)).order.toNat i,

Goal state after:
case succ
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
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
heq :
  X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat * q =
    ↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)
i : ℕ
⊢ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) (X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat * q) ∈
    I ^ (k + 1)
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 : A⟦X⟧
inst✝ : IsAdicComplete I A
⊢ H.div (a • f) = a • H.div f

Tactic:
have H1 := (H.isWeierstrassDivisionAt_div_mod f).smul a
  have H2 := H.isWeierstrassDivisionAt_div_mod (a • f)
  exact (H.eq_of_mul_add_eq_mul_add H2.degree_lt H1.degree_lt
    (H2.eq_mul_add.symm.trans H1.eq_mul_add)).1

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' = 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:
hf2,

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 + 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
H : g.IsWeierstrassDivisorAt I
a : A
f✝ f'✝ : A⟦X⟧
inst✝ : IsAdicComplete I A
f f' : A⟦X⟧ ⧸ Ideal.span {g}
⊢ Quotient.lift (fun f ↦ H.mod f) ⋯ (f + f') =
    Quotient.lift (fun f ↦ H.mod f) ⋯ f + Quotient.lift (fun f ↦ H.mod f) ⋯ f'

Tactic:
obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
    obtain ⟨f', rfl⟩ := Ideal.Quotient.mk_surjective f'
    exact H.mod_add f f'

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

Goal state before:
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
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
peq : p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})
⊢ ↑(Submodule.spanFinrank
        (span
          (⇑(algebraMap R[X] (Localization.AtPrime p)) ''
            (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})))) ≤
    ↑p.height

Tactic:
apply le_trans _ (WithBot.coe_le_coe.mpr (Ideal.height_add_one_le_of_lt_of_isPrime lt))

Goal state after:
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] := ⋯
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
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
peq : p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})
⊢ ↑(Submodule.spanFinrank
        (span
          (⇑(algebraMap R[X] (Localization.AtPrime p)) ''
            (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})))) ≤
    ↑(q.height + 1)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f f' g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ (f + f') /ʷ g = f /ʷ g + f' /ʷ g

Tactic:
simp_rw [weierstrassDiv]
  split_ifs <;> simp

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
a : A
f g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ a • f /ʷ g = a • (f /ʷ g)

Tactic:
simp_rw [weierstrassDiv]
  split_ifs <;> simp

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ 0 /ʷ g = 0

Tactic:
simp_rw [weierstrassDiv]
  split_ifs <;> simp

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

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
n : ℕ
hn : NeZero n
I : Ideal R
w✝ : IsSimpleModule R ↥I
e : R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

Tactic:
exact ⟨n, hn, _, _, _, ⟨e⟩⟩

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

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ (v.onQuot ⋯).supp = 0

Tactic:
rw [supp_quot]

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ Ideal.map (Ideal.Quotient.mk v.supp) v.supp = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ x✝ : R
⊢ (if x✝ = 0 then x✝¹ = 0 else True) ∨ if x✝¹ = 0 then x✝ = 0 else True

Tactic:
split_ifs <;> simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ y✝ z✝ : R
x✝ : ¬if 0 = 0 then z✝ = 0 else True
⊢ (if y✝ * z✝ = 0 then x✝¹ * z✝ = 0 else True) → if y✝ = 0 then x✝¹ = 0 else True

Tactic:
split_ifs <;> simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
⊢ ¬if 0 = 0 then 1 = 0 else True

Tactic:
split_ifs <;> simp_all

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

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((rename (Prod.mk 0)) (wittPolynomial p ℤ n)).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
refine Subset.trans (vars_rename _ _) ?_
    simp [wittPolynomial_vars, image_subset_iff]

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

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((rename (Prod.mk 1)) (wittPolynomial p ℤ n)).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
refine Subset.trans (vars_rename _ _) ?_
    simp [wittPolynomial_vars, image_subset_iff]

Goal state after:
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case inr
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ z <+: x ∧ [] <+: y ∧ [] ∈ T ↔ z <+: x ++ y ∧ [] ∈ T

Tactic:
simpa using fun _ ↦ (z.isPrefix_append_of_length hl).symm

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ (coeff b o).support = (map Prod.fst (CNF b o)).toFinset

Tactic:
rw [coeff, lookupFinsupp_support, filter_eq_self.2]

Goal state after:
b o : Ordinal.{u_1}
⊢ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries.keys.toFinset = (map Prod.fst (CNF b o)).toFinset

b o : Ordinal.{u_1}
⊢ ∀ a ∈ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries, decide (a.snd ≠ 0) = true
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
⊢ Monotone gfpApprox

Tactic:
by
  intro f g h
  have : g.dual ≤ f.dual := h
  exact lfpApprox_mono_left this

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
x✝ : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := x✝
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
rcases (s ∩ Iic a).eq_empty_or_nonempty with he | hne
    · simp [he] at h
    · refine ⟨hne, (isLUB_of_mem_closure ?_ h).csSup_eq hne⟩
      exact fun x hx => hx.2

Goal state after: