mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑f
rkeq :
  Module.rank (IsLocalRing.ResidueField R) (maximalIdeal R).Cotangent =
    Module.rank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
⊢ Submodule.spanFinrank (maximalIdeal (AdicCompletion (maximalIdeal R) R)) = Submodule.spanFinrank (maximalIdeal R)

Tactic:
have fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG := by
    simpa [AdicCompletion.maximalIdeal_eq_map] using fg.map _

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑f
rkeq :
  Module.rank (IsLocalRing.ResidueField R) (maximalIdeal R).Cotangent =
    Module.rank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG
⊢ Submodule.spanFinrank (maximalIdeal (AdicCompletion (maximalIdeal R) R)) = Submodule.spanFinrank (maximalIdeal R)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
x✝ : MvPowerSeries σ R
⊢ toAdicCompletionInv σ R ((↑↑(toAdicCompletion σ R).toRingHom).toFun x✝) = x✝

Tactic:
by
    ext; simp [coeff_toAdicCompletionInv, coeff_toAdicCompletion_val_apply_out]

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
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
⊢ (eval I M n).ker ≤ ↑s • restrictScalars R ⊤

Tactic:
← restrictScalars_image_smul_eq (R := AdicCompletion I R),

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
⊢ (eval I M n).ker ≤ restrictScalars R (⇑(algebraMap R (AdicCompletion I R)) '' ↑s • ⊤)
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: 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✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
f g : M →* A
m✝ : M
⊢ (((lift R A M).trans (WithConv.equiv (R[M] →ₐ[R] A)).symm).toFun (f * g)).ofConv (single m✝ 1) =
    (((lift R A M).trans (WithConv.equiv (R[M] →ₐ[R] A)).symm).toFun f *
          ((lift R A M).trans (WithConv.equiv (R[M] →ₐ[R] A)).symm).toFun g).ofConv
      (single m✝ 1)

Tactic:
simp [AlgHom.convMul_apply]

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

Goal state before:
pp: R : Type u_1
A : Type u_3
M : Type u_8
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
f g : WithConv (R[M] →ₐ[R] A)
x : M
⊢ (f * g).ofConv (single x 1) = f.ofConv (single x 1) * g.ofConv (single x 1)

Tactic:
simp [AlgHom.convMul_apply]

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

Goal state before:
pp: case single_zero_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✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : AddMonoid M
f g : Multiplicative M →* A
m✝ : M
⊢ (((lift R A M).trans (WithConv.equiv (R[M] →ₐ[R] A)).symm).toFun (f * g)).ofConv (single m✝ 1) =
    (((lift R A M).trans (WithConv.equiv (R[M] →ₐ[R] A)).symm).toFun f *
          ((lift R A M).trans (WithConv.equiv (R[M] →ₐ[R] A)).symm).toFun g).ofConv
      (single m✝ 1)

Tactic:
simp [AlgHom.convMul_apply]

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

Goal state before:
pp: case right
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : v.intValuation x * v.intValuation inv✝ = 1
⊢ v.intValuation x * v.intValuation inv✝ ≤ (valuation K v) ((algebraMap R K) x)

Tactic:
← mul_one <| v.valuation _ _,

Goal state after:
case right
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : v.intValuation x * v.intValuation inv✝ = 1
⊢ v.intValuation x * v.intValuation inv✝ ≤ (valuation K v) ((algebraMap R K) x) * 1
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
a✝ b✝ : Kˣ ⧸ (powMonoidHom n).range
hx : a✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
hy : b✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
v : HeightOneSpectrum R
hv : v ∉ S
⊢ (v.valuationOfNeZeroMod n) (a✝ * b✝) = 1

Tactic:
map_mul,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
a✝ b✝ : Kˣ ⧸ (powMonoidHom n).range
hx : a✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
hy : b✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
v : HeightOneSpectrum R
hv : v ∉ S
⊢ (v.valuationOfNeZeroMod n) a✝ * (v.valuationOfNeZeroMod n) b✝ = 1
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: 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)
⊢ ∃ r ∈ annihilator R N, IsSMulRegular M r

Tactic:
cases subsingleton_or_nontrivial M

Goal state after:
case inl
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✝ : Subsingleton M
⊢ ∃ r ∈ annihilator R N, IsSMulRegular M r

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
⊢ ∃ r ∈ annihilator R N, IsSMulRegular M r
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
x✝ : A
ha : x✝ ∈ ⊥
⊢ (if x✝ = 0 ∧ 1 = 0 then 1 else 0) = x✝

Tactic:
simp [mem_bot.mp ha]

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ (RingCon.mkₐ R (ringCon R M)) (C a) = (algebraMap R (DividedPowerAlgebra R M)) a

Tactic:
by
  rw [← MvPolynomial.algebraMap_eq, AlgHom.commutes]

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
i : ℕ
le_rad : I ≤ (Module.annihilator R ↑N).radical
a : R
rs' : List R
k : ℕ
hk : a ^ k ∈ Module.annihilator R ↑N
reg : IsSMulRegular (↑M) a ∧ RingTheory.Sequence.IsRegular (QuotSMulTop a ↑M) rs'
mem : a ∈ I ∧ ∀ a ∈ rs', a ∈ I
len : rs'.length = n
hi : 0 < n + 1
⊢ Subsingleton (Ext N M 0)

Tactic:
have : Subsingleton (N →ₗ[R] M) := subsingleton_linearMap_iff.mpr ⟨a ^ k, hk, reg.1.pow k⟩

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
i : ℕ
le_rad : I ≤ (Module.annihilator R ↑N).radical
a : R
rs' : List R
k : ℕ
hk : a ^ k ∈ Module.annihilator R ↑N
reg : IsSMulRegular (↑M) a ∧ RingTheory.Sequence.IsRegular (QuotSMulTop a ↑M) rs'
mem : a ∈ I ∧ ∀ a ∈ rs', a ∈ I
len : rs'.length = n
hi : 0 < n + 1
this : Subsingleton (↑N →ₗ[R] ↑M)
⊢ Subsingleton (Ext N M 0)
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
a✝ b✝ : A
hx : a✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n a✝) = hJ.dpow n (f a✝)
hy : b✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n b✝) = hJ.dpow n (f b✝)
n : ℕ
k : ℕ × ℕ
⊢ f (hI.dpow k.1 a✝ * hI.dpow k.2 b✝) = hJ.dpow k.1 (f a✝) * hJ.dpow k.2 (f b✝)

Tactic:
map_mul,

Goal state after:
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
a✝ b✝ : A
hx : a✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n a✝) = hJ.dpow n (f a✝)
hy : b✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n b✝) = hJ.dpow n (f b✝)
n : ℕ
k : ℕ × ℕ
⊢ f (hI.dpow k.1 a✝) * f (hI.dpow k.2 b✝) = hJ.dpow k.1 (f a✝) * hJ.dpow k.2 (f b✝)
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)}
n : ℕ
⊢ f (r ^ n * hI.dpow n x) = hJ.dpow n (f (r * x))

Tactic:
map_mul,

Goal state after:
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)}
n : ℕ
⊢ f (r ^ n) * f (hI.dpow n x) = hJ.dpow n (f (r * x))
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)}
n : ℕ
⊢ f (r ^ n) * f (hI.dpow n x) = hJ.dpow n (f (r * x))

Tactic:
map_mul,

Goal state after:
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)}
n : ℕ
⊢ f (r ^ n) * f (hI.dpow n x) = hJ.dpow n (f r * f x)
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: 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₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
| IsRegular M as ↔ IsRegular M₂ bs

Tactic:
congr <;> rw [isRegular_iff, ne_comm, ← Quotient.nontrivial_iff]

Goal state after:
case a
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₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
| IsWeaklyRegular M as ∧ Nontrivial (M ⧸ Ideal.ofList as • ⊤)

case b
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₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
| IsWeaklyRegular M₂ bs ∧ Nontrivial (M₂ ⧸ Ideal.ofList bs • ⊤)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: 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
n : ℕ
r : R
a : M
⊢ dp S n (f (r • a)) = r ^ n • dp S n (f a)

Tactic:
by
  rw [f.map_smul, algebra_compatible_smul S r (f a),
    DividedPowerAlgebra.dp_smul, ← map_pow, algebraMap_smul]

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 (e.symm a✝ ^ n✝ * hI.dpow n✝ (e.symm x✝)) = a✝ ^ n✝ * e (hI.dpow n✝ (e.symm x✝))

Tactic:
map_mul,

Goal state after:
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 (e.symm a✝ ^ n✝) * e (hI.dpow n✝ (e.symm x✝)) = a✝ ^ n✝ * e (hI.dpow n✝ (e.symm x✝))
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case cons.refine_1
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₂ : List R
r : R
l₁✝ l₂✝ : List R
a✝ : l₁✝ ~ l₂✝
ih :
  ∀ (rs₀ : List R),
    rs₀ ++ l₁✝ <+~ rs →
      rs₀ ++ l₂✝ <+~ rs →
        IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₁✝ → IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₂✝
rs₀ : List R
H₁ : rs₀ ++ r :: l₁✝ <+~ rs
H₃ : rs₀ ++ r :: l₂✝ <+~ rs
h : IsSMulRegular (M ⧸ Ideal.ofList rs₀ • ⊤) r ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₀) • ⊤) l₁✝
e : (M ⧸ Ideal.ofList (r :: rs₀) • ⊤) ≃ₗ[R] QuotSMulTop r (M ⧸ Ideal.ofList rs₀ • ⊤) :=
  quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
⊢ r :: rs₀ ++ l₁✝ <+~ rs

Tactic:
exact List.perm_middle.subperm_right.mp ‹_›

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

Goal state before:
pp: case cons.refine_2
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₂ : List R
r : R
l₁✝ l₂✝ : List R
a✝ : l₁✝ ~ l₂✝
ih :
  ∀ (rs₀ : List R),
    rs₀ ++ l₁✝ <+~ rs →
      rs₀ ++ l₂✝ <+~ rs →
        IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₁✝ → IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₂✝
rs₀ : List R
H₁ : rs₀ ++ r :: l₁✝ <+~ rs
H₃ : rs₀ ++ r :: l₂✝ <+~ rs
h : IsSMulRegular (M ⧸ Ideal.ofList rs₀ • ⊤) r ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₀) • ⊤) l₁✝
e : (M ⧸ Ideal.ofList (r :: rs₀) • ⊤) ≃ₗ[R] QuotSMulTop r (M ⧸ Ideal.ofList rs₀ • ⊤) :=
  quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
⊢ r :: rs₀ ++ l₂✝ <+~ rs

Tactic:
exact List.perm_middle.subperm_right.mp ‹_›

Goal state after:
Module: Mathlib.RingTheory.DualNumber

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

Tactic:
rw [← fst_pow, hn, fst_zero]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
x : A
hx : x ∈ ↑K
⊢ f x ∈ ↑J

Tactic:
exact hf.1 (mem_map_of_mem f (hK.1 hx))

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
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB : Function.Surjective ⇑fAB
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
⊢ (map g (map f N)).toSubmodule = fBC.ker

Tactic:
map_toSubmodule g (map f N),

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))
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB : Function.Surjective ⇑fAB
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
⊢ (baseChangeMkQ C (map f N).toSubmodule).ker = fBC.ker
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
u : Rˣ
⊢ (coeff 0) (invUnitsSub u) = 1 /ₚ u

Tactic:
coeff_invUnitsSub,

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

pp: case neg
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : ¬d 1 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

Tactic:
· by_cases hd₀ : d 0 = 0
      · simp [hd₀, hd₁]
      simp [hd₁, PowerSeries.coeff_X_pow]
      grind

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : ¬d 1 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:

Tactic:
_ = F.toPowerSeries.subst ![F.toPowerSeries.subst ![PowerSeries.X, 0], 0] := by
      have : PowerSeries.HasSubst (subst ![PowerSeries.X (R := R), 0] F.toPowerSeries) := by
        refine PowerSeries.HasSubst.of_constantCoeff_zero' ?_
        rw [PowerSeries.constantCoeff, PowerSeries.X, constantCoeff_subst_eq_zero HasSubst.X_zero
          (by simp) F.zero_constantCoeff]
      rw [PowerSeries.subst, subst_comp_subst_apply _ this.const]
      · congr! 2 with d
        fin_cases d
        · simp [← PowerSeries.subst_def, PowerSeries.subst_X this]
        · simp [← PowerSeries.subst_def, ← PowerSeries.coe_substAlgHom this]
      · exact HasSubst.X_zero
    _ = _ := by
      have : ![0, 0] = (0 : Fin 2 → PowerSeries R) := by
        ext x : 1; fin_cases x <;> rfl
      simp [F.assoc', this, subst_zero_of_constantCoeff_zero F.zero_constantCoeff,
        PowerSeries.HasSubst.X', PowerSeries.HasSubst]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
ab : α × β
x✝ : (∃ i, ¬(s i).coeff gh.1 = 0) ∧ (∃ i, ¬(t i).coeff gh.2 = 0) ∧ gh.1 +ᵥ gh.2 = g
hab : ¬(s ab.1).coeff gh.1 • (t ab.2).coeff gh.2 = 0
hsupp :
  ∀ (a : α) (b : β),
    ¬(s a).coeff gh.1 • (t b).coeff gh.2 = 0 → ¬(s.toFun a).coeff gh.1 = 0 ∧ ¬(t.toFun b).coeff gh.2 = 0
⊢ ¬(s ab.1).coeff gh.1 = 0 ∧ ¬(t ab.2).coeff gh.2 = 0

Tactic:
exact hsupp ab.1 ab.2 hab

Goal state after: