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

Goal state before:
pp: case inl
σ : 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)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : 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

pp: case inr
σ : 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)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : 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

Tactic:
· rw [pairMap_of_snd_mem_fst σ h1]
    simp only [← prod_erase_mul t.fst (fun j ↦ (X j : MvPolynomial σ R)) h1,
      mul_assoc (∏ a ∈ erase t.fst t.snd, X a), card_erase_of_mem h1]
    nth_rewrite 1 [← pow_one (X t.snd)]
    simp only [← pow_add, add_comm]
    have h3 : 1 ≤ #t.1 := lt_iff_add_one_le.mp (card_pos.mpr ⟨t.snd, h1⟩)
    rw [← tsub_tsub_assoc h.left h3, ← neg_neg ((-1 : MvPolynomial σ R) ^ (#t.1 - 1)),
      h2 (#t.1 - 1), Nat.sub_add_cancel h3]
    simp

Goal state after:
case inr
σ : 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)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : 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.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
v : ι → ↥(toModuleCatObj R (↑M) j)
i : ι
⊢ single j i 1 • single i j 1 • ↑(v i) = ↑(v i)

Tactic:
obtain ⟨y, hy⟩ := by simpa [-SetLike.coe_mem] using (v i).2

Goal state after:
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
v : ι → ↥(toModuleCatObj R (↑M) j)
i : ι
y : ↑M
hy : single j j 1 • y = ↑(v i)
⊢ single j i 1 • single i j 1 • ↑(v i) = ↑(v i)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
F : K⟦X⟧
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F) ∈ adicCompletionIntegers K⟮X⟯ (idealX K)

Tactic:
by
  rw [mem_adicCompletionIntegers, valuation_compare, val_le_one_iff_eq_coe]
  exact ⟨F, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : Field K
⊢ K⟦X⟧ ≃ₐ[K] ↥(adicCompletionIntegers K⟮X⟯ (idealX K))

Tactic:
by
  apply AlgEquiv.ofRingEquiv (f := powerSeriesRingEquiv K)
  intro a
  rw [PowerSeries.algebraMap_eq, RingHom.algebraMap_toAlgebra, ← Subtype.coe_inj,
    powerSeriesRingEquiv_coe_apply,
    RingHom.codRestrict_apply _ _ (algebraMap_C_mem_adicCompletionIntegers K)]
  simp

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
⊢ ∃ s g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
obtain ⟨n, f, fsurj⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp fin

Goal state after:
k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj : Function.Surjective ⇑f
⊢ ∃ s g, Function.Injective ⇑g ∧ g.IsIntegral
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case refine_3
p : ℕ
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (n : ℕ), (ghostComponent n) (x✝ + y✝).verschiebungFun = (ghostComponent n) (x✝.verschiebungFun + y✝.verschiebungFun)

Tactic:
rintro ⟨⟩

Goal state after:
case refine_3.zero
p : ℕ
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (ghostComponent 0) (x✝ + y✝).verschiebungFun = (ghostComponent 0) (x✝.verschiebungFun + y✝.verschiebungFun)

case refine_3.succ
p : ℕ
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n✝ : ℕ
⊢ (ghostComponent (n✝ + 1)) (x✝ + y✝).verschiebungFun =
    (ghostComponent (n✝ + 1)) (x✝.verschiebungFun + y✝.verschiebungFun)
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : verschiebung w = 0
n : ℕ
⊢ coeff 0 n.succ = coeff 0 n

Tactic:
simp only [zero_coeff]

Goal state after:
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
i : ℕ
hi : i < n
⊢ C (↑p ^ i) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ i) ^ p ^ (n - i) * C (⅟↑p ^ n) -
      C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * C (⅟↑p ^ n) =
    ∑ i_1 ∈ range (p ^ (n - i)),
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
            C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))))

Tactic:
rw [← IH i hi]

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
i : ℕ
hi : i < n
⊢ C (↑p ^ i) * (X i ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ p ^ (n - i) *
        C (⅟↑p ^ n) -
      C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * C (⅟↑p ^ n) =
    ∑ i_1 ∈ range (p ^ (n - i)),
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
            C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))))
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
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
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
⊢ ∀ (n : ℕ), (ghostComponent n) (verschiebung (x * frobenius y)) = (ghostComponent n) (verschiebung x * y)

Tactic:
rintro ⟨⟩

Goal state after:
case refine_3.zero
p : ℕ
hp : Fact (Nat.Prime p)
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
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
⊢ (ghostComponent 0) (verschiebung (x * frobenius y)) = (ghostComponent 0) (verschiebung x * y)

case refine_3.succ
p : ℕ
hp : Fact (Nat.Prime p)
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
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
n✝ : ℕ
⊢ (ghostComponent (n✝ + 1)) (verschiebung (x * frobenius y)) = (ghostComponent (n✝ + 1)) (verschiebung x * y)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) +
        -↑p / ↑p ^ n / ↑p ^ (n - i - v p (j + 1)) * ↑((p ^ (n - i)).choose (j + 1)) *
          ↑p ^ (i + j + (n - i - v p (j + 1))) -
      (↑((p ^ (n - i)).choose (j + 1)) / ↑p ^ (n - i - v p (j + 1)) * ↑p ^ (j - v p (j + 1)) * ↑p +
        -↑p / ↑p ^ n / ↑p ^ (n - i - v p (j + 1)) * ↑((p ^ (n - i)).choose (j + 1)) * ↑p ^ (j - v p (j + 1) + n)) =
    0

Tactic:
field [hp.1.ne_zero]

Goal state after:
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
⊢ v ↑p ^ 1 ≤ v ↑p ^ (1 / ↑p + 1 / ↑p)

Tactic:
refine rpow_le_rpow_of_exponent_ge hvp (map_natCast (algebraMap O K) p ▸ hv.2 _) ?_

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 / ↑p + 1 / ↑p ≤ 1
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
n : ℕ
⊢ ((WittVector.map g) (f x y)).coeff n = (f ((WittVector.map g) x) ((WittVector.map g) y)).coeff n

Tactic:
simp +unfoldPartialApp only [map_coeff, hf, map_aeval, peval, uncurry]

Goal state after:
p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
n : ℕ
⊢ (eval₂Hom (g.comp (algebraMap ℤ R)) fun i ↦ g (![x.coeff, y.coeff] i.1 i.2)) (φ n) =
    (aeval fun a ↦ ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] a.1 a.2) (φ n)
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hfg : ¬f + g = 0
hf : ∃ n, (coeff n) f ≠ 0
hg : ∃ n, (coeff n) g ≠ 0
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)

Tactic:
replace hfg : ∃ n, coeff n (f + g) ≠ 0 := not_forall.1 fun h => hfg <| Perfection.ext h

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ∃ n, (coeff n) f ≠ 0
hg : ∃ n, (coeff n) g ≠ 0
hfg : ∃ n, (coeff n) (f + g) ≠ 0
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: case refine_1
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ liftFun f 1 = 1

Tactic:
intros
    rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
    simp [RingHom.mem_ker, f_compat]

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

Goal state before:
pp: case refine_2
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ ∀ (x y : S), liftFun f (x * y) = liftFun f x * liftFun f y

Tactic:
intros
    rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
    simp [RingHom.mem_ker, f_compat]

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

Goal state before:
pp: case refine_3
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ liftFun f 0 = 0

Tactic:
intros
    rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
    simp [RingHom.mem_ker, f_compat]

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

Goal state before:
pp: case refine_4
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ ∀ (x y : S), liftFun f (x + y) = liftFun f x + liftFun f y

Tactic:
intros
    rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
    simp [RingHom.mem_ker, f_compat]

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

Goal state before:
pp: case refine_2
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
⊢ ∃ c, x = c * ↑p ^ n

Tactic:
· use (frobeniusEquiv p k).symm^[n] (x.shift n)
    rw [← iterate_verschiebung_iterate_frobenius]
    calc
    _ = verschiebung^[n] (x.shift n) := by
      simpa using eq_iterate_verschiebung (x := x) (n := n) h
    _ = _ := by
      congr
      rw [← Function.comp_apply (f := frobenius^[n]), ← Function.Commute.comp_iterate]
      · rw [← WittVector.frobeniusEquiv_apply, ← RingEquiv.coe_trans]
        simp
      · 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.Polynomial.Dickson

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

Tactic:
rw [dickson_add_two, C_1, Nat.cast_add, Nat.cast_two, Chebyshev.S_add_two,
      dickson_two_one_eq_chebyshev_S (n + 1), 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.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ IsLeftCancelMulZero Rᵐᵒᵖ ∧ IsCancelAdd Rᵐᵒᵖ ↔ IsRightCancelMulZero R ∧ IsCancelAdd R

Tactic:
MulOpposite.isLeftCancelMulZero_iff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ IsRightCancelMulZero R ∧ IsCancelAdd Rᵐᵒᵖ ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
heq : 1 - PowerSeries.X = ↑(1 - X)
⊢ (PowerSeries.coeff n) (↑p * (1 - PowerSeries.X) * ↑(invOneSubPow F (d + 1))) =
    eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))

Tactic:
heq,

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
heq : 1 - PowerSeries.X = ↑(1 - X)
⊢ (PowerSeries.coeff n) (↑p * ↑(1 - X) * ↑(invOneSubPow F (d + 1))) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))
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
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ p.hilbertPoly d = 0

Tactic:
heq,

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
⊢ (q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p).hilbertPoly d = 0
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
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).natDegree = d - rootMultiplicity 1 p - 1

Tactic:
heq,

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
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
⊢ ((q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p).hilbertPoly d).natDegree =
    d - rootMultiplicity 1 p - 1
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
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ (rTensor M A.val.toLinearMap).range
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (φ R gen).toLinearMap) p = t
⊢ s ∈ (φ R gen).range

Tactic:
hgen

Goal state after:
R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ (rTensor M A.val.toLinearMap).range
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (φ R gen).toLinearMap) p = t
⊢ s ∈ A ⊔ Algebra.adjoin R ↑{s}
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
w✝⁴ : Type v
w✝³ : AddCommGroup w✝⁴
w✝² : Module R w✝⁴
w✝¹ : Free R w✝⁴
w✝ : Module.Finite R w✝⁴
f✝ : w✝⁴ →ₗ[R] ↑M
surjf : Function.Surjective ⇑f✝
S : ShortComplex (ModuleCat R) := f✝.shortComplexKer
hS : S.ShortExact
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L 0)) → HasProjectiveDimensionLT M 0
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (0 + 1))
this : Subsingleton (Ext M S.X₁ 1)
f' : Ext M S.X₂ 0
f : M ⟶ S.X₂
hf' : f ≫ S.g = 𝟙 M
hf : Ext.mk₀ f = f'
⊢ CategoryTheory.Projective M

Tactic:
exact (Retract.mk f S.g hf').projective

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

Goal state before:
pp: R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : LinearOrderedCommMonoidWithZero ΓR
inst✝² : LinearOrderedCommMonoidWithZero ΓA
inst✝¹ : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
x : R
⊢ vA ((algebraMap R A) x) = 1 ↔ vR x = 1

Tactic:
simpa only [le_antisymm_iff, map_one] using
    and_congr (val_map_le_iff vR vA x 1) (val_map_le_iff vR vA 1 x)

Goal state after:
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
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Tactic:
exact solution_spec' _ ha₁ _

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

Goal state before:
pp: case inl
o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 ≤ 1
⊢ CNF 0 o = [(0, o)]

pp: case inr
o : Ordinal.{u_1}
ho : o ≠ 0
hb : 1 ≤ 1
⊢ CNF 1 o = [(0, o)]

Tactic:
exacts [CNF.zero_left ho, CNF.one_left ho]

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

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

Tactic:
rw [zero_right, foldr_nil]

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l : Lists' α true
⊢ l ⊆ l

Tactic:
rw [← Lists'.of_toList l]; exact ofList_subset (List.Subset.refl _)

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case antisymm
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : l₁.Subset l₂
h₂ : l₂.Subset l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Tactic:
exact ⟨h₁, h₂⟩

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ : Lists' α false
l₂ : Lists' α true
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rintro ⟨⟩

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ : Lists' α true
l₂ : Lists' α false
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rintro ⟨⟩

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

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
⊢ (match Ordering.lt, e₁, e₂ with
    | Ordering.lt, a, b => a < b
    | Ordering.eq, a, b => a = b
    | Ordering.gt, a, b => b < a) →
    (Ordering.lt.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
      (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)

Tactic:
case =>

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

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
⊢ (match Ordering.gt, e₁, e₂ with
    | Ordering.lt, a, b => a < b
    | Ordering.eq, a, b => a = b
    | Ordering.gt, a, b => b < a) →
    (Ordering.gt.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
      (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)

Tactic:
case =>

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

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₁ < ↑n₂ ∧ Ordering.lt = Ordering.lt ∨ ↑n₂ ≤ ↑n₁ ∧ (if ↑n₂ < ↑n₁ then Ordering.gt else Ordering.eq) = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
case =>

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

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₁ < ↑n₂ ∧ Ordering.lt = Ordering.gt ∨ ↑n₂ ≤ ↑n₁ ∧ (if ↑n₂ < ↑n₁ then Ordering.gt else Ordering.eq) = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
case =>

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

Goal state before:
pp: o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : a₁ < a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.lt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

Tactic:
case =>

Goal state after: