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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
n : ℕ
M : ModuleCat R
inst✝¹ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
N : ModuleCat R
inst✝ : Module.Finite R ↑N
h_supp : Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I
h_ext : ∀ i < n, Subsingleton (Ext N M i)
⊢ ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs

Tactic:
by
  induction n generalizing M with
  | zero =>
    have : Nontrivial M := (Submodule.nontrivial_iff R).mp (nontrivial_of_lt _ _ smul_lt)
    use []
    simp [isRegular_iff]
  | succ n ih =>
    rw [Module.support_eq_zeroLocus, PrimeSpectrum.zeroLocus_eq_iff] at h_supp
    -- use `Ext N M 0` vanish to obtain an `M`-regular element `x` in `Ann(N)`
    have : Subsingleton (N ⟶ M) := Ext.addEquiv₀.subsingleton_congr.mp (h_ext 0 n.zero_lt_succ)
    have : Subsingleton (N →ₗ[R] M) := ModuleCat.homAddEquiv.symm.subsingleton
    obtain ⟨x, mem_ann, hx⟩ := subsingleton_linearMap_iff.mp this
    -- take a power of it to make `xᵏ` fall into `I`
    obtain ⟨k, hk⟩ := le_of_le_of_eq Ideal.le_radical h_supp mem_ann
    -- verify that `N` indeed make `M ⧸ xᵏM` satisfy the induction hypothesis
    have h_ext' : ∀ i < n, Subsingleton (Ext N (ModuleCat.of R (QuotSMulTop (x ^ k) M)) i) := by
      intro i hi
      -- the vanishing of `Ext` is obtained from the (covariant) long exact sequence given by
      -- `M.smulShortComplex (x ^ k)`
      have zero1 := AddCommGrpCat.isZero_of_iff_subsingleton.mpr (h_ext i (by omega))
      have zero2 := AddCommGrpCat.isZero_of_iff_subsingleton.mpr (h_ext (i + 1) (by omega))
      exact AddCommGrpCat.subsingleton_of_isZero <| ShortComplex.Exact.isZero_of_both_zeros
        ((Ext.covariant_sequence_exact₃' N (hx.pow k).smulShortComplex_shortExact) i (i + 1) rfl)
        (zero1.eq_zero_of_src _) (zero2.eq_zero_of_tgt _)
    obtain ⟨rs, len, mem, reg⟩ := ih (ModuleCat.of R (QuotSMulTop (x ^ k) M))
      (smul_top_quotSMulTop_ne_top_of_smul_top_ne_top hk smul_lt.ne).lt_top h_ext'
    use x ^ k :: rs
    simpa [len, hk] using ⟨mem, hx.pow k, reg⟩

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case succ
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
n : ℕ
h : ↑n ! * dp R n x = dp R 1 x ^ n
⊢ ↑(n + 1)! * dp R (n + 1) x = dp R 1 x ^ (n + 1)

Tactic:
rw [pow_succ, ← h, mul_assoc, dp_mul, nsmul_eq_mul, ← mul_assoc, ← Nat.cast_mul]

Goal state after:
case succ
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
n : ℕ
h : ↑n ! * dp R n x = dp R 1 x ^ n
⊢ ↑(n + 1)! * dp R (n + 1) x = ↑(n ! * (n + 1).choose n) * dp R (n + 1) x
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case h
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
n : ℕ
l : M
⊢ dp R n (f l) = ↑(X (n, f l))

Tactic:
dp

Goal state after:
case h
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
n : ℕ
l : M
⊢ ↑(X (n, f l)) = ↑(X (n, f l))
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n✝ : ℕ
x✝ y✝ : B
hx : x✝ ∈ J
hy : y✝ ∈ J
⊢ e (hI.dpow n✝ (e.symm (x✝ + y✝))) = ∑ k ∈ antidiagonal n✝, e (hI.dpow k.1 (e.symm x✝)) * e (hI.dpow k.2 (e.symm y✝))

Tactic:
simp only [map_add]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n✝ : ℕ
x✝ y✝ : B
hx : x✝ ∈ J
hy : y✝ ∈ J
⊢ e (hI.dpow n✝ (e.symm x✝ + e.symm y✝)) =
    ∑ k ∈ antidiagonal n✝, e (hI.dpow k.1 (e.symm x✝)) * e (hI.dpow k.2 (e.symm y✝))
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
hlt : ↑(padicValNat p n !) < ↑n
hnorm : 0 < ‖↑n !‖
⊢ 1 < ↑p

pp: case hmn
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
hlt : ↑(padicValNat p n !) < ↑n
hnorm : 0 < ‖↑n !‖
⊢ -↑x.valuation * ↑n < -(↑n !).valuation

Tactic:
· exact_mod_cast Nat.Prime.one_lt hp.elim

Goal state after:
case hmn
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
hlt : ↑(padicValNat p n !) < ↑n
hnorm : 0 < ‖↑n !‖
⊢ -↑x.valuation * ↑n < -(↑n !).valuation
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
⊢ dpow I m (dpow I k x) = ↑(m.uniformBell k) * dpow I (m * k) x

Tactic:
rw [dpow_eq_of_mem (dpow_mem hk hx), dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_pow, ← pow_mul, ← mul_assoc, mul_comm k, hxmk, mul_zero, mul_zero, mul_zero]

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.Injective ⇑(map P.toExtendScalars)

Tactic:
by
  rw [← LinearMap.ker_eq_bot, H1Cotangent.map, LinearMap.ker_restrict,
    ← cotangentExtendScalarsEquiv_symm_toLinearMap, LinearEquiv.ker,
    Submodule.comap_bot, Submodule.ker_subtype]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f₀ f₁ f₂ : MvPowerSeries σ R
h₀ : PowerSeries.HasSubst f₀
h₁ : PowerSeries.HasSubst f₁
h₂ : PowerSeries.HasSubst f₂
aux₁ : HasSubst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂]
aux₂ : HasSubst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries]
this : HasSubst ![f₀, f₁, f₂]
⊢ subst ![subst ![f₀, f₁] F.toPowerSeries, f₂] F.toPowerSeries =
    subst ![f₀, f₁, f₂] (subst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂] F.toPowerSeries)

Tactic:
rw [subst_comp_subst_apply aux₁ this]

Goal state after:
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f₀ f₁ f₂ : MvPowerSeries σ R
h₀ : PowerSeries.HasSubst f₀
h₁ : PowerSeries.HasSubst f₁
h₂ : PowerSeries.HasSubst f₂
aux₁ : HasSubst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂]
aux₂ : HasSubst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries]
this : HasSubst ![f₀, f₁, f₂]
⊢ subst ![subst ![f₀, f₁] F.toPowerSeries, f₂] F.toPowerSeries =
    subst (fun s ↦ subst ![f₀, f₁, f₂] (![subst ![Y₀, Y₁] F.toPowerSeries, Y₂] s)) F.toPowerSeries
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos.refine_2
Γ : 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
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
i : (_ : ℕ) × ℕ × ℕ
his : i ∉ (fun x ↦ ⟨x.1 + x.2, x⟩) '' ↑⋯.toFinset
hisc :
  ∀ (j k : ℕ), ⟨j + k, (j, k)⟩ = i → (PowerSeries.coeff k) b • (PowerSeries.coeff j) a • (x ^ j * x ^ k).coeff g = 0
hi : i.fst ∈ image (fun i ↦ i.1 + i.2) ⋯.toFinset ∧ i.snd.1 + i.snd.2 = i.fst
⊢ ((PowerSeries.coeff i.snd.2) b * (PowerSeries.coeff i.snd.1) a) • (x ^ (i.snd.1 + i.snd.2)).coeff g = 0

Tactic:
mul_smul,

Goal state after:
case pos.refine_2
Γ : 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
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
i : (_ : ℕ) × ℕ × ℕ
his : i ∉ (fun x ↦ ⟨x.1 + x.2, x⟩) '' ↑⋯.toFinset
hisc :
  ∀ (j k : ℕ), ⟨j + k, (j, k)⟩ = i → (PowerSeries.coeff k) b • (PowerSeries.coeff j) a • (x ^ j * x ^ k).coeff g = 0
hi : i.fst ∈ image (fun i ↦ i.1 + i.2) ⋯.toFinset ∧ i.snd.1 + i.snd.2 = i.fst
⊢ (PowerSeries.coeff i.snd.2) b • (PowerSeries.coeff i.snd.1) a • (x ^ (i.snd.1 + i.snd.2)).coeff g = 0
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝² : PartialOrder Γ
inst✝¹ : AddCommMonoid R
ι : Type ?u.20
inst✝ : Finite ι
x : R⟦Γ⟧
⊢ (⋃ a, x.support).IsPWO

Tactic:
by
    cases isEmpty_or_nonempty ι
    · simp
    · exact Eq.mpr (congrArg (fun s ↦ s.IsPWO) (Set.iUnion_const x.support)) x.isPWO_support

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : ¬0 < x.orderTop
⊢ ↑0 < ((powers x) n).orderTop

Tactic:
simp [h, hn]

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

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 : Γ
⊢ {a | ((fun n ↦ x ^ n) a).coeff g ≠ 0}.Finite

Tactic:
have hpwo : Set.IsPWO (⋃ n, support (x ^ n)) :=
    isPWO_iUnion_support_powers (zero_le_orderTop_iff.mp <| le_of_lt hx)

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
⊢ {a | ((fun n ↦ x ^ n) a).coeff g ≠ 0}.Finite
Module: Mathlib.RingTheory.HopfAlgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ a * (antipode R) a = 1

Tactic:
by
  simpa [ha, -mul_antipode_lTensor_comul_apply] using mul_antipode_lTensor_comul_apply (R := R) a

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
F : IdealFilter A
inst✝ : F.IsUniform
x₀ : A
I : Ideal A
hI : I ∈ F
⊢ ∃ V ∈ F.addGroupFilterBasis.sets, V ⊆ (fun x ↦ x₀ * x) ⁻¹' ↑I

Tactic:
exact ⟨I, ⟨I, hI, rfl⟩, fun a ha ↦ Ideal.mul_mem_left I x₀ ha⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
⊢ Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) ↔ I ⊓ J = I * J

Tactic:
let f : J ⧸ (I • ⊤ : Submodule R J) →ₗ[R] R ⧸ I :=
    Submodule.mapQ _ _ J.subtype <| by
      simp [← Submodule.map_le_iff_le_comap, Ideal.mul_le_left]
  have : J.subtype.lTensor (R ⧸ I) =
      (TensorProduct.rid R (R ⧸ I)).symm ∘ₗ f ∘ₗ TensorProduct.quotTensorEquivQuotSMul J I := by
    ext
    simp [f, ← Ideal.Quotient.algebraMap_eq, Algebra.TensorProduct.tmul_one_eq_one_tmul]
  rw [this]
  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective,
    EquivLike.injective_comp, ← LinearMap.ker_eq_bot, f, Submodule.ker_mapQ,
    ← LinearMap.le_ker_iff_map, Submodule.ker_mkQ,
    ← (Submodule.map_le_map_iff_of_injective J.injective_subtype)]
  simp [inf_comm, le_antisymm_iff, Ideal.mul_le_inf (I := I) (J := J)]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
h' : IsIdempotentElem I
⊢ I.Pure

Tactic:
rw [Ideal.isIdempotentElem_iff_of_fg _ h] at h'

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
h' : ∃ e, IsIdempotentElem e ∧ I = R ∙ e
⊢ I.Pure
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝⁴ : p.IsPrime
this✝³ : (map f p).IsPrime
h : (map f p).height ≤ 1
h_lt : map f q < map f p
this✝² : (map f q).IsPrime
this✝¹ : (map f p).FiniteHeight
this✝ : map f q ∈ minimalPrimes (R ⧸ span t)
this : comap f (map f q) ∈ (comap f ⊥).minimalPrimes
⊢ q ∈ (span t).minimalPrimes

Tactic:
rwa [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot,
      mk_ker, sup_eq_left.mpr hI'q] at this

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

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ ↑(IsLocalRing.maximalIdeal R).height ≠ ⊤

Tactic:
· rw [← WithBot.coe_top, ne_eq, WithBot.coe_inj]
    exact ((IsLocalRing.maximalIdeal R).finiteHeight_iff.mp
      (IsLocalRing.maximalIdeal R).finiteHeight_of_isNoetherianRing).resolve_left
        Ideal.IsPrime.ne_top'

Goal state after:
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
h : p.height ≤ ↑t.card
⊢ p.height ≤ (map (Quotient.mk I) p).height + ↑(Submodule.spanFinrank I)

Tactic:
refine le_trans h (hs ▸ ?_)
    norm_cast
    have : (Submodule.FG.finite_generators hI).toFinset.card = I.spanFinrank := by
      rw [← Set.ncard_eq_toFinset_card (hs := Submodule.FG.finite_generators hI)]
      exact Submodule.FG.generators_ncard hI
    grind

Goal state after:
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:
simpa [← hl] using! hq

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case pos
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
hq : (q.colon Set.univ).radical = ↑p
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = q

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (map_le_iff_le_comap.mp (map_le_localized₀ S f q))
    obtain ⟨b, hb, a, ha⟩ := hx
    rw [IsLocalizedModule.mk'_eq_iff, ← LinearMap.map_smul_of_tower] at ha
    obtain ⟨c, hc⟩ := (IsLocalizedModule.eq_iff_exists S f).mp ha
    replace hb := q.smul_mem c hb
    rw [← Submonoid.smul_def, hc, smul_smul] at hb
    apply (hqp.mem_or_mem hb).resolve_right
    grind [Submonoid.mem_iInf, mem_primeCompl_iff]

Goal state after:
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
⊢ HasProjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)

Tactic:
have proj := ModuleCat.projective_of_categoryTheory_projective S.X₂

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₂
⊢ HasProjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case mp
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
β : S
hβ : Function.Surjective ⇑(aeval ((residue S) β))
s : S
a✝ : s ∈ ⊤
⊢ s ∈ Subalgebra.toSubmodule R[β] ⊔ maximalIdeal R • ⊤

Tactic:
obtain ⟨p, hp⟩ := hβ (residue S s)

Goal state after:
case mp
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
β : S
hβ : Function.Surjective ⇑(aeval ((residue S) β))
s : S
a✝ : s ∈ ⊤
p : (ResidueField R)[X]
hp : (aeval ((residue S) β)) p = (residue S) s
⊢ s ∈ Subalgebra.toSubmodule R[β] ⊔ maximalIdeal R • ⊤
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0

Tactic:
simp only [Ideal.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot, hP, Polynomial.X_ne_zero,
      not_false_iff, and_self_iff]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Valued.v ((ofPowerSeries ℤ K) f) ≤ exp (-↑d)
⊢ n < d → (PowerSeries.coeff n) f = 0

Tactic:
intro hnd
  apply (PowerSeries.X_pow_dvd_iff).mp _ n hnd
  rwa [← LaurentSeries.coe_algebraMap, valuation_def, valuation_of_algebraMap,
    intValuation_le_pow_iff_dvd (PowerSeries.idealX K) f d, PowerSeries.idealX,
    Ideal.span_singleton_pow, Ideal.span_singleton_dvd_span_singleton_iff_dvd] at H

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

Goal state before:
pp: q : ℚ
⊢ IsLocalization.IsInteger ℤ q ↔ q ∈ Set.range Int.cast

Tactic:
simp [IsLocalization.IsInteger]

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : Sₚ
⊢ ∃ a, (algebraMap S (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) a = (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) x

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq (algebraMapSubmonoid S p.primeCompl) x

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
⊢ ∃ a,
    (algebraMap S (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) a =
      (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) (mk' Sₚ x s)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf✝ : f ∈ S ∩ T
hf : ¬f = 0
⊢ ∃ N, ∀ (g : K⸨X⸩), Valued.v (g - f) ≤ 1 → ∀ n < N, g.coeff n = 0

Tactic:
refine ⟨min (f.2.isWF.min (HahnSeries.support_nonempty_iff.mpr hf)) 0 - 1, fun _ hg n hn ↦ ?_⟩

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf✝ : f ∈ S ∩ T
hf : ¬f = 0
x✝ : K⸨X⸩
hg : Valued.v (x✝ - f) ≤ 1
n : ℤ
hn : n < min (⋯.min ⋯) 0 - 1
⊢ x✝.coeff n = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case h₀
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
j : Fin n
hij : j ∈ {i_1 | ↑⟨i, ⋯⟩ ≤ ↑i_1}
hji : j ≠ ⟨i, hin⟩
⊢ m ≤ ↑j

Tactic:
rw [mem_filter_univ] at hij

Goal state after:
case h₀
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
j : Fin n
hij : ↑⟨i, ⋯⟩ ≤ ↑j
hji : j ≠ ⟨i, hin⟩
⊢ m ≤ ↑j
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
hle : a.totalDegree ≤ b.totalDegree
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ a.totalDegree + b.totalDegree = 1

Tactic:
simpa [totalDegree_mul_of_isDomain, ha₀, hb₀, hp] using congr(($hab).totalDegree).symm

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∑ x ∈ (range k).disjiUnion (fun x ↦ powersetCard x univ) ⋯, ∑ y, f (x, y) =
    ∑ a ∈ antidiagonal k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j, f (A, j)

Tactic:
sum_disjiUnion

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∑ i ∈ range k, ∑ x ∈ powersetCard i univ, ∑ y, f (x, y) =
    ∑ a ∈ antidiagonal k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j, f (A, j)
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁶ : Ring R
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module (Matrix ι ι R) M
inst✝¹ : Module R M
inst✝ : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
this : Commute (diagonal fun x ↦ r) (single i i 1)
⊢ single i i 1 • r • x = (single i i 1 * diagonal fun x ↦ r) • x

Tactic:
mul_smul,

Goal state after:
R : Type u
ι : Type v
inst✝⁶ : Ring R
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module (Matrix ι ι R) M
inst✝¹ : Module R M
inst✝ : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
this : Commute (diagonal fun x ↦ r) (single i i 1)
⊢ single i i 1 • r • x = single i i 1 • (diagonal fun x ↦ r) • x