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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
⊢ (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * C 1 =
    X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)

Tactic:
C_1,

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
⊢ (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * 1 =
    X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.Defs

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

Tactic:
apply constantCoeff_wittStructureInt p _ _ n
  simp only [neg_zero, map_neg, constantCoeff_X]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ X n = X n * C ((↑p * ⅟↑p) ^ n)

Tactic:
mul_invOf_self,

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ X n = X n * C (1 ^ n)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ p ^ (n + 1 - k) = p * p ^ (n - k)

Tactic:
rw [← pow_succ', ← tsub_add_eq_add_tsub hk]

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)
⊢ (↑p * ⅟↑p) ^ n = 1

Tactic:
mul_invOf_self,

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)
⊢ 1 ^ n = 1
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
⊢ X n ^ p + 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 1 * X n ^ p + 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:
C_1,

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
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + 1 * X n ^ p + 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.WittVector.Truncated

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
⊢ ⨅ i, RingHom.ker (WittVector.truncate i) = ⊥

Tactic:
rw [Submodule.eq_bot_iff]

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
⊢ ∀ x ∈ ⨅ i, RingHom.ker (WittVector.truncate i), x = 0
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
n : ℕ
⊢ init n (x + y) = init n (init n x + init n y)

Tactic:
init_ring using wittAdd_vars

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
a : R
n : ℕ
h : 2 ≤ n
⊢ dickson k a n = X * dickson k a (n - 1) - C a * dickson k a (n - 2)

Tactic:
by
  obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h
  rw [add_comm]
  exact dickson_add_two k a n

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

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

Tactic:
C_1,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * dickson 1 1 (n + 1) - 1 * dickson 1 1 n = Chebyshev.C R ↑(n + 2)
Module: Mathlib.RingTheory.Polynomial.Dickson

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

Tactic:
C_1,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * dickson 2 1 (n + 1) - 1 * dickson 2 1 n = Chebyshev.S R ↑(n + 2)
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: case zero
x : ℝ
⊢ Real.exp (-(x ^ 2 / 2)) = (aeval x) (C 1) * Real.exp (-(x ^ 2 / 2))

Tactic:
C_1,

Goal state after:
case zero
x : ℝ
⊢ Real.exp (-(x ^ 2 / 2)) = (aeval x) 1 * Real.exp (-(x ^ 2 / 2))
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝ : Field F
d : ℕ
⊢ hilbertPoly 0 d = 0

Tactic:
delta hilbertPoly; induction d with
  | zero => simp only
  | succ d _ => simp only [coeff_zero, zero_smul, Finset.sum_const_zero]

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

Goal state before:
pp: ⊢ catalanSeries ^ 2 * X + 1 = catalanSeries

Tactic:
by
  ext n
  cases n with
  | zero => simp
  | succ n =>
    simp_rw [add_comm, map_add, coeff_one, if_neg n.succ_ne_zero, zero_add, coeff_succ_mul_X, sq,
      coeff_mul, catalanSeries_coeff, catalan_succ']

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h✝ : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
this : (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (rTensor N (inclusion hP₁_le)) u₁ = (rTensor N (inclusion hP₁_le)) u'₁
s : Finset S
hs : span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
⊢ (rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype)) u =
    (rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype)) u'

Tactic:
have k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype
    = inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j := by ext; rfl

Goal state after:
case right
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h✝ : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
this : (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (rTensor N (inclusion hP₁_le)) u₁ = (rTensor N (inclusion hP₁_le)) u'₁
s : Finset S
hs : span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j
⊢ (rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype)) u =
    (rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype)) u'
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 := ⋯
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) := ⋯
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := ⋯
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ⋯
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
⊢ Function.Surjective ⇑((Ideal.span {x} • ⊤).mkQ ∘ₗ g)

Tactic:
Submodule.ideal_span_singleton_smul x ⊤,

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
⊢ Function.Surjective ⇑((x • ⊤).mkQ ∘ₗ g)
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⟧ := ⋯
s : A⟦X⟧ := ⋯
n : ℕ := ⋯
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := ⋯
s₁ : A⟦X⟧ := ⋯
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := ⋯
⊢ f - g * q' = s + g * (q - q')

Tactic:
simp_rw [s]

Goal state after:
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⁻¹
⊢ f - g * q' = f - g * q + g * (q - q')
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ IsRegularLocalRing R ↔ ↑(Module.finrank (ResidueField R) (CotangentSpace R)) = ringKrullDim R

Tactic:
by
  rw [isRegularLocalRing_iff, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace]

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

Goal state before:
pp: case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L n)) → HasProjectiveDimensionLT M n
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))
⊢ HasProjectiveDimensionLT M (n + 1)

Tactic:
rcases Module.exists_finite_presentation R M with ⟨_, _, _, _, _, f, surjf⟩
    let S : ShortComplex (ModuleCat.{v} R) := f.shortComplexKer
    have hS : S.ShortExact := LinearMap.shortExact_shortComplexKer surjf
    match n with
    | 0 =>
      simp only [zero_add, ← projective_iff_hasProjectiveDimensionLT_one]
      have : Subsingleton (Ext M S.X₁ 1) := h S.X₁ inferInstance
      rcases Ext.covariant_sequence_exact₃ M hS (Ext.mk₀ (𝟙 M)) (zero_add 1)
        (Subsingleton.eq_zero _) with ⟨f', hf'⟩
      rcases (Ext.mk₀_bijective M S.X₂).2 f' with ⟨f, hf⟩
      rw [← hf, Ext.mk₀_comp_mk₀, (Ext.mk₀_bijective _ _).1.eq_iff] at hf'
      exact (Retract.mk f S.g hf').projective
    | n + 1 =>
      rw [hS.hasProjectiveDimensionLT_X₃_iff n inferInstance]
      have (L : ModuleCat.{v} R) : Subsingleton (Ext S.X₁ L (n + 1)) ↔
        Subsingleton (Ext M L (n + 2)) := by
        have (m : ℕ) : Subsingleton (Ext S.X₂ L (m + 1)) := Ext.subsingleton_of_projective S.X₂ L m
        have isi : IsIso (AddCommGrpCat.ofHom (hS.extClass.precomp L (add_comm 1 _))) :=
          (Ext.contravariantSequence_exact hS L (n + 1) (n + 2)
            (add_comm 1 _)).isIso_map' 1 (by decide)
              ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_src _)
                ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_tgt _)
        exact (asIso (AddCommGrpCat.ofHom (hS.extClass.precomp L
          (add_comm 1 _)))).addCommGroupIsoToAddEquiv.subsingleton_congr
      apply hn S.X₁
      simpa [this] using h

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
H : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
⊢ g.IsWeierstrassFactorization (Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - r) ↑⋯.unit⁻¹

Tactic:
have H1 : r.degree < (g.map (IsLocalRing.residue A)).order.toNat := H.1
  set n := (g.map (IsLocalRing.residue A)).order.toNat
  set f := Polynomial.X ^ n - r
  replace H1 : r.degree < (Polynomial.X (R := A) ^ n).degree := by rwa [Polynomial.degree_X_pow]
  have hfdeg : f.natDegree = n := by
    suffices f.degree = n by rw [Polynomial.natDegree, this]; rfl
    rw [Polynomial.degree_sub_eq_left_of_degree_lt H1, Polynomial.degree_X_pow]
  refine ⟨⟨⟨fun {i} hi ↦ ?_⟩, .sub_of_left (Polynomial.monic_X_pow _) H1⟩, Units.isUnit _, ?_⟩
  · rw [hfdeg] at hi
    simp_rw [f, Polynomial.coeff_sub, Polynomial.coeff_X_pow, if_neg hi.ne, zero_sub, neg_mem_iff]
    have := H.coeff_f_sub_r_mem hi
    rwa [map_sub, coeff_X_pow, if_neg hi.ne, zero_sub, neg_mem_iff, Polynomial.coeff_coe] at this
  · have := congr($(H.2) * ↑(H.isUnit_of_map_ne_zero hg).unit⁻¹)
    rw [add_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, ← sub_eq_iff_eq_add] at this
    simp_rw [← this, f, Polynomial.coe_sub, Polynomial.coe_pow, Polynomial.coe_X, sub_mul]

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 ↥(isotypicComponent R M S)

Tactic:
rw [isotypicComponent, sSup_eq_iSup]
  refine isSemisimpleModule_biSup_of_isSemisimpleModule_submodule fun m ⟨e⟩ ↦ ?_
  have := IsSemisimpleModule.congr e
  infer_instance

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

Goal state before:
pp: case h_option
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsRegularRing R
ι : Type u_2
inst✝¹ : Finite ι
α✝ : Type u_2
inst✝ : Fintype α✝
IH : IsRegularRing (MvPolynomial α✝ R)
⊢ IsRegularRing (MvPolynomial (Option α✝) R)

Tactic:
exact IsRegularRing.of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv.symm

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
inst✝ : IsSemisimpleRing R
⊢ ∃ n D d x x_1, (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))

Tactic:
have ⟨n, S, d, _, hd, ⟨e⟩⟩ := exists_algEquiv_pi_matrix_end_mulOpposite R₀ R
  classical exact ⟨n, _, d, inferInstance, inferInstance, hd, ⟨e⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁹ : CommRing R'
inst✝⁸ : CommRing S'
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : Module.Flat R S
surj : Function.Surjective ⇑(algebraMap R R')
surjS : Function.Surjective ⇑(algebraMap S S')
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥
smoothq : FormallySmooth R' S'
P : Extension R S := (Generators.self R S).toExtension
this : FormallySmooth R P.Ring := instFormallySmoothMvPolynomial S
IP : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) (RingHom.ker (algebraMap R R'))
s' : S'
⊢ (MvPolynomial.aeval ⇑(algebraMap S S')) (MvPolynomial.X (Classical.choose ⋯)) = s'

Tactic:
by simp [Classical.choose_spec (surjS s')]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate n)).comp
      (lift (fun k ↦ (zmodEquivTrunc p k).toRingHom.comp (PadicInt.toZModPow k)) ⋯) =
    PadicInt.toZModPow n

Tactic:
rw [RingHom.comp_assoc, truncate_comp_lift, ← RingHom.comp_assoc]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((zmodEquivTrunc p n).symm.toRingHom.comp (zmodEquivTrunc p n).toRingHom).comp (PadicInt.toZModPow n) =
    PadicInt.toZModPow n
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((zmodEquivTrunc p n).symm.toRingHom.comp (zmodEquivTrunc p n).toRingHom).comp (PadicInt.toZModPow n) =
    PadicInt.toZModPow n

Tactic:
simp only [RingEquiv.symm_toRingHom_comp_toRingHom, RingHom.id_comp]

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

Goal state before:
pp: case succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
⊢ (frobenius (frobeniusRotation p ha₁ ha₂) * a₁).coeff (n + 1) = (frobeniusRotation p ha₁ ha₂ * a₂).coeff (n + 1)

Tactic:
simp only [nthRemainder_spec, WittVector.coeff_frobenius_charP,
      frobeniusRotation, coeff_mk, frobeniusRotationCoeff]

Goal state after:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
⊢ succNthVal p n a₁ a₂ (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂))))
        (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) (truncateFun (n + 1) a₂)
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)
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y ↦
    f₀ fun a ↦
      Subtype.casesOn a fun a ha ↦
        Function.uncurry ![x, y]
          (let S := {a | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
        peval (polyOfInterest p n) ![fun i ↦ x.coeff i, fun i ↦ y.coeff i]

Tactic:
use f

Goal state after:
case h
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)
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k := ⋯
⊢ ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      peval (polyOfInterest p n) ![fun i ↦ x.coeff i, fun i ↦ y.coeff i]
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 : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      (x * y).coeff (n + 1) =
        x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
          f (truncateFun (n + 1) x) (truncateFun (n + 1) y)

Tactic:
use f

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
⊢ ∀ (x y : 𝕎 k),
    (x * y).coeff (n + 1) =
      x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
        f (truncateFun (n + 1) x) (truncateFun (n + 1) y)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

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

pp: case refine_2
b o : Ordinal.{u_1}
⊢ ∀ (o : Ordinal.{u_1}),
    o ≠ 0 →
      foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o →
        foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Tactic:
· rw [zero_right, foldr_nil]

Goal state after:
case refine_2
b o : Ordinal.{u_1}
⊢ ∀ (o : Ordinal.{u_1}),
    o ≠ 0 →
      foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o →
        foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o e c : Ordinal.{u_1}
h : (e, c) ∈ CNF b o
⊢ (coeff b o) e = c

Tactic:
by
  rw [coeff, lookupFinsupp_apply, mem_lookup_iff.2, Option.getD_some]
  simpa

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
⊢ lfpApprox f x (succ #α).ord ∈ fixedPoints ⇑f

Tactic:
by
  let ⟨a, ha, b, hb, hne, hf⟩ := exists_lfpApprox_eq_lfpApprox f x
  cases le_total a b with
  | inl hab => exact lfpApprox_mem_fixedPoints_of_eq f hx (hne.lt_of_le hab) ha.le hf
  | inr hba => exact lfpApprox_mem_fixedPoints_of_eq f hx (hne.symm.lt_of_le hba) hb.le hf.symm

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

Goal state before:
pp: case single_add.h.inr
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
e₂ : Ordinal.{u_1}
he₂✝ : e₂ ∈ (f₁ + f₂).support
he₂ : e₂ ∈ f₂.support
⊢ e₂ ≤ e₁

Tactic:
· apply h _ _ _ he₂
        simp_all

Goal state after: