mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
⊢ ⊤ = p.contentIdeal * q.contentIdeal

Tactic:
by simp [hp, hq]

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
a✝ : G × G × G
x✝ : ↑A
⊢ (ModuleCat.Hom.hom (chainsMap₃ f φ ≫ d₃₂ B) ∘ₗ lsingle a✝) x✝ =
    (ModuleCat.Hom.hom (d₃₂ A ≫ chainsMap₂ f φ) ∘ₗ lsingle a✝) x✝

Tactic:
simpa using

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
a✝ : G × G × G
x✝ : ↑A
⊢ single (Prod.map (⇑f) (⇑f) a✝.2) ((B.ρ (f a✝.1⁻¹)) ((Hom.hom φ) x✝)) =
    single (Prod.map (⇑f) (⇑f) a✝.2) ((Hom.hom φ) ((A.ρ a✝.1⁻¹) x✝))
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
a✝ : G × G × G
x✝ : ↑A
⊢ (ModuleCat.Hom.hom (chainsMap₃ f φ ≫ d₃₂ B) ∘ₗ lsingle a✝) x✝ =
    (ModuleCat.Hom.hom (d₃₂ A ≫ chainsMap₂ f φ) ∘ₗ lsingle a✝) x✝

Tactic:
simpa [d₃₂, map_add, map_sub, ← map_inv]
      using congr(Finsupp.single _ $((hom_comm_apply φ _ _).symm))

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
r : R
⊢ Epi (M.smulShortComplex r).g

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
r : R
⊢ Function.Surjective ⇑(r • ⊤).mkQ
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
h : x ∉ Set.range fun x ↦ single x 1
this : LinearIndepOn R id (insert x (Set.range fun x ↦ single x 1))
⊢ x.coeff.sum single ∉ span R (Set.range fun x ↦ single x 1)

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
h : x ∉ Set.range fun x ↦ single x 1
this : LinearIndepOn R id (insert x (Set.range fun x ↦ single x 1))
⊢ x ∉ span R (Set.range fun x ↦ single x 1)
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : Ideal R
inst✝ : p.IsPrime
ass : p ∈ associatedPrimes R M
⊢ Ideal.comap (algebraMap R (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p)) ∈ associatedPrimes R M

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : Ideal R
inst✝ : p.IsPrime
ass : p ∈ associatedPrimes R M
⊢ p ∈ associatedPrimes R M
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: 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 : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
a : ↥T
⊢ (algebraMap R R') ↑a ∈ p

Tactic:
simpa using

Goal state after:
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 : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
a : ↥T
⊢ ↑a ∈ Ideal.span ↑T
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
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
v' i' : R
vi✝ : (algebraMap R K) v' * (algebraMap R K) i' = 1
vi : v' * i' = 1
iv✝ : (algebraMap R K) i' * (algebraMap R K) v' = 1
iv : i' * v' = 1
hx :
  (powMonoidHom n) { val := (algebraMap R K) v', inv := (algebraMap R K) i', val_inv := vi✝, inv_val := iv✝ } =
    (Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  (algebraMap R K) (v' ^ n) = (algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := (algebraMap R K) i', inv := (algebraMap R K) v', val_inv := iv✝, inv_val := vi✝ } ^ n =
    (algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ (powMonoidHom n) { val := v', inv := i', val_inv := vi, inv_val := iv } =
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }

Tactic:
simpa using

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
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
v' i' : R
vi✝ : (algebraMap R K) v' * (algebraMap R K) i' = 1
vi : v' * i' = 1
iv✝ : (algebraMap R K) i' * (algebraMap R K) v' = 1
iv : i' * v' = 1
hx :
  (powMonoidHom n) { val := (algebraMap R K) v', inv := (algebraMap R K) i', val_inv := vi✝, inv_val := iv✝ } =
    (Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  (algebraMap R K) (v' ^ n) = (algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := (algebraMap R K) i', inv := (algebraMap R K) v', val_inv := iv✝, inv_val := vi✝ } ^ n =
    (algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ v' ^ n = val✝
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
r : R
reg : IsSMulRegular M r
mem_ann : r ∈ annihilator R N
f : N →ₗ[R] M
x : N
this : r • f x = r • 0
⊢ f x = 0 x

Tactic:
simpa using

Goal state after:
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
r : R
reg : IsSMulRegular M r
mem_ann : r ∈ annihilator R N
f : N →ₗ[R] M
x : N
this : r • f x = r • 0
⊢ f x = 0
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: 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

Tactic:
exact ⟨0, ⟨Submodule.zero_mem (Module.annihilator R N), IsSMulRegular.zero⟩⟩

Goal state after:
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)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝¹ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) := Nₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) := Mₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
x✝ : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this : (maximalIdeal (Localization.AtPrime p)).IsPrime ∧ ∃ x, maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
x : LocalizedModule.AtPrime p M
hx : maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
⊢ Nontrivial (Dual p.ResidueField Nₚ')

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝¹ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) := Nₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) := Mₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
x✝ : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this : (maximalIdeal (Localization.AtPrime p)).IsPrime ∧ ∃ x, maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
x : LocalizedModule.AtPrime p M
hx : maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
⊢ Nontrivial Nₚ'
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝² : CommRing R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
hr : r ∈ I
hI : I • ⊤ ≠ ⊤
eq : I • ⊤ = ⊤
⊢ ¬Submodule.comap (r • ⊤).mkQ (I • ⊤) = Submodule.comap (r • ⊤).mkQ ⊤

Tactic:
simpa using

Goal state after:
R : Type u
inst✝² : CommRing R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
hr : r ∈ I
hI : I • ⊤ ≠ ⊤
eq : I • ⊤ = ⊤
⊢ ¬I • ⊤ = ⊤
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
k : ℕ
hk : x ^ k ∈ I
h_ext' : ∀ i < n, Subsingleton (Ext N (of R (QuotSMulTop (x ^ k) ↑M)) i)
rs : List R
len : rs.length = n
mem : ∀ r ∈ rs, r ∈ I
reg : RingTheory.Sequence.IsRegular (↑(of R (QuotSMulTop (x ^ k) ↑M))) rs
⊢ (x ^ k :: rs).length = n + 1 ∧ (∀ r ∈ x ^ k :: rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) (x ^ k :: rs)

Tactic:
simpa using

Goal state after:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
k : ℕ
hk : x ^ k ∈ I
h_ext' : ∀ i < n, Subsingleton (Ext N (of R (QuotSMulTop (x ^ k) ↑M)) i)
rs : List R
len : rs.length = n
mem : ∀ r ∈ rs, r ∈ I
reg : RingTheory.Sequence.IsRegular (↑(of R (QuotSMulTop (x ^ k) ↑M))) rs
⊢ (∀ a ∈ rs, a ∈ I) ∧ IsSMulRegular (↑M) (x ^ k) ∧ RingTheory.Sequence.IsRegular (QuotSMulTop (x ^ k) ↑M) rs
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 : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ (fun g ↦ g ∘ ⇑(RingCon.mkₐ R (ringCon R M))) ⇑f = (fun g ↦ g ∘ ⇑(RingCon.mkₐ R (ringCon R M))) ⇑g

Tactic:
simpa using

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ f.comp (RingCon.mkₐ R (ringCon R M)) = g.comp (RingCon.mkₐ R (ringCon R M))
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 : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g ↔ ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)

Tactic:
by
  refine ⟨fun h _ _ ↦ by rw [h], fun h ↦ ?_⟩
  rw [DFunLike.ext'_iff]
  apply Function.Surjective.injective_comp_right mkAlgHom_surjective
  simpa [← AlgHom.coe_comp] using MvPolynomial.algHom_ext fun ⟨n, m⟩ ↦ h n m

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
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 : ℕ × ℕ
⊢ hJ.dpow k.1 (f a✝) * f (hI.dpow k.2 b✝) = hJ.dpow k.1 (f a✝) * hJ.dpow k.2 (f b✝)

Tactic:
hy.2

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 : ℕ × ℕ
⊢ hJ.dpow k.1 (f a✝) * hJ.dpow k.2 (f b✝) = hJ.dpow k.1 (f a✝) * hJ.dpow k.2 (f b✝)
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case pos.refine_2
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ ha : a ∈ I
m : ℕ
b : A
hb : b ∈ S
⊢ (RingHom.id A) (hI.dpow m b) = hI'.dpow m ((RingHom.id A) b)

Tactic:
simpa using

Goal state after:
case pos.refine_2
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ ha : a ∈ I
m : ℕ
b : A
hb : b ∈ S
⊢ hI.dpow m b = hI'.dpow m b
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
x✝ : A
hx : x✝ ∈ I
⊢ (if hx : x✝ ∈ I then ⋯.choose else 0) = x✝

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
x✝ : A
hx : x✝ ∈ I
⊢ hJ.dpow 1 (f x✝) = f x✝
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n : ℕ
x : A
hn : n ≠ 0
hx : x ∈ I
⊢ (if hx : x ∈ I then ⋯.choose else 0) ∈ I

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n : ℕ
x : A
hn : n ≠ 0
hx : x ∈ I
⊢ ⋯.choose ∈ I
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n : ℕ
x y : A
hx : x ∈ I
hy : y ∈ I
hxy : x + y ∈ I
⊢ (if hx : x + y ∈ I then ⋯.choose else 0) =
    ∑ k ∈ Finset.antidiagonal n, (if hx : x ∈ I then ⋯.choose else 0) * if hx : y ∈ I then ⋯.choose else 0

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n : ℕ
x y : A
hx : x ∈ I
hy : y ∈ I
hxy : x + y ∈ I
⊢ hJ.dpow n (f x + f y) = ∑ x_1 ∈ Finset.antidiagonal n, hJ.dpow x_1.1 (f x) * hJ.dpow x_1.2 (f y)
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n : ℕ
a x : A
hx : x ∈ I
hax : a * x ∈ I
⊢ (if hx : a * x ∈ I then ⋯.choose else 0) = a ^ n * if hx : x ∈ I then ⋯.choose else 0

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n : ℕ
a x : A
hx : x ∈ I
hax : a * x ∈ I
⊢ hJ.dpow n (f a * f x) = f a ^ n * hJ.dpow n (f x)
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
m✝ n✝ : ℕ
x✝ : A
hx : x✝ ∈ I
⊢ ((if hx : x✝ ∈ I then ⋯.choose else 0) * if hx : x✝ ∈ I then ⋯.choose else 0) =
    ↑((m✝ + n✝).choose m✝) * if hx : x✝ ∈ I then ⋯.choose else 0

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
m✝ n✝ : ℕ
x✝ : A
hx : x✝ ∈ I
⊢ hJ.dpow m✝ (f x✝) * hJ.dpow n✝ (f x✝) = ↑((m✝ + n✝).choose m✝) * hJ.dpow (m✝ + n✝) (f x✝)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
n✝ : ℕ
x✝ : A
hn : n✝ ≠ 0
hx : x✝ ∈ J
⊢ (if x✝ ∈ J then hI.dpow n✝ x✝ else 0) ∈ J

Tactic:
simp [if_pos hx, hJ.dpow_mem _ hn hx]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
inst✝ : (x : A) → Decidable (x ∈ J)
hJ : hI.IsSubDPIdeal J
⊢ (dividedPowers hI hJ).IsDPMorphism hI (RingHom.id A)

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
inst✝ : (x : A) → Decidable (x ∈ J)
hJ : hI.IsSubDPIdeal J
⊢ J ≤ I ∧ ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ J, hI.dpow n a = (dividedPowers hI hJ).dpow n a
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: 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
⊢ I = Ideal.span {ε}

Tactic:
refine le_antisymm ?_ ?_ <;> intro x

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 ∈ Ideal.span {ε}

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
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
h : (fun J ↦ ⟨J.carrier, ⋯⟩) J = (fun J ↦ ⟨J.carrier, ⋯⟩) J'
⊢ J = J'

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
h : (fun J ↦ ⟨J.carrier, ⋯⟩) J = (fun J ↦ ⟨J.carrier, ⋯⟩) J'
⊢ J.carrier = J'.carrier
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
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
r : K[ε]
hr : ε = r * y
⊢ p * r * y ∈ I

Tactic:
exact Ideal.mul_mem_left _ _ hyI

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
this : ∃ c, fst x * c.fst = fst y ∨ fst y * c.fst = fst x
⊢ ∃ c, ε * x * c = ε * y ∨ ε * y * c = ε * x

Tactic:
simpa using

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
this : ∃ c, fst x * c.fst = fst y ∨ fst y * c.fst = fst x
⊢ ∃ c, fst x * fst c = fst y ∨ fst y * fst c = fst x
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
inst✝⁴ : Field k
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsFiniteSplit k R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ
e : R ≃ₐ[k] Fin n → k
p' : Ideal (Fin n → k) := comap e.symm p
i : Fin n
hq : PrimeSpectrum.comap (Pi.evalRingHom (fun i ↦ k) i) ⊥ = { asIdeal := p', isPrime := ⋯ }
g : (R ⧸ p) ≃ₐ[k] k :=
  (p.quotientEquivAlg p' e ⋯).trans ((quotientEquivAlgOfEq k ⋯).trans (quotientKerAlgEquivOfSurjective ⋯))
⊢ Function.Bijective ⇑(algebraMap k (R ⧸ p))

Tactic:
simpa using

Goal state after:
k : Type u_1
R : Type u_2
inst✝⁴ : Field k
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsFiniteSplit k R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ
e : R ≃ₐ[k] Fin n → k
p' : Ideal (Fin n → k) := comap e.symm p
i : Fin n
hq : PrimeSpectrum.comap (Pi.evalRingHom (fun i ↦ k) i) ⊥ = { asIdeal := p', isPrime := ⋯ }
g : (R ⧸ p) ≃ₐ[k] k :=
  (p.quotientEquivAlg p' e ⋯).trans ((quotientEquivAlgOfEq k ⋯).trans (quotientKerAlgEquivOfSurjective ⋯))
⊢ Function.Bijective ⇑g.symm