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

Goal state before:
pp: case cons
R : Type u_1
M₄ : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M₄
inst✝⁸ : Module R M₄
rs✝ : List R
M✝ : Type u_6
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
r : R
rs : List R
h₄ : IsSMulRegular M✝ r
h2✝ : IsWeaklyRegular (QuotSMulTop r M✝) rs
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
ih :
  Exact ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f₁) ⋯)
    ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f₂) ⋯)
f₃ : M₃ →ₗ[R] M✝
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
⊢ Exact ⇑((Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f₁ ⋯)
    ⇑((Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f₂ ⋯)

Tactic:
have H₁ := quotOfListConsSMulTopEquivQuotSMulTopInner_naturality r rs f₁

Goal state after:
case cons
R : Type u_1
M₄ : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M₄
inst✝⁸ : Module R M₄
rs✝ : List R
M✝ : Type u_6
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
r : R
rs : List R
h₄ : IsSMulRegular M✝ r
h2✝ : IsWeaklyRegular (QuotSMulTop r M✝) rs
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
ih :
  Exact ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f₁) ⋯)
    ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f₂) ⋯)
f₃ : M₃ →ₗ[R] M✝
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
H₁ :
  ↑(quotOfListConsSMulTopEquivQuotSMulTopInner M₂ r rs) ∘ₗ
      (Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f₁ ⋯ =
    (Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f₁) ⋯ ∘ₗ
      ↑(quotOfListConsSMulTopEquivQuotSMulTopInner M r rs)
⊢ Exact ⇑((Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f₁ ⋯)
    ⇑((Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f₂ ⋯)
Module: Mathlib.RingTheory.DualNumber

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

Tactic:
simp_rw [Ideal.mem_span_singleton', (commute_eps_right _).eq, eq_comm, ← dvd_def]

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

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

Tactic:
simp_rw [Ideal.mem_span_singleton', (commute_eps_right _).eq, eq_comm, ← dvd_def]

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

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
k : Type u
inst✝⁸ : Field k
Ω✝ : Type w
inst✝⁷ : Field Ω✝
inst✝⁶ : Algebra R Ω✝
S : Type w
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Ω✝
inst✝² : IsScalarTower R S Ω✝
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
X : FintypeCat
x : ↑(Opposite.unop (Opposite.op (of Ω (X.obj → Ω)))).obj
i : X.obj
⊢ (Algebra.FormallyEtale.equivPiOfIsSepClosed Ω (X.obj → Ω)) x
      (PrimeSpectrum.comap (Pi.evalRingHom (fun a ↦ Ω) i) default) =
    x i

Tactic:
rw [← Pi.coe_evalAlgHom Ω]

Goal state after:
R : Type u
inst✝⁹ : CommRing R
k : Type u
inst✝⁸ : Field k
Ω✝ : Type w
inst✝⁷ : Field Ω✝
inst✝⁶ : Algebra R Ω✝
S : Type w
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Ω✝
inst✝² : IsScalarTower R S Ω✝
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
X : FintypeCat
x : ↑(Opposite.unop (Opposite.op (of Ω (X.obj → Ω)))).obj
i : X.obj
⊢ (Algebra.FormallyEtale.equivPiOfIsSepClosed Ω (X.obj → Ω)) x
      (PrimeSpectrum.comap (↑(Pi.evalAlgHom Ω (fun a ↦ Ω) i)) default) =
    x i
Module: Mathlib.RingTheory.HahnSeries.Binomial

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

Tactic:
rw [← this]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : g ∈ s.hsum.support
⊢ g ∈ ⋃ a, (s a).support

Tactic:
rw [mem_support, coeff_hsum, finsum_eq_sum _ (s.finite_co_support _)] at hg
  obtain ⟨a, _, h2⟩ := exists_ne_zero_of_sum_ne_zero hg
  rw [Set.mem_iUnion]
  exact ⟨a, h2⟩

Goal state after:
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
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
⊢ (⋃ a, (f a • s a).support).IsPWO

Tactic:
refine Set.IsPWO.mono s.isPWO_iUnion_support fun g hg => ?_
    simp_all only [Set.mem_iUnion, mem_support, coeff_smul, ne_eq]
    obtain ⟨i, hi⟩ := hg
    exact Exists.intro i <| right_ne_zero_of_smul hi

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⟦Γ⟧
f : R⟦X⟧
⊢ ((heval x) f).coeff 0 = constantCoeff f

Tactic:
rw [coeff_heval, finsum_eq_single (fun n => ((powerSeriesFamily x f).coeff 0) n) 0,
    ← PowerSeries.coeff_zero_eq_constantCoeff_apply]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ((powerSeriesFamily x f).coeff 0) 0 = (coeff 0) f

Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ∀ (x_1 : ℕ), x_1 ≠ 0 → ((powerSeriesFamily x f).coeff 0) x_1 = 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✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
ab : α × β
x : Γ'
hx : x ∈ ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support
⊢ x ∈ {a | (VAddAntidiagonal a ⋯).Nonempty}

Tactic:
simp only [Set.mem_ofPred_eq]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
ab : α × β
x : Γ'
hx : x ∈ ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support
⊢ (VAddAntidiagonal x ⋯).Nonempty
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
⊢ (1 - x) * (powers x).hsum = 1

Tactic:
by
  rw [← hsum_smul, sub_smul 1 x (powers x), one_smul, hsum_sub, ←
    hsum_embDomain (x • powers x) ⟨Nat.succ, Nat.succ_injective⟩, embDomain_succ_smul_powers hx]
  simp

Goal state after:
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⟦Γ⟧
⊢ IsUnit x.leadingCoeff → IsUnit x

Tactic:
rintro ⟨⟨u, i, ui, iu⟩, hx⟩
    rw [Units.val_mk] at hx
    rw [hx] at iu
    have h :=
      SummableFamily.one_sub_self_mul_hsum_powers (unit_aux x iu _ (neg_add_cancel x.order))
    rw [sub_sub_cancel] at h
    exact isUnit_of_mul_isUnit_right (.of_mul_eq_one _ 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 : Γ
r : R
⊢ ((single a) r)⁻¹ = (single (-a)) r⁻¹

Tactic:
obtain rfl | hr := eq_or_ne r 0
  · simp [inv_def]
  · simp [inv_def, hr]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingUp R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.head.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.head L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver q.asIdeal
Q : Ideal S
PQlt : P < Q
hQ : Q.IsPrime
Qlo : Q.LiesOver l.head.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
head : RelSeries.head L = { asIdeal := Q, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
⊢ (RelSeries.cons L { asIdeal := P, isPrime := ⋯ } ⋯).length = (l.cons q lt).length

Tactic:
simpa using len

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : Ideal R[X]
ism : (comap C p).IsMaximal
ne : p ≠ Ideal.map C (comap C p)
q : Ideal R := comap C p
this✝ : Field (R ⧸ q) := Quotient.field q
ne' : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p ≠ ⊥
y : (R ⧸ q)[X]
mony : y.Monic
hy : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p = span {y}
this : y ∈ lifts (Ideal.Quotient.mk q)
⊢ ∃ f, f.Monic ∧ p = Ideal.map C (comap C p) ⊔ span {f}

Tactic:
rcases Polynomial.lifts_and_natDegree_eq_and_monic this mony with ⟨f, hf, deg, monf⟩

Goal state after:
R : Type u_1
inst✝ : CommRing R
p : Ideal R[X]
ism : (comap C p).IsMaximal
ne : p ≠ Ideal.map C (comap C p)
q : Ideal R := comap C p
this✝ : Field (R ⧸ q) := Quotient.field q
ne' : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p ≠ ⊥
y : (R ⧸ q)[X]
mony : y.Monic
hy : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p = span {y}
this : y ∈ lifts (Ideal.Quotient.mk q)
f : R[X]
hf : map (Ideal.Quotient.mk q) f = y
deg : f.natDegree = y.natDegree
monf : f.Monic
⊢ ∃ f, f.Monic ∧ p = Ideal.map C (comap C p) ⊔ span {f}
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case h.succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
this : p.IsPrime
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
⊢ p.height ≤ ↑(n + 1)

Tactic:
wlog hR : ∃ (_ : IsLocalRing R), p = maximalIdeal R

Goal state after:
case h.succ.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
this✝ : p.IsPrime
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
⊢ p.height ≤ ↑(n + 1)

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
this : p.IsPrime
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
hR : ∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ p.height ≤ ↑(n + 1)
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
⊢ Continuous fun a ↦ ↑a

Tactic:
apply Continuous.mk

Goal state after:
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
⊢ ∀ (s : Set ↑(P.diagram.obj H).toProfinite.toTop), IsOpen s → IsOpen ((fun a ↦ ↑a) ⁻¹' s)
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
this : IsClosed (Set.range ⇑(Hom.hom P.toLimit))
⊢ Set.range ⇑(Hom.hom P.toLimit) = Set.univ

Tactic:
← closure_eq_iff_isClosed.mpr this,

Goal state after:
P : ProfiniteGrp.{u}
this : IsClosed (Set.range ⇑(Hom.hom P.toLimit))
⊢ closure (Set.range ⇑(Hom.hom P.toLimit)) = Set.univ
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case refine_3
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
hJ₁ : ⊤ ≤ I
hJ₂ : Submodule.spanRank ⊤ ≤ ↑I.height.toNat
hJ₃ : I.height ≤ ⊤.height
⊢ False

Tactic:
exact hI (top_le_iff.mp hJ₁)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
ι : Type u_2
inst✝ : Finite ι
⊢ ringKrullDim (MvPolynomial ι R) = ringKrullDim R + ↑(Nat.card ι)

Tactic:
by
  induction ι using Finite.induction_empty_option with
  | of_equiv e H =>
    convert! ← H using 1
    · exact ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv
    · rw [Nat.card_congr e]
  | h_empty => simp
  | h_option IH =>
    simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one,
      ← add_assoc] at IH ⊢
    rw [ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv,
      Polynomial.ringKrullDim_of_isNoetherianRing, IH]

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
⊢ P.height ≤ p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height

Tactic:
have hsP'sub : (s' : Set <| S ⧸ (Ideal.map (algebraMap R S) p)) ⊆ (P' : Set <| S ⧸ _) :=
    fun x hx ↦ hP'.le (Ideal.subset_span hx)

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
⊢ P.height ≤ p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: case nil
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsNoetherianRing R
inst✝³ : IsLocalRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
reg : Sequence.IsRegular M []
⊢ supportDim R (M ⧸ ofList [] • ⊤) + ↑[].length = supportDim R M

Tactic:
rw [ofList_nil, Submodule.bot_smul]
    simpa using supportDim_eq_of_equiv (Submodule.quotEquivOfEqBot ⊥ rfl)

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsNoetherianRing R
inst✝³ : IsLocalRing R
x : R
rs' : List R
ih :
  ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : Module R M] [Module.Finite R M],
    Sequence.IsRegular M rs' → supportDim R (M ⧸ ofList rs' • ⊤) + ↑rs'.length = supportDim R M
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
reg : Sequence.IsRegular M (x :: rs')
isu : IsUnit x
⊢ ⊤ = ofList (x :: rs') • ⊤

Tactic:
by simp [span_singleton_eq_top.mpr isu]

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)
h : Ideal.span (Set.range fun i ↦ (algebraMap S T) ↑i.fst * ↑i.snd) = ⊤
⊢ IsLocalIso R T

Tactic:
by
    have (i : ι) : IsStandardOpenImmersion R (T'' i.1 i.2) :=
      have : IsScalarTower R (Localization.Away i.1.1) (T' i.1.1) :=
        IsScalarTower.to₁₃₄ _ S _ _
      have : IsStandardOpenImmersion (Localization.Away i.1.1) (T'' i.1.1 i.2.1) := i.2.2
      have : IsStandardOpenImmersion R (Localization.Away i.1.1) := i.1.2
      .trans _ (Localization.Away i.1.1) _
    exact .of_span_range_eq_top _ h fun i : ι ↦ T'' i.1 i.2

Goal state after:
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)
⊢ Injective R M

Tactic:
rw [← Baer.iff_injective, Baer.iff_surjective]
  intro I
  let _ : FinitePresentation R I := finitePresentation_of_finite R I
  apply surjective_of_localized_maximal _ (fun m _ ↦ ?_)
  let Rₘ := Localization.AtPrime m
  let Mₘ := LocalizedModule m.primeCompl M
  let f := LocalizedModule.mkLinearMap m.primeCompl M
  let h : R →ₗ[R] Rₘ := Algebra.linearMap R Rₘ
  let Iₘ : Ideal Rₘ := Submodule.localized' Rₘ m.primeCompl h I
  let g : I →ₗ[R] Iₘ := I.toLocalized' Rₘ m.primeCompl h
  let gM := IsLocalizedModule.mapExtendScalars m.primeCompl g f Rₘ
  let hM := IsLocalizedModule.mapExtendScalars m.primeCompl h f Rₘ
  have eq'' : Iₘ.subtype.restrictScalars R = IsLocalizedModule.map m.primeCompl g h I.subtype :=
    IsLocalizedModule.ext m.primeCompl g (IsLocalizedModule.map_units h) (by ext; simp [g, h, Iₘ])
  have eq' : (Iₘ.subtype.lcomp Rₘ Mₘ).restrictScalars R =
    IsLocalizedModule.map m.primeCompl hM gM (I.subtype.lcomp R M) :=
    IsLocalizedModule.ext m.primeCompl hM (IsLocalizedModule.map_units gM) <| LinearMap.ext
      fun l ↦ LinearMap.restrictScalars_injective R (IsLocalizedModule.ext m.primeCompl g
        (IsLocalizedModule.map_units f) (by ext; simp +zetaDelta [-Algebra.linearMap_apply]))
  have eq : Iₘ.subtype.lcomp Rₘ Mₘ = IsLocalizedModule.mapExtendScalars m.primeCompl hM gM Rₘ
    (I.subtype.lcomp R M) := by
    simp [IsLocalizedModule.mapExtendScalars, ← eq']
  have MB : Baer Rₘ Mₘ := Baer.of_injective (H m ‹_›)
  have surj : Function.Surjective (LinearMap.lcomp Rₘ Mₘ (Submodule.subtype Iₘ)) :=
    Baer.iff_surjective.mp MB Iₘ
  rw [eq] at surj
  rw [← LinearMap.coe_restrictScalars (R := R),
    LocalizedModule.restrictScalars_map_eq m.primeCompl hM gM]
  simpa using! surj

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) β = β₀
⊢ ⊤.toSubalgebra = ⊤

Tactic:
IntermediateField.top_toSubalgebra

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) β = β₀
⊢ ⊤ = ⊤