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

Goal state before:
pp: case cons
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst : AddCommGroup M] [inst_1 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsWeaklyRegular M (r :: rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) rs₂

Tactic:
let e := quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁

Goal state after:
case cons
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst : AddCommGroup M] [inst_1 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) ≃ₗ[R] QuotSMulTop r M ⧸ Ideal.ofList rs₁ • ⊤ :=
  quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
⊢ IsWeaklyRegular M (r :: rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) rs₂
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
h : ⊤ = ⊥ • ⊤
⊢ False

Tactic:
bot_smul,

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
h : ⊤ = ⊥
⊢ False
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n m : ℕ
x : A
hm : m ≠ 0
hx : x ∈ I
⊢ (if hx : (if hx : x ∈ I then ⋯.choose else 0) ∈ I then ⋯.choose else 0) =
    ↑(n.uniformBell m) * if hx : x ∈ I then ⋯.choose else 0

Tactic:
simp only [dif_pos hx, ← hf.eq_iff, map_mul, map_natCast]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n m : ℕ
x : A
hm : m ≠ 0
hx : x ∈ I
⊢ f (if hx_1 : (if hx : x ∈ I then ⋯.choose else 0) ∈ I then ⋯.choose else 0) = ↑(n.uniformBell m) * f ⋯.choose
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:
dpow_eq_of_mem (dpow_mem hk hx),

Goal state after:
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
⊢ (↑m !)⁻¹ʳ * dpow I k x ^ m = ↑(m.uniformBell k) * dpow I (m * k) x
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case mpr.h2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ (x ^ n * x ^ n).snd = snd 0

Tactic:
snd_mul,

Goal state after:
case mpr.h2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ (x ^ n).fst • (x ^ n).snd + MulOpposite.op (x ^ n).fst • (x ^ n).snd = snd 0
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
⊢ hI.IsSubDPIdeal (iSup J)

Tactic:
rw [iSup_eq_span, span_isSubDPIdeal_iff (Set.iUnion_subset_iff.mpr <| fun i ↦ (hJ i).1)]
  simp_rw [Set.mem_iUnion]
  rintro n hn a ⟨i, ha⟩
  exact span_mono (Set.subset_iUnion _ i) (subset_span ((hJ i).2 n hn ha))

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
rcases isUnit_or_isNilpotent a with ha | ha

Goal state after:
case inl
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsUnit a
⊢ ∃ c, a * c = b ∨ b * c = a

case inr
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
⊢ ∃ c, a * c = b ∨ b * c = a
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: case succ.inr
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
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
Pi.add_apply,

Goal state after:
case succ.inr
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 p + Module.rankAtStalk U p = n + 1
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : S
s : ↥Q.primeCompl
⊢ IsLocalization.mk' (Localization.AtPrime Q) (φ x) ⟨φ ↑s, ⋯⟩ -
      IsLocalization.mk' (Localization.AtPrime Q) (x ^ Nat.card (R ⧸ Ideal.under R Q))
        (s ^ Nat.card (R ⧸ Ideal.under R Q)) ∈
    maximalIdeal (Localization.AtPrime Q)

Tactic:
rw [← IsLocalization.mk'_sub,
    IsLocalization.AtPrime.mk'_mem_maximal_iff (Localization.AtPrime Q) Q]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : S
s : ↥Q.primeCompl
⊢ φ x * ↑(s ^ Nat.card (R ⧸ Ideal.under R Q)) - x ^ Nat.card (R ⧸ Ideal.under R Q) * ↑⟨φ ↑s, ⋯⟩ ∈ Q
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]
s : Fin (Nat.succ 0).succ.succ
⊢ IsNilpotent (constantCoeff (![f₀, f₁, f₂] s))

Tactic:
fin_cases s <;> simpa

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

Goal state before:
pp: case h
Γ : 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
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
hz : n = 0
this : g = 0 ∧ (PowerSeries.constantCoeff a * PowerSeries.constantCoeff b) • 1 ≠ 0
⊢ (0, 0) ∈ ↑(Set.Finite.toFinset ⋯) ∧ (0, 0).1 + (0, 0).2 = n

Tactic:
simp [this.2, this.1, h, hz, smul_smul, mul_comm]

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

Goal state before:
pp: case pos
Γ : 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 : Γ
⊢ ∑ x_1 ∈ image (fun i ↦ i.1 + i.2) ⋯.toFinset,
      ∑ i ∈ HasAntidiagonal.antidiagonal x_1,
        ((PowerSeries.coeff i.1) a * (PowerSeries.coeff i.2) b) • (x ^ x_1).coeff g =
    ∑ x_1 ∈ ⋯.toFinset, (PowerSeries.coeff x_1.2) b • (PowerSeries.coeff x_1.1) a • (x ^ x_1.1 * x ^ x_1.2).coeff g

Tactic:
sum_sigma'

Goal state after:
case pos
Γ : 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 : Γ
⊢ ∑ x_1 ∈ (image (fun i ↦ i.1 + i.2) ⋯.toFinset).sigma HasAntidiagonal.antidiagonal,
      ((PowerSeries.coeff x_1.snd.1) a * (PowerSeries.coeff x_1.snd.2) b) • (x ^ x_1.fst).coeff g =
    ∑ x_1 ∈ ⋯.toFinset, (PowerSeries.coeff x_1.2) b • (PowerSeries.coeff x_1.1) a • (x ^ x_1.1 * x ^ x_1.2).coeff g
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
h : (single (-x.order)) i * x * (SummableFamily.powers (1 - (single (-x.order)) i * x)).hsum = 1
⊢ IsUnit x

Tactic:
exact isUnit_of_mul_isUnit_right (.of_mul_eq_one _ h)

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
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:
refine Submodule.sum_mem _ ?_
          simp only [Finset.mem_Ico]
          rintro i ⟨h2i, _⟩
          have aux : n + 2 ≤ i * (n + 1) := by trans 2 * (n + 1) <;> nlinarith only [h2i]
          refine Ideal.mul_mem_left _ _ (Ideal.pow_le_pow_right aux ?_)
          rw [pow_mul']
          exact Ideal.pow_mem_pow ((Ideal.neg_mem_iff _).2 <| Ideal.mul_mem_right _ _ ih) _

Goal state after:
Module: Mathlib.Topology.Algebra.ClopenNhdofOne

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
⊢ ∃ H, ↑H ⊆ W

Tactic:
by
  rcases exist_openSubgroup_sub_clopen_nhds_of_one WClopen einW with ⟨H, hH⟩
  have : Subgroup.FiniteIndex H.toSubgroup := H.finiteIndex_of_finite_quotient
  use { toSubgroup := Subgroup.normalCore H
        isOpen' := Subgroup.isOpen_of_isClosed_of_finiteIndex _ (H.normalCore_isClosed H.isClosed) }
  exact fun _ b ↦ hH (H.normalCore_le b)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
⊢ I ≤ RingHom.ker (algebraMap R (Localization.AtPrime p))

Tactic:
by
  intro x hx
  obtain ⟨y, hy, heq⟩ := h _ hx
  have : IsUnit (algebraMap R (Localization.AtPrime p) (1 - y)) := by
    rw [IsLocalization.algebraMap_isUnit_iff p.primeCompl]
    refine ⟨1 - y, fun hz ↦ p.one_notMem ?_, by simp⟩
    rw [← sub_add_cancel 1 y]
    exact Ideal.add_mem _ hz (hle hy)
  have hzero : x * (1 - y) = 0 := by simp [mul_sub, ← heq]
  simp only [RingHom.mem_ker, ← this.mul_left_eq_zero, ← RingHom.map_mul, hzero, RingHom.map_zero]

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.PID

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
P : Ideal R
hlt : P < I
hP : P.IsPrime
this : IsPrincipalIdealRing (R ⧸ P)
⊢ I.IsMaximal

Tactic:
have : (I.map (Ideal.Quotient.mk P)).IsMaximal := by
    have := Ideal.map_isPrime_of_surjective (f := Ideal.Quotient.mk P) Ideal.Quotient.mk_surjective
      (I := I) (by simpa using hlt.le)
    refine IsPrime.to_maximal_ideal ?_
    rw [ne_eq, Ideal.map_eq_bot_iff_le_ker, Ideal.mk_ker]
    exact hlt.not_ge

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
P : Ideal R
hlt : P < I
hP : P.IsPrime
this✝ : IsPrincipalIdealRing (R ⧸ P)
this : (Ideal.map (Ideal.Quotient.mk P) I).IsMaximal
⊢ I.IsMaximal
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

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

Tactic:
have : IsClosed (Set.range P.toLimit) :=
    P.toLimit.hom.continuous_toFun.isClosedMap.isClosed_range
  rw [← Set.range_eq_univ, ← closure_eq_iff_isClosed.mpr this,
    Dense.closure_eq (denseRange_toLimit P)]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
⊢ under R (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p)) (RelSeries.head lq)).asIdeal ≤ p

Tactic:
· conv_rhs => rw [LiesOver.over (p := p) (P := P), under_def]
      refine comap_mono (le_trans (comap_mono (lq.head_le_last)) ?_)
      simp [hlq, map_le_iff_le_comap, LiesOver.over (p := p) (P := P)]

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
I J : Submodule R M
hIJ : I ≠ J
hJ : ∃ a ∈ s, {I ∈ s | (I.colon Set.univ).radical = (a.colon Set.univ).radical}.inf id = J
I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
⊢ ((fun x1 x2 ↦ x1 ≠ x2) on fun J ↦ (J.colon Set.univ).radical) I J

Tactic:
obtain ⟨J', hJ', hJ⟩ := hJ

Goal state after:
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
I J : Submodule R M
hIJ : I ≠ J
I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
⊢ ((fun x1 x2 ↦ x1 ≠ x2) on fun J ↦ (J.colon Set.univ).radical) I J
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro
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
⊢ False

Tactic:
have key := Group.card_center_add_sum_card_noncenter_eq_card (Dˣ)

Goal state after:
case intro
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
key : card ↥(Subgroup.center Dˣ) + ∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card = card Dˣ
⊢ False
Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
Iₛ : Ideal Rₛ
⊢ Function.Surjective ⇑(LinearMap.lcomp Rₛ Mₛ (Submodule.subtype Iₛ))

Tactic:
g

Goal state after:
R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
Iₛ : Ideal Rₛ
g : ↥Iₛ →ₗ[Rₛ] Mₛ
⊢ ∃ a, (LinearMap.lcomp Rₛ Mₛ (Submodule.subtype Iₛ)) a = g
Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
I : Ideal R
x✝¹ : FinitePresentation R ↥I := finitePresentation_of_finite R ↥I
m : Ideal R
x✝ : m.IsMaximal
Rₘ : Type u := Localization.AtPrime m
Mₘ : Type (max u v) := LocalizedModule m.primeCompl M
f : M →ₗ[R] LocalizedModule m.primeCompl M := LocalizedModule.mkLinearMap m.primeCompl M
h : R →ₗ[R] Rₘ := Algebra.linearMap R Rₘ
Iₘ : Ideal Rₘ := Submodule.localized' Rₘ m.primeCompl h I
g : ↥I →ₗ[R] ↥Iₘ := Submodule.toLocalized' Rₘ m.primeCompl h I
gM : (↥I →ₗ[R] M) →ₗ[R] ↥Iₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl g f Rₘ
hM : (R →ₗ[R] M) →ₗ[R] Rₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl h f Rₘ
eq'' : ↑R (Submodule.subtype Iₘ) = (IsLocalizedModule.map m.primeCompl g h) (Submodule.subtype I)
eq' :
  ↑R (LinearMap.lcomp Rₘ Mₘ (Submodule.subtype Iₘ)) =
    (IsLocalizedModule.map m.primeCompl hM gM) (LinearMap.lcomp R M (Submodule.subtype I))
eq :
  LinearMap.lcomp Rₘ Mₘ (Submodule.subtype Iₘ) =
    (IsLocalizedModule.mapExtendScalars m.primeCompl hM gM Rₘ) (LinearMap.lcomp R M (Submodule.subtype I))
MB : Baer Rₘ Mₘ
surj :
  Function.Surjective
    ⇑((IsLocalizedModule.mapExtendScalars m.primeCompl hM gM Rₘ) (LinearMap.lcomp R M (Submodule.subtype I)))
⊢ Function.Surjective
    ⇑(↑(IsLocalizedModule.iso m.primeCompl gM).symm ∘ₗ
        (IsLocalizedModule.map m.primeCompl hM gM) (LinearMap.lcomp R M (Submodule.subtype I)) ∘ₗ
          ↑(IsLocalizedModule.iso m.primeCompl hM))

Tactic:
simpa using! surj

Goal state after:
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝ : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h1 : Ideal.span (⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)}) = ⊤
g : S
hg : IsStandardOpenImmersion R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion S (Localization.Away x)
⊢ (algebraMap S T) g * x ∈ Ideal.span (Set.range fun i ↦ (algebraMap S T) ↑i.fst * ↑i.snd)

Tactic:
refine Ideal.subset_span ⟨⟨⟨g, hg⟩, ⟨x, ?_⟩⟩, rfl⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝ : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h1 : Ideal.span (⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)}) = ⊤
g : S
hg : IsStandardOpenImmersion R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion S (Localization.Away x)
⊢ x ∈ t ↑⟨g, hg⟩
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: F : Type u
inst✝ : Field F
n✝ : ℤ
n : ℕ
⊢ (single ↑n) 1 = (single 1) 1 ^ ↑n

Tactic:
| =>

Goal state after:
F : Type u
inst✝ : Field F
n✝ : ℤ
n : ℕ
⊢ (single ↑n) 1 = (single 1) 1 ^ ↑n
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: F : Type u
inst✝ : Field F
n✝ : ℤ
n : ℕ
⊢ (single (-↑(n + 1))) 1 = (single 1) 1 ^ (-↑(n + 1))

Tactic:
| =>

Goal state after:
F : Type u
inst✝ : Field F
n✝ : ℤ
n : ℕ
⊢ (single (-↑(n + 1))) 1 = (single 1) 1 ^ (-↑(n + 1))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
P : K⟮X⟯
f : K[X]
⊢ ∀ (q : K[X]),
    q ≠ 0 →
      (polynomialValuationX K) (RatFunc.mk f q) =
        (valuation K⸨X⸩ (PowerSeries.idealX K)) ((algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.mk f q))

Tactic:
g

Goal state after:
K : Type u_2
inst✝ : Field K
P : K⟮X⟯
f g : K[X]
⊢ g ≠ 0 →
    (polynomialValuationX K) (RatFunc.mk f g) =
      (valuation K⸨X⸩ (PowerSeries.idealX K)) ((algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.mk f g))
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
let F := powerSeriesPart f

Goal state after:
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
⊢ Valued.v f ≤ exp (-D)