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

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
s : (j : OpenNormalSubgroup G) → (stabilizerHomSurjectiveAuxFunctor P Q σ).obj j
hs : s ∈ (stabilizerHomSurjectiveAuxFunctor P Q σ).sections
a : ↑(ProfiniteGrp.of G).toProfinite.toTop :=
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv) ⟨fun N ↦ ↑↑(s N), ⋯⟩
this : ∀ (N : OpenNormalSubgroup G), ↑a = ↑↑(s N)
⊢ (stabilizerHom Q P G) ⟨a, ⋯⟩ = σ

Tactic:
ext x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    obtain ⟨N, hN⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
      (stabilizer_isOpen G x) (one_mem _)
    lift x to B' N.1.1 using fun g ↦ hN g.2
    change Ideal.Quotient.mk Q (QuotientGroup.mk (s := N) a • x).1 = _
    rw [this]
    exact DFunLike.congr_fun (s N).2 (Ideal.Quotient.mk _ x)

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : (Ideal.Quotient.mk P) ↑s ≠ 0
h₂ : (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) ↑s) ≠ 0
⊢ (algebraMap S (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) x =
    (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) ((algebraMap S Sₚ) x)

Tactic:
Quotient.mk_algebraMap

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : (Ideal.Quotient.mk P) ↑s ≠ 0
h₂ : (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) ↑s) ≠ 0
⊢ (algebraMap S (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) x = (algebraMap S (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) x
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
D : WithZero (Multiplicative ℤ)
hD : D ≠ 0
f : K⸨X⸩
⊢ Valued.v f ≤ D ↔ ∀ n < -D.log, f.coeff n = 0

Tactic:
cases D

Goal state after:
case zero
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
hD : 0 ≠ 0
⊢ Valued.v f ≤ 0 ↔ ∀ n < -log 0, f.coeff n = 0

case coe
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
a✝ : Multiplicative ℤ
hD : ↑a✝ ≠ 0
⊢ Valued.v f ≤ ↑a✝ ↔ ∀ n < -(↑a✝).log, f.coeff n = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case coe
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
D : Multiplicative ℤ
hD : ↑D ≠ 0
⊢ Valued.v f ≤ ↑D ↔ ∀ n < -(↑D).log, f.coeff n = 0

Tactic:
cases D

Goal state after:
case coe.ofAdd
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
a✝ : ℤ
hD : ↑(Multiplicative.ofAdd a✝) ≠ 0
⊢ Valued.v f ≤ ↑(Multiplicative.ofAdd a✝) ↔ ∀ n < -(↑(Multiplicative.ofAdd a✝)).log, f.coeff n = 0
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsPrime
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
⊢ (length (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))
        (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P) ⧸
          Ideal.map (algebraMap Rₚ (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))) (maximalIdeal Rₚ))).toNat =
    (length (Localization.AtPrime P)
        (Localization.AtPrime P ⧸ Ideal.map (algebraMap R (Localization.AtPrime P)) p)).toNat

Tactic:
let R₁ := Localization.AtPrime (P.map (algebraMap S Sₚ))

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsPrime
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
R₁ : Type u_4 := Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P)
⊢ (length (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))
        (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P) ⧸
          Ideal.map (algebraMap Rₚ (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))) (maximalIdeal Rₚ))).toNat =
    (length (Localization.AtPrime P)
        (Localization.AtPrime P ⧸ Ideal.map (algebraMap R (Localization.AtPrime P)) p)).toNat
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN : ∀ (g : K⸨X⸩), Valued.v (g - f) ≤ 1 → ∀ n < N, g.coeff n = 0
g : K⸨X⸩
⊢ g ∈ S ∩ T → g ∈ {x | (fun f ↦ ∀ n < N, f.coeff n = 0) x}

Tactic:
hg

Goal state after:
case h
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN : ∀ (g : K⸨X⸩), Valued.v (g - f) ≤ 1 → ∀ n < N, g.coeff n = 0
g : K⸨X⸩
hg : g ∈ S ∩ T
⊢ g ∈ {x | (fun f ↦ ∀ n < N, f.coeff n = 0) x}
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := max ℓ D
⊢ ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n

Tactic:
simp only [Set.mem_Iio, Set.mem_Icc, Set.subset_iInter_iff]

Goal state after:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := max ℓ D
⊢ ∀ i < D, (⋂ n, ⋂ (_ : n < ℓ), φ n) ∩ ⋂ n, ⋂ (_ : ℓ ≤ n ∧ n ≤ N), φ n ⊆ φ i
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
⊢ sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)

Tactic:
← Finsupp.sum_single (Finsupp.embDomain _ _)

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
⊢ sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff ((Finsupp.embDomain ι c).sum Finsupp.single)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
⊢ Function.Surjective ⇑(esymmAlgHom (Fin m) R n)

Tactic:
intro p
  obtain ⟨q, rfl⟩ := (esymmAlgHom_fin_bijective R m).2 p
  rw [← AlgHom.mem_range]
  induction q using MvPolynomial.induction_on with
  | C r => rw [← algebraMap_eq, AlgHom.commutes]; apply Subalgebra.algebraMap_mem
  | add p q hp hq => rw [map_add]; exact Subalgebra.add_mem _ hp hq
  | mul_X p i hp =>
    rw [map_mul]
    apply Subalgebra.mul_mem _ hp
    rw [AlgHom.mem_range]
    refine ⟨X ⟨i, i.2.trans_le h⟩, ?_⟩
    simp_rw [esymmAlgHom, aeval_X]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
q : ℕ
hq : q ≠ 0
i : MvPowerSeries σ R
⊢ (expand (p * q) ⋯) i = ((expand p hp).comp (expand q hq)) i

Tactic:
simp [expand, pow_mul, subst_comp_subst_apply (HasSubst.X_pow hq) (HasSubst.X_pow hp),
    subst_pow (HasSubst.X_pow hp), subst_X (HasSubst.X_pow hp)]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : d ∈ Function.support ((expand p hp) φ)
this : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ := Finsupp.mapRange (fun n ↦ n / p) ⋯ d
eq_aux : p • m = d
⊢ d ∈ (fun x ↦ p • x) '' Function.support φ

Tactic:
rw [Function.mem_support, ← eq_aux, ← coeff_apply (expand p hp φ), coeff_expand_smul,
    coeff_apply] at hd

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
this : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ := Finsupp.mapRange (fun n ↦ n / p) ⋯ d
hd : φ m ≠ 0
eq_aux : p • m = d
⊢ d ∈ (fun x ↦ p • x) '' Function.support φ
Module: Mathlib.RingTheory.NormTrace

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2
b : Basis ι A B
this : Fintype ι
⊢ ∃ r, ((leftMulMatrix b) (1 + a • x)).det = 1 + ((leftMulMatrix b) x).trace * a + r * a ^ 2

Tactic:
simp only [map_add, map_one, map_smul, Matrix.det_one_add_smul a]

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2
b : Basis ι A B
this : Fintype ι
⊢ ∃ r,
    1 + ((leftMulMatrix b) x).trace * a +
        Polynomial.eval a (1 + Polynomial.X • ((leftMulMatrix b) x).map ⇑Polynomial.C).det.divX.divX * a ^ 2 =
      1 + ((leftMulMatrix b) x).trace * a + r * a ^ 2
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n) = (Int.castRingHom ℚ) 0

Tactic:
constantCoeff_wittStructureRat,

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ 0 = (Int.castRingHom ℚ) 0

case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff ((map (Int.castRingHom ℚ)) Φ) = 0
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 y : 𝕎 R), (x * y).coeff = fun n ↦ peval (wittMul p n) ![x.coeff, y.coeff]

Tactic:
intros; ext; exact mul_coeff _ _ _

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

Goal state before:
pp: p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
n : ℕ
⊢ (eval₂Hom (g.comp (algebraMap ℤ R)) fun i ↦ g (x.coeff i)) (φ n) = (aeval fun i ↦ g (x.coeff i)) (φ n)

Tactic:
RingHom.ext_int _ (algebraMap ℤ S),

Goal state after:
p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
n : ℕ
⊢ (eval₂Hom (algebraMap ℤ S) fun i ↦ g (x.coeff i)) (φ n) = (aeval fun i ↦ g (x.coeff i)) (φ n)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case succ
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
k : ℕ
ih :
  (coeff (Nat.find h + k)) 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 + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (Nat.find h + k + 1)) f
h1 : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
h2 : (Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p) ≠ 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 + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))

Tactic:
ih (coeff_nat_find_add_ne_zero k),

Goal state after:
case succ
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
k : ℕ
ih :
  (coeff (Nat.find h + k)) 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 + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (Nat.find h + k + 1)) f
h1 : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
h2 : (Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p) ≠ 0
⊢ ModP.preVal K v O p ((coeff (Nat.find h + k)) f) ^ p ^ (Nat.find h + k) =
    ModP.preVal K v O p ((coeff (Nat.find h + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))
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 : ℕ
ih : (⇑verschiebung ∘ ⇑frobenius)^[n] x = x * ↑p ^ n
⊢ (⇑verschiebung ∘ ⇑frobenius) (x * ↑p ^ n) = x * (↑p ^ n * ↑p)

Tactic:
comp_apply,

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 : ℕ
ih : (⇑verschiebung ∘ ⇑frobenius)^[n] x = x * ↑p ^ n
⊢ verschiebung (frobenius (x * ↑p ^ n)) = x * (↑p ^ n * ↑p)
Module: Mathlib.RingTheory.WittVector.Identities

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

Tactic:
rw [← comp_apply (f := verschiebung^[n]),
      ← Function.Commute.comp_iterate verschiebung_frobenius_comm]
  induction n with
  | zero => simp
  | succ n ih =>
    rw [iterate_succ_apply', ih, pow_succ, comp_apply, verschiebung_frobenius, mul_assoc]

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

Goal state before:
pp: ⊢ hermite 1 = X

Tactic:
hermite_succ,

Goal state after:
⊢ X * hermite 0 - derivative (hermite 0) = X
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:
hermite_succ,

Goal state after:
n k : ℕ
⊢ (X * hermite n - derivative (hermite n)).coeff (k + 1) = (hermite n).coeff k - (↑k + 2) * (hermite n).coeff (k + 2)
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: case succ
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ (-1) ^ n *
      (deriv (fun x ↦ (aeval x) (hermite n)) x * Real.exp (-(x ^ 2 / 2)) +
        (aeval x) (hermite n) * (-x * Real.exp (-(x ^ 2 / 2)))) =
    (-1) ^ n * -1 * ((aeval x) (hermite (n + 1)) * Real.exp (-(x ^ 2 / 2)))

pp: case succ.hc
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x ↦ (aeval x) (hermite n)) x

pp: case succ.hd
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x ↦ Real.exp (-(x ^ 2 / 2))) x

Tactic:
hermite_succ,

Goal state after:
case succ
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ (-1) ^ n *
      (deriv (fun x ↦ (aeval x) (hermite n)) x * Real.exp (-(x ^ 2 / 2)) +
        (aeval x) (hermite n) * (-x * Real.exp (-(x ^ 2 / 2)))) =
    (-1) ^ n * -1 * ((aeval x) (X * hermite n - derivative (hermite n)) * Real.exp (-(x ^ 2 / 2)))

case succ.hc
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x ↦ (aeval x) (hermite n)) x

case succ.hd
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x ↦ Real.exp (-(x ^ 2 / 2))) x
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
⊢ ((↑d !)⁻¹ • (ascPochhammer F d).comp (X - C ↑k + 1)).natDegree = d

Tactic:
natDegree_smul _ (inv_ne_zero hne),

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
⊢ ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree = d
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ (preHilbertPoly F d k).coeff d = (↑d !)⁻¹

Tactic:
coeff_preHilbertPoly_self

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ (↑d !)⁻¹ = (↑d !)⁻¹
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

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

Tactic:
by
  rw [deriv_gaussian_eq_hermite_mul_gaussian]
  field_simp
  rw [← pow_mul]
  simp

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

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

Tactic:
PowerSeries.coeff_mul,

Goal state after:
case succ
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
⊢ ∑ p_1 ∈ Finset.antidiagonal n, (PowerSeries.coeff p_1.1) ↑p * (PowerSeries.coeff p_1.2) ↑(invOneSubPow F (d + 1)) =
    ∑ i ∈ p.support, p.coeff i * ↑((n + d - i).choose d)
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
hc : 1 = ∑ k ∈ Finset.range f.natDegree.succ, a.coeff k * b.coeff (f.natDegree - k)
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))

Tactic:
Finset.sum_range_succ,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
hc :
  1 =
    ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x) +
      a.coeff f.natDegree * b.coeff (f.natDegree - f.natDegree)
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ (IsCancelMulZero R ∧ IsCancelAdd R) ∧ Nontrivial R ↔ (IsCancelMulZero R ∧ Nontrivial R) ∧ IsCancelAdd R

Tactic:
and_right_comm

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

Goal state before:
pp: A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra ℚ A
A' : Type u_2
inst✝¹ : CommRing A'
inst✝ : Algebra ℚ A'
f : A →+* A'
⊢ (map f) (log A) = log A'

Tactic:
ext n; simp only [coeff_map, coeff_log]; split_ifs <;> simp [RingHom.map_rat_algebraMap]

Goal state after: