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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
N : WithBot ℕ∞
⊢ injectiveDimension M ≤ N ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ N

Tactic:
induction N with
  | bot =>
    simp only [le_bot_iff, injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
    apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)
    intro p hp
    exact h ⟨p, hp.isPrime⟩
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n

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

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
n : ℕ
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
⊢ HasProjectiveDimensionLE M n ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n

Tactic:
by
  induction n generalizing M with
  | zero =>
    simp only [HasProjectiveDimensionLE, zero_add, ← projective_iff_hasProjectiveDimensionLT_one]
    refine ⟨fun h p ↦ ?_, fun h ↦ ?_⟩
    · let : Small.{v} (Localization p.asIdeal.primeCompl) :=
        small_of_surjective Localization.mkHom_surjective
      rw [← IsProjective.iff_projective]
      exact Module.projective_of_isLocalizedModule p.1.primeCompl
        (M.localizedModuleMkLinearMap p.1.primeCompl)
    · rw [← IsProjective.iff_projective]
      have : Module.FinitePresentation R M := Module.finitePresentation_of_finite R M
      apply Module.projective_of_localization_maximal (fun p hp ↦ ?_)
      have : Module.Projective (Localization.AtPrime p) (M.localizedModule p.primeCompl) := by
        let : Small.{v} (Localization.AtPrime p) :=
          small_of_surjective Localization.mkHom_surjective
        simpa [IsProjective.iff_projective] using h ⟨p, hp⟩
      exact Module.Projective.of_equiv (LinearEquiv.extendScalarsOfIsLocalization p.primeCompl
        (Localization.AtPrime p) (IsLocalizedModule.linearEquiv p.primeCompl
        (M.localizedModuleMkLinearMap p.primeCompl)
        (LocalizedModule.mkLinearMap p.primeCompl M)))
  | succ n ih =>
    rcases Module.exists_finite_presentation R M with ⟨P, _, _, _, _, f, surjf⟩
    let S := f.shortComplexKer
    have S_exact := LinearMap.shortExact_shortComplexKer surjf
    have proj := ModuleCat.projective_of_categoryTheory_projective S.X₂
    let Sp (p : MaximalSpectrum R) := S.map (ModuleCat.localizedModuleFunctor p.1.primeCompl)
    have Sp_exact (p : MaximalSpectrum R) : (Sp p).ShortExact :=
      S_exact.map_of_exact (ModuleCat.localizedModuleFunctor p.asIdeal.primeCompl)
    specialize ih (ModuleCat.of R (LinearMap.ker f))
    have projp (p : MaximalSpectrum R) : Projective (Sp p).X₂ :=
      (ModuleCat.localizedModuleFunctor.{v} p.1.primeCompl).projective_obj_of_projective proj
    simp only [HasProjectiveDimensionLE] at ih ⊢
    rw [S_exact.hasProjectiveDimensionLT_X₃_iff n proj, ih]
    exact (forall_congr' (fun p ↦ (Sp_exact p).hasProjectiveDimensionLT_X₃_iff n (projp p))).symm

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
P : K[X]
hP : P = 0
⊢ 0 = (idealX K).intValuation 0

Tactic:
Valuation.map_zero

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
P : K[X]
hP : P = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
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
hDs : 0 < D + ↑s
d : ℕ
hd : D + ↑s = ↑d
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-(D + ↑s))

Tactic:
hd

Goal state after:
case neg
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
hDs : 0 < D + ↑s
d : ℕ
hd : D + ↑s = ↑d
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-↑d)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
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 : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = ↑s
hDs : 0 < D - ↑s
d : ℕ
hd : D - ↑s = ↑d
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-(D - ↑s))

Tactic:
hd

Goal state after:
case neg
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 : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = ↑s
hDs : 0 < D - ↑s
d : ℕ
hd : D - ↑s = ↑d
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-↑d)
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
refine ⟨fun hnD n hn => coeff_zero_of_lt_valuation K hnD hn, fun h_val_f => ?_⟩
  let F := powerSeriesPart f
  by_cases! ord_nonpos : f.order ≤ 0
  · obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat ord_nonpos
    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]
    · by_cases! hDs : D + s ≤ 0
      · apply le_trans ((PowerSeries.idealX K).valuation_le_one F)
        rwa [← log_le_iff_le_exp one_ne_zero, le_neg, log_one, neg_zero]
      · obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le hDs.le
        rw [hd]
        apply (intValuation_le_iff_coeff_lt_eq_zero K F).mpr
        intro n hn
        rw [powerSeriesPart_coeff f n, hs]
        apply h_val_f
        lia
    · simp [ne_eq, zero_lt_iff]
  · obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat <| neg_nonpos_of_nonneg ord_nonpos.le
    rw [neg_inj] at hs
    rw [← f.single_order_mul_powerSeriesPart, hs, map_mul, valuation_single_zpow, mul_comm,
      ← le_mul_inv_iff₀, ← exp_neg, ← exp_add, neg_neg]
    · by_cases! hDs : D - s ≤ 0
      · apply le_trans ((PowerSeries.idealX K).valuation_le_one F)
        rw [← log_le_iff_le_exp one_ne_zero, log_one]
        lia
      · obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le hDs.le
        rw [← neg_neg (-D + ↑s), ← sub_eq_neg_add, neg_sub, hd]
        apply (intValuation_le_iff_coeff_lt_eq_zero K F).mpr
        intro n hn
        rw [powerSeriesPart_coeff f n, hs]
        apply h_val_f (s + n)
        lia
    · simp [ne_eq, zero_lt_iff]

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

Goal state before:
pp: case add_single
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
⊢ ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) (f✝ + fun₀ | i => b✝) r))) =
    (accumulate n m) ⇑(f✝ + fun₀ | i => b✝)

Tactic:
have := i.2.trans_le hnm
    rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
        Monic.supDegree_mul_of_ne_zero_left toLex.injective toLex_add, ofLex_add, Finsupp.coe_add,
        ih, Finsupp.coe_add, map_add, Monic.supDegree_pow rfl toLex_add toLex.injective, ofLex_smul,
        Finsupp.coe_smul, supDegree_esymm this, ← map_nsmul, ← Finsupp.coe_smul,
        Finsupp.smul_single, nsmul_one, Nat.cast_id]
    · exact monic_esymm this
    · exact (monic_esymm this).pow toLex_add toLex.injective
    · rwa [Ne, ← leadingCoeff_eq_zero toLex.injective, leadingCoeff_esymmAlgHomMonomial _ hnm]

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

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∈ t.1
h3 : 1 ≤ #t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - (#t.1 - 1))) +
      (-1) ^ (#t.1 - 1) * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - (#t.1 - 1))) =
    0

Tactic:
← neg_neg ((-1 : MvPolynomial σ R) ^ (#t.1 - 1)),

Goal state after:
case inl
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∈ t.1
h3 : 1 ≤ #t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - (#t.1 - 1))) +
      - -(-1) ^ (#t.1 - 1) * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - (#t.1 - 1))) =
    0
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| (expand p hp) (C r * 1)

Tactic:
← smul_eq_C_mul,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| (expand p hp) (r • 1)
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
m : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
d : σ →₀ ℕ
⊢ d ≠ m → (coeff d) φ * (coeff (p • m)) (d.prod fun s e ↦ (X s ^ p) ^ e) = 0

Tactic:
hd

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
d : σ →₀ ℕ
hd : d ≠ m
⊢ (coeff d) φ * (coeff (p • m)) (d.prod fun s e ↦ (X s ^ p) ^ e) = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) *
      (↑k * esymm σ R k -
        (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2) =
    (-1) ^ (k + 1) *
      ((-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2)
⊢ psum σ R k =
    (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ x ∈ antidiagonal k with x.1 < k ∧ 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2

Tactic:
simp only [mul_sub_left_distrib, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k + 1, rfl⟩, one_mul,
    filter_filter (fun a : ℕ × ℕ ↦ a.fst < k) (fun a ↦ ¬0 < a.fst)]
    at sub_both_sides

Goal state after:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
⊢ psum σ R k =
    (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ x ∈ antidiagonal k with x.1 < k ∧ 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
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 : σ →₀ ℕ
⊢ d ∈ Function.support ((expand p hp) φ) → d ∈ (fun x ↦ p • x) '' Function.support φ

Tactic:
hd

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : d ∈ Function.support ((expand p hp) φ)
⊢ d ∈ (fun x ↦ p • x) '' Function.support φ
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 : σ →₀ ℕ
⊢ d ∈ (fun x ↦ p • x) '' Function.support φ → d ∈ Function.support ((expand p hp) φ)

Tactic:
hd

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : d ∈ (fun x ↦ p • x) '' Function.support φ
⊢ d ∈ Function.support ((expand p hp) φ)
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
f g : M → S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
hC' : 0 ≤ C
a : M
this : 0 ≤ C a
⊢ ‖∑ p ∈ antidiagonal a, f p.1 * g p.2‖ * C a ≤ (antidiagonal a).sup' ⋯ fun i ↦ ‖f i.1‖ * C i.1 * (‖g i.2‖ * C i.2)

Tactic:
grw [(nonempty_antidiagonal _).norm_sum_le_sup'_norm, Finset.sup'_mul₀ this]

Goal state after:
M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
f g : M → S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
hC' : 0 ≤ C
a : M
this : 0 ≤ C a
⊢ ((antidiagonal a).sup' ⋯ fun i ↦ ‖f i.1 * g i.2‖ * C a) ≤
    (antidiagonal a).sup' ⋯ fun i ↦ ‖f i.1‖ * C i.1 * (‖g i.2‖ * C i.2)
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) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
⊢ ∀ l ∈ ofFn ⇑v, l < up

Tactic:
by
  grind

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) →₀ ℕ
a : k
ha : a ≠ 0
h : ∀ (i : Fin n), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
i : Fin n
x✝ : i ∈ Finset.univ
⊢ v i.succ * (Polynomial.X ^ up ^ ↑i.succ + Polynomial.C (MvPolynomial.X i)).natDegree = up ^ ↑i.succ * v i.succ

Tactic:
natDegree_X_pow_add_C,

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
h : ∀ (i : Fin n), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
i : Fin n
x✝ : i ∈ Finset.univ
⊢ v i.succ * up ^ ↑i.succ = up ^ ↑i.succ * v i.succ
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
h : ∃ N, ∀ n ≥ N, ∃ z, (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]
⊢ x.teichmullerFun = y

Tactic:
by
  obtain ⟨N, h⟩ := h
  refine (IsHausdorff.eq_iff_smodEq (I := I)).mpr fun n ↦ ?_
  rw [smul_eq_mul, Ideal.mul_top]
  obtain hn | hn := le_total n N
  · obtain ⟨z, hz₁, hz₂⟩ := h N le_rfl
    exact ((teichmullerFun_sModEq hz₁).trans hz₂).mono <| Ideal.pow_le_pow_right (by omega)
  · obtain ⟨z, hz₁, hz₂⟩ := h n hn
    exact ((teichmullerFun_sModEq hz₁).trans hz₂).mono <| Ideal.pow_le_pow_right (by omega)

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 w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
⊢ Ideal.map (T f) I = Ideal.map (↑g.symm) (Ideal.map g (Ideal.map (T f) I))

Tactic:
have : g.symm.toRingEquiv.toRingHom.comp g = RingHom.id _ :=
    g.toRingEquiv.symm_toRingHom_comp_toRingHom

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
this : g.symm.toRingEquiv.toRingHom.comp ↑g = RingHom.id (MvPolynomial (Fin (n + 1)) k)
⊢ Ideal.map (T f) I = Ideal.map (↑g.symm) (Ideal.map g (Ideal.map (T f) I))
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i : ℕ
H : i ∈ (range n).biUnion fun i ↦ (C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars
⊢ i ∈ range n

Tactic:
rw [mem_biUnion] at H

Goal state after:
case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i : ℕ
H : ∃ a ∈ range n, i ∈ (C (↑p ^ a) * xInTermsOfW p ℚ a ^ p ^ (n - a)).vars
⊢ i ∈ range n
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
H : n ∈ (range n).biUnion fun i ↦ (C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars
⊢ False

Tactic:
rw [mem_biUnion] at H

Goal state after:
case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
H : ∃ a ∈ range n, n ∈ (C (↑p ^ a) * xInTermsOfW p ℚ a ^ p ^ (n - a)).vars
⊢ False
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
idx : Type u_1
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)
⊢ f = g

Tactic:
by
  ext1 n
  apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  rw [← funext_iff] at h
  replace h :=
    congr_arg (fun fam => bind₁ (MvPolynomial.map (Int.castRingHom ℚ) ∘ fam) (xInTermsOfW p ℚ n)) h
  simpa only [Function.comp_def, map_bind₁, map_wittPolynomial, ← bind₁_bind₁,
    bind₁_wittPolynomial_xInTermsOfW, bind₁_X_right] using h

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)
⊢ f = g

Tactic:
by
  ext1 n
  apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  rw [← funext_iff] at h
  replace h :=
    congr_arg (fun fam => bind₁ (MvPolynomial.map (Int.castRingHom ℚ) ∘ fam) (xInTermsOfW p ℚ n)) h
  simpa only [Function.comp_def, map_bind₁, map_wittPolynomial, ← bind₁_bind₁,
    bind₁_wittPolynomial_xInTermsOfW, bind₁_X_right] using h

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPoly p n) = frobeniusPolyRat p n

Tactic:
frobeniusPoly,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (X n ^ p + C ↑p * frobeniusPolyAux p n) = frobeniusPolyRat p n
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
⊢ ∀ (n_1 : ℕ),
    (fun m ↦
            if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
            else x ^ p ^ (n - m))
          (n_1 + 1) ^
        p =
      (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        n_1

Tactic:
intro m
    obtain (h1 | h1 | h1) : n ≤ m ∨ n = m + 1 ∨ ¬ n ≤ m + 1 := by lia
    · have h1' : n ≤ m + 1 := by lia
      simp only [h1', ↓reduceDIte, h1, Nat.leRec_succ, ← frobenius_def]
      exact Classical.choose_spec (h _)
    · subst h1
      simp [← frobenius_def]
    · have h1' : ¬ n ≤ m := by lia
      have : n - m = (n - (m + 1)) + 1 := by lia
      simp [h1, h1', this, pow_succ, pow_mul]

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

Goal state before:
pp: case refine_3
p : ℕ
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (n : ℕ), (ghostComponent n) (x✝ + y✝).verschiebungFun = (ghostComponent n) (x✝.verschiebungFun + y✝.verschiebungFun)

Tactic:
rintro ⟨⟩ <;> ghost_simp

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),
    (-x).coeff = fun n ↦ (aeval x.coeff) ((fun n ↦ (rename Prod.snd) (wittNeg p n)) n)

Tactic:
intros; funext n
      rw [neg_coeff, aeval_eq_eval₂Hom, eval₂Hom_rename]
      apply eval₂Hom_congr rfl _ rfl
      ext ⟨i, k⟩; fin_cases i; rfl

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
hf : IsPoly p f
g : R →+* S
x : 𝕎 R
⊢ (WittVector.map g) (f x) = f ((WittVector.map g) x)

Tactic:
obtain ⟨φ, hf⟩ := hf
  ext n
  simp_rw [map_coeff, hf, map_aeval, funext (map_coeff g _), RingHom.ext_int _ (algebraMap ℤ S),
    aeval_eq_eval₂Hom]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n) = X n ^ p

Tactic:
frobeniusPoly,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom (ZMod p))) (X n ^ p + C ↑p * frobeniusPolyAux p n) = X n ^ p
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
⊢ teichmullerFun p 1 = 1

Tactic:
ext ⟨⟩
    · rw [one_coeff_zero]; rfl
    · rw [one_coeff_eq_of_pos _ _ _ (Nat.succ_pos _)]; rfl

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

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

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

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : 𝕎 (R ⧸ 𝔭)
h : 𝔭 ^ (0 + 1) = 𝔭
⊢ (quotEquivOfEq h) ((ghostComponentModPPow 0) x) = (ghostComponent 0) x

Tactic:
obtain ⟨y, hy⟩ := map_surjective _ Ideal.Quotient.mk_surjective x

Goal state after:
R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : 𝕎 (R ⧸ 𝔭)
h : 𝔭 ^ (0 + 1) = 𝔭
y : 𝕎 R
hy : (map (Ideal.Quotient.mk 𝔭)) y = x
⊢ (quotEquivOfEq h) ((ghostComponentModPPow 0) x) = (ghostComponent 0) x