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

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
i : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
⊢ (ModuleCat.matrixEquivalence R i).functor.map (r • f) = r • (ModuleCat.matrixEquivalence R i).functor.map f

Tactic:
by
    ext (v : ι → X)
    simp only [ModuleCat.matrixEquivalence_functor, ModuleCat.toMatrixModCat_obj_carrier,
      ModuleCat.toMatrixModCat_map, ModuleCat.hom_smul, ModuleCat.hom_ofHom, LinearMap.smul_apply]
    ext i
    simp only [LinearMap.mapMatrixModule_apply, LinearMap.compLeft_apply, Function.comp_apply,
      LinearMap.smul_apply]
    change _ = ((algebraMap R₀ (Matrix ι ι R) r) • ((ModuleCat.Hom.hom f).mapMatrixModule ι v)) i
    simp [Matrix.algebraMap_matrix_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
a : R
⊢ IsRestricted c (C a)

Tactic:
simpa [monomial_zero_eq_C_apply] using isRestricted_monomial c 0 a

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((Polynomial.C.comp MvPolynomial.C) (MvPolynomial.coeff v f)).leadingCoeff *
      ∏ i, ((MvPolynomial.finSuccEquiv k n) ((T f) (MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

Tactic:
coe_comp

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((⇑Polynomial.C ∘ ⇑MvPolynomial.C) (MvPolynomial.coeff v f)).leadingCoeff *
      ∏ i, ((MvPolynomial.finSuccEquiv k n) ((T f) (MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j + n - m = i + j + (n - i - m)

Tactic:
add_comm i j,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j + n - m = j + i + (n - i - m)
Module: Mathlib.RingTheory.WittVector.MulP

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ (x * ↑(n + 1)).coeff k = (aeval x.coeff) (wittMulN p (n + 1) k)

Tactic:
rw [wittMulN, Nat.cast_add, Nat.cast_one, mul_add, mul_one, aeval_bind₁, add_coeff]
    apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
    ext1 ⟨b, i⟩
    fin_cases b
    · simp [Function.uncurry, Matrix.cons_val_zero, ih]
    · simp [Function.uncurry, Matrix.cons_val_one, aeval_X]

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

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ (-x✝).coeff n = (aeval x✝.coeff) ((fun n ↦ (rename Prod.snd) (wittNeg p n)) n)

Tactic:
rw [neg_coeff, aeval_eq_eval₂Hom, eval₂Hom_rename]

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ peval (wittNeg p n) ![x✝.coeff] = (eval₂Hom (algebraMap ℤ R✝) (x✝.coeff ∘ Prod.snd)) (wittNeg p n)
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
h : (↑p ^ i).coeff i = 1
⊢ (verschiebung (↑p ^ i)).coeff (i + 1) ^ p = 1

Tactic:
verschiebung_coeff_succ,

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
h : (↑p ^ i).coeff i = 1
⊢ (↑p ^ i).coeff i ^ p = 1
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → (↑p ^ i).coeff j = 0
n✝ : ℕ
hj : n✝ + 1 ≠ i + 1
⊢ (verschiebung (↑p ^ i)).coeff (n✝ + 1) ^ p = 0

Tactic:
verschiebung_coeff_succ,

Goal state after:
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → (↑p ^ i).coeff j = 0
n✝ : ℕ
hj : n✝ + 1 ≠ i + 1
⊢ (↑p ^ i).coeff n✝ ^ p = 0
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n✝ : ℕ
⊢ (verschiebung (frobenius x)).coeff (n✝ + 1) = x.coeff n✝ ^ p

Tactic:
verschiebung_coeff_succ,

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n✝ : ℕ
⊢ (frobenius x).coeff n✝ = x.coeff n✝ ^ p
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ (verschiebung ((⇑verschiebung)^[n] x)).coeff (m' + 1) = 0

Tactic:
verschiebung_coeff_succ,

Goal state after:
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ ((⇑verschiebung)^[n] x).coeff m' = 0
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (x y : R), teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y

Tactic:
by
    intro x y
    rcases counit_surjective R x with ⟨x, rfl⟩
    rcases counit_surjective R y with ⟨y, rfl⟩
    simp only [← map_teichmullerFun, ← map_mul, teichmuller_mul_aux₂]

Goal state after:
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₁
⊢ Function.LeftInverse (fun g ↦ ⟨fun k ↦ (truncate k).comp g, ⋯⟩) fun f ↦ lift ↑f ⋯

Tactic:
rintro ⟨f, hf⟩; simp only [truncate_comp_lift]

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
n : ℕ
⊢ (∃ c, x = c * ↑p ^ n) ↔ ∀ m < n, x.coeff m = 0

Tactic:
refine ⟨fun ⟨u, hu⟩ m hm ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
x✝ : ∃ c, x = c * ↑p ^ n
m : ℕ
hm : m < n
u : 𝕎 k
hu : x = u * ↑p ^ n
⊢ x.coeff m = 0

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
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

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

Tactic:
rw [hermite_succ, coeff_sub, coeff_X_mul, coeff_derivative, mul_comm]

Goal state after:
n k : ℕ
⊢ (hermite n).coeff k - (↑(k + 1) + 1) * (hermite n).coeff (k + 1 + 1) =
    (hermite n).coeff k - (↑k + 2) * (hermite n).coeff (k + 2)
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
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
ht : (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)
⊢ (rTensor N (h.comp φ).toLinearMap) (f.toFun' A p) = (rTensor N ψ.toLinearMap) (f.toFun' B q)

Tactic:
← φ.val_comp_rangeRestrict,

Goal state after:
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
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
ht : (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)
⊢ (rTensor N (h.comp (φ.range.val.comp φ.rangeRestrict)).toLinearMap) (f.toFun' A p) =
    (rTensor N ψ.toLinearMap) (f.toFun' B q)
Module: Mathlib.RingTheory.Regular.Free

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
kerf : f.ker = x • ⊤
fg : g.ker.FG
⊢ g.ker ≤ x • g.ker

Tactic:
intro y

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
kerf : f.ker = x • ⊤
fg : g.ker.FG
y : I →₀ R
⊢ y ∈ g.ker → y ∈ x • g.ker
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
by_cases eqbot : p = ⊥

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : p = ⊥
⊢ IsRegularLocalRing (Localization.AtPrime p)

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : ¬p = ⊥
⊢ IsRegularLocalRing (Localization.AtPrime p)
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
a✝ : Module.Finite R ↑L
zero : Subsingleton (Ext (of R (QuotSMulTop x ↑M)) L (n + 2))
exac :
  { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
      X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.Exact
this✝ : S.f = x • 𝟙 M
epi : Function.Surjective ⇑((Ext.mk₀ (x • 𝟙 M)).precomp L ⋯)
ntr : Nontrivial (Ext M L (n + 1))
this : x ∈ (annihilator R (Ext M L (n + 1))).jacobson
⊢ ⊤ ≤ x • ⊤

Tactic:
intro y

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
zero : Subsingleton (Ext (of R (QuotSMulTop x ↑M)) L (n + 2))
exac :
  { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
      X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.Exact
this✝ : S.f = x • 𝟙 M
epi : Function.Surjective ⇑((Ext.mk₀ (x • 𝟙 M)).precomp L ⋯)
ntr : Nontrivial (Ext M L (n + 1))
this : x ∈ (annihilator R (Ext M L (n + 1))).jacobson
y : Ext M L (n + 1)
⊢ y ∈ ⊤ → y ∈ x • ⊤
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
inst✝ : IsAdicComplete I A
⊢ Ideal.span {↑f} = Ideal.span {g}

Tactic:
rw [H.eq_mul, Ideal.span_singleton_mul_right_unit H.isUnit]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
inst✝ : IsAdicComplete I A
x : A⟦X⟧ ⧸ Ideal.span {g}
⊢ Ideal.span {g} = Ideal.span {↑f}

Tactic:
rw [H.eq_mul, Ideal.span_singleton_mul_right_unit H.isUnit]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ ↑p.1 < ((map (IsLocalRing.residue A)) g).order

Tactic:
· rw [← ENat.lt_lift_iff (h := order_finite_iff_ne_zero.2 hg), ENat.lift_eq_toNat_of_lt_top]
      refine (Finset.HasAntidiagonal.antidiagonal.fst_le hp).lt_of_ne ?_
      contrapose hnotMem
      rwa [Finset.mem_singleton, Finset.HasAntidiagonal.antidiagonal_congr hp (by simp)]

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

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup S
inst✝² : Module R M
inst✝¹ : Module R S
inst✝ : IsSemisimpleModule R M
h : IsIsotypicOfType R M S
⊢ ∃ ι, Nonempty (M ≃ₗ[R] ι →₀ S)

Tactic:
have ⟨s, e, _, hs⟩ := IsSemisimpleModule.exists_linearEquiv_dfinsupp R M
  classical exact ⟨s, ⟨e.trans (DFinsupp.mapRange.linearEquiv fun m : s ↦ (h m.1).some)
    |>.trans (finsuppLequivDFinsupp R).symm⟩⟩

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Ring R
x✝ : IsSimpleRing R ∧ IsArtinianRing R
left✝ : IsSimpleRing R
right✝ : IsArtinianRing R
this : IsSemisimpleRing R
⊢ IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R

Tactic:
isSimpleRing_iff_isTwoSided_imp

Goal state after:
case refine_1
R : Type u
inst✝ : Ring R
right✝ : IsArtinianRing R
this : IsSemisimpleRing R
x✝ : (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) ∧ IsArtinianRing R
left✝ : Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
⊢ IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: case refine_2
R : Type u
inst✝ : Ring R
left✝¹ : IsSemisimpleRing R
right✝ : Nontrivial R
x✝ : IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R
left✝ : ∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤
⊢ IsSimpleRing R ∧ IsArtinianRing R

Tactic:
isSimpleRing_iff_isTwoSided_imp

Goal state after:
case refine_2
R : Type u
inst✝ : Ring R
left✝¹ : IsSemisimpleRing R
right✝ : Nontrivial R
x✝ : IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R
left✝ : ∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤
⊢ (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) ∧ IsArtinianRing R
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:
simp [WittVector.mul_coeff_zero, inverseCoeff, hA]

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

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
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
⊢ a = (fun x ↦ ↑p * x)^[m] b

Tactic:
convert! hcm using 2

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
⊢ (fun x ↦ ↑p * x) = ⇑verschiebung ∘ ⇑frobenius
Module: Mathlib.SetTheory.Cardinal.EventuallyConst

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
f : α → β
inst✝ : Nonempty α
hf : Monotone f
hf' : ¬IsCofinal (range (rangeSplitting f))
i : α
hi : ∀ y ∈ range (rangeSplitting f), y < i
j : α
hij : i ≤ j
⊢ f j ≤ f (rangeSplitting f ⟨f j, ⋯⟩)

Tactic:
apply_rangeSplitting f

Goal state after:
α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
f : α → β
inst✝ : Nonempty α
hf : Monotone f
hf' : ¬IsCofinal (range (rangeSplitting f))
i : α
hi : ∀ y ∈ range (rangeSplitting f), y < i
j : α
hij : i ≤ j
⊢ f j ≤ ↑⟨f j, ⋯⟩
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
S T : ↥(tree A)
x y x✝¹ : List A
a : A
x✝ : x✝¹ ++ [a] ∈ (fun x_1 ↦ x ++ x_1) ⁻¹' ↑T
⊢ (fun x_1 ↦ x ++ x_1) x✝¹ ++ [a] ∈ T

Tactic:
by rwa [List.append_assoc]

Goal state after:
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x : List A
⊢ pullSub (subAt T x) x ≤ T

Tactic:
intro y

Goal state after:
A : Type u_1
T : ↥(tree A)
x y : List A
⊢ y ∈ ↑(pullSub (subAt T x) x) → y ∈ ↑T
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: case right
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₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * ↑n₁ = o₁
hn₃ : o * ↑n₃ = o₃
⊢ o₁ + o * ↑n₃ = o₂

Tactic:
hn₃,

Goal state after:
case right
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₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * ↑n₁ = o₁
hn₃ : o * ↑n₃ = o₃
⊢ o₁ + o₃ = o₂
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: 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}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ (single e' x + f) e' = x

Tactic:
add_apply,

Goal state after:
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}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ (single e' x) e' + f e' = x
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case pos
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}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
a : Ordinal.{u_1}
ha : a ∈ f.support
⊢ (single e' x + f) a = f a

Tactic:
add_apply,

Goal state after:
case pos
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}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
a : Ordinal.{u_1}
ha : a ∈ f.support
⊢ (single e' x) a + f a = f a
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case pos
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
e' : Ordinal.{u_1}
he' : e' ∈ f.support
⊢ (single e x + f) e' = f e'

Tactic:
add_apply,

Goal state after:
case pos
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
e' : Ordinal.{u_1}
he' : e' ∈ f.support
⊢ (single e x) e' + f e' = f e'
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case refine_2.refine_2
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
⊢ enumOrd s '' Set.Iio a ⊆ s

Tactic:
apply (Set.image_subset_range ..).trans_eq
      rw [range_enumOrd hs]

Goal state after: