mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
n : ℕ
⊢ map (MonoidHom.id G) (φ ≫ ψ) n = map (MonoidHom.id G) φ n ≫ map (MonoidHom.id G) ψ n

Tactic:
by
  rw [map, chainsMap_id_comp, HomologicalComplex.homologyMap_comp]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
i k : ℕ
h : i ≤ i + k
⊢ (powSMulQuotInclusion I M ⋯ ⊤) ((transitionMap I (↥(I ^ n • ⊤)) h) ((fun i ↦ ofValEqZeroAux I ⋯ hxn) (i + k))) =
    (powSMulQuotInclusion I M ⋯ ⊤) ((fun i ↦ ofValEqZeroAux I ⋯ hxn) i)

Tactic:
ofValEqZeroAux_prop,

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
i k : ℕ
h : i ≤ i + k
⊢ (powSMulQuotInclusion I M ⋯ ⊤) ((transitionMap I (↥(I ^ n • ⊤)) h) ((fun i ↦ ofValEqZeroAux I ⋯ hxn) (i + k))) =
    ↑x (i + n)
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
e : M ≃* N
⊢ (counitAlgHom R A[N]).comp ↑(domCongr R A e) = counitAlgHom R A[M]

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
x✝ : ℕ
h1 : p.coeff x✝ ≠ 0
h2 : 1 ≤ (v.intAdicAbv hb) (p.coeff x✝)
⊢ x✝ ∈ p.support

Tactic:
by simp [h1]

Goal state after:
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
⊢ (counitAlgHom R (AddMonoidAlgebra A (Additive M))).comp ↑(toAdditiveAlgEquiv R A M) = counitAlgHom R A[M]

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_8
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommMonoid M
f : R →+* S
⊢ (comulAlgHom S S[M]).comp (mapRingHom M f) =
    (Algebra.TensorProduct.mapRingHom f (mapRingHom M f) (mapRingHom M f) ⋯ ⋯).comp (comulAlgHom R R[M]).toRingHom

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_8
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommMonoid M
f : R →+* S
⊢ (counitAlgHom S S[M]).comp (mapRingHom M f) = f.comp (counitAlgHom R R[M]).toRingHom

Tactic:
by ext <;> simp

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

Goal state before:
pp: case single_one_right
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 : R[G] →ₐc[R] R[H]
x : G
⊢ single ((mapDomainOfBialgHom f) x) 1 = f (single x 1)

Tactic:
exact single_mapDomainOfBialgHomFun_one f x

Goal state after:
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✝¹ : AddMonoid M
inst✝ : AddMonoid N
⊢ (counitAlgHom R (MonoidAlgebra A (Multiplicative M))).comp ↑(toMultiplicativeAlgEquiv R A M) = counitAlgHom R A[M]

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_8
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : AddCommMonoid M
f : R →+* S
⊢ (comulAlgHom S S[M]).comp (mapRingHom M f) =
    (Algebra.TensorProduct.mapRingHom f (mapRingHom M f) (mapRingHom M f) ⋯ ⋯).comp (comulAlgHom R R[M]).toRingHom

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_8
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : AddCommMonoid M
f : R →+* S
⊢ (counitAlgHom S S[M]).comp (mapRingHom M f) = f.comp (counitAlgHom R R[M]).toRingHom

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case toIsPrime
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
eqtop : p = ⊤
⊢ False

Tactic:
simp [eqtop, Ideal.comap_top, Ideal.isPrime_iff] at hp

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

Goal state before:
pp: case h.mul_X
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
g : MvPolynomial (ℕ × M) R
nm : ℕ × M
h : P ↑g
⊢ P (↑g * ↑(X nm))

Tactic:
exact h_dp _ _ _ h

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

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx : x ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}
⊢ r • x ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}

Tactic:
refine ⟨I.smul_mem r hx.1, (fun n ↦ ?_)⟩
    rw [smul_eq_mul, hI.dpow_mul hx.1, map_mul, map_mul, map_pow,
      hJ.dpow_mul (hf (mem_map_of_mem f hx.1)), hx.2 n]

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
⊢ IsWeaklyRegular M (r :: rs) ∧ ¬⊤ = Ideal.ofList (r :: rs) • ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) ∧
        ¬⊤ = Ideal.ofList (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) • ⊤

Tactic:
isWeaklyRegular_cons_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 (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) ∧
      ¬⊤ = Ideal.ofList (r :: rs) • ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) ∧
        ¬⊤ = Ideal.ofList (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) • ⊤
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'
⊢ IsWeaklyRegular (M₂ ⊗[R] N) (r :: rs')

Tactic:
| @cons N _ _ r rs' h1 _ ih =>

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 (QuotSMulTop r N ⊗[R] M₂) rs'
⊢ IsWeaklyRegular (N ⊗[R] M₂) (r :: rs')

Tactic:
| @cons N _ _ r rs' h1 _ ih =>

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

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

Tactic:
by
  induction h₄ generalizing M M₂ M₃ with
  | nil =>
    apply (Exact.iff_of_ladder_linearEquiv ?_ ?_).mp h₁₂
    any_goals exact quotEquivOfEqBot _ <|
      Eq.trans (congrArg (· • ⊤) Ideal.ofList_nil) (bot_smul ⊤)
    all_goals exact quot_hom_ext _ _ _ fun _ => rfl
  | cons r rs h₄ _ ih =>
    specialize ih
      (map_first_exact_on_four_term_exact_of_isSMulRegular_last h₁₂ h₂₃ h₄)
      (map_exact r h₂₃ h₃) (map_surjective r h₃)
    have H₁ := quotOfListConsSMulTopEquivQuotSMulTopInner_naturality r rs f₁
    have H₂ := quotOfListConsSMulTopEquivQuotSMulTopInner_naturality r rs f₂
    exact (Exact.iff_of_ladder_linearEquiv H₁.symm H₂.symm).mp ih

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherian R M
rs rs' : List R
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
h4 : ⊤ ≠ Ideal.ofList rs • ⊤
x : R
h6 : x ∈ {r | r ∈ rs}
⊢ x ∈ IsLocalRing.maximalIdeal R

Tactic:
refine IsLocalRing.le_maximalIdeal ?_ (Ideal.subset_span h6)

Goal state after:
case refine_1
R : Type u_1
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherian R M
rs rs' : List R
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
h4 : ⊤ ≠ Ideal.ofList rs • ⊤
x : R
h6 : x ∈ {r | r ∈ rs}
⊢ Ideal.span {r | r ∈ rs} ≠ ⊤
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit k R
p : PrimeSpectrum R
⊢ (fun f ↦ { asIdeal := RingHom.ker f, isPrime := ⋯ })
      ((fun p ↦ (↑(AlgEquiv.ofBijective (ofId k (R ⧸ p.asIdeal)) ⋯).symm).comp (Ideal.Quotient.mkₐ k p.asIdeal)) p) =
    p

Tactic:
by
    ext : 1
    dsimp
    rw [← AlgHom.comap_ker, ← RingHom.ker_coe_toRingHom, AlgEquiv.toAlgHom_toRingHom,
      AlgHom.ker_coe_equiv, ← RingHom.ker_eq_comap_bot, ← RingHom.ker_coe_toRingHom,
      Ideal.Quotient.mkₐ_ker]

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Submodule.comap P.cotangentComplex.ker.subtype (↑P.cotangentExtendScalarsEquiv.symm).ker = ⊥

Tactic:
LinearEquiv.ker,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Submodule.comap P.cotangentComplex.ker.subtype ⊥ = ⊥
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ dpow hI f n (f a) = f (hI.dpow n a)

Tactic:
by
  classical
  simp only [dpow, Function.extend_def]
  have h : ∃ (a_1 : I), f ↑a_1 = f a := by use ⟨a, ha⟩
  rw [dif_pos h, ← sub_eq_zero, ← map_sub, ← RingHom.mem_ker]
  apply (hI.isSubDPIdeal_inf_iff.mp hIf) (Submodule.coe_mem _) ha
  rw [RingHom.mem_ker, map_sub, sub_eq_zero, h.choose_spec]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hx' : x ∉ J
⊢ dpow hI f n x = 0

Tactic:
rw [dpow, Function.extend_def, dif_neg, Pi.zero_apply]
    rintro ⟨⟨a, ha⟩, rfl⟩
    exact (hIJ ▸ hx') (apply_coe_mem_map f I ⟨a, ha⟩)

Goal state after:
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
⊢ map (g.comp f) N = map g (map f N)

Tactic:
let : IsScalarTower A B C := by apply IsScalarTower.of_algebraMap_eq'; rfl

Goal state after:
R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
⊢ map (g.comp f) N = map g (map f N)
Module: Mathlib.RingTheory.FormalGroup.Basic

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

Tactic:
rw [subst_comp_subst_apply aux₁ this]
      congr! 2 with s
      fin_cases s
      · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue,
          Matrix.cons_val_zero, subst_comp_subst_apply HasSubst.X_X this]
        congr! 2 with s
        fin_cases s <;> simp [subst_X this]
      · simp [subst_X this]

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

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
d n : ℕ
⊢ (coeff n) ((rescale (-1)) ↑(invOneSubPow A d)) = (coeff n) (binomialSeries A (-↑d))

Tactic:
coeff_rescale,

Goal state after:
A : Type u_2
inst✝ : CommRing A
d n : ℕ
⊢ (-1) ^ n * (coeff n) ↑(invOneSubPow A d) = (coeff n) (binomialSeries A (-↑d))
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
⊢ (powerSeriesFamily x 1).hsum = 1

Tactic:
simp only [hsum, smulFamily_toFun, coeff_one, powers_toFun, ite_smul, one_smul, zero_smul]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
⊢ { coeff := fun g ↦ ∑ᶠ (i : ℕ), (if i = 0 then (if 0 < x.orderTop then x else 0) ^ i else 0).coeff g,
      isPWO_support' := ⋯ } =
    1
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case h
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
⊢ (heval x) ↑u * (heval x) u.inv = 1

Tactic:
← heval_mul,

Goal state after:
case h
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
⊢ (heval x) (↑u * u.inv) = 1
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
tfae_2_to_1 :
  (∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R),
          (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀) →
    HenselianLocalRing R
⊢ [HenselianLocalRing R,
      ∀ (f : R[X]),
        f.Monic →
          ∀ (a₀ : ResidueField R),
            (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀,
      ∀ {K : Type u} [inst : Field K] (φ : R →+* K),
        Surjective ⇑φ →
          ∀ (f : R[X]),
            f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀].TFAE

Tactic:
tfae_have 1 → 3
  | hR, K, _K, φ, hφ, f, hf, a₀, h₁, h₂ => by
    obtain ⟨a₀, rfl⟩ := hφ a₀
    have H := HenselianLocalRing.is_henselian f hf a₀
    simp only [← ker_eq_maximalIdeal φ hφ, eval₂_at_apply, RingHom.mem_ker] at H h₁ h₂
    obtain ⟨a, ha₁, ha₂⟩ := H h₁ (by
      contrapose h₂
      rwa [← mem_nonunits_iff, ← mem_maximalIdeal, ← ker_eq_maximalIdeal φ hφ,
        RingHom.mem_ker] at h₂)
    refine ⟨a, ha₁, ?_⟩
    rwa [φ.map_sub, sub_eq_zero] at ha₂

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
tfae_2_to_1 :
  (∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R),
          (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀) →
    HenselianLocalRing R
tfae_1_to_3 :
  HenselianLocalRing R →
    ∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀
⊢ [HenselianLocalRing R,
      ∀ (f : R[X]),
        f.Monic →
          ∀ (a₀ : ResidueField R),
            (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀,
      ∀ {K : Type u} [inst : Field K] (φ : R →+* K),
        Surjective ⇑φ →
          ∀ (f : R[X]),
            f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀].TFAE
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingUp R S
inst✝ : HasGoingUp S T
⊢ HasGoingUp R T

Tactic:
rw [iff_specializingMap_primeSpectrumComap, IsScalarTower.algebraMap_eq R S T]
  simp only [PrimeSpectrum.comap_comp]
  apply SpecializingMap.comp
  · rwa [← iff_specializingMap_primeSpectrumComap]
  · rwa [← iff_specializingMap_primeSpectrumComap]

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

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : WfDvdMonoid R
x : R
hx : Prime x
p : Ideal R
inst✝³ : p.IsPrime
hxp : x ∉ p
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
this : Disjoint ↑(Submonoid.powers x) ↑p
hpbot : ¬p = ⊥
hi : Function.Injective ⇑(algebraMap R S)
hpb : map (algebraMap R S) p ≠ ⊥
g : S
hg : map (algebraMap R S) p = S ∙ g
hg0 : g ≠ 0
a : R
n : ℤ
hxa : ¬x ∣ a
hag : selfZPow x S n * (algebraMap R S) a = g
hu : IsUnit (selfZPow x S n)
⊢ ∀ (y : R), x * y ∈ R ∙ a → y ∈ R ∙ a

Tactic:
· intro y hy
      rw [mem_span_singleton] at hy ⊢
      exact (hx.left_dvd_or_dvd_right_of_dvd_mul hy).resolve_left hxa

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

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
x✝ : ∃ B, B.sets = {x | ∃ I ∈ F, ↑I = x}
B : RingFilterBasis A
hB : B.sets = {x | ∃ I ∈ F, ↑I = x}
I : Ideal A
hI : I ∈ F
a : A
⊢ ↑I ∈ {x | ∃ I ∈ F, ↑I = x}

Tactic:
by simpa

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
hx' : ¬IsUnit x
⊢ span {x} ≠ ⊤

Tactic:
by simpa

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
x : PrimeSpectrum A
m : M
hm : ∀ (r : A), r • m = 0 → r ∈ x.asIdeal
r : R
e : r • m = 0
⊢ (algebraMap R A) r • m = 0

Tactic:
by simpa

Goal state after:
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 ∈ (span ↑hs.toFinset).minimalPrimes

Tactic:
by simpa

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
r : R
p : Ideal R
inst✝ : p.IsPrime
hrm : r ∈ p
⊢ {r} ⊆ ↑p

Tactic:
by simpa

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
r : R
p : Ideal R
inst✝ : p.IsPrime
hrp : r ∈ p
⊢ {r} ⊆ ↑?m.31

Tactic:
by simpa

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

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
h : x ∈ (annihilator R M).jacobson
a✝ : Nontrivial M
p : LTSeries ↑(support R M)
hxp : x ∈ (↑(RelSeries.last p)).asIdeal
q : LTSeries (PrimeSpectrum R)
hxq : x ∈ (q.toFun 1).asIdeal
hq : (p.map Subtype.val ⋯).length = q.length
h0 : ↑(RelSeries.head p) = RelSeries.head q
right✝ : RelSeries.last (p.map Subtype.val ⋯) = RelSeries.last q
hp0 : p.length = 0
hb : supportDim R (QuotSMulTop x M) ≠ ⊥
⊢ ↑0 ≤ supportDim R (QuotSMulTop x M) + 1

Tactic:
← WithBot.coe_unbot (supportDim R (QuotSMulTop x M)) hb

Goal state after:
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
h : x ∈ (annihilator R M).jacobson
a✝ : Nontrivial M
p : LTSeries ↑(support R M)
hxp : x ∈ (↑(RelSeries.last p)).asIdeal
q : LTSeries (PrimeSpectrum R)
hxq : x ∈ (q.toFun 1).asIdeal
hq : (p.map Subtype.val ⋯).length = q.length
h0 : ↑(RelSeries.head p) = RelSeries.head q
right✝ : RelSeries.last (p.map Subtype.val ⋯) = RelSeries.last q
hp0 : p.length = 0
hb : supportDim R (QuotSMulTop x M) ≠ ⊥
⊢ ↑0 ≤ ↑((supportDim R (QuotSMulTop x M)).unbot hb) + 1