mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ ∀ (i : { s // Submodule.span R ↑s = I }), p.height ≤ ↑(↑i).card

Tactic:
rintro ⟨s, (rfl : span s = I)⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
⊢ p.height ≤ ↑(↑⟨s, ⋯⟩).card
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
⊢ Continuous fun a ↦ (Subtype.val ∘ ⇑P.toLimitFun) a H

Tactic:
dsimp only [Functor.comp_obj, CompHausLike.coe_of, Functor.comp_map,
    CompHausLike.toCompHausLike_map, CompHausLike.compHausLikeToTop_map, Set.mem_ofPred_eq,
    toLimitFun, MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply]

Goal state after:
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
⊢ Continuous fun a ↦ ↑a
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑(P.diagram.obj H).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
x : ↑P.toProfinite.toTop
⊢ ↑x = i ↔ x ∈ Quotient.out i • (↑H.toOpenSubgroup).carrier

Tactic:
← QuotientGroup.out_eq' i,

Goal state after:
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑(P.diagram.obj H).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
x : ↑P.toProfinite.toTop
⊢ ↑x = ↑(Quotient.out i) ↔ x ∈ Quotient.out i • (↑H.toOpenSubgroup).carrier
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : PrimeSpectrum R
⊢ Order.krullDim (PrimeSpectrum (p.asIdeal.Fiber R[X])) ≤ ↑1

Tactic:
← ringKrullDim,

Goal state after:
R : Type u_1
inst✝ : CommRing R
p : PrimeSpectrum R
⊢ ringKrullDim (p.asIdeal.Fiber R[X]) ≤ ↑1
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this✝ : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset
⊢ p ∈ (span (↑o ∪ Submodule.generators I)).minimalPrimes

Tactic:
span_union,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this✝ : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset
⊢ p ∈ (span ↑o ⊔ span (Submodule.generators I)).minimalPrimes
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
r : R
p : Ideal R
inst✝ : p.IsPrime
hrm : r ∈ p
⊢ p.height ≤ (map (Quotient.mk (span {r})) p).height + 1

Tactic:
by
  convert! height_le_height_add_encard_of_subset { r } (p := p) (by simpa)
  simp

Goal state after:
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
⊢ (↑(Finset.image (fun t ↦ t.inf id)
          (Finset.image (fun J ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s))).Pairwise
    ((fun x1 x2 ↦ x1 ≠ x2) on fun J ↦ (J.colon Set.univ).radical)

Tactic:
· intro I hI J hJ hIJ
    simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ
    obtain ⟨I', hI', hI⟩ := hI
    obtain ⟨J', hJ', hJ⟩ := hJ
    simp only [Function.onFun, ne_eq]
    contrapose hIJ
    suffices (I'.colon Set.univ).radical = (J'.colon Set.univ).radical by
      rw [← hI, ← hJ, this]
    · rw [← hI, colon_finsetInf,
        radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ
      rw [hIJ, ← hJ, colon_finsetInf,
        radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq]

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ p ∈ radical '' ↑t

Tactic:
have htp : t.inf radical ≤ p := by
    rw [← hp.1.1.radical]
    refine le_trans ?_ (radical_mono hp.1.2)
    rw [← ht.inf_eq, ← radicalInfTopHom_apply, map_finset_inf]
    rfl

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
htp : t.inf radical ≤ p
⊢ p ∈ radical '' ↑t
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    HasProjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
inst✝ : Module.Finite R ↑M
P : Type v
w✝³ : AddCommGroup P
w✝² : Module R P
w✝¹ : Module.Free R P
w✝ : Module.Finite R P
f : P →ₗ[R] ↑M
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
S_exact : f.shortComplexKer.ShortExact
proj : Projective S.X₂
⊢ HasProjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)

Tactic:
let Sp (p : MaximalSpectrum R) := S.map (ModuleCat.localizedModuleFunctor p.1.primeCompl)

Goal state after:
case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    HasProjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
inst✝ : Module.Finite R ↑M
P : Type v
w✝³ : AddCommGroup P
w✝² : Module R P
w✝¹ : Module.Free R P
w✝ : Module.Finite R P
f : P →ₗ[R] ↑M
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
S_exact : f.shortComplexKer.ShortExact
proj : Projective S.X₂
Sp : (p : MaximalSpectrum R) → ShortComplex (ModuleCat (Localization p.asIdeal.primeCompl)) :=
  fun p ↦ S.map (localizedModuleFunctor p.asIdeal.primeCompl)
⊢ HasProjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
β : S
hadj : R[β] = ⊤
⊢ map (residue R) (minpoly R β) = minpoly (ResidueField R) ((residue S) β)

Tactic:
have h := minpoly.monic <| Algebra.IsIntegral.isIntegral (R := R) β
  -- Both monic, same degree, divisibility ⟹ equal
  refine eq_of_monic_of_dvd_of_natDegree_le
    (minpoly.monic <| Algebra.IsIntegral.isIntegral <| residue S β)
    (h.map _) (minpoly.dvd (ResidueField R) (residue S β) ?_) ?_
  · rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl]
    simp
  · have : Module.Free R S := Module.free_of_flat_of_isLocalRing
    have hβ₀ := (adjoin_residue_eq_top_iff_adjoin_eq_top β).mpr hadj
    rw [h.natDegree_map _,
      ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
      finrank_eq_finrank_residueField,
      (IsAdjoinRootMonic.mkOfAdjoinEqTop' hβ₀).finrank]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((⇑(derivative R))^[k] f).coeff n = (k.factorial • (hasseDeriv R k) f).coeff n

Tactic:
induction k generalizing f with

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
⊢ (⇑(derivative R))^[k] f = k.factorial • (hasseDeriv R k) f

Tactic:
ext n
  induction k generalizing f with
  | zero => simp
  | succ k ih =>
    rw [Function.iterate_succ, Function.comp_apply, ih, derivative_apply, hasseDeriv_comp,
      Nat.choose_symm_add, Nat.choose_one_right, Nat.factorial, mul_nsmul]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
z : R⸨X⸩
h : order z < 0
⊢ ∃ x, z * (algebraMap R⟦X⟧ R⸨X⸩) ↑x.2 = (algebraMap R⟦X⟧ R⸨X⸩) x.1

Tactic:
· refine ⟨⟨powerSeriesPart z, PowerSeries.X ^ Int.natAbs z.order, ⟨_, rfl⟩⟩, ?_⟩
      simp only [coe_algebraMap, ofPowerSeries_powerSeriesPart]
      rw [mul_comm _ z]
      refine congr rfl ?_
      rw [ofPowerSeries_X_pow, Int.ofNat_natAbs_of_nonpos]
      exact h.le

Goal state after:
Module: Mathlib.RingTheory.Localization.Pi

Goal state before:
pp: case pos
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst✝⁵ : (i : ι) → CommSemiring (R i)
inst✝⁴ : (i : ι) → CommSemiring (S i)
inst✝³ : (i : ι) → Algebra (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst✝² : ∀ (i : ι), IsLocalization (Submonoid.map (Pi.evalRingHom R i) M) (S i)
inst✝¹ : ∀ (i : ι), Ring.KrullDimLE 0 (R i)
inst✝ : ∀ (i : ι), IsLocalRing (R i)
i : ι
h₀ : 0 ∈ Submonoid.map (Pi.evalRingHom R i) M
⊢ Surjective (↑↑(algebraMap (R i) (S i))).1

pp: case neg
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst✝⁵ : (i : ι) → CommSemiring (R i)
inst✝⁴ : (i : ι) → CommSemiring (S i)
inst✝³ : (i : ι) → Algebra (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst✝² : ∀ (i : ι), IsLocalization (Submonoid.map (Pi.evalRingHom R i) M) (S i)
inst✝¹ : ∀ (i : ι), Ring.KrullDimLE 0 (R i)
inst✝ : ∀ (i : ι), IsLocalRing (R i)
i : ι
h₀ : 0 ∉ Submonoid.map (Pi.evalRingHom R i) M
⊢ Surjective (↑↑(algebraMap (R i) (S i))).1

Tactic:
· have := uniqueOfZeroMem h₀ (S := (S i))
    exact surjective_to_subsingleton (algebraMap (R i) (S i))

Goal state after:
case neg
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst✝⁵ : (i : ι) → CommSemiring (R i)
inst✝⁴ : (i : ι) → CommSemiring (S i)
inst✝³ : (i : ι) → Algebra (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst✝² : ∀ (i : ι), IsLocalization (Submonoid.map (Pi.evalRingHom R i) M) (S i)
inst✝¹ : ∀ (i : ι), Ring.KrullDimLE 0 (R i)
inst✝ : ∀ (i : ι), IsLocalRing (R i)
i : ι
h₀ : 0 ∉ Submonoid.map (Pi.evalRingHom R i) M
⊢ Surjective (↑↑(algebraMap (R i) (S i))).1
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))⁻¹ * Valued.v ((ofPowerSeries ℤ K) F - (algebraMap K⟮X⟯ K⸨X⸩) ↑P) < ↑γ

Tactic:
← PowerSeries.coe_X,

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 ((ofPowerSeries ℤ K) PowerSeries.X ^ s))⁻¹ * Valued.v ((ofPowerSeries ℤ K) F - (algebraMap K⟮X⟯ K⸨X⸩) ↑P) <
    ↑γ
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✝
this : ↑i < m
⊢ (accumulate n m) ⇑f✝ + ⇑(ofLex (supDegree (⇑toLex) (esymm (Fin m) R (↑i + 1) ^ b✝))) =
    (accumulate n m) ⇑f✝ + (accumulate n m) ⇑fun₀ | i => b✝

pp: case add_single.hq
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✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1) ^ b✝)

pp: case add_single.hp
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✝
this : ↑i < m
⊢ esymmAlgHomMonomial (Fin m) f✝ r ≠ 0

Tactic:
Monic.supDegree_pow rfl toLex_add toLex.injective,

Goal state after:
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✝
this : ↑i < m
⊢ (accumulate n m) ⇑f✝ + ⇑(ofLex (b✝ • supDegree (⇑toLex) (esymm (Fin m) R (↑i + 1)))) =
    (accumulate n m) ⇑f✝ + (accumulate n m) ⇑fun₀ | i => b✝

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✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1))

case add_single.hq
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✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1) ^ b✝)

case add_single.hp
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✝
this : ↑i < m
⊢ esymmAlgHomMonomial (Fin m) f✝ r ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
h2 : #t.1 - 1 = k
⊢ False

Tactic:
rw [← h2] at h

Goal state after:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ #t.1 - 1
h2 : #t.1 - 1 = k
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
n : ℕ
⊢ (map (iterateFrobenius R p n)) ((expand (p ^ n) ⋯) f) = f ^ p ^ n

Tactic:
by
  induction n with
  | zero => simp [map_id]
  | succ k n_ih =>
    symm
    conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
    simp_rw [← map_frobenius_expand p hp, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]

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 : ℕ
⊢ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ -
      (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ)
        (∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    (bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Tactic:
sub_right_inj

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* Perfection N p
m : M
n : ℕ
⊢ (coeffMonoidHom N p 0) (f ((powMulEquiv M (p ^ n)).symm m)) = (coeffMonoidHom N p n) (f m)

Tactic:
← coeffMonoidHom_pow_p_pow _ 0 n,

Goal state after:
M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* Perfection N p
m : M
n : ℕ
⊢ (coeffMonoidHom N p (0 + n)) (f ((powMulEquiv M (p ^ n)).symm m) ^ p ^ n) = (coeffMonoidHom N p n) (f m)
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
hn : ¬n = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ (n - 1))

Tactic:
· obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
    rw [Nat.succ_eq_add_one, add_tsub_cancel_right]
    simp only [map_mul]
    rw [map_natCast, hom_bind₁]
    calc
      _ = ghostComponent (n + 1) (verschiebung <| mk p x) := by
       apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
       funext k
       simp only [← aeval_verschiebungPoly]
       exact eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl
      _ = _ := by rw [ghostComponent_verschiebung]; rfl

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

Goal state before:
pp: case neg
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : ¬P m
⊢ 0 + (if ¬P m then X m else 0) ^ p ^ (n - m) = X m ^ p ^ (n - m)

Tactic:
if_pos,

Goal state after:
case neg
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : ¬P m
⊢ 0 + X m ^ p ^ (n - m) = X m ^ p ^ (n - m)

case neg.hc
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : ¬P m
⊢ ¬P m
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
x : TruncatedWittVector p n R
⊢ ∃ a, (truncate hm) a = x

Tactic:
obtain ⟨x, rfl⟩ := WittVector.truncate_surjective (p := p) _ R x

Goal state after:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
x : 𝕎 R
⊢ ∃ a, (truncate hm) a = (WittVector.truncate n) x
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: case h
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
n : ℕ
this : ↑p = (Ideal.Quotient.mk (𝔭 ^ (n + 1))) ↑p
⊢ ↑p ^ (n + 1) ∈ 𝔭 ^ (n + 1)

Tactic:
exact Ideal.pow_mem_pow (mem_span_singleton_self _) _

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ dickson 1 1 (m * n) = (dickson 1 1 m).comp (dickson 1 1 n)

Tactic:
rw [h]

Goal state after:
R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ dickson 1 ((Int.castRingHom R) 1) (m * n) =
    (dickson 1 ((Int.castRingHom R) 1) m).comp (dickson 1 ((Int.castRingHom R) 1) n)
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ map (ZMod.castHom ⋯ K) (dickson 1 1 p) = map (ZMod.castHom ⋯ K) (X ^ p)

Tactic:
rw [map_dickson, Polynomial.map_pow, map_X]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ dickson 1 ((ZMod.castHom ⋯ K) 1) p = X ^ p
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
trinomial : R → R[X] := fun r ↦ a • X ^ 2 + r • X + C a
ht : ∀ (r : R), (X + C 1) * trinomial r = a • X ^ 3 + (a + r) • X ^ 2 + (a + r) • X + C a
⊢ (fun x ↦ (X + C 1) * x) (trinomial b) = (fun x ↦ (X + C 1) * x) (trinomial c)

Tactic:
by simp_rw [ht, eq]

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

Goal state before:
pp: n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ 1 = 0

Tactic:
rwa [key, left_eq_add] at h1

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

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap

Tactic:
have hπ (x : S) : π (g • x) = π x := (Ideal.Quotient.mk_eq_mk_iff_sub_mem (g • x) x).mpr (hg x)

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
hπ : ∀ (x : S), π (g • x) = π x
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
this :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
x : ℕ
hx : x ∈ Ico 1 n
⊢ (if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) = (x - 1).largeSchroder * (n - x).largeSchroder

Tactic:
have hx' : 0 < x := by grind

Goal state after:
n : ℕ
hn : 0 < n
this :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
x : ℕ
hx : x ∈ Ico 1 n
hx' : 0 < x
⊢ (if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) = (x - 1).largeSchroder * (n - x).largeSchroder
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f x y : M →ₚₗ[R] N
m : M
⊢ (x + y).ground m = (x.ground + y.ground) m

Tactic:
simp [ground]

Goal state after: