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

Goal state before:
pp: case zero
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
h : ∃ n, (coeff n) f ≠ 0
hfn : (coeff (Nat.find h + 0)) f ≠ 0
⊢ ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O p ((coeff (Nat.find h + 0)) f) ^ p ^ (Nat.find h + 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k : ℕ
⊢ ((⇑frobenius)^[0] x).coeff k = x.coeff k ^ p ^ 0

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ (⇑verschiebung ∘ ⇑frobenius)^[0] x = x * ↑p ^ 0

Tactic:
| zero =>

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

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

Tactic:
rw [← hx, ← hy, select_add_select_not P z]

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

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

Tactic:
simp only [z, mk.eq_1]
      split_ifs with y0
      · rw [y0, add_zero]
      · rw [h n |>.resolve_right y0, zero_add]

Goal state after:
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
x : R♭
⊢ (fontaineTheta R p) ((teichmuller p) x) = untilt x

Tactic:
rw [IsHausdorff.eq_iff_smodEq (I := 𝔭)]

Goal state after:
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
x : R♭
⊢ ∀ (n : ℕ), (fontaineTheta R p) ((teichmuller p) x) ≡ untilt x [SMOD 𝔭 ^ n • ⊤]
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

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

Tactic:
apply_fun PowerSeries.coeff g.natDegree at H

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f h : R⟦X⟧
g : R[X]
distinguish : g.IsDistinguishedAt I
notMem : PowerSeries.constantCoeff h ∉ I
eq : f = ↑g * h
mapf : (PowerSeries.map (Ideal.Quotient.mk I)) f = ↑(X ^ g.natDegree) * (PowerSeries.map (Ideal.Quotient.mk I)) h
H : (PowerSeries.coeff g.natDegree) ((PowerSeries.map (Ideal.Quotient.mk I)) f) = (PowerSeries.coeff g.natDegree) 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case zero
⊢ hermite 0 = (fun p ↦ X * p - derivative p)^[0] 1

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case zero
k : ℕ
⊢ (hermite 0).coeff (0 + k + 1) = 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case zero
⊢ (hermite 0).coeff 0 = 1

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n : ℕ
⊢ (hermite n).coeff n = 1

Tactic:
induction n with
  | zero => exact coeff_C
  | succ n ih =>
    rw [coeff_hermite_succ_succ, ih, coeff_hermite_of_lt, mul_zero, sub_zero]
    simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case zero
k : ℕ
hnk : Odd (0 + k)
⊢ (hermite 0).coeff k = 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

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

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

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

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
⊢ (hermite (2 * (n + 1) + (k + 1))).coeff (k + 1) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + (k + 1)).choose (k + 1))

Tactic:
let hermite_explicit : ℕ → ℕ → ℤ := fun n k =>
      (-1) ^ n * (2 * n - 1)‼ * Nat.choose (2 * n + k) k

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

Goal state before:
pp: case zero
F : Type u_1
inst✝ : Field F
⊢ (match 0 with
    | 0 => 0
    | d.succ => ∑ i ∈ support 0, coeff 0 i • preHilbertPoly F d i) =
    0

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
⊢ (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F 0)) =
    eval (↑n)
      (match 0 with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)

Tactic:
| zero =>

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

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

Tactic:
(opRingEquiv R).isLeftCancelMulZero_iff,

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

Goal state before:
pp: case zero
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ (p * (1 - X) ^ 0).hilbertPoly (d + 0) = p.hilbertPoly d

Tactic:
| zero =>

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d e : ℕ
⊢ (p * (1 - X) ^ e).hilbertPoly (d + e) = p.hilbertPoly d

Tactic:
induction e with

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

Goal state before:
pp: case zero
⊢ (coeff 0) (catalanSeries ^ 2 * X + 1) = (coeff 0) catalanSeries

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
⊢ IsRestricted c f ↔ Tendsto (fun t ↦ ‖(coeff t) f‖ * c ^ t) cofinite (𝓝 0)

Tactic:
IsRestricted,

Goal state after:
R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
⊢ MvPowerSeries.IsRestricted (fun x ↦ c) f ↔ Tendsto (fun t ↦ ‖(coeff t) f‖ * c ^ t) cofinite (𝓝 0)
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
⊢ radical n = 1 ↔ n ≤ 1

Tactic:
rw [← radical_le_one_iff]
  grind [radical_pos n]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
inst✝ : IsLocalRing A
hg : (map (IsLocalRing.residue A)) g ≠ 0
⊢ (coeff ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) g).order.toNat) g ∉ IsLocalRing.maximalIdeal A

Tactic:
have h := coeff_order hg

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
inst✝ : IsLocalRing A
hg : (map (IsLocalRing.residue A)) g ≠ 0
h : (coeff ((map (IsLocalRing.residue A)) g).order.toNat) ((map (IsLocalRing.residue A)) g) ≠ 0
⊢ (coeff ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) g).order.toNat) g ∉ IsLocalRing.maximalIdeal A
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case zero
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
i : ℕ
hi : i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i) (f - g * H.seq f 0) ∈ I ^ 0

Tactic:
| zero =>

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
f : A⟦X⟧
k i✝ : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i✝ ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
key : f - g * q' = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹
i : ℕ
⊢ ∀ (i : ℕ), (coeff i) ↑((trunc n) g) ∈ I

Tactic:
simp [n, g.coeff_trunc_order_mem]

Goal state after:
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) ≡ 0 [SMOD I ^ k • ⊤]

Tactic:
SModEq.zero,

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
inst✝ : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
hi : ¬i < ((map (Ideal.Quotient.mk I)) g).order.toNat
k : ℕ
⊢ (coeff i) (f - g * H.div f) ∈ I ^ k • ⊤
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = ↑r
this : ∀ (k i : ℕ), (coeff i) q ∈ I ^ k
i k : ℕ
⊢ (coeff i) q ≡ 0 [SMOD I ^ k • ⊤]

Tactic:
SModEq.zero,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = ↑r
this : ∀ (k i : ℕ), (coeff i) q ∈ I ^ k
i k : ℕ
⊢ (coeff i) q ∈ I ^ k • ⊤
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case zero
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = ↑r
⊢ ∀ (i : ℕ), (coeff i) q ∈ I ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: case zero
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L 0)
⊢ HasProjectiveDimensionLT M 0

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
M : Type u_1
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
⊢ ⇑(rTensor N h.toLinearMap) ∘ toFun S f = toFun T f ∘ ⇑(rTensor M h.toLinearMap)

Tactic:
by
  ext t
  simp only [Function.comp_apply, PolynomialLaw.isCompat_apply]

Goal state after:
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: case zero
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Small.{v, u} R
inst✝³ : IsLocalRing R
inst✝² : IsNoetherianRing R
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
reg : IsWeaklyRegular (↑M) rs
mem : ∀ r ∈ rs, r ∈ maximalIdeal R
len : rs.length = 0
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑0

Tactic:
| zero =>

Goal state after:
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✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
reg : IsWeaklyRegular (↑M) rs
mem : ∀ r ∈ rs, r ∈ maximalIdeal R
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑rs.length

Tactic:
generalize len : rs.length = n
  induction n generalizing M rs with
  | zero =>
    rw [List.length_eq_zero_iff.mp len, Ideal.ofList_nil, Submodule.bot_smul]
    simpa using projectiveDimension_eq_of_iso (Submodule.quotEquivOfEqBot ⊥ rfl).toModuleIso
  | succ n hn =>
    match rs with
    | [] => simp at len
    | x :: rs' =>
      simp only [List.mem_cons, forall_eq_or_imp] at mem
      simp only [isWeaklyRegular_cons_iff] at reg
      have := nontrivial_quotSMulTop_of_mem_maximalIdeal M mem.1
      simp only [List.length_cons, Nat.add_right_cancel_iff] at len
      rw [Nat.cast_add, Nat.cast_one, projectiveDimension_eq_of_iso
        (Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner M x rs').toModuleIso, add_comm _ 1,
        ← add_assoc, ← projectiveDimension_quotSMulTop_eq_succ_of_isSMulRegular M x reg.1 mem.1,
        ← hn (ModuleCat.of R (QuotSMulTop x M)) rs' reg.2 mem.2 len]

Goal state after:
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 S
⊢ IsSemisimpleModule R ↥(⨆ a ∈ {m | Nonempty (↥m ≃ₗ[R] S)}, a)

Tactic:
refine isSemisimpleModule_biSup_of_isSemisimpleModule_submodule fun m ⟨e⟩ ↦ ?_

Goal state after:
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 S
m : Submodule R M
x✝ : m ∈ {m | Nonempty (↥m ≃ₗ[R] S)}
e : ↥m ≃ₗ[R] S
⊢ IsSemisimpleModule R ↥m
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝¹ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝ : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this : pS.IsPrime
⊢ IsLocalization.AtPrime (Localization.AtPrime pS) p

Tactic:
convert IsLocalization.isLocalization_isLocalization_atPrime_isLocalization pc
      (Localization.AtPrime pS) pS

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝¹ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝ : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this : pS.IsPrime
⊢ p = comap (algebraMap R[X] S) pS
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
⊢ ∀ (a b : (ValueGroupWithZero R)ˣ), a = b

Tactic:
intro a

Goal state after:
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a : (ValueGroupWithZero R)ˣ
⊢ ∀ (b : (ValueGroupWithZero R)ˣ), a = b
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✝
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Algebra K A
ΓR : Type u_6
ΓA : Type u_7
ΓK : Type u_8
inst✝³ : LinearOrderedCommGroupWithZero ΓR
inst✝² : LinearOrderedCommGroupWithZero ΓK
inst✝¹ : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vK : Valuation K ΓK
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
⊢ ∀ x ∈ vR.integer, (algebraMap R A) x ∈ vA.integer

Tactic:
simp [Valuation.mem_integer_iff, val_map_le_one_iff vR vA]

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

Goal state before:
pp: case zero
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 }).coeff 0 = coeff 1 0

Tactic:
| zero =>

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ (fromPadicInt p).comp (toPadicInt p) = RingHom.id (𝕎 (ZMod p))

Tactic:
by
  apply WittVector.hom_ext
  intro n
  rw [fromPadicInt, ← RingHom.comp_assoc, truncate_comp_lift, RingHom.comp_assoc]
  simp only [toPadicInt, toZModPow, RingHom.comp_id, PadicInt.lift_spec, RingHom.id_comp, ←
    RingHom.comp_assoc, RingEquiv.toRingHom_comp_symm_toRingHom]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.NatCount

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ↑(count p n) ≤ {k | p k}.encard

Tactic:
simp only [Set.encard, ENat.card, Set.coe_ofPred, Cardinal.natCast_le_toENat]

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ↑(count p n) ≤ Cardinal.mk { k // p k }
Module: Mathlib.SetTheory.Cardinal.NatCount

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ↑(count p n) ≤ Cardinal.mk { k // p k }

Tactic:
exact Nat.count_le_cardinal n

Goal state after:
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: case refine_1
x✝ : ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : lift.{u + 1, max u (v + 1)} univ.{v, u} ≤ lift.{u + 1, max u (v + 1)} (lift.{v + 1, u} #α)
⊢ univ.{v, u + 1} < univ.{u, v + 1}

Tactic:
lift_univ,

Goal state after:
case refine_1
x✝ : ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, u + 1} ≤ lift.{u + 1, max u (v + 1)} (lift.{v + 1, u} #α)
⊢ univ.{v, u + 1} < univ.{u, v + 1}
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: case h
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ lift.{u + 1, max u (v + 1)} univ.{v, u} ≤ lift.{u + 1, max u (v + 1)} (lift.{v + 1, u} #α)

Tactic:
lift_univ,

Goal state after:
case h
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ univ.{v, u + 1} ≤ lift.{u + 1, max u (v + 1)} (lift.{v + 1, u} #α)
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
⊢ y ∈ pullSub T x → ∃ z ∈ T, y = x ++ z

Tactic:
by
    intro ⟨h1, h2⟩; use y.drop x.length, h2
    nth_rw 1 [← List.take_append_drop x.length y]
    simpa [-List.take_append_drop, List.prefix_iff_eq_take, hl] using h1

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

Goal state before:
pp: b o : Ordinal.{u_2}
C : Ordinal.{u_2} → Sort u_1
ho : o ≠ 0
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ (if h : o = 0 then ⋯ ▸ H0 else H o h (CNF.rec b H0 H (o % b ^ log b o))) = H o ho (CNF.rec b H0 H (o % b ^ log b o))

Tactic:
dif_neg

Goal state after:
b o : Ordinal.{u_2}
C : Ordinal.{u_2} → Sort u_1
ho : o ≠ 0
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ H o ?hnc (CNF.rec b H0 H (o % b ^ log b o)) = H o ho (CNF.rec b H0 H (o % b ^ log b o))

case hnc
b o : Ordinal.{u_2}
C : Ordinal.{u_2} → Sort u_1
ho : o ≠ 0
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ ¬o = 0
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
⊢ Monotone (lfpApprox f x)

Tactic:
intro a

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
⊢ ∀ ⦃b : Ordinal.{u}⦄, a ≤ b → lfpApprox f x a ≤ lfpApprox f x b
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case ofList.cons
α : Type u_1
l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ (a : Lists α), a ∈ (ofList t).toList → a ∈ l₂) → ofList t ⊆ l₂
H : ∀ (a : Lists α), a ∈ (ofList (h :: t)).toList → a ∈ l₂
⊢ ofList (h :: t) ⊆ l₂

Tactic:
simp only [to_ofList, ofList, toList_cons, List.mem_cons, forall_eq_or_imp] at *
      exact cons_subset.2 ⟨H.1, t_ih H.2⟩

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C0
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : α), trans (atom a)

Tactic:
intro a

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

Goal state before:
pp: case D1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : Lists α) (l : Lists' α true),
    trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'

Tactic:
intro a

Goal state after:
case D1
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : Lists α
⊢ ∀ (l : Lists' α true),
    trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: 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
⊢ ⨆ b, ⨆ (_ : b < i), f (lfpApprox f x b) ≤ a

Tactic:
iSup₂_le_iff,

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
⊢ ∀ i_1 < i, f (lfpApprox f x i_1) ≤ a