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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ PowerSeries.subst F.zeroX F.zeroX = subst ![0, subst ![0, PowerSeries.X] F.toPowerSeries] F.toPowerSeries

Tactic:
PowerSeries.subst,

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ subst (fun x ↦ F.zeroX) F.zeroX = subst ![0, subst ![0, PowerSeries.X] F.toPowerSeries] F.toPowerSeries
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![f, 0] F.toPowerSeries = PowerSeries.subst f (subst ![PowerSeries.X, 0] F.toPowerSeries)

Tactic:
PowerSeries.subst,

Goal state after:
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![f, 0] F.toPowerSeries = subst (fun x ↦ f) (subst ![PowerSeries.X, 0] F.toPowerSeries)
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ ![f, 0] ((fun i ↦ i) ⟨1, ⋯⟩) = subst (fun x ↦ f) (![PowerSeries.X, 0] ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
simp [subst, eval₂]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![0, f] F.toPowerSeries = PowerSeries.subst f (subst ![0, PowerSeries.X] F.toPowerSeries)

Tactic:
PowerSeries.subst,

Goal state after:
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![0, f] F.toPowerSeries = subst (fun x ↦ f) (subst ![0, PowerSeries.X] F.toPowerSeries)
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ ![0, f] ((fun i ↦ i) ⟨0, ⋯⟩) = subst (fun x ↦ f) (![0, PowerSeries.X] ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
simp [subst, eval₂]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f g : R⟦σ →₀ ℕ⟧
n : σ →₀ ℕ
⊢ (f * g).coeff n = (MvPowerSeries.coeff n) (f.coeff * g.coeff)

Tactic:
simp_rw [coeff_mul]

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f g : R⟦σ →₀ ℕ⟧
n : σ →₀ ℕ
⊢ ∑ ij ∈ Finset.antidiagonal ⋯ ⋯ n, f.coeff ij.1 * g.coeff ij.2 = (MvPowerSeries.coeff n) (f.coeff * g.coeff)
Module: Mathlib.RingTheory.Ideal.UFD

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : UniqueFactorizationMonoid R
p : Ideal R
inst✝ : p.IsPrime
hph : p.height = 1
hpn : p ≠ ⊥
⊢ Submodule.IsPrincipal p

Tactic:
obtain ⟨x, hxmem, hxp⟩ := Ideal.IsPrime.exists_mem_prime_of_ne_bot ‹_› hpn

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : UniqueFactorizationMonoid R
p : Ideal R
inst✝ : p.IsPrime
hph : p.height = 1
hpn : p ≠ ⊥
x : R
hxmem : x ∈ p
hxp : Prime x
⊢ Submodule.IsPrincipal p
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
J : Ideal R
⊢ J.FG → Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J))

Tactic:
hJ

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
J : Ideal R
hJ : J.FG
⊢ Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J))
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p I : Ideal R
inst✝ : p.IsPrime
h : I ≤ p
⊢ ↑p.height ≤ ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)

Tactic:
trans (p.map (Ideal.Quotient.mk I)).height + I.spanFinrank
  · norm_cast; exact Ideal.height_le_height_add_spanFinrank_of_le h
  · gcongr
    have : (Ideal.map (Ideal.Quotient.mk I) p).IsPrime :=
      Ideal.isPrime_map_quotientMk_of_isPrime h
    exact Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'

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

Goal state before:
pp: case e'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
ι : Type u_2
inst✝ : Finite ι
α✝ β✝ : Type u_2
e : α✝ ≃ β✝
H : ringKrullDim (MvPolynomial α✝ R) = ringKrullDim R + ↑(Nat.card α✝)
⊢ ringKrullDim (MvPolynomial α✝ R) = ringKrullDim (MvPolynomial β✝ R)

pp: case e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
ι : Type u_2
inst✝ : Finite ι
α✝ β✝ : Type u_2
e : α✝ ≃ β✝
H : ringKrullDim (MvPolynomial α✝ R) = ringKrullDim R + ↑(Nat.card α✝)
⊢ ringKrullDim R + ↑(Nat.card α✝) = ringKrullDim R + ↑(Nat.card β✝)

Tactic:
· exact ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv

Goal state after:
case e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
ι : Type u_2
inst✝ : Finite ι
α✝ β✝ : Type u_2
e : α✝ ≃ β✝
H : ringKrullDim (MvPolynomial α✝ R) = ringKrullDim R + ↑(Nat.card α✝)
⊢ ringKrullDim R + ↑(Nat.card α✝) = ringKrullDim R + ↑(Nat.card β✝)
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
J : Submodule R M
⊢ J ∈ s → ({I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}.inf id).IsPrimary

Tactic:
hJ

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
J : Submodule R M
hJ : J ∈ s
⊢ ({I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}.inf id).IsPrimary
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I : Submodule R M
hI :
  I ∈
    ↑(Finset.image (fun t ↦ t.inf id)
        (Finset.image (fun J ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s))
J : Submodule R M
⊢ J ∈
      ↑(Finset.image (fun t ↦ t.inf id)
          (Finset.image (fun J ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s)) →
    I ≠ J → ((fun x1 x2 ↦ x1 ≠ x2) on fun J ↦ (J.colon Set.univ).radical) I J

Tactic:
hJ

Goal state after:
case refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I : Submodule R M
hI :
  I ∈
    ↑(Finset.image (fun t ↦ t.inf id)
        (Finset.image (fun J ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s))
J : Submodule R M
hJ :
  J ∈
    ↑(Finset.image (fun t ↦ t.inf id)
        (Finset.image (fun J ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s))
⊢ I ≠ J → ((fun x1 x2 ↦ x1 ≠ x2) on fun J ↦ (J.colon Set.univ).radical) I J
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : IsLasker R M
N : Submodule R M
⊢ ∃ t, N.IsMinimalPrimaryDecomposition t

Tactic:
by
  obtain ⟨s, hs1, hs2⟩ := h N
  obtain ⟨t, h1, h2, h3, h4⟩ :=
    exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition hs1 hs2
  exact ⟨t, h1, h2, h3, h4⟩

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
⊢ ∃ a, (LinearMap.lcomp Rₛ Mₛ (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I).subtype) a = g

Tactic:
obtain ⟨⟨g', a⟩, e : a.1 • g = _⟩ := surj S (mapExtendScalars S (I.toLocalized' _ _ _) f Rₛ) g

Goal state after:
R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
g' : ↥I →ₗ[R] M
a : ↥S
e : ↑a • g = (mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ) (g', a).1
⊢ ∃ a, (LinearMap.lcomp Rₛ Mₛ (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I).subtype) a = g
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝² : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this✝¹ : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h1 : Ideal.span (⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)}) = ⊤
g : S
hg : IsStandardOpenImmersion R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion S (Localization.Away x)
this✝ : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this : IsScalarTower S (Localization.Away x) (T'' g x)
⊢ IsLocalization (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g)) (T'' g x)

Tactic:
have : algebraMapSubmonoid (Localization.Away x) (.powers g) =
      algebraMapSubmonoid (Localization.Away x) (.powers (algebraMap S T g)) := by
        simp [IsScalarTower.algebraMap_apply S T (Localization.Away x)]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝³ : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this✝² : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h1 : Ideal.span (⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)}) = ⊤
g : S
hg : IsStandardOpenImmersion R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion S (Localization.Away x)
this✝¹ : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this✝ : IsScalarTower S (Localization.Away x) (T'' g x)
this :
  algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g) =
    algebraMapSubmonoid (Localization.Away x) (Submonoid.powers ((algebraMap S T) g))
⊢ IsLocalization (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g)) (T'' g x)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
s : ℕ
⊢ Valued.v ((ofPowerSeries ℤ K) PowerSeries.X) ^ s = exp (-↑s)

Tactic:
valuation_def,

Goal state after:
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ((ofPowerSeries ℤ K) PowerSeries.X) ^ s = exp (-↑s)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) f) ≤ exp (-↑d)
hnd : n < d
⊢ PowerSeries.X ^ d ∣ f

Tactic:
valuation_def,

Goal state after:
K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : (valuation K⸨X⸩ (PowerSeries.idealX K)) ((algebraMap K⟦X⟧ K⸨X⸩) f) ≤ exp (-↑d)
hnd : n < d
⊢ PowerSeries.X ^ d ∣ f
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
d : ℕ
f : K⟦X⟧
this : PowerSeries.X ^ d ∣ f ↔ ∀ n < d, (PowerSeries.coeff n) f = 0
⊢ Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) f) ≤ exp (-↑d) ↔ PowerSeries.X ^ d ∣ f

Tactic:
valuation_def,

Goal state after:
K : Type u_2
inst✝ : Field K
d : ℕ
f : K⟦X⟧
this : PowerSeries.X ^ d ∣ f ↔ ∀ n < d, (PowerSeries.coeff n) f = 0
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ((algebraMap K⟦X⟧ K⸨X⸩) f) ≤ exp (-↑d) ↔ PowerSeries.X ^ d ∣ f
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ Valued.v f ≤ exp (-D)

Tactic:
rw [← f.single_order_mul_powerSeriesPart, hs, map_mul, valuation_single_zpow, neg_neg, mul_comm,
      ← le_mul_inv_iff₀, exp_neg, ← mul_inv, ← exp_add, ← exp_neg]

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-(D + ↑s))

case pos
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ 0 < exp ↑s
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case refine_4
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h✝ : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
r : R
p : MvPolynomial σ R
x✝ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h : IsWeightedHomogeneous w ((pderiv i) p) n'
⊢ IsWeightedHomogeneous w ((pderiv i) (r • p)) n'

Tactic:
rw [(pderiv i).map_smul]; exact (weightedHomogeneousSubmodule ..).smul_mem _ h

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this : i ≤ m - 1
hm : m - 1 < m
⊢ (accumulate n m) (invAccumulate n m s) ⟨m - 1, hm⟩ = s ⟨m - 1, hm⟩

Tactic:
· have := (Nat.sub_one_add_one <| Nat.ne_zero_of_lt hm).symm
    rw [accumulate_last (hm.trans_le hmn) this, invAccumulate, dif_pos hm, dif_neg this.not_gt,
      Nat.sub_zero]
    intro j hj
    rw [invAccumulate, dif_neg hj.not_gt, Nat.zero_sub]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ Valued.v
      (((single 1) 1 ^ s)⁻¹ * (ofPowerSeries ℤ K) F -
        (algebraMap K⟮X⟯ K⸨X⸩) 1 / (single 1) 1 ^ s * (algebraMap K⟮X⟯ K⸨X⸩) ↑P) <
    ↑γ

Tactic:
simp only [map_one]

Goal state after:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ Valued.v (((single 1) 1 ^ s)⁻¹ * (ofPowerSeries ℤ K) F - 1 / (single 1) 1 ^ s * (algebraMap K⟮X⟯ K⸨X⸩) ↑P) < ↑γ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ antidiagonal k
⊢ ∑ A ∈ powersetCard a.1 univ, ∑ j, weight σ R k (A, j) = (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2

Tactic:
simp only [esymm, psum, weight, ← mul_assoc, mul_sum]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ antidiagonal k
⊢ ∑ x ∈ powersetCard a.1 univ, ∑ j, ((-1) ^ #x * ∏ a ∈ x, X a) * X j ^ (k - #x) =
    ∑ i, (∑ i ∈ powersetCard a.1 univ, (-1) ^ a.1 * ∏ a ∈ i, X a) * X i ^ a.2
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
not_le : ¬p • m ≤ p • n
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))

Tactic:
rw [coeff_trunc', ← hm, if_neg not_le, MvPolynomial.coeff_expand_smul _ hp, coeff_trunc',
        if_neg h_le]

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n =
    C (1 / ↑p ^ n) *
      ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) Φ -
        ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))

Tactic:
by
  calc
    wittStructureRat p Φ n = C (1 / (p : ℚ) ^ n) * (wittStructureRat p Φ n * C ((p : ℚ) ^ n)) := ?_
    _ = _ := by rw [wittStructureRat_rec_aux]
  rw [mul_left_comm, ← C_mul, div_mul_cancel₀, C_1, mul_one]
  exact pow_ne_zero _ (Nat.cast_ne_zero.2 hp.1.ne_zero)

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

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

Tactic:
rw [xInTermsOfW_eq, map_mul, map_sub, bind₁_X_right, algHom_C, map_sum,
    show X n = (X n * C ((p : R) ^ n)) * C ((⅟p : R) ^ n) by
      rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]]

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (W_ R n - ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))) *
      (algebraMap R (MvPolynomial ℕ R)) (⅟↑p ^ n) =
    X n * C (↑p ^ n) * C (⅟↑p ^ n)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (wittStructureInt p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

Tactic:
rw [← vars_map_of_injective _ this, map_wittStructureInt]

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
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 : ℕ
⊢ peval (wittNeg p n) ![x✝.coeff] = (eval₂Hom (algebraMap ℤ R✝) x✝.coeff) ((fun n ↦ (rename Prod.snd) (wittNeg p n)) n)

Tactic:
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: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
⊢ (↑p ^ i).coeff i = 1

Tactic:
induction i with
  | zero => simp only [one_coeff_zero, pow_zero]
  | succ i h =>
    rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP,
      verschiebung_coeff_succ, h, one_pow]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: 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
n : ℕ
hfn : (coeff n) f ≠ 0
⊢ valAux K v O p f = ModP.preVal K v O p ((coeff n) f) ^ p ^ n

Tactic:
have h : ∃ n, coeff n f ≠ 0 := ⟨n, hfn⟩

Goal state after:
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
n : ℕ
hfn : (coeff n) f ≠ 0
h : ∃ n, (coeff n) f ≠ 0
⊢ valAux K v O p f = ModP.preVal K v O p ((coeff n) f) ^ p ^ n
Module: Mathlib.RingTheory.WittVector.Domain

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

Tactic:
exact ih fun i hi => h _ (hi.trans (Nat.lt_succ_self _))

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : wa.coeff 0 ≠ 0
ha : (⇑verschiebung)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : wb.coeff 0 ≠ 0
hb : (⇑verschiebung)^[nb] wb ≠ 0
⊢ ((⇑verschiebung)^[na] wa * (⇑verschiebung)^[nb] wb).coeff (na + nb) ≠ coeff 0 (na + nb)

Tactic:
iterate_verschiebung_mul_coeff,

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : wa.coeff 0 ≠ 0
ha : (⇑verschiebung)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : wb.coeff 0 ≠ 0
hb : (⇑verschiebung)^[nb] wb ≠ 0
⊢ wa.coeff 0 ^ p ^ nb * wb.coeff 0 ^ p ^ na ≠ coeff 0 (na + nb)