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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ 0)) = (Int.castRingHom ℚ) (constantCoeff Φ)

Tactic:
map_wittStructureInt,

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) 0) = (Int.castRingHom ℚ) (constantCoeff Φ)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) 0) = (Int.castRingHom ℚ) (constantCoeff Φ)

Tactic:
constantCoeff_wittStructureRat_zero,

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff ((map (Int.castRingHom ℚ)) Φ) = (Int.castRingHom ℚ) (constantCoeff Φ)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ n)) = (Int.castRingHom ℚ) 0

Tactic:
map_wittStructureInt,

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n) = (Int.castRingHom ℚ) 0
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ C ↑p *
      ((MvPolynomial.map (Int.castRingHom ℚ)) (X (n + 1)) -
        (MvPolynomial.map (Int.castRingHom ℚ))
          (∑ i ∈ range n,
            ∑ j ∈ range (p ^ (n - i)),
              (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
                C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))))) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C ↑p * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)

Tactic:
map_X,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ C ↑p *
      (X (n + 1) -
        (MvPolynomial.map (Int.castRingHom ℚ))
          (∑ i ∈ range n,
            ∑ j ∈ range (p ^ (n - i)),
              (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
                C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))))) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C ↑p * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R : Type u
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ 0) (wittPolynomial p R n) = 0

Tactic:
← aeval_eq_bind₁,

Goal state after:
p : ℕ
R : Type u
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n : ℕ
⊢ (aeval 0) (wittPolynomial p R n) = 0
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ C ↑p ^ i *
        ((C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (j + 1) *
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
          ↑((p ^ (n - i)).choose (j + 1))) *
      C ⅟↑p ^ n =
    C ↑p *
      (((MvPolynomial.map (Int.castRingHom ℚ)) (X i) ^ p) ^ (p ^ (n - i) - (j + 1)) *
          (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))))

Tactic:
map_X,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ C ↑p ^ i *
        ((C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (j + 1) *
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
          ↑((p ^ (n - i)).choose (j + 1))) *
      C ⅟↑p ^ n =
    C ↑p *
      ((X i ^ p) ^ (p ^ (n - i) - (j + 1)) * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))))
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case pos
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 : v ↑p = 0
⊢ v ↑p ≤ v ↑p ^ (1 / ↑p) * v ↑p ^ (1 / ↑p)

Tactic:
hvp

Goal state after:
case pos
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 : v ↑p = 0
⊢ 0 ≤ 0 ^ (1 / ↑p) * 0 ^ (1 / ↑p)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom (ZMod p))) (X n) ^ p +
      (MvPolynomial.map (Int.castRingHom (ZMod p))) (C ↑p) *
        (MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPolyAux p n) =
    X n ^ p

Tactic:
map_X,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ X n ^ p +
      (MvPolynomial.map (Int.castRingHom (ZMod p))) (C ↑p) *
        (MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPolyAux p n) =
    X n ^ p
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ x✝.frobeniusFun.coeff n = (aeval x✝.coeff) (frobeniusPoly p n)

Tactic:
apply coeff_frobeniusFun

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

Goal state before:
pp: case zero.mk'
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
coeff✝ : ℕ → R
h : ∀ i < 0, { coeff := coeff✝ }.coeff i = 0
⊢ { coeff := coeff✝ } = (⇑verschiebung)^[0] ({ coeff := coeff✝ }.shift 0)

Tactic:
simp [shift]

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

Goal state before:
pp: p n : ℕ
R : Type u_1
x : 𝕎 R
i : Fin n
⊢ TruncatedWittVector.coeff i (truncateFun n x) = x.coeff ↑i

Tactic:
truncateFun,

Goal state after:
p n : ℕ
R : Type u_1
x : 𝕎 R
i : Fin n
⊢ TruncatedWittVector.coeff i (TruncatedWittVector.mk p fun i ↦ x.coeff ↑i) = x.coeff ↑i
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
n : ℕ
⊢ (select P z).coeff n = x.coeff n

Tactic:
rw [select, coeff_mk, coeff_mk]

Goal state after:
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
n : ℕ
⊢ (if P n then if P n then x.coeff n else y.coeff n else 0) = x.coeff n
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
n : ℕ
⊢ (select (fun i ↦ ¬P i) z).coeff n = y.coeff n

Tactic:
rw [select, coeff_mk, coeff_mk]

Goal state after:
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
n : ℕ
⊢ (if ¬P n then if P n then x.coeff n else y.coeff n else 0) = y.coeff n
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case pos
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
f : PreTilt O p
hf0 : f = 0
⊢ (val K v O hv p) f = 0 ↔ f = 0

Tactic:
rw [hf0]

Goal state after:
case pos
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
f : PreTilt O p
hf0 : f = 0
⊢ (val K v O hv p) 0 = 0 ↔ 0 = 0
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: case inl
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
x : R
m n : ℕ
h✝ : m ≠ n
h : m < n
⊢ ((teichmuller p) x * ↑p ^ n).coeff m = 0

Tactic:
exact WittVector.mul_pow_charP_coeff_zero (teichmuller p x) h

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
⊢ x.coeff i = ∑ s ≤ n, ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ s) (x.coeff s)) * ↑p ^ s).coeff i

Tactic:
rw [Finset.sum_eq_add_sum_sdiff_singleton_of_mem (Finset.mem_Iic.mpr (Nat.lt_succ_iff.mp hi))]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
⊢ x.coeff i =
    ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i).coeff i +
      ∑ x_1 ∈ Finset.Iic n \ {i},
        ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ x_1) (x.coeff x_1)) * ↑p ^ x_1).coeff i
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Goal state before:
pp: case left
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f h : R⟦X⟧
g : R[X]
distinguish : g.IsDistinguishedAt I
notMem : PowerSeries.constantCoeff h ∉ I
eq : f = ↑g * h
this : Nontrivial R
mapf : (PowerSeries.map (Ideal.Quotient.mk I)) f = ↑(X ^ g.natDegree) * (PowerSeries.map (Ideal.Quotient.mk I)) h
⊢ (PowerSeries.coeff g.natDegree) ((PowerSeries.map (Ideal.Quotient.mk I)) f) ≠ 0

Tactic:
simp [mapf, PowerSeries.coeff_X_pow_mul', eq_zero_iff_mem, notMem]

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
hy : y = 0
⊢ x = y + y⁻¹ ∨ y = 0 ↔ y ^ 2 - x * y + 1 = 0 ∨ y = 0

pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ x = y + y⁻¹ ∨ y = 0 ↔ y ^ 2 - x * y + 1 = 0 ∨ y = 0

Tactic:
· simp only [hy, or_true]

Goal state after:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ x = y + y⁻¹ ∨ y = 0 ↔ y ^ 2 - x * y + 1 = 0 ∨ y = 0
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) = (-1) ^ n * deriv^[n] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x / Real.exp (-(x ^ 2 / 2))

Tactic:
deriv_gaussian_eq_hermite_mul_gaussian

Goal state after:
n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) =
    (-1) ^ n * ((-1) ^ n * (aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2))) / Real.exp (-(x ^ 2 / 2))
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
p : ℕ
hp : p ≠ 0
f : R →+* S
φ : R⟦X⟧
⊢ (map f) ((expand p hp) φ) = (expand p hp) ((map f) φ)

Tactic:
by
  simp [map, expand, MvPowerSeries.map_expand]

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
r a b : R
f✝ g : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ ↑(n + 1) • f = ↑n • f + f

Tactic:
simp only [Nat.cast_add, Nat.cast_one, add_smul, one_smul]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
B : Subalgebra R S
hB : B.FG
⊢ (φ R (Exists.choose hB)).range = B

Tactic:
simp only [range_φ, hB.choose_spec]

Goal state after:
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
a : A
f f' : A⟦X⟧
inst✝ : IsPrecomplete I A
i m n✝ n : ℕ
hn : m ≤ n
ih : (coeff i) (H.seq f m) ≡ (coeff i) (H.seq f n) [SMOD I ^ m • ⊤]
⊢ (coeff i) (H.seq f (n + 1)) - (coeff i) (H.seq f n) ∈ I ^ m • ⊤

Tactic:
smul_eq_mul,

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a : A
f f' : A⟦X⟧
inst✝ : IsPrecomplete I A
i m n✝ n : ℕ
hn : m ≤ n
ih : (coeff i) (H.seq f m) ≡ (coeff i) (H.seq f n) [SMOD I ^ m • ⊤]
⊢ (coeff i) (H.seq f (n + 1)) - (coeff i) (H.seq f n) ∈ I ^ m * ⊤
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case neg
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 : ℕ
⊢ (coeff i) (f - g * H.div f) ∈ I ^ k • ⊤

Tactic:
smul_eq_mul,

Goal state after:
case neg
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 : ℕ
⊢ (coeff i) (f - g * H.div f) ∈ I ^ k * ⊤
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 : g * q = ↑r
this : ∀ (k i : ℕ), (coeff i) q ∈ I ^ k
i k : ℕ
⊢ (coeff i) q ∈ I ^ k • ⊤

Tactic:
smul_eq_mul,

Goal state after:
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 : g * q = ↑r
this : ∀ (k i : ℕ), (coeff i) q ∈ I ^ k
i k : ℕ
⊢ (coeff i) q ∈ I ^ k * ⊤
Module: Mathlib.RingTheory.RegularLocalRing.Defs

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

Tactic:
have := IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain
      R eqbot (Localization.AtPrime p)
    infer_instance

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
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
a : A[X]
ha : a ∈ Ideal.span {g}
⊢ a ∈ Ideal.comap (Polynomial.coeToPowerSeries.algHom A) (Ideal.span {↑g})

Tactic:
by
    obtain ⟨b, hb⟩ := Ideal.mem_span_singleton'.1 ha
    simp only [Ideal.mem_comap, Polynomial.coeToPowerSeries.algHom_apply, Algebra.algebraMap_self,
      map_id, id_eq, Ideal.mem_span_singleton']
    exact ⟨b, by simp [← hb]⟩

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 : (coeff n) ((map (IsLocalRing.residue A)) X ^ n) = (coeff n) ((map (IsLocalRing.residue A)) (g * q + ↑r))
⊢ IsUnit q

Tactic:
map_X,

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 : (coeff n) (X ^ n) = (coeff n) ((map (IsLocalRing.residue A)) (g * q + ↑r))
⊢ 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:
← this,

Goal state after:
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
⊢ X ^ n * ↑⋯.unit⁻¹ - ↑r * ↑⋯.unit⁻¹ = ↑f * ↑⋯.unit⁻¹
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
inst✝² : IsSemisimpleModule R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule R ↥S
⊢ ∃ n, ∃ (_ : NeZero n), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] Fin n → ↥S)

Tactic:
have ⟨n, e⟩ := (h S).linearEquiv_fun

Goal state after:
R : Type u_2
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsSemisimpleModule R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule R ↥S
n : ℕ
e : Nonempty (M ≃ₗ[R] Fin n → ↥S)
⊢ ∃ n, ∃ (_ : NeZero n), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] Fin n → ↥S)
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: S : Type u_2
inst✝³ : DivisionRing S
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module S N
inst✝ : IsSimpleModule S N
I : Ideal S
hI : I.IsMaximal
e : N ≃ₗ[S] S ⧸ I
⊢ Nonempty (N ≃ₗ[S] S)

Tactic:
exact ⟨e ≪≫ₗ I.quotEquivOfEqBot ((eq_bot_or_eq_top I).resolve_right hI.ne_top)⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ IsOpenMap (PrimeSpectrum.comap C)

Tactic:
rintro U ⟨s, z⟩

Goal state after:
R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (PrimeSpectrum.comap C '' U)
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
⊢ False

Tactic:
have := solution_spec p a₁ a₂

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ False
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

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

Tactic:
have := solution_spec p a₁ a₂

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (↑p ^ (n + 1) * polyOfInterest p n).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
rw [mul_polyOfInterest_aux5]
  apply Subset.trans (vars_sub_subset _)
  refine union_subset ?_ ?_
  · apply remainder_vars
  · apply wittPolyProdRemainder_vars

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

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x : List A
⊢ x ∈ pullSub T x ↔ [] ∈ T

Tactic:
simpa using mem_pullSub_append (y := [])

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

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

Tactic:
by
  ext z; rcases le_total x.length z.length with hl | hl
  · by_cases hp : x <+: z
    · obtain ⟨z, rfl⟩ := hp
      simp [pullSub, List.take_add]
    · constructor <;> intro ⟨h, _⟩ <;>
        [skip; replace h := by simpa [List.take_take] using h.take x.length] <;>
        cases hp <| List.prefix_iff_eq_take.mpr (h.eq_of_length (by simpa)).symm
  · rw [mem_pullSub_short hl, mem_pullSub_short (by simp), mem_pullSub_short (by simp; lia)]
    simpa using fun _ ↦ (z.isPrefix_append_of_length hl).symm

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

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
⊢ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂

Tactic:
rcases eq_or_ne o₁ 0 with (rfl | h₁)

Goal state after:
case inl
o₂ : Ordinal.{u_1}
hcomm : AddCommute 0 o₂
ih : ∀ y < 0 + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : 0 ≤ o₂
⊢ ∃ o n₁ n₂, o * ↑n₁ = 0 ∧ o * ↑n₂ = o₂

case inr
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
⊢ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
⊢ trans (atom a)

Tactic:
l₂

Goal state after:
case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
l₂ : Lists α
⊢ ∀ ⦃l₃ : Lists α⦄, atom a ~ l₂ → l₂ ~ l₃ → atom a ~ l₃
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
⊢ trans (of' l₁)

Tactic:
l₂

Goal state after:
case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂ : Lists α
⊢ ∀ ⦃l₃ : Lists α⦄, of' l₁ ~ l₂ → l₂ ~ l₃ → of' l₁ ~ l₃