mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < n✝ + 1
⊢ m ≤ n✝ * m + m

Tactic:
apply Nat.le_add_left

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (optionEquivLeft σ R) (C r) = PowerSeries.C (C r)

Tactic:
by
  simpa using optionEquivLeft_monomial (0 : Option σ →₀ ℕ) (r : R)

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: case cons
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ih : ↑s ⊆ {a | IsGroupLikeElem R a} → LinearIndepOn R id ↑s
hs : ↑(Finset.cons a s has) ⊆ {a | IsGroupLikeElem R a}
⊢ LinearIndepOn R id ↑(Finset.cons a s has)

Tactic:
| cons a s has ih =>

Goal state after:
Module: Mathlib.RingTheory.Congruence.Star

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : R
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star y✝ * Star.star w✝) (Star.star (x✝ * z✝))

Tactic:
star_mul

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : R
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star y✝ * Star.star w✝) (Star.star z✝ * Star.star x✝)
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Bialgebra R A
inst✝⁴ : Bialgebra R B
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid O
inst✝ : Subsingleton M
r : R[M]
⊢ (Algebra.ofId R R[M]).comp (counitAlgHom R R[M]) = AlgHom.id R R[M]

Tactic:
ext g : 2

Goal state after:
case single_one_right
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Bialgebra R A
inst✝⁴ : Bialgebra R B
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid O
inst✝ : Subsingleton M
r : R[M]
g : M
⊢ (((Algebra.ofId R R[M]).comp (counitAlgHom R R[M])) (single g 1)).coeff = ((AlgHom.id R R[M]) (single g 1)).coeff
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
⊢ mapShortComplexH2 f 0 = 0

Tactic:
by
  refine ShortComplex.hom_ext _ _ ?_ ?_ ?_
  all_goals
  { simp only [shortComplexH2]
    ext
    simp }

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ mapShortComplexH2 (MonoidHom.id G) (𝟙 A) = 𝟙 (shortComplexH2 A)

Tactic:
by
  refine ShortComplex.hom_ext _ _ ?_ ?_ ?_
  all_goals
  { simp only [shortComplexH2]
    ext
    simp }

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
g : G
⊢ (fun m ↦ single m 1) ((mapDomainOfBialgHom (mapDomainBialgHom R f)) g) = (fun m ↦ single m 1) (f g)

Tactic:
simp [single_mapDomainOfBialgHom]

Goal state after:
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
⊢ False

Tactic:
have loc_ne_zero : p' ∈ Module.support R N := Module.mem_support_iff_of_finite.mpr hp

Goal state after:
case inr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : p' ∈ support R N
⊢ False
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_4
inst✝⁷ : CommSemiring S
N : Type u_5
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Module S N
f : M →ₗ[R] N
inst✝³ : Algebra R S
inst✝² : IsScalarTower R S N
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : M ≃ₗ[R] N
⊢ (map R ↑g).comp (map R ↑g.symm) = AlgHom.id R (DividedPowerAlgebra R N)

Tactic:
by simp [← map_comp, map_id]

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

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_4
inst✝⁷ : CommSemiring S
N : Type u_5
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Module S N
f : M →ₗ[R] N
inst✝³ : Algebra R S
inst✝² : IsScalarTower R S N
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : M ≃ₗ[R] N
⊢ (map R ↑g.symm).comp (map R ↑g) = AlgHom.id R (DividedPowerAlgebra R M)

Tactic:
by simp [← map_comp, map_id]

Goal state after:
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case cons
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module.Flat R M₂
rs : List R
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
r : R
rs' : List R
h1 : IsSMulRegular N r
h2✝ : IsWeaklyRegular (QuotSMulTop r N) rs'
ih : IsWeaklyRegular (M₂ ⊗[R] QuotSMulTop r N) rs'
e : M₂ ⊗[R] QuotSMulTop r N ≃ₗ[R] QuotSMulTop r (M₂ ⊗[R] N) := tensorQuotSMulTopEquivQuotSMulTop r M₂ N
⊢ IsWeaklyRegular (M₂ ⊗[R] N) (r :: rs')

Tactic:
exact ((e.isWeaklyRegular_congr rs').mp ih).cons (h1.lTensor M₂)

Goal state after:
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✝ : ℕ
a✝ x✝ : B
hx : x✝ ∈ J
⊢ e (hI.dpow n✝ (e.symm (a✝ * x✝))) = a✝ ^ n✝ * e (hI.dpow n✝ (e.symm x✝))

Tactic:
simp only [map_mul]
    rw [hI.dpow_mul (symm_apply_mem_of_equiv_iff.mpr (h ▸ hx))]
    rw [map_mul, map_pow]
    simp only [RingEquiv.apply_symm_apply]

Goal state after:
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 : ℕ
x y : A
hx : x ∈ I
hy : y ∈ I
hxy : x + y ∈ I
⊢ (if hx : x + y ∈ I then ⋯.choose else 0) =
    ∑ k ∈ Finset.antidiagonal n, (if hx : x ∈ I then ⋯.choose else 0) * if hx : y ∈ I then ⋯.choose else 0

Tactic:
simpa only [dif_pos hxy, dif_pos hx, dif_pos hy, ← hf.eq_iff, map_sum, map_mul,
      (Exists.choose_spec (_ : ∃ a, ∃ _, f a = _)).2, map_add]
      using hJ.dpow_add (hIJ ▸ I.mem_map_of_mem f hx) (hIJ ▸ I.mem_map_of_mem f hy)

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

Goal state before:
pp: case smul
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S
hSI : span S ≤ I
z a x : A
hxI : x ∈ Submodule.span A S
hx : ∀ (m : ℕ), m ≠ 0 → hI.dpow m x ∈ span S
m : ℕ
hm : m ≠ 0
⊢ hI.dpow m (a • x) ∈ span S

Tactic:
rw [smul_eq_mul, hI.dpow_mul (hSI hxI)]

Goal state after:
case smul
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S
hSI : span S ≤ I
z a x : A
hxI : x ∈ Submodule.span A S
hx : ∀ (m : ℕ), m ≠ 0 → hI.dpow m x ∈ span S
m : ℕ
hm : m ≠ 0
⊢ a ^ m * hI.dpow m x ∈ span S
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
⊢ ∀ (n : ℕ), n ≠ 0 → hI.dpow n 0 ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
exact fun _ hn ↦ by simp only [hI.dpow_eval_zero hn, zero_mem]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
i : ι
x : A
hx : x ∈ Subsemiring.closure s
⊢ ↑(((decompose 𝒜) x) i) ∈ Subsemiring.closure s

Tactic:
induction hx using Subsemiring.closure_induction generalizing i with

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
⊢ mk 1 * (1 - X) = 1

Tactic:
rw [mul_comm, PowerSeries.ext_iff]
  intro n
  cases n with
  | zero => simp
  | succ n => simp [sub_mul]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: case succ
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ invOneSubPow S (d + 1) = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯ ^ (d + 1))⁻¹

Tactic:
exact (DivisionMonoid.inv_eq_of_mul _ (invOneSubPow S (d + 1)) <| by
        rw [← Units.val_eq_one, Units.val_mul, Units.val_pow_eq_pow_val]
        exact (invOneSubPow S (d + 1)).inv_val).symm

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
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc : (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • (x ^ n).coeff g ≠ 0
⊢ ((PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • x ^ (c.1 + c.2)).coeff g ≠ 0

Tactic:
hcn

Goal state after:
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
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc : (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • (x ^ n).coeff g ≠ 0
⊢ ((PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • x ^ n).coeff g ≠ 0
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
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
i : (_ : ℕ) × ℕ × ℕ
hi : i ∈ (image (fun i ↦ i.1 + i.2) ⋯.toFinset).sigma HasAntidiagonal.antidiagonal
his : i ∉ (fun x ↦ ⟨x.1 + x.2, x⟩) '' ↑⋯.toFinset
m n : ℕ
⊢ (PowerSeries.coeff n) b • (PowerSeries.coeff m) a • (x ^ m * x ^ n).coeff g ≠ 0 → ⟨m + n, (m, n)⟩ ≠ i

Tactic:
simp only [powers_of_orderTop_pos h, Set.Finite.coe_toFinset, Set.mem_image,
          Function.mem_support, ne_eq, Prod.exists, not_exists, not_and] at his

Goal state after:
Γ : 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 : (_ : ℕ) × ℕ × ℕ
hi : i ∈ (image (fun i ↦ i.1 + i.2) ⋯.toFinset).sigma HasAntidiagonal.antidiagonal
m n : ℕ
his :
  ∀ (x_1 x_2 : ℕ),
    ¬(PowerSeries.coeff x_2) b • (PowerSeries.coeff x_1) a • (x ^ x_1 * x ^ x_2).coeff g = 0 →
      ¬⟨x_1 + x_2, (x_1, x_2)⟩ = i
⊢ (PowerSeries.coeff n) b • (PowerSeries.coeff m) a • (x ^ m * x ^ n).coeff g ≠ 0 → ⟨m + n, (m, n)⟩ ≠ i
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
f : α →₀ R⟦Γ⟧
g : Γ
⊢ {a | (f a).coeff g ≠ 0}.Finite

Tactic:
refine f.support.finite_toSet.subset fun a ha => ?_
    simp only [mem_coe, Finsupp.mem_support_iff, Ne]
    contrapose ha
    simp [ha]

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

Goal state before:
pp: case neg
Γ : 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
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
b : β
h : b ∈ {a | (if h : a ∈ Set.range ⇑f then s (Classical.choose h) else 0).coeff g ≠ 0}
hb : b ∉ Set.range ⇑f
⊢ b ∈ ⇑f '' Function.support fun a ↦ (s a).coeff g

Tactic:
· simp only [Ne, Set.mem_ofPred_eq, dif_neg hb, coeff_zero, not_true_eq_false] at h

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
a b : Γ
r s : R
⊢ (single a) r / (single b) s = (single (a - b)) (r / s)

Tactic:
rw [div_eq_mul_inv, sub_eq_add_neg, div_eq_mul_inv, inv_single, single_mul_single]

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

Goal state before:
pp: case h.succ.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
this✝ : p.IsPrime
hp : maximalIdeal (Localization p.primeCompl) ∈ under R ⁻¹' (span ↑s).minimalPrimes
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
hn : s.card ≤ n + 1
this :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
    p ∈ (span ↑s).minimalPrimes →
      p.IsPrime →
        ∀ (n : ℕ),
          (∀ 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) →
            s.card ≤ n + 1 → (∃ (x : IsLocalRing R), p = maximalIdeal R) → p.height ≤ ↑(n + 1)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ (maximalIdeal (Localization p.primeCompl)).height ≤ ↑(n + 1)

Tactic:
← IsLocalization.minimalPrimes_map p.primeCompl,

Goal state after:
case h.succ.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
this✝ : p.IsPrime
hp : maximalIdeal (Localization p.primeCompl) ∈ (map (algebraMap R (Localization p.primeCompl)) (span ↑s)).minimalPrimes
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
hn : s.card ≤ n + 1
this :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
    p ∈ (span ↑s).minimalPrimes →
      p.IsPrime →
        ∀ (n : ℕ),
          (∀ 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) →
            s.card ≤ n + 1 → (∃ (x : IsLocalRing R), p = maximalIdeal R) → p.height ≤ ↑(n + 1)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ (maximalIdeal (Localization p.primeCompl)).height ≤ ↑(n + 1)
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
hI' : ∃ y < I, y.IsPrime
⊢ I.IsMaximal

Tactic:
obtain ⟨P, hlt, hP⟩ := hI'

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
⊢ I.IsMaximal
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
reg : IsSMulRegular R x
hx : x ∈ Ring.jacobson R
⊢ ringKrullDim (R ⧸ span {x}) + 1 = ringKrullDim R

Tactic:
have h : span {x} = x • (⊤ : Ideal R) := by simp [← Submodule.ideal_span_singleton_smul]
  rw [ringKrullDim_eq_of_ringEquiv (quotientEquivAlgOfEq R h).toRingEquiv,
    ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson reg hx]

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

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
N : Submodule R M
H : ∀ (P : Ideal R) [inst : P.IsMaximal], (localized' (Rₚ P) P.primeCompl (f P) N).FG
⊢ N.FG

Tactic:
← Module.Finite.iff_fg

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
N : Submodule R M
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) ↥(localized' (Rₚ P) P.primeCompl (f P) N)
⊢ Module.Finite R ↥N
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)[β₀] = ⊤

Tactic:
← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite _ _),

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) β = β₀
⊢ (ResidueField R)⟮β₀⟯.toSubalgebra = ⊤
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := ⋯
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = ↑s
hDs : D - ↑s ≤ 0
⊢ 1 ≤ exp (-D + ↑s)

Tactic:
rw [← log_le_iff_le_exp one_ne_zero, log_one]

Goal state after:
case pos
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
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = ↑s
hDs : D - ↑s ≤ 0
⊢ 0 ≤ -D + ↑s
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
Rₚ : Type u_3
inst✝¹³ : CommRing Rₚ
inst✝¹² : Algebra R Rₚ
inst✝¹¹ : IsLocalization.AtPrime Rₚ p
inst✝¹⁰ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra S Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝⁵ : Algebra R Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
inst✝² : p.IsMaximal
inst✝¹ : P.IsMaximal
inst✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
⊢ (maximalIdeal Rₚ).inertiaDeg' (Ideal.map (algebraMap S Sₚ) P) = p.inertiaDeg' P

Tactic:
rw [inertiaDeg'_algebraMap, inertiaDeg'_algebraMap]

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
Rₚ : Type u_3
inst✝¹³ : CommRing Rₚ
inst✝¹² : Algebra R Rₚ
inst✝¹¹ : IsLocalization.AtPrime Rₚ p
inst✝¹⁰ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra S Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝⁵ : Algebra R Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
inst✝² : p.IsMaximal
inst✝¹ : P.IsMaximal
inst✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
⊢ finrank (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P) = finrank (R ⧸ p) (S ⧸ P)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
d : ℤ
hd : d ∈ Function.support (coeff hℱ)
hNd : ¬⋯.choose ≤ d
⊢ False

Tactic:
exact hd ((exists_lb_support hℱ).choose_spec d (not_le.mp hNd))

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d

Tactic:
by
  obtain ⟨⟨N₁, hN₁⟩, ⟨N₂, hN₂⟩⟩ := exists_lb_eventual_support hℱ, exists_lb_support hℱ
  refine ⟨min N₁ N₂, ℱ.3 hN₁ fun _ hf d hd ↦ ?_⟩
  rw [hf d (lt_of_lt_of_le hd (min_le_left _ _)), hN₂ d (lt_of_lt_of_le hd (min_le_right _ _))]

Goal state after:
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
H : IsUnit p
⊢ False

Tactic:
simp [(MvPolynomial.isUnit_iff_totalDegree_of_isReduced.mp H).2] at hp

Goal state after: