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

Goal state before:
pp: case e'_2
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
⊢ AddSubgroup.map f (Ideal.ofList [] • ⊤).toAddSubgroup = AddSubgroup.map f ⊥

Tactic:
rw [Ideal.ofList_nil, bot_smul, bot_toAddSubgroup]

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

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
⊢ (Ideal.ofList [] • ⊤).toAddSubgroup = ⊥

Tactic:
rw [Ideal.ofList_nil, bot_smul, bot_toAddSubgroup]

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

Goal state before:
pp: case nil
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
⊢ AddSubgroup.map f (Ideal.ofList [] • ⊤).toAddSubgroup = (Ideal.ofList [] • ⊤).toAddSubgroup

Tactic:
| nil =>

Goal state after:
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
r : R
rs : List R
⊢ (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs) ∧ ¬⊤ = Ideal.ofList (r :: rs) • ⊤ ↔
    IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs ∧ ⊤ ≠ Ideal.ofList rs • ⊤

Tactic:
top_eq_ofList_cons_smul_iff,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs) ∧ ¬⊤ = Ideal.ofList rs • ⊤ ↔
    IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs ∧ ⊤ ≠ Ideal.ofList 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
r : R
rs : List R
⊢ (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(algebraMap R (R ⧸ Ideal.span {r}))) rs)) ∧
      ¬⊤ = Ideal.ofList (r :: rs) • ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(algebraMap R (R ⧸ Ideal.span {r}))) rs) ∧ ¬⊤ = Ideal.ofList rs • ⊤

Tactic:
top_eq_ofList_cons_smul_iff,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(algebraMap R (R ⧸ Ideal.span {r}))) rs)) ∧
      ¬⊤ = Ideal.ofList rs • ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(algebraMap R (R ⧸ Ideal.span {r}))) rs) ∧ ¬⊤ = Ideal.ofList rs • ⊤
Module: Mathlib.RingTheory.Regular.RegularSequence

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

Tactic:
| nil =>

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

Goal state before:
pp: case nil
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✝
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₃
f₃ : M₃ →ₗ[R] M✝
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
⊢ Exact ⇑((Ideal.ofList [] • ⊤).mapQ (Ideal.ofList [] • ⊤) f₁ ⋯)
    ⇑((Ideal.ofList [] • ⊤).mapQ (Ideal.ofList [] • ⊤) f₂ ⋯)

Tactic:
| nil =>

Goal state after:
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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ y ^ k.2 * x ^ k.1 ∈ ↑(I ^ m)

Tactic:
← Finset.mem_antidiagonal.mp hk,

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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ y ^ k.2 * x ^ k.1 ∈ ↑(I ^ (k.1 + k.2))
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case nil
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
rs : List R
h✝ : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K := torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ rs₀ : List R
H₁ H₃ : rs₀ ++ [] <+~ rs
h : IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) []
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) []

Tactic:
| nil =>

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

Goal state before:
pp: case hbc
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 ∈ Ideal.span {↑p ^ 1}

Tactic:
pow_one

Goal state after:
case hbc
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 ∈ Ideal.span {↑p}
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hm : n ≠ 0
hx : x ∈ Ideal.span {↑p}
hiff : ‖⟨dpow' p n ↑x, ⋯⟩‖ ≤ ↑p ^ (-↑1) ↔ ⟨dpow' p n ↑x, ⋯⟩ ∈ Ideal.span {↑p ^ 1}
⊢ ⟨dpow' p n ↑x, ⋯⟩ ∈ Ideal.span {↑p}

Tactic:
pow_one

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hm : n ≠ 0
hx : x ∈ Ideal.span {↑p}
hiff : ‖⟨dpow' p n ↑x, ⋯⟩‖ ≤ ↑p ^ (-↑1) ↔ ⟨dpow' p n ↑x, ⋯⟩ ∈ Ideal.span {↑p}
⊢ ⟨dpow' p n ↑x, ⋯⟩ ∈ Ideal.span {↑p}
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
p q : hI.SubDPIdeal
h : (fun s ↦ ↑s.carrier) p = (fun s ↦ ↑s.carrier) q
⊢ p = q

Tactic:
rw [SetLike.coe_set_eq] at h
    cases p; cases q; congr

Goal state after:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Etale R S
algInst✝ : Algebra (S ⊗[R] S) S := (TensorProduct.lmul' R).toAlgebra
this : Etale R (S ⊗[R] S)
⊢ (TensorProduct.lmul' R).Flat

Tactic:
have : Etale (S ⊗[R] S) S := .of_restrictScalars R _ _

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Etale R S
algInst✝ : Algebra (S ⊗[R] S) S := (TensorProduct.lmul' R).toAlgebra
this✝ : Etale R (S ⊗[R] S)
this : Etale (S ⊗[R] S) S
⊢ (TensorProduct.lmul' R).Flat
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 Ω
A B : FiniteEtale R
f : A ⟶ B
⊢ (baseChange R R).map f ≫ (isoMk (Algebra.TensorProduct.lid R ↑B.obj)).hom =
    (isoMk (Algebra.TensorProduct.lid R ↑A.obj)).hom ≫ (𝟭 (FiniteEtale R)).map f

Tactic:
dsimp [baseChange]

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 Ω
A B : FiniteEtale R
f : A ⟶ B
⊢ ofHom (Algebra.TensorProduct.map (AlgHom.id R R) (Hom.hom f.hom)) ≫ (isoMk (Algebra.TensorProduct.lid R ↑B.obj)).hom =
    (isoMk (Algebra.TensorProduct.lid R ↑A.obj)).hom ≫ f
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
⊢ P.cotangentComplex ∘ₗ
      ↑((P.h1CotangentExtendScalarsEquiv.symm.trans (P.extendScalars.h1CotangentEquivOfSurjective ⋯)).trans
          P.cotangentExtendScalarsEquiv) =
    H1Cotangent.δ R P.Ring S

Tactic:
LinearEquiv.coe_trans,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ P.cotangentComplex ∘ₗ
      ↑P.cotangentExtendScalarsEquiv ∘ₗ
        ↑(P.h1CotangentExtendScalarsEquiv.symm.trans (P.extendScalars.h1CotangentEquivOfSurjective ⋯)) =
    H1Cotangent.δ R P.Ring S
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
⊢ P.cotangentComplex ∘ₗ
      ↑P.cotangentExtendScalarsEquiv ∘ₗ
        ↑(P.h1CotangentExtendScalarsEquiv.symm.trans (P.extendScalars.h1CotangentEquivOfSurjective ⋯)) =
    H1Cotangent.δ R P.Ring S

Tactic:
LinearEquiv.coe_trans,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ P.cotangentComplex ∘ₗ
      ↑P.cotangentExtendScalarsEquiv ∘ₗ
        ↑(P.extendScalars.h1CotangentEquivOfSurjective ⋯) ∘ₗ ↑P.h1CotangentExtendScalarsEquiv.symm =
    H1Cotangent.δ R P.Ring S
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
⊢ ↑((P.h1CotangentExtendScalarsEquiv.symm.trans (P.extendScalars.h1CotangentEquivOfSurjective ⋯)).trans
          P.cotangentExtendScalarsEquiv) ∘ₗ
      Algebra.H1Cotangent.map R P.Ring S S =
    h1Cotangentι ∘ₗ H1Cotangent.map (defaultHom R S P)

Tactic:
LinearEquiv.coe_trans,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (↑P.cotangentExtendScalarsEquiv ∘ₗ
        ↑(P.h1CotangentExtendScalarsEquiv.symm.trans (P.extendScalars.h1CotangentEquivOfSurjective ⋯))) ∘ₗ
      Algebra.H1Cotangent.map R P.Ring S S =
    h1Cotangentι ∘ₗ H1Cotangent.map (defaultHom R S P)
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
⊢ (↑P.cotangentExtendScalarsEquiv ∘ₗ
        ↑(P.h1CotangentExtendScalarsEquiv.symm.trans (P.extendScalars.h1CotangentEquivOfSurjective ⋯))) ∘ₗ
      Algebra.H1Cotangent.map R P.Ring S S =
    h1Cotangentι ∘ₗ H1Cotangent.map (defaultHom R S P)

Tactic:
LinearEquiv.coe_trans,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (↑P.cotangentExtendScalarsEquiv ∘ₗ
        ↑(P.extendScalars.h1CotangentEquivOfSurjective ⋯) ∘ₗ ↑P.h1CotangentExtendScalarsEquiv.symm) ∘ₗ
      Algebra.H1Cotangent.map R P.Ring S S =
    h1Cotangentι ∘ₗ H1Cotangent.map (defaultHom R S P)
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case inr
ι : 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 : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx✝ : x ∈ insert 0 s
hx : x ∈ s
j : ι
hj : x ∈ 𝒜 j
⊢ ↑(((decompose 𝒜) x) i) ∈ insert 0 s

Tactic:
obtain rfl | h := eq_or_ne i j

Goal state after:
case inr.inl
ι : 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 : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx✝ : x ∈ insert 0 s
hx : x ∈ s
hj : x ∈ 𝒜 i
⊢ ↑(((decompose 𝒜) x) i) ∈ insert 0 s

case inr.inr
ι : 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✝ : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx✝ : x ∈ insert 0 s
hx : x ∈ s
j : ι
hj : x ∈ 𝒜 j
h : i ≠ j
⊢ ↑(((decompose 𝒜) x) i) ∈ insert 0 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.localize.IsArithFrobAt (maximalIdeal (Localization.AtPrime Q))

Tactic:
have h : Nat.card (R ⧸ (maximalIdeal _).comap (algebraMap R (Localization.AtPrime Q))) =
      Nat.card (R ⧸ Q.under R) := by
    congr 2
    rw [← Ideal.under_def, ← Ideal.under_under (B := S), Localization.AtPrime.under_maximalIdeal]
  intro x
  obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq Q.primeCompl x
  simp only [localize, coe_mk, Localization.localRingHom_mk', RingHom.coe_coe, h,
    ← IsLocalization.mk'_pow]
  rw [← IsLocalization.mk'_sub,
    IsLocalization.AtPrime.mk'_mem_maximal_iff (Localization.AtPrime Q) Q]
  simp only [SubmonoidClass.coe_pow, ← Ideal.Quotient.eq_zero_iff_mem]
  simp [H.mk_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
u : Rˣ
⊢ 1 /ₚ u ^ 1 = 1 /ₚ u

Tactic:
pow_one

Goal state after:
R : Type u_1
inst✝ : Ring R
u : Rˣ
⊢ 1 /ₚ u = 1 /ₚ u
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
aux₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
aux₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
subst_X aux₁,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
aux₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
aux₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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).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

Tactic:
refine (Finset.sum_of_injOn (fun x => ⟨x.1 + x.2, x⟩) (fun _ _ _ _ => by simp) ?_ ?_
      (fun _ _ => by simp [smul_smul, mul_comm, pow_add])).symm

Goal state after:
case pos.refine_1
Γ : 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 : Γ
⊢ Set.MapsTo (fun x ↦ ⟨x.1 + x.2, x⟩) ↑⋯.toFinset
    ↑((image (fun i ↦ i.1 + i.2) ⋯.toFinset).sigma HasAntidiagonal.antidiagonal)

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 ∈ (image (fun i ↦ i.1 + i.2) ⋯.toFinset).sigma HasAntidiagonal.antidiagonal,
    i ∉ (fun x ↦ ⟨x.1 + x.2, x⟩) '' ↑⋯.toFinset →
      ((PowerSeries.coeff i.snd.1) a * (PowerSeries.coeff i.snd.2) b) • (x ^ i.fst).coeff g = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

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

Tactic:
constantCoeff_subst_eq_zero HasSubst.zero_X
          (by simp) F.zero_constantCoeff

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ 0 = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ PowerSeries.subst f (subst ![PowerSeries.X, 0] F.toPowerSeries) = f

Tactic:
by
      simp [Xzero_eq_X, PowerSeries.subst_X hf]

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

Goal state before:
pp: case pos
Γ : 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 : α ↪ β
b : β
g : Γ
hb : b ∈ Set.range ⇑f
h : g ∈ (s (Classical.choose hb)).support
⊢ g ∈ ⋃ a, (s a).support

Tactic:
exact Set.mem_iUnion.2 ⟨Classical.choose hb, 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)
⊢ ∀ (c_1 : ℕ),
    2 ≤ c_1 ∧ c_1 < ((taylor (c n)) f).natDegree + 2 →
      ((taylor (c n)) f).coeff c_1 * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ c_1 ∈
        I ^ (n + 1 + 1)

Tactic:
rintro i ⟨h2i, _⟩

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : UniqueFactorizationMonoid R
p : Ideal R
inst✝ : p.IsPrime
hph : p.height = 1
⊢ Submodule.IsPrincipal p

Tactic:
have hpn : p ≠ ⊥ := p.ne_bot_of_height_eq_one hph
  obtain ⟨x, hxmem, hxp⟩ := Ideal.IsPrime.exists_mem_prime_of_ne_bot ‹_› hpn
  exact ⟨x, p.eq_span_singleton_of_height_eq_one hph hxmem hxp⟩

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

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
⊢ ∀ {x y : Set A}, x ∈ {x | ∃ I ∈ F, ↑I = x} → y ∈ {x | ∃ I ∈ F, ↑I = x} → ∃ z ∈ {x | ∃ I ∈ F, ↑I = x}, z ⊆ x ∩ y

Tactic:
by
    rintro s t ⟨I, hI, rfl⟩ ⟨J, hJ, rfl⟩
    exact ⟨I ⊓ J, ⟨I ⊓ J, Order.PFilter.inf_mem hI hJ, rfl⟩, fun _ h ↦ h⟩

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
⊢ supportDim R M ≠ ⊥

Tactic:
have : Nonempty (Module.support R M) := nonempty_support_of_nontrivial.to_subtype

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
this : Nonempty ↑(support R M)
⊢ supportDim R M ≠ ⊥
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Set R
hs : s.Finite
hI : p ∈ (span s).minimalPrimes
⊢ p.height ≤ ↑s.ncard

Tactic:
by
  rw [s.ncard_eq_toFinset_card hs]
  exact Ideal.height_le_card_of_mem_minimalPrimes_span_finset (by simpa)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsMaximal
this : (Ideal.map C p).LiesOver p
⊢ (Ideal.map C p).height = p.height

Tactic:
simp [height_eq_height_add_of_liesOver_of_hasGoingDown p]

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

Goal state before:
pp: case h_option
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
ι : Type u_2
inst✝¹ : Finite ι
α✝ : Type u_2
inst✝ : Fintype α✝
IH : ringKrullDim (MvPolynomial α✝ R) = ringKrullDim R + ↑(Fintype.card α✝)
⊢ ringKrullDim (MvPolynomial α✝ R) + 1 = ringKrullDim R + ↑(Fintype.card α✝) + 1

Tactic:
IH

Goal state after:
case h_option
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
ι : Type u_2
inst✝¹ : Finite ι
α✝ : Type u_2
inst✝ : Fintype α✝
IH : ringKrullDim (MvPolynomial α✝ R) = ringKrullDim R + ↑(Fintype.card α✝)
⊢ ringKrullDim R + ↑(Fintype.card α✝) + 1 = ringKrullDim R + ↑(Fintype.card α✝) + 1
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p
a✝¹ : Nontrivial M
a✝ : Nontrivial (QuotSMulTop x M)
⊢ supportDim R (QuotSMulTop x M) + 1 ≤ supportDim R M

Tactic:
have : Nonempty (Module.support R M) := nonempty_support_of_nontrivial.to_subtype

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p
a✝¹ : Nontrivial M
a✝ : Nontrivial (QuotSMulTop x M)
this : Nonempty ↑(support R M)
⊢ supportDim R (QuotSMulTop x M) + 1 ≤ supportDim R M
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
⊢ 1 = Fin.castSucc 1

Tactic:
simp [Fin.one_eq_mk_of_lt h1]

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case pos
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)
IH :
  ∀ s_1 ∈ s,
    (s.erase s_1).inf id = N → ∃ t ⊆ s.erase s_1, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
hs : s.inf id = N
H : ∀ J ∈ s, ¬(s.erase J).inf id ≤ J
⊢ ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
exact ⟨s, Finset.Subset.rfl, hs, H⟩

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

Goal state after: