mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂
a✝ : x ∈ ⊤
X : G →₀ ↥S →₀ ↑A
hX : mapRange ⇑(ConcreteCategory.hom (chains₁ToCoinvariantsKer (res S.subtype A))) ⋯ X = x
Y : ↥S →₀ ↑A :=
  X.sum fun g f ↦ (mapRange.linearMap (A.ρ g⁻¹)) ((lmapDomain (↑A) k fun s ↦ (MulAut.conjNormal g⁻¹) s) f) - f
⊢ x ∈
    Submodule.comap
      (ModuleCat.Hom.hom
        ((mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂ ≫ (shortComplexH1 A).pOpcycles))
      (ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles)).range

Tactic:
let Z : G × G →₀ A := X.sum fun g f =>
    lmapDomain _ k (fun s => (g, g⁻¹ * s.1 * g)) f - lmapDomain _ k (fun s => (s.1, g)) f

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂
a✝ : x ∈ ⊤
X : G →₀ ↥S →₀ ↑A
hX : mapRange ⇑(ConcreteCategory.hom (chains₁ToCoinvariantsKer (res S.subtype A))) ⋯ X = x
Y : ↥S →₀ ↑A :=
  X.sum fun g f ↦ (mapRange.linearMap (A.ρ g⁻¹)) ((lmapDomain (↑A) k fun s ↦ (MulAut.conjNormal g⁻¹) s) f) - f
Z : G × G →₀ ↑A :=
  X.sum fun g f ↦ (lmapDomain (↑A) k fun s ↦ (g, g⁻¹ * ↑s * g)) f - (lmapDomain (↑A) k fun s ↦ (↑s, g)) f
⊢ x ∈
    Submodule.comap
      (ModuleCat.Hom.hom
        ((mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂ ≫ (shortComplexH1 A).pOpcycles))
      (ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles)).range
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
e : ↥T → ℕ
g : ↥T → ↥S
hg : ∀ (a : ↥T), g a • ↑a ^ e a • m = 0
a : R
ha : a ∈ ↑T
⊢ g ⟨a, ha⟩ ∣ ∏ a, g a

Tactic:
apply Finset.dvd_prod_of_mem g (Finset.mem_univ ⟨a, ha⟩)

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
a✝ b✝ : A
hx : a✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n a✝) = hJ.dpow n (f a✝)
hy : b✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n b✝) = hJ.dpow n (f b✝)
n : ℕ
⊢ f (hI.dpow n (a✝ + b✝)) = hJ.dpow n (f a✝ + f b✝)

Tactic:
hI.dpow_add hx.1 hy.1,

Goal state after:
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
a✝ b✝ : A
hx : a✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n a✝) = hJ.dpow n (f a✝)
hy : b✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n b✝) = hJ.dpow n (f b✝)
n : ℕ
⊢ f (∑ k ∈ Finset.antidiagonal n, hI.dpow k.1 a✝ * hI.dpow k.2 b✝) = hJ.dpow n (f a✝ + f b✝)
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
h : map f I ≤ J
⊢ hI.IsDPMorphism hJ f

Tactic:
exact ⟨h, fun a ha ↦ by
      rw [← fromGens_coe hI hJ hS h hdp, (fromGens hI hJ hS h hdp).dpow_comp a ha]⟩

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case refine_1
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
⊢ x ∈ I → ∃ a, x = ε * a

Tactic:
← dvd_def

Goal state after:
case refine_1
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
⊢ x ∈ I → ε ∣ x
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
x✝ : ℕ
hn : x✝ ≠ 0
x : A
hx : ∀ i ∈ insert ⊤ S, x ∈ i.carrier
⊢ ∀ i ∈ insert ⊤ S, hI.dpow x✝ x ∈ i.carrier

Tactic:
exact fun s hs ↦ s.dpow_mem _ hn x (hx s hs)

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
⊢ (∃ a, x = ε * a) → x ∈ I

Tactic:
← dvd_def

Goal state after:
case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
⊢ ε ∣ x → x ∈ I
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Field k
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra k R
inst✝³ : Algebra R S
inst✝² : IsSepClosed k
inst✝¹ : EssFiniteType k R
inst✝ : FormallyEtale k R
⊢ IsFiniteSplit k R

Tactic:
have := FormallyUnramified.finite_of_free k R
  have : IsArtinianRing R := isArtinian_of_tower k inferInstance
  exact .of_algEquiv (Algebra.FormallyEtale.equivPiOfIsSepClosed k R).symm

Goal state after:
Module: Mathlib.RingTheory.Flat.LocallyFree

Goal state before:
pp: case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
h✝ : Nontrivial R
⊢ ∃ a ∉ p, Free (Localization.Away a) (LocalizedModule.Away a M)

Tactic:
· let Rₚ := Localization.AtPrime p
    let n := rankAtStalk M ⟨p, inferInstance⟩
    let f : (Fin n →₀ R) →ₗ[R] Fin n →₀ Rₚ := Finsupp.mapRange.linearMap (Algebra.linearMap R Rₚ)
    let g : M →ₗ[R] LocalizedModule.AtPrime p M := LocalizedModule.mkLinearMap p.primeCompl M
    obtain ⟨φ, -, -, hφps⟩ := exists_localizedMap_surjective_of_surjective p.primeCompl f g
      ((finBasis Rₚ (LocalizedModule.AtPrime p M)).repr.restrictScalars R).symm.surjective
    obtain ⟨a, hap, hφas⟩ := by
      refine exists_localizedMap_away_surjective_of_localizedMap_atPrime_surjective p φ ?_
      simpa [LocalizedModule.coe_map_eq f g]
    have : Module.Free (Localization.Away a) (LocalizedModule.Away a (Fin n →₀ R)) :=
      free_of_isLocalizedModule (Submonoid.powers a) (mkLinearMap (Submonoid.powers a) (Fin n →₀ R))
    let φₐ : LocalizedModule.Away a (Fin n →₀ R) →ₗ[Localization.Away a] LocalizedModule.Away a M :=
      LocalizedModule.map (Submonoid.powers a) φ
    refine ⟨a, hap, Module.Free.of_equiv <| LinearEquiv.ofBijective φₐ <|
      bijective_of_surjective_of_rankAtStalk_eq hφas <| fun m _ ↦ ?_⟩
    obtain ⟨𝔪, _, hm𝔪⟩ : ∃ 𝔪 : Ideal R, 𝔪.IsMaximal ∧ PrimeSpectrum.comap
        (algebraMap R (Localization (Submonoid.powers a))) ⟨m, inferInstance⟩ ≤ 𝔪 :=
      (m.comap (algebraMap R (Localization.Away a))).exists_le_maximal Ideal.IsPrime.ne_top'
    simp [rankAtStalk_isBaseChange (LocalizedModule.isBaseChange (Submonoid.powers a) _),
      rankAtStalk_eq_of_le_of_finite_of_flat' M hm𝔪, h 𝔪, n]

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Function.Surjective ⇑(map (defaultHom R S P))

Tactic:
← LinearMap.range_eq_top,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (map (defaultHom R S P)).range = ⊤
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: case e'_4
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
G : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulSemiringAction G S
inst✝⁶ : SMulCommClass G R S
Q : Ideal S
inst✝⁵ : Finite G
inst✝⁴ : Algebra.IsInvariant R S G
inst✝³ : Q.IsPrime
inst✝² : Finite (S ⧸ Q)
Q' : Ideal S
inst✝¹ : Q'.IsPrime
inst✝ : Finite (S ⧸ Q')
H : Ideal.under R Q = Ideal.under R Q'
P : Ideal R
hP : P.IsPrime
h₁ : P = Ideal.under R Q
h₂ : P = Ideal.under R Q'
⊢ arithFrobAt R G Q' = ⋯.choose ⟨Q', ⋯⟩

Tactic:
subst h₂

Goal state after:
case e'_4
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
G : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulSemiringAction G S
inst✝⁶ : SMulCommClass G R S
Q : Ideal S
inst✝⁵ : Finite G
inst✝⁴ : Algebra.IsInvariant R S G
inst✝³ : Q.IsPrime
inst✝² : Finite (S ⧸ Q)
Q' : Ideal S
inst✝¹ : Q'.IsPrime
inst✝ : Finite (S ⧸ Q')
H : Ideal.under R Q = Ideal.under R Q'
hP : (Ideal.under R Q').IsPrime
h₁ : Ideal.under R Q' = Ideal.under R Q
⊢ arithFrobAt R G Q' = ⋯.choose ⟨Q', ⋯⟩
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: case inr.right.refine_1
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h✝ : Nontrivial A
this : ((binomialFamily x r) 0).coeff 0 = 1
⊢ ∀ (b : ℕ), ∀ g' ∈ ((binomialFamily x r) b).support, 0 ≤ g'

pp: case inr.right.refine_2
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h✝ : Nontrivial A
this : ((binomialFamily x r) 0).coeff 0 = 1
⊢ ∀ (b : ℕ), b ≠ 0 → ((binomialFamily x r) b).coeff 0 = 0

Tactic:
· intro b g' hg'
        exact binomialFamily_mem_support hx r b hg'

Goal state after:
case inr.right.refine_2
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h✝ : Nontrivial A
this : ((binomialFamily x r) 0).coeff 0 = 1
⊢ ∀ (b : ℕ), b ≠ 0 → ((binomialFamily x r) b).coeff 0 = 0
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
g : Γ
h : 0 < x.orderTop
⊢ {a | (x ^ a).coeff g ≠ 0}.Finite

Tactic:
exact pow_finite_co_support h g

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

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot (L ⊓ K) K
k : A
hk : k ∈ K
I : Ideal A
hI : I ∈ F
hI_le : I ≤ Submodule.colon (L ⊓ K) {k}
hcol : Submodule.colon (L ⊓ K) {k} = Submodule.colon L {k}
⊢ I ≤ Submodule.colon L {k}

Tactic:
simpa [hcol] using hI_le

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

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot L K
k : A
hk : k ∈ K
I : Ideal A
hI : I ∈ F
hI_le : I ≤ Submodule.colon L {k}
hcol : Submodule.colon (L ⊓ K) {k} = Submodule.colon L {k}
⊢ I ≤ Submodule.colon (L ⊓ K) {k}

Tactic:
simpa [hcol] using hI_le

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
⊢ DenseRange ⇑(Hom.hom P.toLimit)

Tactic:
apply dense_iff_inter_open.mpr

Goal state after:
P : ProfiniteGrp.{u}
⊢ ∀ (U : Set ↑(limit P.diagram).toProfinite.toTop),
    IsOpen U → U.Nonempty → (U ∩ Set.range ⇑(Hom.hom P.toLimit)).Nonempty
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
⊢ DenseRange ⇑(Hom.hom P.toLimit)

Tactic:
apply dense_iff_inter_open.mpr
  rintro U ⟨s, hsO, hsv⟩ ⟨⟨spc, hspc⟩, uDefaultSpec⟩
  simp_rw [← hsv, Set.mem_preimage] at uDefaultSpec
  rcases (isOpen_pi_iff.mp hsO) _ uDefaultSpec with ⟨J, fJ, hJ1, hJ2⟩
  let M := iInf (fun (j : J) => j.1.1.1)
  have hM : M.Normal := Subgroup.normal_iInf_normal fun j => j.1.isNormal'
  have hMOpen : IsOpen (M : Set P) := by
    rw [Subgroup.coe_iInf]
    exact isOpen_iInter_of_finite fun i => i.1.1.isOpen'
  let m : OpenNormalSubgroup P := { M with isOpen' := hMOpen }
  rcases QuotientGroup.mk'_surjective M (spc m) with ⟨origin, horigin⟩
  use (toLimit P) origin
  refine ⟨?_, origin, rfl⟩
  rw [← hsv]
  apply hJ2
  intro a a_in_J
  let M_to_Na : m ⟶ a := (iInf_le (fun (j : J) => j.1.1.1) ⟨a, a_in_J⟩).hom
  rw [← (P.toLimit origin).property M_to_Na]
  change (P.toFiniteQuotientFunctor.map M_to_Na) (QuotientGroup.mk' M origin) ∈ _
  rw [horigin]
  exact Set.mem_of_eq_of_mem (hspc M_to_Na) (hJ1 a a_in_J).2

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
w✝ : IsLocalRing R
this✝ : (maximalIdeal R).IsPrime
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : maximalIdeal R ∈ (span (insert x ↑s')).minimalPrimes
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : ↑s' ⊆ ↑(q ⊔ span {x}).radical
t✝ : ↑↑s' → R
ht : Set.range t✝ ⊆ ↑q
hspan : ↑s' ⊆ ↑(span (Set.range t✝) ⊔ span {x}).radical
t : Finset R := Finset.image t✝ Finset.univ
⊢ ↑t = Set.range t✝

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
w✝ : IsLocalRing R
this✝ : (maximalIdeal R).IsPrime
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : maximalIdeal R ∈ (span (insert x ↑s')).minimalPrimes
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : ↑s' ⊆ ↑(q ⊔ span {x}).radical
t✝ : ↑↑s' → R
ht : Set.range t✝ ⊆ ↑q
hspan : ↑s' ⊆ ↑(span (Set.range t✝) ⊔ span {x}).radical
t : Finset R := Finset.image t✝ Finset.univ
⊢ ↑s' ⊆ ↑(span (insert x (Set.range t✝))).radical

Tactic:
· simp [t]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
w✝ : IsLocalRing R
this✝ : (maximalIdeal R).IsPrime
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : maximalIdeal R ∈ (span (insert x ↑s')).minimalPrimes
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : ↑s' ⊆ ↑(q ⊔ span {x}).radical
t✝ : ↑↑s' → R
ht : Set.range t✝ ⊆ ↑q
hspan : ↑s' ⊆ ↑(span (Set.range t✝) ⊔ span {x}).radical
t : Finset R := Finset.image t✝ Finset.univ
⊢ ↑s' ⊆ ↑(span (insert x (Set.range t✝))).radical
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
s : Set R
hs : s ⊆ ↑p
⊢ span s ≤ p

Tactic:
simpa [span_le]

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
s : Finset (Submodule R M)
hs : s ⊆ t
hs' : Finset.image (fun q ↦ (q.colon Set.univ).radical) s = Finset.image Subtype.val s₀
⊢ comap (mkLinearMap (⨅ q ∈ s₀, (↑q).primeCompl) M)
      (localized₀ (⨅ q ∈ s₀, (↑q).primeCompl) (mkLinearMap (⨅ q ∈ s₀, (↑q).primeCompl) M) N) =
    ⨅ q ∈ s, q

Tactic:
by
  set S := ⨅ q ∈ s₀, q.1.primeCompl
  set f := mkLinearMap S M
  rw [← ht.inf_eq, ← localized₀FrameHom_apply, map_finset_inf, Submodule.comap_finsetInf]
  simp_rw [Function.comp_def, id_eq, localized₀FrameHom_apply]
  suffices ∀ q ∈ t, (localized₀ S f q).comap f = if q ∈ s then q else ⊤ by
    rw [Finset.inf_congr rfl this, Finset.inf_ite, Finset.inf_top, inf_top_eq,
      Finset.filter_mem_eq_inter, Finset.inter_eq_right.mpr hs, Finset.inf_eq_iInf]
  refine fun q hqt ↦ (IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite s₀ hs₀ q
    (ht.primary hqt) ⟨(q.colon Set.univ).radical, ht.mem_associatedPrimes hqt⟩ rfl).trans
    (ite_cond_congr (Iff.trans ?_ (ht.injOn.mem_image_iff hs hqt)).eq)
  grind [Finset.mem_image_of_mem]

Goal state after:
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
⊢ Subring.center D = ⊤

Tactic:
by
  classical
  cases nonempty_fintype D
  induction hn : Fintype.card D using Nat.strong_induction_on generalizing D with | _ n IH
  apply InductionHyp.center_eq_top
  intro R hR x y hx hy
  suffices (⟨y, hy⟩ : R) ∈ Subring.center R by
    rw [Subring.mem_center_iff] at this
    simpa using this ⟨x, hx⟩
  let R_dr : DivisionRing R := Fintype.divisionRingOfIsDomain R
  rw [IH (Fintype.card R) _ R inferInstance rfl]
  · trivial
  rw [← hn, ← Subring.card_top D]
  convert! Set.card_lt_card hR

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : MvPolynomial σ 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, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]

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

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
⊢ (-1) ^ (k + 1) * ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
      (-1) ^ (k + 1) * ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    0

Tactic:
← left_distrib,

Goal state after:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
⊢ (-1) ^ (k + 1) *
      (∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t) =
    0
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
f : MvPolynomial (Fin (d + 1)) k
fi : f ∈ I
fne : f ≠ 0
ϕ : MvPolynomial (Fin d) k ⧸ ker (hom2 f I) →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I := kerLiftAlg (hom2 f I)
this : Nontrivial (MvPolynomial (Fin (d + 1)) k ⧸ I)
s : ℕ
left✝ : s ≤ d
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ ker (hom2 f I)
injg : Function.Injective ⇑g
intg : g.IsIntegral
a : MvPolynomial (Fin d) k
⊢ ((kerLiftAlg (hom2 f I)).comp (Quotient.mkₐ k (ker (hom2 f I)))) a = (hom2 f I) a

Tactic:
by
          simp only [AlgHom.coe_comp, Quotient.mkₐ_eq_mk, Function.comp_apply, kerLiftAlg_mk]

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 : ℕ
hp : Fact (Nat.Prime p)
x y : ModP O p
hx : x ^ p ≠ 0
hy : y ^ p ≠ 0
⊢ x * y ≠ 0

Tactic:
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
  obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y
  have h1p : (0 : ℝ) < 1 / p := one_div_pos.2 (Nat.cast_pos.2 hp.1.pos)
  rw [← (Ideal.Quotient.mk (Ideal.span {(p : O)})).map_mul]
  rw [← (Ideal.Quotient.mk (Ideal.span {(p : O)})).map_pow] at hx hy
  rw [← v_p_lt_val hv] at hx hy ⊢
  rw [map_pow, v.map_pow, ← rpow_lt_rpow_iff h1p, ← rpow_natCast, ← rpow_mul,
    mul_one_div_cancel (Nat.cast_ne_zero.2 hp.1.ne_zero : (p : ℝ) ≠ 0), rpow_one] at hx hy
  rw [map_mul, v.map_mul]; refine lt_of_le_of_lt ?_ (mul_lt_mul'' hx hy zero_le zero_le)
  by_cases hvp : v p = 0
  · rw [hvp]; exact zero_le
  replace hvp := zero_lt_iff.2 hvp
  conv_lhs => rw [← rpow_one (v p)]
  rw [← rpow_add (ne_of_gt hvp)]
  refine rpow_le_rpow_of_exponent_ge hvp (map_natCast (algebraMap O K) p ▸ hv.2 _) ?_
  rw [← add_div, div_le_one (Nat.cast_pos.2 hp.1.pos : 0 < (p : ℝ))]; exact mod_cast hp.1.two_le

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:
rw [frobeniusPoly, map_add, map_pow, map_mul, map_X, map_C]
  simp only [Int.cast_natCast, add_zero, eq_intCast, ZMod.natCast_self, zero_mul, C_0]

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ frobeniusFun 1 = 1

Tactic:
refine
      IsPoly.ext (IsPoly.comp (hg := frobeniusFun_isPoly p) (hf := WittVector.oneIsPoly))
        (IsPoly.comp (hg := WittVector.oneIsPoly) (hf := frobeniusFun_isPoly p)) ?_ _ 0
    simp only [Function.comp_apply, map_one, forall_const]
    ghost_simp

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

Goal state before:
pp: case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0

Tactic:
rw [Finset.mem_range]; intro h; exact (h (Nat.succ_pos n)).elim

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

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ (teichmullerFun p 1).coeff (n✝ + 1) = coeff 1 (n✝ + 1)

Tactic:
rw [one_coeff_eq_of_pos _ _ _ (Nat.succ_pos _)]

Goal state after:
case succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ (teichmullerFun p 1).coeff (n✝ + 1) = 0
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
⊢ x ∈ Ideal.span {↑p} ↔ x.coeff 0 = 0

Tactic:
simp_rw [Ideal.mem_span_singleton, dvd_def, mul_comm]
  refine ⟨fun ⟨u, hu⟩ ↦ ?_, fun h ↦ ?_⟩
  · rw [hu, mul_charP_coeff_zero]
  · use (frobeniusEquiv p k).symm (x.shift 1)
    calc
    _ = verschiebung (x.shift 1) := by
      simpa using eq_iterate_verschiebung (n := 1) (by simp [h])
    _ = _ := by
      rw [← verschiebung_frobenius, ← frobeniusEquiv_apply,
          RingEquiv.apply_symm_apply (frobeniusEquiv p k) _]

Goal state after: