mathlib-initiative/mathlib-tactics huggingface dataset:
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
m n k : ℕ
hm : (Perfection.coeff (ModP O p) p (max (max m n) k)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max (max m n) k)) g ≠ 0
hk : (Perfection.coeff (ModP O p) p (max (max m n) k)) (f + g) ≠ 0
⊢ valAux K v O p (f + g) ≤
    max (ModP.preVal K v O p ((coeff (max (max m n) k)) f) ^ p ^ max (max m n) k)
      (ModP.preVal K v O p ((coeff (max (max m n) k)) g) ^ p ^ max (max m n) k)

Tactic:
valAux_eq hv hk,

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
m n k : ℕ
hm : (Perfection.coeff (ModP O p) p (max (max m n) k)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max (max m n) k)) g ≠ 0
hk : (Perfection.coeff (ModP O p) p (max (max m n) k)) (f + g) ≠ 0
⊢ ModP.preVal K v O p ((coeff (max (max m n) k)) (f + g)) ^ p ^ max (max m n) k ≤
    max (ModP.preVal K v O p ((coeff (max (max m n) k)) f) ^ p ^ max (max m n) k)
      (ModP.preVal K v O p ((coeff (max (max m n) k)) g) ^ p ^ max (max m n) k)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: 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₁
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
k₁✝ : ℕ
⊢ ∀ (k₂ : ℕ) (hk : k₁✝ ≤ k₂),
    (TruncatedWittVector.truncate hk).comp ((fun k ↦ (truncate k).comp g) k₂) = (fun k ↦ (truncate k).comp g) k₁✝

Tactic:
_

Goal state after:
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₁
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
k₁✝ k₂✝ : ℕ
⊢ ∀ (hk : k₁✝ ≤ k₂✝),
    (TruncatedWittVector.truncate hk).comp ((fun k ↦ (truncate k).comp g) k₂✝) = (fun k ↦ (truncate k).comp g) k₁✝
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: case insert
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ insert a S' ∧ (x r).coeff n ≠ 0}
n : ℕ
this✝ : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ S' ∧ (x r).coeff n ≠ 0}
hind : ∀ (n : ℕ), (∑ s ∈ S', x s).coeff n = ∑ s ∈ S', (x s).coeff n
this : ∀ (n : ℕ), (x a).coeff n = 0 ∨ (∑ s ∈ S', x s).coeff n = 0
⊢ (x a + ∑ s ∈ S', x s).coeff n = (x a).coeff n + ∑ s ∈ S', (x s).coeff n

Tactic:
coeff_add_of_disjoint n _ _ this,

Goal state after:
case insert
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ insert a S' ∧ (x r).coeff n ≠ 0}
n : ℕ
this✝ : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ S' ∧ (x r).coeff n ≠ 0}
hind : ∀ (n : ℕ), (∑ s ∈ S', x s).coeff n = ∑ s ∈ S', (x s).coeff n
this : ∀ (n : ℕ), (x a).coeff n = 0 ∨ (∑ s ∈ S', x s).coeff n = 0
⊢ (x a).coeff n + (∑ s ∈ S', x s).coeff n = (x a).coeff n + ∑ s ∈ S', (x s).coeff n
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + k)
⊢ (hermite (n + 1)).coeff k = 0

Tactic:
cases k with
    | zero =>
      rw [Nat.succ_add_eq_add_succ] at hnk
      rw [coeff_hermite_succ_zero, ih hnk, neg_zero]
    | succ k =>
      rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]
      · rwa [Nat.succ_add_eq_add_succ] at hnk
      · rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk
        exact (Nat.odd_add.mp hnk).mpr even_two

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

Goal state before:
pp: case succ
F : Type u_1
inst✝ : Field F
p q : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (p + q).support, (p + q).coeff i • preHilbertPoly F d i) =
    (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i) +
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ q.support, q.coeff i • preHilbertPoly F d i
⊢ (match d + 1 with
    | 0 => 0
    | d.succ => ∑ i ∈ (p + q).support, (p + q).coeff i • preHilbertPoly F d i) =
    (match d + 1 with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i) +
      match d + 1 with
      | 0 => 0
      | d.succ => ∑ i ∈ q.support, q.coeff i • preHilbertPoly F d i

Tactic:
simp only
      rw [← sum_def _ fun _ r => r • _]
      exact sum_add_index _ _ _ (fun _ => zero_smul ..) (fun _ _ _ => add_smul ..)

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

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

Tactic:
by
  ext n
  have : (n + 1) = algebraMap ℚ A (n + 1) := by simp
  rw [coeff_derivative, coeff_log, coeff_mk]
  grind

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:
Ideal.mul_top,

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.TensorProduct.DirectLimitFG

Goal state before:
pp: case h.right
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0 →
    ∃ B, B.FG ∧ ∃ (x : A ≤ B), (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
hu'✝ : (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' : (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
⊢ (rTensor M (B.val.toLinearMap ∘ₗ (Subalgebra.inclusion hAB).toLinearMap)) u = t

Tactic:
← hu

Goal state after:
case h.right
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0 →
    ∃ B, B.FG ∧ ∃ (x : A ≤ B), (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
hu'✝ : (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' : (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
⊢ (rTensor M (B.val.toLinearMap ∘ₗ (Subalgebra.inclusion hAB).toLinearMap)) u = (rTensor M A.val.toLinearMap) u
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:
Ideal.mul_top,

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.Regular.ProjectiveDimension

Goal state before:
pp: 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)
n✝ n : ℕ
S : ShortComplex (ModuleCat R) := M.smulShortComplex x
hS : S.ShortExact
h : HasProjectiveDimensionLE (of R (QuotSMulTop x ↑M)) (n + 1)
L : ModuleCat R
⊢ Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))

Tactic:
_

Goal state after:
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)
n✝ n : ℕ
S : ShortComplex (ModuleCat R) := M.smulShortComplex x
hS : S.ShortExact
h : HasProjectiveDimensionLE (of R (QuotSMulTop x ↑M)) (n + 1)
L : ModuleCat R
a✝ : Module.Finite R ↑L
⊢ Subsingleton (Ext M L (n + 1))
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: case e'_2
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ toFun R f ∘ ⇑(TensorProduct.lid R M).symm) x =
    (rTensor N (Algebra.ofId R S).toLinearMap) (toFun R f (1 ⊗ₜ[R] x))

pp: case e'_3
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (rTensor M (Algebra.ofId R S).toLinearMap) (1 ⊗ₜ[R] x)

Tactic:
· simp only [Function.comp_apply, TensorProduct.lid_symm_apply, TensorProduct.includeRight_lid]
    congr

Goal state after:
case e'_3
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (rTensor M (Algebra.ofId R S).toLinearMap) (1 ⊗ₜ[R] x)
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✝ : IsAdicComplete I A
r : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
h1 : (H.mod ↑r).degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
h2 : ↑r = g * H.div ↑r + ↑(H.mod ↑r)
⊢ g * H.div ↑r + ↑(H.mod ↑r) = g * 0 + ↑r

Tactic:
simpa using h2.symm

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
H : g.IsWeierstrassDivisorAt I
inst✝ : IsAdicComplete I A
r : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
h1 : (H.mod ↑r).degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
h2 : ↑r = g * H.div ↑r + ↑(H.mod ↑r)
⊢ H.div ↑r = 0

Tactic:
exact (H.eq_of_mul_add_eq_mul_add (q := H.div r) (q' := 0) h1 hr (by simpa using h2.symm)).1

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}
b : A[X]
hb : b * g = a
⊢ ∃ a_1, a_1 * ↑g = ↑a

Tactic:
exact ⟨b, by simp [← hb]⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
⊢ IsRegularRing R[X]

Tactic:
apply isRegularRing_iff.mpr (fun p hp ↦ ?_)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
⊢ IsRegularLocalRing (Localization.AtPrime p)
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
⊢ IsRegularRing R[X]

Tactic:
by
  apply isRegularRing_iff.mpr (fun p hp ↦ ?_)
  let q := p.comap C
  let S := (Localization.AtPrime q)[X]
  let pc := Submonoid.map Polynomial.C.toMonoidHom q.primeCompl
  let : Algebra R[X] S := algebra R (Localization.AtPrime q)
  have : IsLocalization pc S := Polynomial.isLocalization _ _
  let pS := p.map (algebraMap R[X] S)
  have disj : Disjoint (pc : Set R[X]) (p : Set R[X]) := by
    simpa [pc, q] using! Set.disjoint_image_left.mpr
      (Set.disjoint_compl_left_iff_subset.mpr (fun _ a ↦ a))
  have : pS.IsPrime := IsLocalization.isPrime_of_isPrime_disjoint pc _ _ ‹_› disj
  have : IsLocalization.AtPrime (Localization.AtPrime pS) p := by
    convert IsLocalization.isLocalization_isLocalization_atPrime_isLocalization pc
      (Localization.AtPrime pS) pS
    exact (IsLocalization.under_map_of_isPrime_disjoint pc _ ‹_› disj).symm
  have := isRegularRing_iff.mp ‹_› q
  have eq : comap C pS = maximalIdeal (Localization.AtPrime q) := by
    rw [← IsLocalization.map_under q.primeCompl _ (comap C pS),
      ← IsLocalization.map_under q.primeCompl _ (maximalIdeal (Localization.AtPrime q))]
    simp only [comap_comap, S, pS]
    rw [← Polynomial.algebraMap_eq (R := Localization.AtPrime q),
      ← IsScalarTower.algebraMap_eq R (Localization.AtPrime q) (Localization.AtPrime q)[X],
      IsScalarTower.algebraMap_eq R R[X] (Localization.AtPrime q)[X], ← comap_comap,
      ← Ideal.under_def R[X], IsLocalization.under_map_of_isPrime_disjoint pc _ ‹_› disj]
    simp [q, IsLocalization.AtPrime.under_maximalIdeal (Localization.AtPrime q) q]
  have := isRegularLocalRing_localization_atPrime_of_comap_eq_maximalIdeal _ pS eq
  exact IsRegularLocalRing.of_ringEquiv (IsLocalization.algEquiv p.primeCompl
    (Localization.AtPrime pS) (Localization.AtPrime p)).toRingEquiv

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

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

Tactic:
rw [wittPolyProdRemainder]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ i ∈ range n, ↑p ^ i * wittMul p i ^ p ^ (n - i)).vars ⊆ univ ×ˢ range n
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ↑p ^ (n + 1) * X (1, n + 1) *
        ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    remainder p n

Tactic:
1,

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
      ↑p ^ (n + 1) * X (0, n + 1) *
        ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    ↑p ^ (n + 1) * X (1, n + 1) *
      ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
      ↑p ^ (n + 1) * X (0, n + 1) *
        ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    ↑p ^ (n + 1) * X (1, n + 1) *
      ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))

Tactic:
1,

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
    ↑p ^ (n + 1) * X (0, n + 1) *
      ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (1, n + 1)) +
      ↑p ^ (n + 1) * X (1, n + 1) *
        ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    remainder p n

Tactic:
1,

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
      ↑p ^ (n + 1) * X (0, n + 1) *
        (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
          ↑p ^ (n + 1) * X (1, n + 1)) +
    ↑p ^ (n + 1) * X (1, n + 1) *
      ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
s : Set (Set α)
inst✝ : OrderTop α
hs : ∀ x ∈ s, IsClub x
⊢ IsClub (⋂₀ s)

Tactic:
refine ⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, ?_⟩

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
s : Set (Set α)
inst✝ : OrderTop α
hs : ∀ x ∈ s, IsClub x
⊢ IsCofinal (⋂₀ s)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

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

Tactic:
by
  simp [CNF.ne_zero ho]

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

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

Tactic:
by
  simp [CNF.ne_zero ho]

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

Goal state before:
pp: case left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ x ≤ ⨆ b, lfpApprox f x ↑b

Tactic:
refine le_iSup_of_le ⟨0, ha.bot_lt⟩ (by simp [lfpApprox_zero])

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case cons'
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b b✝ : Bool
a : Lists' α b✝
l : Lists' α true
IH₁ :
  C ⟨b✝, a⟩ ×'
    match b✝, a with
    | true, l => D l
    | false, x => PUnit
IH :
  C ⟨true, l⟩ ×'
    match true, l with
    | true, l => D l
    | false, x => PUnit
this : D (a.cons' l)
⊢ C ⟨true, a.cons' l⟩ ×'
    match true, a.cons' l with
    | true, l => D l
    | false, x => PUnit

Tactic:
exact ⟨C1 _ this, this⟩

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
⊢ lfpApprox f x i ≤ a

Tactic:
induction i using WellFoundedLT.induction with

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
⊢ lfpApprox f x i ≤ a
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr.inl
b : Ordinal.{u_1}
hb : b ≤ 1
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ (coeff b o) 0 = (single 0 o) 0

Tactic:
apply coeff_of_mem_CNF
      rw [CNF.of_le_one hb ho]
      simp

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

Goal state before:
pp: case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
e' : Ordinal.{u_1}
he' : e' ∈ f.support.sort fun x1 x2 ↦ x1 ≥ x2
⊢ ∀ (b_1 : Ordinal.{u_1}), b ^ e' * ((single e x) e' + f e') + b_1 = b ^ e' * f e' + b_1

Tactic:
_

Goal state after:
case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
e' : Ordinal.{u_1}
he' : e' ∈ f.support.sort fun x1 x2 ↦ x1 ≥ x2
b✝ : Ordinal.{u_1}
⊢ b ^ e' * ((single e x) e' + f e') + b✝ = b ^ e' * f e' + b✝
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
⊢ coeff b (eval b (single e x + f)) = single e x + f

Tactic:
have IH' (e') : f e' < b := by
      by_cases he' : e' ∈ f.support
      · apply (hf e').trans_eq'
        rw [add_apply, single_eq_of_ne, zero_add]
        exact (hf' _ he').ne
      · rw [notMem_support_iff.1 he']
        exact hb.pos

Goal state after:
case single_add
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ coeff b (eval b (single e x + f)) = single e x + f
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x z : PSet.{u_1}
⊢ z ∈ x → z ∈ (⋃₀ x).powerset

Tactic:
_

Goal state after:
x z : PSet.{u_1}
a✝ : z ∈ x
⊢ z ∈ (⋃₀ x).powerset
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x z : PSet.{u_1}
a✝ : z ∈ x
z✝ : PSet.{u_1}
⊢ z✝ ∈ z → z✝ ∈ ⋃₀ x

Tactic:
_

Goal state after:
x z : PSet.{u_1}
a✝¹ : z ∈ x
z✝ : PSet.{u_1}
a✝ : z✝ ∈ z
⊢ z✝ ∈ ⋃₀ x
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: a : Ordinal.{u}
h : a < ω ^ a
⊢ ω ^ a = veblen 0 a

Tactic:
veblen_zero_apply

Goal state after:
a : Ordinal.{u}
h : a < ω ^ a
⊢ ω ^ a = ω ^ a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case refine_1.inl
a x : Ordinal.{u}
h : a < (fun a ↦ ω ^ a) a
this : a.invVeblen₁ = 0
⊢ veblen 0 a = ω ^ x → x.invVeblen₁ = 0 ∧ x.invVeblen₂ = a

Tactic:
have := invVeblen₂_of_lt_opow h

Goal state after:
case refine_1.inl
a x : Ordinal.{u}
h : a < (fun a ↦ ω ^ a) a
this✝ : a.invVeblen₁ = 0
this : a.invVeblen₂ = a
⊢ veblen 0 a = ω ^ x → x.invVeblen₁ = 0 ∧ x.invVeblen₂ = a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case refine_2
o a x : Ordinal.{u}
h : a < veblen o a
x✝ : x.invVeblen₁ = o ∧ x.invVeblen₂ = a
hx : x.invVeblen₁ = o
ha : x.invVeblen₂ = a
⊢ veblen o a = ω ^ x

Tactic:
· convert! ← veblen_invVeblen₁_invVeblen₂ x

Goal state after:
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x✝ x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
o : Ordinal.{u}
h : o < x.rank
⊢ lift.{u + 1, u} o < ⨆ i, succ (lift.{u + 1, u} (↑i).rank)

Tactic:
simpa [Ordinal.lt_iSup_iff] using lt_rank_iff.1 h

Goal state after:
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x y : ZFSet.{u_1}
⊢ (x ∪ y).rank ≤ max x.rank y.rank

Tactic:
simp_rw [rank_le_iff, mem_union, lt_max_iff]
    intro
    apply Or.imp <;> apply rank_lt_of_mem

Goal state after:
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x z : ZFSet.{u_1}
⊢ z ∈ x → z ∈ (⋃₀ x).powerset

Tactic:
_

Goal state after:
x z : ZFSet.{u_1}
a✝ : z ∈ x
⊢ z ∈ (⋃₀ x).powerset
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x z : ZFSet.{u_1}
a✝ : z ∈ x
x✝ : ZFSet.{u_1}
⊢ x✝ ∈ z → x✝ ∈ ⋃₀ x

Tactic:
_

Goal state after:
x z : ZFSet.{u_1}
a✝¹ : z ∈ x
x✝ : ZFSet.{u_1}
a✝ : x✝ ∈ z
⊢ x✝ ∈ ⋃₀ x