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

Goal state before:
pp: n✝ : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n✝ →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n✝ + 1)
h✝ : Nontrivial R
this✝⁴ : Nontrivial S
U : Type u
w✝⁶ : CommRing U
w✝⁵ : Algebra S U
e✝ : S ⊗[R] S ≃ₐ[S] S × U
algInst✝¹ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝³ : IsScalarTower S (S × U) U
this✝² : Etale S U
this✝¹ : Module.Finite S U
this✝ : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n✝ + 1
this : Module.rankAtStalk U = ↑n✝
V : Type u
w✝⁴ : CommRing V
w✝³ : Algebra S V
w✝² : Module.FaithfullyFlat S V
w✝¹ : Module.Finite S V
w✝ : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst✝ : Algebra R V := ((algebraMap S V).comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S V := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R V))
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  (TensorProduct.cancelBaseChange R S V V S).symm.trans
    ((TensorProduct.congr AlgEquiv.refl e✝).trans
      ((TensorProduct.prodRight S V V S U).trans
        (((TensorProduct.rid S V V).prodCongr f).trans
          (((AlgEquiv.funUnique V Unit V).symm.prodCongr AlgEquiv.refl).trans
            (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V).symm))))
p : PrimeSpectrum R
⊢ 0 < Module.rankAtStalk S p

Tactic:
simp [hn]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
⊢ Ideal.map f I ≤ hK.dpEqualizer hK'

Tactic:
by
  rw [Ideal.map, span_le]
  rintro b ⟨a, ha, rfl⟩
  exact ⟨hI_le_K (mem_map_of_mem f ha), fun n ↦ by rw [hIK.2 a ha, hIK'.2 a ha]⟩

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: 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
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
this : Ideal.under R (Ideal.map ((MulSemiringAction.toRingEquiv G S) τ) Q) = Ideal.under R Q
⊢ (MulSemiringAction.toAlgHom R S (τ * σ * τ⁻¹)) x - x ^ Nat.card (R ⧸ Ideal.under R (τ • Q)) ∈ τ • Q

Tactic:
rw [Ideal.pointwise_smul_eq_comap, Ideal.mem_comap]

Goal state after:
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
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
this : Ideal.under R (Ideal.map ((MulSemiringAction.toRingEquiv G S) τ) Q) = Ideal.under R Q
⊢ (RingEquiv.symm ((MulSemiringAction.toRingAut G S) τ))
      ((MulSemiringAction.toAlgHom R S (τ * σ * τ⁻¹)) x -
        x ^ Nat.card (R ⧸ Ideal.under R (Ideal.comap (RingEquiv.symm ((MulSemiringAction.toRingAut G S) τ)) Q))) ∈
    Q
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
f : PowerSeries R
g : Γ
hg : g = 0
n : ℕ
hn : n ≠ 0
⊢ ((powerSeriesFamily 0 f) n).coeff 0 = 0

Tactic:
simp [hn]

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

Goal state before:
pp: case pos
Γ : 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
n : ℕ
hn : n = 0
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r)) n = 0 ^ n

Tactic:
simp [hn]

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

Goal state before:
pp: case neg
Γ : 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
n : ℕ
hn : ¬n = 0
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r)) n = 0 ^ n

Tactic:
simp [hn]

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

Goal state before:
pp: Γ : 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
⊢ 0 < ((binomialFamily x r).hsum - 1).orderTop

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial A
  · simp [Subsingleton.eq_zero ((binomialFamily x r).hsum - 1)]
  · refine (orderTop_self_sub_one_pos_iff (binomialFamily x r).hsum).mpr ?_
    constructor
    · exact hsum_orderTop_of_le (by simp [hx]) (fun b g hg => binomialFamily_mem_support
        hx r b hg) fun b hb => coeff_eq_zero_of_lt_orderTop <| binomialFamily_orderTop_pos hx r <|
        Nat.zero_lt_of_ne_zero hb
    · have : (binomialFamily x r 0).coeff 0 = 1 := by simp [hx]
      rw [← this]
      refine hsum_leadingCoeff_of_le (g := 0) (a := 0) (by simp [hx]) ?_ ?_
      · intro b g' hg'
        exact binomialFamily_mem_support hx r b hg'
      · intro b hb
        exact coeff_eq_zero_of_lt_orderTop <| binomialFamily_orderTop_pos hx r <|
        Nat.zero_lt_of_ne_zero hb

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
g : Γ
n : ℕ
hn : n ≠ 0
⊢ (if n = 0 then (if 0 < x.orderTop then x else 0) ^ n else 0).coeff g = 0

Tactic:
simp [hn]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
n : ℕ
hn : n ≠ 0
⊢ (if n = 0 then r • (if 0 < x.orderTop then x else 0) ^ n else 0).coeff g = 0

Tactic:
simp [hn]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
n : ℕ
hn : n ≠ 1
⊢ ({ toFun := fun a ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } n).coeff g = 0

Tactic:
simp [hn]

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

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

Tactic:
have : ![0, 0] = (0 : Fin 2 → PowerSeries R) := by
        ext x : 1; fin_cases x <;> rfl

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : ![0, 0] = 0
⊢ subst ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] F.toPowerSeries = F.Xzero
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ F.zeroX = PowerSeries.X

Tactic:
have : Invertible (F.zeroX.coeff 1) := (coeff_one_zeroX F) ▸ invertibleOne

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : Invertible ((PowerSeries.coeff 1) F.zeroX)
⊢ F.zeroX = PowerSeries.X
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ F.zeroX = PowerSeries.X

Tactic:
by
  have : Invertible (F.zeroX.coeff 1) := (coeff_one_zeroX F) ▸ invertibleOne
  calc
    _ = F.zeroX.substInv.subst (F.zeroX.subst F.zeroX) := by
      have aux₀ : PowerSeries.HasSubst F.zeroX :=
        PowerSeries.HasSubst.of_constantCoeff_zero' <| F.constantCoeff_zeroX
      rw [← PowerSeries.subst_comp_subst_apply aux₀ aux₀, PowerSeries.subst_substInv_left _
        F.constantCoeff_zeroX, PowerSeries.subst_X aux₀, zeroX]
    _ = _ := by
      rw [zeroX_subst_zeroX, F.zeroX.subst_substInv_left F.constantCoeff_zeroX]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
s : SummableFamily Γ R α
⊢ (x • s).hsum = x * s.hsum

Tactic:
by
  rw [hsum_smul_module, of_symm_smul_of_eq_mul]

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ.refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∑ k ∈ Finset.range 2, ((taylor (c n)) f).coeff k * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k ∈
    I ^ (n + 1 + 1)

pp: case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∑ k ∈ Finset.Ico 2 (((taylor (c n)) f).natDegree + 2),
      ((taylor (c n)) f).coeff k * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k ∈
    I ^ (n + 1 + 1)

Tactic:
· rw [← one_add_one_eq_two, Finset.sum_range_succ, Finset.range_one, Finset.sum_singleton,
            taylor_coeff_zero, taylor_coeff_one, pow_zero, pow_one, mul_one, mul_neg,
            mul_left_comm, Ring.mul_inverse_cancel _ (hf'c n), mul_one, add_neg_cancel]
          exact Ideal.zero_mem _

Goal state after:
case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∑ k ∈ Finset.Ico 2 (((taylor (c n)) f).natDegree + 2),
      ((taylor (c n)) f).coeff k * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k ∈
    I ^ (n + 1 + 1)
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : c 0 + -(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ) ≡ a [SMOD I]
⊢ a ≡ a₀ + 0 [SMOD I]

Tactic:
refine ha.symm.trans (SModEq.rfl.add ?_)

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : c 0 + -(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ) ≡ a [SMOD I]
⊢ -(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ) ≡ 0 [SMOD I]
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.Pure
inst✝ : J.Pure
h : zeroLocus ↑I = zeroLocus ↑J
s : Set (PrimeSpectrum R)
hs : zeroLocus ↑I = s
⊢ RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal)) =
    RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal))

Tactic:
generalize ht : zeroLocus (J : Set R) = t

Goal state after:
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.Pure
inst✝ : J.Pure
h : zeroLocus ↑I = zeroLocus ↑J
s : Set (PrimeSpectrum R)
hs : zeroLocus ↑I = s
t : Set (PrimeSpectrum R)
ht : zeroLocus ↑J = t
⊢ RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal)) =
    RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal))
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
⊢ I.height ≤ ↑(Submodule.spanFinrank I)

Tactic:
by
  have : I.spanFinrank = I.spanRank.toENat := by
    rw [Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I), map_natCast]
  exact this ▸ height_le_spanRank_toENat I hI

Goal state after:
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

pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
s : Set R
hs : s ⊆ ↑p
⊢ ringKrullDim (R ⧸ span s) + ↑(Submodule.spanFinrank (span s)) ≤ ringKrullDim (R ⧸ span s) + ↑s.encard

Tactic:
· simpa [span_le]

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
s : Set R
hs : s ⊆ ↑p
⊢ ringKrullDim (R ⧸ span s) + ↑(Submodule.spanFinrank (span s)) ≤ ringKrullDim (R ⧸ span s) + ↑s.encard
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : LTSeries (PrimeSpectrum R)
x : R
hx : x ∈ (RelSeries.last p).asIdeal
⊢ ∃ q,
    x ∈ (q.toFun 1).asIdeal ∧
      p.length = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q

Tactic:
generalize hp : p.length = n

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : LTSeries (PrimeSpectrum R)
x : R
hx : x ∈ (RelSeries.last p).asIdeal
n : ℕ
hp : p.length = n
⊢ ∃ q,
    x ∈ (q.toFun 1).asIdeal ∧ n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx✝ : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 : p.toFun ⟨p.length - 2, ⋯⟩ < q
hq : q < RelSeries.last p
Q : LTSeries (PrimeSpectrum R)
hx : x ∈ (Q.toFun 1).asIdeal
hQ : n = Q.length
hh : ((RelSeries.eraseLast p).eraseLast.snoc q h2).head = RelSeries.head Q
hl : ((RelSeries.eraseLast p).eraseLast.snoc q h2).last = RelSeries.last Q
h1 : 1 < Q.length + 1
h : 1 = Fin.castSucc 1
⊢ (RelSeries.last Q, RelSeries.last p) ∈ {(a, b) | a < b}

Tactic:
by simpa [← hl] using! hq

Goal state after:
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
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
⊢ ∃ t,
    t.inf id = N ∧
      (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
        (↑t).Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on fun J ↦ (J.colon Set.univ).radical)

Tactic:
refine ⟨(s.image fun J ↦ {I ∈ s | (I.colon .univ).radical = (J.colon .univ).radical}).image
    fun t ↦ t.inf id, ?_, ?_, ?_⟩

Goal state after:
case refine_1
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)).inf
      id =
    N

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 ∈
        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.IsPrimary

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)
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case refine_3
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
h : n ≤ 1
⊢ False

Tactic:
obtain ⟨x, hx⟩ := finrank_le_one_iff.mp h

Goal state after:
case refine_3
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ c, c • x = w
⊢ False
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₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
this : ∀ q ∈ t, comap f (localized₀ S f q) = if q ∈ s then q else ⊤
⊢ (t.inf fun i ↦ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) i)) = ⨅ q ∈ s, q

Tactic:
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]

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

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

Tactic:
induction n generalizing M with
  | zero =>
    simp only [HasInjectiveDimensionLE, zero_add, ← injective_iff_hasInjectiveDimensionLT_one]
    refine ⟨fun h m ↦ ?_, fun h ↦ ?_⟩
    · let _ : Small.{v} (Localization m.1.primeCompl) :=
        small_of_surjective Localization.mkHom_surjective
      let _ : Module.Injective R M := Module.injective_module_of_injective_object R M
      rw [← Module.injective_iff_injective_object]
      exact Module.injective_of_isLocalizedModule m.1.primeCompl
        (M.localizedModuleMkLinearMap m.1.primeCompl)
    · rw [← Module.injective_iff_injective_object]
      apply Module.injective_of_localization_maximal (fun p hp ↦ ?_)
      let : Small.{v} (Localization.AtPrime p) := small_of_surjective Localization.mkHom_surjective
      have : Module.Injective (Localization.AtPrime p) (M.localizedModule p.primeCompl) := by
        simpa [Module.injective_iff_injective_object] using h ⟨p, hp⟩
      rw [← Module.Baer.iff_injective] at this ⊢
      exact Module.Baer.of_equiv (LinearEquiv.extendScalarsOfIsLocalization p.primeCompl
        (Localization.AtPrime p) (IsLocalizedModule.linearEquiv p.primeCompl
        (M.localizedModuleMkLinearMap p.primeCompl)
        (LocalizedModule.mkLinearMap p.primeCompl M))) this
  | succ n ih =>
    have ei : EnoughInjectives (ModuleCat.{v} R) := inferInstance
    rcases ei.1 M with ⟨I, inj, f, monof⟩
    let S := ShortComplex.mk f (cokernel.π f) (cokernel.condition f)
    have S_exact : S.ShortExact := { exact := ShortComplex.exact_cokernel f }
    let Sp (m : MaximalSpectrum R) := S.map (ModuleCat.localizedModuleFunctor m.1.primeCompl)
    have Sp_exact (m : MaximalSpectrum R) : (Sp m).ShortExact :=
      S_exact.map_of_exact (ModuleCat.localizedModuleFunctor m.1.primeCompl)
    have ih' := ih S.X₃
    simp only [HasInjectiveDimensionLE] at ih' ⊢
    rw [← S_exact.hasInjectiveDimensionLT_X₃_iff n inj, ih']
    have injp (m : MaximalSpectrum R) : Injective (Sp m).X₂ :=
      (ModuleCat.localizedModuleFunctor.{v} m.1.primeCompl).injective_obj _
    exact (forall_congr' (fun p ↦ (Sp_exact p).hasInjectiveDimensionLT_X₃_iff n (injp p)))

Goal state after:
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✝ : FormallyUnramified R S
β₀ : ResidueField S
hβ₀ : (ResidueField R)⟮β₀⟯ = ⊤
β : S
hβ : (residue S) β = β₀
⊢ (ResidueField R)⟮β₀⟯.toSubalgebra = ⊤

Tactic:
hβ₀,

Goal state after:
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✝ : FormallyUnramified R S
β₀ : ResidueField S
hβ₀ : (ResidueField R)⟮β₀⟯ = ⊤
β : S
hβ : (residue S) β = β₀
⊢ ⊤.toSubalgebra = ⊤
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x.powerSeriesPart = 0 ↔ x = 0

Tactic:
constructor
  · contrapose!
    simp only [ne_eq]
    intro h
    rw [PowerSeries.ext_iff, not_forall]
    use 0
    simpa
  · rintro rfl
    simp

Goal state after: