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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : t ∈ pairs σ k
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(pairMap σ t).1 * ((∏ a ∈ (pairMap σ t).1, X a) * X (pairMap σ t).2 ^ (k - #(pairMap σ t).1)) =
    0

Tactic:
rw [mem_pairs] at h

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(pairMap σ t).1 * ((∏ a ∈ (pairMap σ t).1, X a) * X (pairMap σ t).2 ^ (k - #(pairMap σ t).1)) =
    0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

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

Tactic:
induction he : p.supDegree toLex using WellFoundedLT.induction generalizing p with | _ t ih
   =>  _ 

Goal state after:
case right.inr.ind
R : Type u_3
inst✝ : CommRing R
n : ℕ
t : Lex (Fin n →₀ ℕ)
ih :
  ∀ y < t,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
he : supDegree (⇑toLex) p = t
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case mpr
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w✝ : Set K⟮X⟯
hT : w✝ ∈ nhds 0
pre_T : (fun x ↦ x.2 - x.1) ⁻¹' w✝ ⊆ S
⊢ ∃ t,
    (∃ t_1 ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
      (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' t ⊆ S

Tactic:
obtain ⟨d, hd⟩ := Valued.mem_nhds.mp hT

Goal state after:
case mpr
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w✝ : Set K⟮X⟯
hT : w✝ ∈ nhds 0
pre_T : (fun x ↦ x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ w✝
⊢ ∃ t,
    (∃ t_1 ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
      (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' t ⊆ S
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

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

Tactic:
have : {a ∈ antidiagonal k | a.fst < k ∧ ¬0 < a.fst} = {(0, k)} := by
    ext a
    rw [mem_filter, mem_antidiagonal, mem_singleton]
    refine ⟨?_, by rintro rfl; lia⟩
    rintro ⟨ha, ⟨_, ha0⟩⟩
    rw [← ha, Nat.eq_zero_of_not_pos ha0, zero_add, ← Nat.eq_zero_of_not_pos ha0]

Goal state after:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
this : {a ∈ antidiagonal k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}
⊢ psum σ R k =
    (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ x ∈ antidiagonal k with x.1 < k ∧ 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

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

Tactic:
exact tendsto_antidiagonal (by simp [Finsupp.prod_add_index', pow_add]) hf hg

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
σ : Type u_2
inst✝ : IsUltrametricDist R
c : σ → ℝ
f g : MvPowerSeries σ R
hf : IsRestricted c f
hg : IsRestricted c g
⊢ IsRestricted c (f * g)

Tactic:
by
  classical
  rw [← isRestricted_abs_iff, IsRestricted] at *
  exact tendsto_antidiagonal (by simp [Finsupp.prod_add_index', pow_add]) hf hg

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

Goal state before:
pp: case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑(p ^ k * p ^ (n - k + 1)) ∣
    ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Tactic:
Nat.cast_mul,

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑(p ^ k) * ↑(p ^ (n - k + 1)) ∣
    ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    (MvPolynomial.eval x) ↑p * (MvPolynomial.eval x) (wittPolynomial p ℤ n)

Tactic:
map_natCast,

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    ↑p * (MvPolynomial.eval x) (wittPolynomial p ℤ n)
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ((teichmuller p) 0).coeff 0 = coeff 0 0

Tactic:
· rw [zero_coeff]; rfl

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

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n✝ : ℕ
⊢ ((teichmuller p) 0).coeff (n✝ + 1) = coeff 0 (n✝ + 1)

Tactic:
· rw [zero_coeff]; rfl

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: 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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
hp : Nat.Prime p
this : Nontrivial (PreTilt O p)
a✝ b✝ : PreTilt O p
hfg : (val K v O hv p) a✝ ≠ 0 ∧ (val K v O hv p) b✝ ≠ 0
⊢ (val K v O hv p) a✝ * (val K v O hv p) b✝ ≠ 0

Tactic:
exact mul_ne_zero hfg.1 hfg.2

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case inl
n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

Tactic:
rw [(by lia : n = 2 * m + k),
      Nat.add_sub_cancel, Nat.mul_div_cancel_left _ (Nat.succ_pos 1), coeff_hermite_explicit]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ ∃! h, ∃ N, ∀ n > N, (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h

Tactic:
use hilbertPoly p d

Goal state after:
case h
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ (fun h ↦ ∃ N, ∀ n > N, (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h) (p.hilbertPoly d) ∧
    ∀ (y : F[X]),
      (fun h ↦ ∃ N, ∀ n > N, (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h) y → y = p.hilbertPoly d
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: case a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ ↑((n + x)! / x !) * C (↑(n.choose x) * (-1) ^ x) = ↑n ! * C ((-1) ^ x * ↑(n.choose x) * ↑((n + x).choose n))

Tactic:
C_mul (b := ((n + x).choose n : ℤ)),

Goal state after:
case a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ ↑((n + x)! / x !) * C (↑(n.choose x) * (-1) ^ x) = ↑n ! * (C ((-1) ^ x * ↑(n.choose x)) * C ↑((n + x).choose n))
Module: Mathlib.RingTheory.PowerSeries.Catalan

Goal state before:
pp: case succ
n : ℕ
⊢ (coeff (n + 1)) 1 + (coeff (n + 1)) (catalanSeries ^ 2 * X) = (coeff (n + 1)) catalanSeries

Tactic:
coeff_one,

Goal state after:
case succ
n : ℕ
⊢ (if n + 1 = 0 then 1 else 0) + (coeff (n + 1)) (catalanSeries ^ 2 * X) = (coeff (n + 1)) catalanSeries
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: 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
r a b : R
f✝ g✝ f g : M →ₚₗ[R] N
x✝³ : Type u
x✝² : CommSemiring x✝³
x✝¹ : Algebra R x✝³
x✝ : x✝³ ⊗[R] M
⊢ (f + g).toFun' x✝³ x✝ = (g + f).toFun' x✝³ x✝

Tactic:
simp only [add_def, add_comm]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (coeff n) ((d⁄dX A) (log A)) = (coeff n) (mk fun n ↦ (algebraMap ℚ A) ((-1) ^ n))

Tactic:
have : (n + 1) = algebraMap ℚ A (n + 1) := by simp

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ↑n + 1 = (algebraMap ℚ A) (↑n + 1)
⊢ (coeff n) ((d⁄dX A) (log A)) = (coeff n) (mk fun n ↦ (algebraMap ℚ A) ((-1) ^ n))
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ ∑ i ∈ Icc 0 (n - 1), i.largeSchroder * (n - 1 - i).largeSchroder =
    ∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder

Tactic:
← range_succ_eq_Icc_zero

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ ∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder =
    ∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder
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 g : M →ₚₗ[R] N
x✝³ : Type u
x✝² : CommSemiring x✝³
x✝¹ : Algebra R x✝³
x✝ : x✝³ ⊗[R] M
⊢ (f + g).toFun' x✝³ x✝ = (g + f).toFun' x✝³ x✝

Tactic:
simp only [add_def, add_comm]

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
i : ℕ
⊢ ((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g).coeff i ∈ I

Tactic:
rw [coeff_trunc]
  split_ifs with h
  · simpa [← RingHom.mem_ker] using coeff_of_lt_order_toNat _ h
  · exact zero_mem _

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : p = ⊥
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
let : Field (Localization.AtPrime p) := IsField.toField <| by
      simp [isField_iff_maximalIdeal_eq, ← Localization.AtPrime.map_eq_maximalIdeal, eqbot]

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : p = ⊥
this : Field (Localization.AtPrime p) := ⋯.toField
⊢ IsRegularLocalRing (Localization.AtPrime p)
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 : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : r = 0
this : ∀ (k i : ℕ), (coeff i) q ∈ I ^ k
hq : q = 0
⊢ q = 0 ∧ r = 0

Tactic:
exact ⟨hq, heq⟩

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

Goal state before:
pp: 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 := Finset.image (⇑h) s
x : S
hx : x ∈ (φ R s).range
⊢ (h.comp (φ R s).range.val) ⟨x, hx⟩ ∈ (φ R s').range

Tactic:
simp only [range_φ] at hx ⊢

Goal state after:
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 := Finset.image (⇑h) s
x : S
hx✝ : x ∈ (φ R s).range
hx : x ∈ Algebra.adjoin R ↑s
⊢ (h.comp (φ R s).range.val) ⟨x, hx✝⟩ ∈ Algebra.adjoin R ↑s'
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

Tactic:
rw [Polynomial.modByMonic_eq_sub_mul_div]; ring

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    (coeff n) ((map (IsLocalRing.residue A)) g * (map (IsLocalRing.residue A)) q) + (IsLocalRing.residue A) (r.coeff n)
⊢ IsUnit q

Tactic:
Polynomial.coeff_eq_zero_of_degree_lt H1,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 : 1 = (coeff n) ((map (IsLocalRing.residue A)) g * (map (IsLocalRing.residue A)) q) + (IsLocalRing.residue A) 0
⊢ IsUnit q
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case refine_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
hfdeg : f.natDegree = n
this : X ^ n * ↑⋯.unit⁻¹ - ↑r * ↑⋯.unit⁻¹ = g
⊢ g = ↑f * ↑⋯.unit⁻¹

Tactic:
simp_rw [← this, f, Polynomial.coe_sub, Polynomial.coe_pow, Polynomial.coe_X, sub_mul]

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

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Submodule R M
inst✝¹ : IsSimpleModule R ↥N
s : Set (Submodule R M)
inst✝ : IsSemisimpleModule R M
hs : sSup s = ⊤
this : Nontrivial ↥N
w✝ : Submodule R M
compl : IsCompl N w✝
m : Submodule R M
hm : m ∈ s
ne : N.projectionOnto w✝ compl ∘ₗ m.subtype ≠ 0
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)

Tactic:
have ⟨S, ⟨e⟩⟩ := linearEquiv_of_ne_zero ne

Goal state after:
R : Type u_2
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Submodule R M
inst✝¹ : IsSimpleModule R ↥N
s : Set (Submodule R M)
inst✝ : IsSemisimpleModule R M
hs : sSup s = ⊤
this : Nontrivial ↥N
w✝ : Submodule R M
compl : IsCompl N w✝
m : Submodule R M
hm : m ∈ s
ne : N.projectionOnto w✝ compl ∘ₗ m.subtype ≠ 0
S : Submodule R ↥m
e : ↥N ≃ₗ[R] ↥S
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
S : Submodule R M
inst✝ : IsSimpleModule R ↥S
f : M →ₗ[R] N
| map f S.subtype.range

Tactic:
← LinearMap.range_comp

Goal state after:
R : Type u_2
M : Type u
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
S : Submodule R M
inst✝ : IsSimpleModule R ↥S
f : M →ₗ[R] N
| (f ∘ₗ S.subtype).range
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
s : Set ↑(isotypicComponents R M)
c : ↑(isotypicComponents R M)
hc : c ∈ {c | ↑c ≤ ↑(⨆ c ∈ s, ⟨↑c, ⋯⟩)}
hcs : c ∉ s
⊢ ↑(⨆ c ∈ s, ⟨↑c, ⋯⟩) ≤ sSup (isotypicComponents R M \ {↑c})

Tactic:
simp_rw [CompleteSublattice.coe_iSup, iSup₂_le_iff]

Goal state after:
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
s : Set ↑(isotypicComponents R M)
c : ↑(isotypicComponents R M)
hc : c ∈ {c | ↑c ≤ ↑(⨆ c ∈ s, ⟨↑c, ⋯⟩)}
hcs : c ∉ s
⊢ ∀ i ∈ s, ↑i ≤ sSup (isotypicComponents R M \ {↑c})
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: case cons.inl
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
x : ι
l : List ι
ih : (∃ x ∈ l, f x ∈ I) → (List.map f l).prod ∈ I
h : f x ∈ I
⊢ (List.map f (x :: l)).prod ∈ I

Tactic:
simpa only [List.map_cons, List.prod_cons] using I.mul_mem_right _ _ h

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

Goal state before:
pp: p n : ℕ
⊢ wittPolyProd p (n + 1) =
    -(↑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

Tactic:
have mvpz : (p : 𝕄) ^ (n + 1) = MvPolynomial.C ((p : ℤ) ^ (n + 1)) := by norm_cast

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ wittPolyProd p (n + 1) =
    -(↑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
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: case zero
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ (frobenius (frobeniusRotation p ha₁ ha₂) * a₁).coeff 0 = (frobeniusRotation p ha₁ ha₂ * a₂).coeff 0

Tactic:
simp only [WittVector.mul_coeff_zero, WittVector.coeff_frobenius_charP, frobeniusRotation,
      coeff_mk, frobeniusRotationCoeff]

Goal state after:
case zero
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y : List A
h : x ++ y ∈ T
⊢ x ∈ T

Tactic:
induction y generalizing x with

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

Goal state before:
pp: case refine_2
b o✝ o : Ordinal.{u_1}
⊢ o ≠ 0 →
    foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o →
      foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Tactic:
ho

Goal state after:
case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
⊢ foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o →
    foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o
⊢ foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 ((log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)) = o

Tactic:
foldr_cons,

Goal state after:
case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o
⊢ b ^ (log b o, o / b ^ log b o).1 * (log b o, o / b ^ log b o).2 +
      foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) =
    o
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o e : Ordinal.{u_1}
h : e ∉ map Prod.fst (CNF b o)
⊢ (coeff b o) e = 0

Tactic:
rwa [← notMem_support_iff, support_coeff, mem_toFinset]

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : IsMax a
⊢ IsOpen[inst✝²] {a}

Tactic:
convert! isOpen_Ioi (a := b) using 1

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : IsMax a
⊢ {a} = Ioi b
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : ¬IsMax a
⊢ IsOpen[inst✝²] {a}

Tactic:
convert! isOpen_Ioo (a := b) (b := Order.succ a) using 1

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : ¬IsMax a
⊢ {a} = Ioo b (Order.succ a)
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
ho' : ¬IsSuccLimit o
⊢ s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Ioo a o ⊆ s

Tactic:
simp [nhds_eq_pure.2 ho', ho, ho']

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

Goal state before:
pp: e : ONote
n : ℕ+
a₁ a₂ : ONote
h : a₁ < a₂
⊢ e.oadd n a₁ < e.oadd n a₂

Tactic:
lt_def

Goal state after:
e : ONote
n : ℕ+
a₁ a₂ : ONote
h : a₁ < a₂
⊢ (e.oadd n a₁).repr < (e.oadd n a₂).repr