mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ psum σ R k =
    (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ antidiagonal k with a.1 ∈ Set.Ioo 0 k, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2

Tactic:
simp only [Set.Ioo, Set.mem_ofPred_eq, and_comm]
  have hesymm := mul_esymm_eq_sum σ R k
  rw [← (sum_filter_add_sum_filter_not {a ∈ antidiagonal k | a.fst < k}
    (fun a ↦ 0 < a.fst) (fun a ↦ (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd))] at hesymm
  have sub_both_sides := congrArg (· - (-1 : MvPolynomial σ R) ^ (k + 1) *
    ∑ a ∈ {a ∈ antidiagonal k | a.fst < k} with 0 < a.fst,
    (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd) hesymm
  simp only [left_distrib, add_sub_cancel_left] at sub_both_sides
  have sub_both_sides := congrArg ((-1 : MvPolynomial σ R) ^ (k + 1) * ·) sub_both_sides
  simp only [mul_sub_left_distrib, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k + 1, rfl⟩, one_mul,
    filter_filter (fun a : ℕ × ℕ ↦ a.fst < k) (fun a ↦ ¬0 < a.fst)]
    at sub_both_sides
  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]
  rw [this, sum_singleton] at sub_both_sides
  simp only [_root_.pow_zero, esymm_zero, mul_one, one_mul, filter_filter] at sub_both_sides
  exact sub_both_sides.symm

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Filter

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ →o Submodule R M
⊢ EventuallyConst (⇑f) atTop

Tactic:
eventuallyConst_atTop,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ →o Submodule R M
⊢ ∃ i, ∀ (j : ℕ), i ≤ j → f j = f i
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⟦X⟧
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) f) ∈ Valued.v.valuationSubring

Tactic:
simp only [Valuation.mem_valuationSubring_iff]

Goal state after:
K : Type u_2
inst✝ : Field K
f : K⟦X⟧
⊢ Valued.v ((LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) f)) ≤ 1
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
⊢ (T1 f (-1)).comp (T1 f 1) = AlgHom.id k (MvPolynomial (Fin (n + 1)) k)

Tactic:
by simpa using t1_comp_t1_neg f (-1)

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

Goal state before:
pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
⊢ n ∈ {n} ∪ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars ∧
    {n} ∪ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars ⊆ {n} ∪ range n

Tactic:
simp only [true_and, true_or, mem_union, mem_singleton]

Goal state after:
case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
⊢ {n} ∪ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars ⊆ {n} ∪ range n
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
| (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ)
    (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))

Tactic:
simp only [map_sub, bind₁_X_right]

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
| (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ -
    (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
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
⊢ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ k * (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k)) -
      (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ k) * wittStructureInt p Φ k ^ p ^ (n + 1 - k)) =
    0

Tactic:
← map_sub,

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ (map (Int.castRingHom (ZMod (p ^ (n + 1)))))
      (↑p ^ k * (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) -
        C (↑p ^ k) * wittStructureInt p Φ k ^ p ^ (n + 1 - k)) =
    0
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
i : ℕ
hi : i < n
⊢ (map (Int.castRingHom ℚ)) (C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)

Tactic:
simp only [IH i hi, map_mul, map_pow, map_C]

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
i : ℕ
hi : i < n
⊢ C ((Int.castRingHom ℚ) ↑p) ^ i * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i) =
    C ↑p ^ i * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ((Int.castRingHom ℚ)
          (coeff c
            ((bind₁ fun i ↦ (rename fun i_1 ↦ (i, i_1)) (W_ ℤ n)) Φ -
              ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))) /
        ↑↑(p ^ n)).den =
    1

Tactic:
eq_intCast,

Goal state after:
case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ (↑(coeff c
            ((bind₁ fun i ↦ (rename fun i_1 ↦ (i, i_1)) (W_ ℤ n)) Φ -
              ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))) /
        ↑↑(p ^ n)).den =
    1
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m n : ℕ
⊢ (coeffMonoidHom M p (m + n)) f ^ p ^ n = (coeffMonoidHom M p m) f

Tactic:
rw [← map_pow, coeffMonoidHom_pow_p_pow]

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

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

Tactic:
eq_intCast,

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

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* N
x y : M
x✝ : ℕ
⊢ (coeffMonoidHom N p x✝) ⟨fun n ↦ f ((powMulEquiv M (p ^ n)).symm x) * f ((powMulEquiv M (p ^ n)).symm y), ⋯⟩ =
    (coeffMonoidHom N p x✝) ⟨fun n ↦ f ((powMulEquiv M (p ^ n)).symm x), ⋯⟩ *
      (coeffMonoidHom N p x✝) ⟨fun n ↦ f ((powMulEquiv M (p ^ n)).symm y), ⋯⟩

Tactic:
coeffMonoidHom_mk

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

Goal state before:
pp: p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (aeval fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    (aeval fun i ↦ (rename (Prod.mk i)) (W_ R n)) Φ

Tactic:
convert! congr_arg (map (Int.castRingHom R)) (wittStructureInt_prop p Φ n) using 1 <;>
      rw [hom_bind₁] <;>
    apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl

Goal state after:
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ i)) = fun i ↦
    (map (Int.castRingHom R)) (wittStructureInt p Φ i)

p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i ↦ (rename (Prod.mk i)) (W_ R n)) = fun i ↦ (map (Int.castRingHom R)) ((rename (Prod.mk i)) (W_ ℤ n))
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 : ℕ
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
r : O
hr : r * ↑p = Quotient.out ((Ideal.Quotient.mk (Ideal.span {↑p})) x) - x
⊢ ¬v ((algebraMap O K) x) ≤
      v ((algebraMap O K) (Quotient.out ((Ideal.Quotient.mk (Ideal.span {↑p})) x)) - (algebraMap O K) x)

Tactic:
← map_sub,

Goal state after:
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 : ℕ
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
r : O
hr : r * ↑p = Quotient.out ((Ideal.Quotient.mk (Ideal.span {↑p})) x) - x
⊢ ¬v ((algebraMap O K) x) ≤ v ((algebraMap O K) (Quotient.out ((Ideal.Quotient.mk (Ideal.span {↑p})) x) - x))
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 1

pp: case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → (bind₁ onePoly) (C (↑p ^ b) * X b ^ p ^ (n - b)) = 0

pp: case h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0

Tactic:
· simp only [onePoly, one_pow, one_mul, map_pow, C_1, pow_zero, bind₁_X_right, if_true]

Goal state after:
case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → (bind₁ onePoly) (C (↑p ^ b) * X b ^ p ^ (n - b)) = 0

case h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → (bind₁ onePoly) (C (↑p ^ b) * X b ^ p ^ (n - b)) = 0

Tactic:
intro i _hi hi0
    simp only [onePoly, if_neg hi0, zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero, map_pow,
      bind₁_X_right, map_mul]

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
f : PreTilt O p
n : ℕ
hfn : (coeff n) f ≠ 0
⊢ valAux K v O p f = ModP.preVal K v O p ((coeff n) f) ^ p ^ n

Tactic:
by
  have h : ∃ n, coeff n f ≠ 0 := ⟨n, hfn⟩
  rw [valAux, dif_pos h]
  classical
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le (Nat.find_min' h hfn)
  induction k with
  | zero => rfl
  | succ k ih => ?_
  obtain ⟨x, hx⟩ := Ideal.Quotient.mk_surjective (coeff (Nat.find h + k + 1) f)
  have h1 : (Ideal.Quotient.mk _ x : ModP O p) ≠ 0 := hx.symm ▸ hfn
  have h2 : (Ideal.Quotient.mk _ (x ^ p) : ModP O p) ≠ 0 := by
    rw [map_pow, hx, coeff_pow_p]
    exact coeff_nat_find_add_ne_zero k
  rw [ih (coeff_nat_find_add_ne_zero k), ← add_assoc, ← hx, ← coeff_pow_p, ← hx, ← map_pow,
    ModP.preVal_mk hv h1, ModP.preVal_mk hv h2, map_pow, v.map_pow, ← pow_mul, pow_succ']

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y

Tactic:
apply (ghostMap.bijective_of_invertible p (MvPolynomial R ℚ)).1

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
⊢ ghostMap (teichmullerFun p (x * y)) = ghostMap (teichmullerFun p x * teichmullerFun p y)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
⊢ Surjective ⇑(truncate hm)

Tactic:
intro x
  obtain ⟨x, rfl⟩ := WittVector.truncate_surjective (p := p) _ R x
  exact ⟨WittVector.truncate _ x, truncate_wittVector_truncate _ _⟩

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

Goal state before:
pp: case e_a.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ Function.Commute ⇑frobenius ⇑(frobeniusEquiv p k).symm

Tactic:
rw [Function.Commute, Function.Semiconj, ← WittVector.frobeniusEquiv_apply]
        simp only [RingEquiv.apply_symm_apply, RingEquiv.symm_apply_apply, implies_true]

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

Goal state before:
pp: case h
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
⊢ ∀ (n_1 : ℕ),
    Subsingleton
      ↑{r |
          r ∈ Finset.Iic n ∧
            ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ r) (x.coeff r)) * ↑p ^ r).coeff n_1 ≠ 0}

Tactic:
refine fun n ↦ ⟨fun ⟨a, _, ha⟩ ⟨b, _, hb⟩ ↦ ?_⟩
    ext
    dsimp only [ne_eq, Set.mem_ofPred_eq]
    rw [← Not.imp_symm (teichmuller_mul_pow_coeff_of_ne _) ha]
    exact Not.imp_symm (teichmuller_mul_pow_coeff_of_ne _) hb

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
n : ℕ
⊢ map f (dickson k a (n + 2)) = dickson k (f a) (n + 2)

Tactic:
simp only [dickson_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, map_C]
    rw [map_dickson f n, map_dickson f (n + 1)]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * Chebyshev.S R ↑(n + 1) - 1 * dickson 2 1 n = X * Chebyshev.S R (↑n + 1) - Chebyshev.S R ↑n

Tactic:
dickson_two_one_eq_chebyshev_S n

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * Chebyshev.S R ↑(n + 1) - 1 * Chebyshev.S R ↑n = X * Chebyshev.S R (↑n + 1) - Chebyshev.S R ↑n
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case e'_3
n : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + 0).choose 0) =
    -((-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + 1).choose 1))

Tactic:
(by grind : 2 * (n + 1) - 1 = 2 * n + 1),

Goal state after:
case e'_3
n : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * n + 1)‼ * ↑((2 * (n + 1) + 0).choose 0) = -((-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + 1).choose 1))
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * (n + 1) - 1)‼ * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * (n + 1) - 1)‼ * (2 * (n + 1) + k).choose k + (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))

Tactic:
(by grind : 2 * (n + 1) - 1 = 2 * n + 1),

Goal state after:
case e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * n + 1)‼ * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * n + 1)‼ * (2 * (n + 1) + k).choose k + (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
⊢ d * (X + (C 1 - C ↑k)).natDegree = d

Tactic:
← map_sub,

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
⊢ d * (X + C (1 - ↑k)).natDegree = d
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case e_a.e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * n + 1) * (2 * n + 1 + (k + 1) + 1).choose (k + 1) =
    (2 * n + 1) * (2 * (n + 1) + k).choose k + (2 * n + (k + 2)).choose (k + 2) * (k + 2)

Tactic:
(by ring : 2 * (n + 1) + k = 2 * n + 1 + (k + 1)),

Goal state after:
case e_a.e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * n + 1) * (2 * n + 1 + (k + 1) + 1).choose (k + 1) =
    (2 * n + 1) * (2 * n + 1 + (k + 1)).choose k + (2 * n + (k + 2)).choose (k + 2) * (k + 2)
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

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

Tactic:
rintro h ⟨N, hhN⟩

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

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
⊢ p.hilbertPoly d = 0

Tactic:
have heq : p = q * (-1) ^ p.rootMultiplicity 1 * (1 - X) ^ p.rootMultiplicity 1 := by
      simp only [mul_assoc, ← mul_pow, neg_mul, one_mul, neg_sub]
      exact hq1.trans (mul_comm _ _)

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ p.hilbertPoly d = 0
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:
Set.ncard_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 ≤ 0 + 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.Regular.ProjectiveDimension

Goal state before:
pp: case coe
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
aux : ∀ (n : ℕ), projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑n ↔ projectiveDimension M + 1 ≤ ↑n
N : ℕ∞
⊢ projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑N ↔ projectiveDimension M + 1 ≤ ↑N

Tactic:
| coe N =>

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

Goal state before:
pp: case h_empty
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularRing R
ι : Type u_2
inst✝ : Finite ι
⊢ IsRegularRing (MvPolynomial PEmpty.{u_2 + 1} R)

Tactic:
exact IsRegularRing.of_ringEquiv (isEmptyRingEquiv R _).symm

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : K
⊢ v ((minpoly K ((algebraMap K L) x)).coeff 0) = v x

Tactic:
minpoly.eq_X_sub_C,

Goal state after:
K : Type u_1
inst✝³ : Field K
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : K
⊢ v ((X - C x).coeff 0) = v x
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (wittPolyProdRemainder p n).vars ⊆ univ ×ˢ range n

Tactic:
by
  rw [wittPolyProdRemainder]
  refine Subset.trans (vars_sum_subset _ _) ?_
  rw [biUnion_subset]
  intro x hx
  apply Subset.trans (vars_mul _ _)
  refine union_subset ?_ ?_
  · apply Subset.trans (vars_pow _ _)
    have : (p : 𝕄) = C (p : ℤ) := by simp only [Int.cast_natCast, eq_intCast]
    rw [this, vars_C]
    apply empty_subset
  · apply Subset.trans (vars_pow _ _)
    apply Subset.trans (wittMul_vars _ _)
    apply product_subset_product (Subset.refl _)
    simpa using hx

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ sizeOf ⟨b, a⟩ < sizeOf (a.cons' l)

Tactic:
simp only [Sigma.mk.sizeOf_spec, Lists'.cons'.sizeOf_spec, lt_add_iff_pos_right]

Goal state after:
α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ 0 < sizeOf l
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:
← notMem_support_iff,

Goal state after:
b o e : Ordinal.{u_1}
h : e ∉ map Prod.fst (CNF b o)
⊢ e ∉ (coeff b o).support
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o e : Ordinal.{u_1}
h : o < b ^ e
he : e ∈ map Prod.fst (CNF b o)
⊢ False

Tactic:
rw [mem_map] at he

Goal state after:
b o e : Ordinal.{u_1}
h : o < b ^ e
he : ∃ a ∈ CNF b o, a.1 = e
⊢ False
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ IsOpen[inst✝³] s ↔ ∀ o ∈ s, IsSuccLimit o → ∃ a < o, Ioo a o ⊆ s

Tactic:
by
  refine isOpen_iff_mem_nhds.trans <| forall₂_congr fun o ho ↦ ?_
  by_cases ho' : IsSuccLimit o
  · rw [(hasBasis_nhds_Ioc_of_exists_lt (not_isMin_iff.1 ho'.not_isMin)).mem_iff]
    grind
  · simp [nhds_eq_pure.2 ho', ho, ho']

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

Goal state before:
pp: case mpr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb : b < o + 1
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb⟩)

Tactic:
obtain rfl | hb := lt_succ_iff_eq_or_lt.1 hb

Goal state after:
case mpr.inl
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a b : Ordinal.{u}
ha : veblenWith f b a = a
hb : b < b + 1
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb⟩)

case mpr.inr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb✝ : b < o + 1
hb : b < o
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb✝⟩)