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

Goal state before:
pp: case h.h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i < n
hi0 : i ≠ 0
⊢ C ↑p ^ i * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0

Tactic:
rw [IH _ hin (Nat.pos_of_ne_zero hi0), zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (-X 0) = 0

Tactic:
simp only [neg_zero, map_neg, constantCoeff_X]

Goal state after:
Module: Mathlib.RingTheory.Perfection

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

Tactic:
rw [← coeffMonoidHom_pow_p_pow' _ 0 n, zero_add]

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 : ℕ
⊢ (fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ i)) = fun i ↦
    (map (Int.castRingHom R)) (wittStructureInt p Φ i)

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

Tactic:
· 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 ↦ (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: case refine_1.refl
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
⊢ R

Tactic:
exact x

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
⊢ C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (∑ 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:
frobeniusPolyAux_eq,

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 *
      (MvPolynomial.map (Int.castRingHom ℚ))
        (X (n + 1) -
          ∑ 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.Perfection

Goal state before:
pp: case refine_2.inr.inl
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : n = m + 1
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m

Tactic:
subst h1

Goal state after:
case refine_2.inr.inl
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
x : R
m : ℕ
⊢ (fun m_1 ↦
          if h_1 : m + 1 ≤ m_1 then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (m + 1 - m_1))
        (m + 1) ^
      p =
    (fun m_1 ↦
        if h_1 : m + 1 ≤ m_1 then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (m + 1 - m_1))
      m
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
n✝ : ℕ
⊢ ((map f) (verschiebung x)).coeff (n✝ + 1) = (verschiebung ((map f) x)).coeff (n✝ + 1)

Tactic:
· rfl

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ (x * ↑p).coeff 0 = 0

Tactic:
by
  rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_zero,
    zero_pow hp.out.ne_zero]

Goal state after:
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)
⊢ (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
            ((MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) * C ↑p ^ (j + 1)) *
          ↑((p ^ (n - i)).choose (j + 1)) *
        C ↑p ^ i *
      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)))))

Tactic:
mul_comm (C (p : ℚ))

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)
⊢ (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
            ((MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) * C ↑p ^ (j + 1)) *
          ↑((p ^ (n - i)).choose (j + 1)) *
        C ↑p ^ i *
      C ⅟↑p ^ n =
    (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)))) *
      C ↑p
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝ : CommRing R
⊢ Injective out

Tactic:
by
  intro x y h
  ext i
  rw [WittVector.ext_iff] at h
  simpa only [coeff_out] using h ↑i

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ (teichmullerFun p r).coeff 0 ^ p ^ n = r ^ p ^ n

pp: case h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → ↑p ^ b * (teichmullerFun p r).coeff b ^ p ^ (n - b) = 0

pp: case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0

Tactic:
· rfl

Goal state after:
case h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → ↑p ^ b * (teichmullerFun p r).coeff b ^ p ^ (n - b) = 0

case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: case neg
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : ¬i < n
⊢ 0 = 0

pp: case pos
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : i < n
⊢ TruncatedWittVector.coeff ⟨i, hi⟩ (truncateFun n x) = x.coeff i

Tactic:
· rfl

Goal state after:
case pos
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : i < n
⊢ TruncatedWittVector.coeff ⟨i, hi⟩ (truncateFun n x) = x.coeff i
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ ((map f) (teichmullerFun p r)).coeff 0 = (teichmullerFun p (f r)).coeff 0

pp: case succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n✝ : ℕ
⊢ ((map f) (teichmullerFun p r)).coeff (n✝ + 1) = (teichmullerFun p (f r)).coeff (n✝ + 1)

Tactic:
· rfl

Goal state after:
case succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n✝ : ℕ
⊢ ((map f) (teichmullerFun p r)).coeff (n✝ + 1) = (teichmullerFun p (f r)).coeff (n✝ + 1)
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: case pos
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 : ℕ
hn : P n
⊢ x.coeff n = x.coeff n

pp: case neg
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 : ℕ
hn : ¬P n
⊢ 0 = x.coeff n

Tactic:
· rfl

Goal state after:
case neg
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 : ℕ
hn : ¬P n
⊢ 0 = x.coeff n
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: case neg
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 : ℕ
hn : ¬P n
⊢ y.coeff n = y.coeff n

Tactic:
· rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : verschiebung x = 0
⊢ x = 0

Tactic:
_root_.map_eq_zero_iff _ (verschiebung_injective p k)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x = 0
⊢ x = 0
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.Semiconj ⇑frobenius ⇑(frobeniusEquiv p k).symm ⇑(frobeniusEquiv p k).symm

Tactic:
Function.Semiconj,

Goal state after:
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
⊢ ∀ (x : 𝕎 k), frobenius ((frobeniusEquiv p k).symm x) = (frobeniusEquiv p k).symm (frobenius x)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
i : ℕ
⊢ (map (Ideal.Quotient.mk I) f).coeff i = (X ^ f.natDegree).coeff i

Tactic:
by_cases ne : i = f.natDegree

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
i : ℕ
ne : i = f.natDegree
⊢ (map (Ideal.Quotient.mk I) f).coeff i = (X ^ f.natDegree).coeff i

case neg
R : Type u_1
inst✝ : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
i : ℕ
ne : ¬i = f.natDegree
⊢ (map (Ideal.Quotient.mk I) f).coeff i = (X ^ f.natDegree).coeff i
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * dickson 2 0 (n + 1) = X ^ (n + 2)

Tactic:
dickson_two_zero (n + 1),

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * X ^ (n + 1) = X ^ (n + 2)
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: case e_a.a
n m : ℕ
hm : m ∈ range (n + 1)
⊢ (-X ^ 2) ^ m * X ^ (n - m) * ↑(n.choose m) = n.choose m • (-1) ^ m * X ^ (n + m)

Tactic:
neg_pow,

Goal state after:
case e_a.a
n m : ℕ
hm : m ∈ range (n + 1)
⊢ (-1) ^ m * (X ^ 2) ^ m * X ^ (n - m) * ↑(n.choose m) = n.choose m • (-1) ^ m * X ^ (n + m)
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
⊢ (⇑derivative)^[n] (∑ m ∈ range (n + 1), n.choose m • (-1) ^ m * X ^ (n + m)) =
    ∑ x ∈ range (n + 1), ↑((n + x)! / x !) * C (↑(n.choose x) * (-1) ^ x) * X ^ x

Tactic:
by
    rw [iterate_derivative_sum]
    congr! 1 with x _
    rw [show (n.choose x • (-1) ^ x : ℤ[X]) = C (n.choose x • (-1) ^ x) by simp,
      iterate_derivative_C_mul, iterate_derivative_X_pow_eq_smul,
      descFactorial_eq_div (by lia), show n + x - n = x by lia]
    simp only [Int.reduceNeg, nsmul_eq_mul, eq_intCast, Int.cast_mul, Int.cast_natCast,
      Int.cast_pow, Int.cast_neg, Int.cast_one, zsmul_eq_mul]
    ring

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p.degree ≤ 2
⊢ p = C (p.coeff 2) * X ^ 2 + C (p.coeff 1) * X + C (p.coeff 0)

Tactic:
rw [p.as_sum_range_C_mul_X_pow'
    (Nat.lt_of_le_of_lt (natDegree_le_iff_degree_le.mpr hp) (Nat.lt_add_one 2))]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p.degree ≤ 2
⊢ ∑ i ∈ Finset.range (2 + 1), C (p.coeff i) * X ^ i =
    C ((∑ i ∈ Finset.range (2 + 1), C (p.coeff i) * X ^ i).coeff 2) * X ^ 2 +
        C ((∑ i ∈ Finset.range (2 + 1), C (p.coeff i) * X ^ i).coeff 1) * X +
      C ((∑ i ∈ Finset.range (2 + 1), C (p.coeff i) * X ^ i).coeff 0)
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq { P // P.FG }
P : Submodule R M
hP : P.FG
u : ↥P ⊗[R] N
⊢ (directLimit R M N)
      ((Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃x x_1⦄ h ↦ rTensor N (inclusion h)) ⟨P, hP⟩)
        u) =
    (rTensor N P.subtype) u

Tactic:
by
  apply Submodule.FG.rTensor.directLimit_apply

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
f : A⟦X⟧
hf : constantCoeff f = 1
⊢ constantCoeff f.logOf = 0

Tactic:
rw [logOf_eq]
  have h : MvPowerSeries.constantCoeff (f - 1 : A⟦X⟧) = 0 := by
    rw [map_sub, map_one, ← constantCoeff_eq, hf, sub_self]
  exact constantCoeff_subst_eq_zero h _ constantCoeff_log

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

Goal state before:
pp: case pos
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
⊢ (coeff i) (f - g * H.div f) = (coeff i) (f - g * H.div f)

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
⊢ (coeff i) (f - g * H.div f) = 0

Tactic:
· rfl

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
⊢ (coeff i) (f - g * H.div f) = 0
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
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))) → HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1 + 1))
⊢ HasProjectiveDimensionLT M (n + 1 + 1)

Tactic:
hS.hasProjectiveDimensionLT_X₃_iff n inferInstance

Goal state after:
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
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))) → HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1 + 1))
⊢ HasProjectiveDimensionLT S.X₁ (n + 1)
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✝ : IsSemisimpleModule R M
m : ↥(fullyInvariantSubmodule R M)
S : Submodule R M
x✝ : S ∈ {m_1 | IsSimpleModule R ↥m_1 ∧ m_1 ≤ ↑m}
simple : IsSimpleModule R ↥S
le : S ≤ ↑m
c : ↑(isotypicComponents R M) := ⟨isotypicComponent R M ↥S, ⋯⟩
⊢ ↑c ≤ ⨆ i ∈ {c | ↑c ≤ ↑m}, ↑i

Tactic:
exact le_biSup _ (isFullyInvariant_iff_le_imp_isotypicComponent_le.mp m.2 _ le)

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

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁸ : CommSemiring R₀
inst✝⁷ : Ring R
inst✝⁶ : Algebra R₀ R
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite R M
⊢ ∃ n S d,
    (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧
      (∀ (i : Fin n), NeZero (d i)) ∧
        Nonempty (End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (End R ↥(S i)))

Tactic:
by
  choose d pos S _ simple e using fun c : isotypicComponents R M ↦
    (IsIsotypic.isotypicComponents c.2).submodule_linearEquiv_fun
  exact ⟨_, _, _, fun _ ↦ simple _, fun _ ↦ pos _, ⟨.trans (endAlgEquiv R₀ R M) <| .trans
    (.piCongrRight fun c ↦ ((e c).some.conjAlgEquiv R₀).trans (endVecAlgEquivMatrixEnd ..)) <|
    (.piCongrLeft' R₀ _ (Finite.equivFin _))⟩⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hA : A.coeff 0 = ↑a
⊢ A * { coeff := inverseCoeff a A } = 1

Tactic:
by
    ext n
    induction n with
    | zero => simp [WittVector.mul_coeff_zero, inverseCoeff, hA]
    | succ n => ?_
    let H_coeff := A.coeff (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) +
      nthRemainder p n (truncateFun (n + 1) A) fun i : Fin (n + 1) => inverseCoeff a A i
    have H := Units.mul_inv (a ^ p ^ (n + 1))
    linear_combination (norm := skip) -H_coeff * H
    have ha : (a : k) ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1)) := by norm_cast
    have ha_inv : (↑a⁻¹ : k) ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))⁻¹ := by norm_cast
    simp only [nthRemainder_spec, inverseCoeff, succNthValUnits, hA,
      one_coeff_eq_of_pos, Nat.succ_pos', ha_inv, ha, inv_pow]
    ring!

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ((toPadicInt p).comp (fromPadicInt p)) x = (RingHom.id ℤ_[p]) x

Tactic:
rw [toPadicInt_comp_fromPadicInt]

Goal state after:
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:
by
  have := solution_spec p a₁ a₂
  have := Nat.exists_eq_succ_of_ne_zero hp.out.ne_zero
  grind

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ ↑(univ ×ˢ range (n + 1))
S : Set (Fin 2 × ℕ) := {a | a.2 = n ∨ a.2 < n}
ha' : a ∈ S
⊢ a.2 < n + 1

Tactic:
obtain ⟨ha, ha⟩ := ha'

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : Fin 2 × ℕ
f₀ : (↑↑(univ ×ˢ range (a.2 + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p a.2)
x y : TruncatedWittVector p (a.2 + 1) k
ha : a ∈ ↑(univ ×ˢ range (a.2 + 1))
S : Set (Fin 2 × ℕ) := {a_1 | a_1.2 = a.2 ∨ a_1.2 < a.2}
⊢ a.2 < a.2 + 1

case inr
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ ↑(univ ×ˢ range (n + 1))
S : Set (Fin 2 × ℕ) := {a | a.2 = n ∨ a.2 < n}
h✝ : a.2 < n
⊢ a.2 < n + 1
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
h : ∀ x ∈ s, ¬IsStationary x
⊢ ¬IsStationary (⋃₀ s)

Tactic:
not_isStationary_iff

Goal state after:
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
h : ∀ x ∈ s, ∃ t, IsClub t ∧ Disjoint x t
⊢ ∃ t, IsClub t ∧ Disjoint (⋃₀ s) t
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
h : ∀ x ∈ s, ¬IsStationary x
⊢ ¬IsStationary (⋃₀ s)

Tactic:
not_isStationary_iff

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
h : ∀ x ∈ s, ∃ t, IsClub t ∧ Disjoint x t
⊢ ∃ t, IsClub t ∧ Disjoint (⋃₀ s) t
Module: Mathlib.SetTheory.Ordinal.Commute

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

Tactic:
subst h

Goal state after:
case refine_1.ind
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₂
⊢ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: 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₂

Tactic:
exact ⟨o₂, 0, 1, by simp, by simp⟩

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

Goal state before:
pp: case refine_2.inl
b o✝ o : Ordinal.{u}
ho : o ≠ 0
H : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → (log b o, o / b ^ log b o).1 ≤ log b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).1 ≤ log b o

pp: case refine_2.inr
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.1 ≤ log b o

Tactic:
· rfl

Goal state after:
case refine_2.inr
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.1 ≤ log b o