mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: S : Type u_3
inst✝¹ : CommRing S
inst✝ : IsNoetherianRing S
n : ℕ
⊢ IsNoetherianRing (MvPowerSeries (Fin n) S)

Tactic:
induction n with
  | zero =>
    exact isNoetherianRing_of_ringEquiv S (isEmptyEquiv (Fin 0) S).toRingEquiv.symm
  | succ n _ =>
    exact isNoetherianRing_of_ringEquiv (PowerSeries (MvPowerSeries (Fin n) S))
      (finSuccEquiv S n).toRingEquiv.symm

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 ≤ I ^ n • ⊤

Tactic:
simp only [← hs, span_smul_eq]

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 ≤ ↑s • ⊤
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
⊢ (ofPowSMul I M n).range ≤
    ((lsum (AdicCompletion I R)) fun i ↦ (algebraMap R (AdicCompletion I R)) ↑i • LinearMap.id).range

Tactic:
simp only [SetLike.coe_sort_coe]

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
⊢ (ofPowSMul I M n).range ≤
    ((lsum (AdicCompletion I R)) fun i ↦ (algebraMap R (AdicCompletion I R)) ↑i • LinearMap.id).range
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
⊢ ∑ x ∈ s, ∑ y ∈ s, (if x = y then d * c x else 0) • x ⊗ₜ[R] y = d • ∑ x ∈ s, c x • x ⊗ₜ[R] x

Tactic:
simp [Finset.smul_sum, mul_smul]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
I : Submodule R C
⊢ ((∀ ⦃x : C⦄, x ∈ I → x ∈ counit.ker) ∧ ∀ ⦃x : C⦄, x ∈ I → comul x ∈ (TensorProduct.map I.mkQ I.mkQ).ker) ↔
    (∀ ⦃x : C⦄, x ∈ I → x ∈ counit.ker) ∧ ∀ x ∈ I, comul x ∈ (lTensor C I.subtype).range ⊔ (rTensor C I.subtype).range

Tactic:
TensorProduct.map_ker (LinearMap.exact_subtype_mkQ I) I.mkQ_surjective
      (LinearMap.exact_subtype_mkQ I) I.mkQ_surjective

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂
a✝ : x ∈ ⊤
X : G →₀ ↥S →₀ ↑A
hX : mapRange ⇑(ConcreteCategory.hom (chains₁ToCoinvariantsKer (res S.subtype A))) ⋯ X = x
Y : ↥S →₀ ↑A :=
  X.sum fun g f ↦ (mapRange.linearMap (A.ρ g⁻¹)) ((lmapDomain (↑A) k fun s ↦ (MulAut.conjNormal g⁻¹) s) f) - f
Z : G × G →₀ ↑A :=
  X.sum fun g f ↦ (lmapDomain (↑A) k fun s ↦ (g, g⁻¹ * ↑s * g)) f - (lmapDomain (↑A) k fun s ↦ (↑s, g)) f
⊢ (ConcreteCategory.hom (d₂₁ A)) Z =
    mapRange id ⋯ ((lmapDomain (↑A) k Subtype.val) Y) -
      (mapRange.linearMap (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype) (mapDomain id x)

Tactic:
simpa [map_finsuppSum, mapDomain, map_sub, ← hX, sum_single_index, curryLinearEquiv,
    curryEquiv, Finsupp.uncurry, d₂₁, Y, Z, sum_mapRange_index,
    chains₁ToCoinvariantsKer, d₁₀, single_sum, mul_assoc, sub_add_eq_add_sub,
    sum_sum_index, add_smul, sub_sub_sub_eq, lsingle, singleAddHom] using add_comm _ _

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p q : R[X]
P : Ideal R
hpq : (p * q).contentIdeal ≤ P
hPprime : P.IsPrime
⊢ p.contentIdeal * q.contentIdeal ≤ P

Tactic:
hPprime.mul_le

Goal state after:
R : Type u_3
inst✝ : CommRing R
p q : R[X]
P : Ideal R
hpq : (p * q).contentIdeal ≤ P
hPprime : P.IsPrime
⊢ p.contentIdeal ≤ P ∨ q.contentIdeal ≤ P
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : R
⊢ a✝ ∈ ↑p.coeffs → a✝ ∈ ↑(span {p.content})

Tactic:
h1

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : R
h1 : a✝ ∈ ↑p.coeffs
⊢ a✝ ∈ ↑(span {p.content})
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case neg.mp
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✝ : ℕ
⊢ p.coeff x✝ ≠ 0 → 1 ≤ (v.intAdicAbv hb) (p.coeff x✝) → 1 ≤ p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)

Tactic:
h1

Goal state after:
case neg.mp
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
⊢ 1 ≤ (v.intAdicAbv hb) (p.coeff x✝) → 1 ≤ p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
p : Ideal R
hp : p ∈ (annihilator R M).minimalPrimes
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
q_prime : q.IsPrime
hq : Ideal.comap (algebraMap R Rₚ) q ∈ associatedPrimes R M
ann_le : annihilator R M ≤ Ideal.comap (algebraMap R Rₚ) q
⊢ Ideal.comap (algebraMap R Rₚ) q ≤ p

Tactic:
have := (IsLocalization.disjoint_under_iff p.primeCompl Rₚ q).mpr q_prime.ne_top

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
p : Ideal R
hp : p ∈ (annihilator R M).minimalPrimes
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this✝ : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
q_prime : q.IsPrime
hq : Ideal.comap (algebraMap R Rₚ) q ∈ associatedPrimes R M
ann_le : annihilator R M ≤ Ideal.comap (algebraMap R Rₚ) q
this : Disjoint ↑p.primeCompl ↑(Ideal.under R q)
⊢ Ideal.comap (algebraMap R Rₚ) q ≤ p
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: case zero
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.support R ↑N = PrimeSpectrum.zeroLocus ↑I
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < 0, Subsingleton (Ext N M i)
⊢ ∃ rs, rs.length = 0 ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs

Tactic:
have : Nontrivial M := (Submodule.nontrivial_iff R).mp (nontrivial_of_lt _ _ smul_lt)
    use []
    simp [isRegular_iff]

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
i : ℕ
hi : i + 1 < n + 1
⊢ Subsingleton (Ext N M (i + 1))

Tactic:
let g := (AddCommGrpCat.ofHom ((Ext.mk₀ (smulShortComplex M a).f).postcomp N
          (add_zero (i + 1))))

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
i : ℕ
hi : i + 1 < n + 1
g : AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex a).f).postcomp N ⋯)
⊢ Subsingleton (Ext N M (i + 1))
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.zero
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ (x * if k = 0 then 1 else 0) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
split_ifs

Goal state after:
case pos
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
h✝ : k = 0
⊢ x * 1 ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

case neg
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
h✝ : ¬k = 0
⊢ x * 0 ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y

Tactic:
rw [dpow_eq_of_mem (Ideal.add_mem I hx hy)]

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ (↑m !)⁻¹ʳ * (x + y) ^ m = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y
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
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y

Tactic:
rw [dpow_eq_of_mem (Ideal.add_mem I hx hy)]

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
⊢ (↑m !)⁻¹ʳ * (x + y) ^ m = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
m : ℕ
a x : A
hx : x ∈ I
⊢ (↑m !)⁻¹ʳ * (a * x) ^ m = a ^ m * dpow I m x

Tactic:
dpow_eq_of_mem hx,

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
m : ℕ
a x : A
hx : x ∈ I
⊢ (↑m !)⁻¹ʳ * (a * x) ^ m = a ^ m * ((↑m !)⁻¹ʳ * x ^ m)
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

Tactic:
dpow_eq_of_mem hx,

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ (↑m !)⁻¹ʳ * x ^ m * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ (↑m !)⁻¹ʳ * x ^ m * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

Tactic:
dpow_eq_of_mem hx,

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ (↑m !)⁻¹ʳ * x ^ m * ((↑k !)⁻¹ʳ * x ^ k) = ↑((m + k).choose m) * dpow I (m + k) x
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ (↑m !)⁻¹ʳ * x ^ m * ((↑k !)⁻¹ʳ * x ^ k) = ↑((m + k).choose m) * dpow I (m + k) x

Tactic:
dpow_eq_of_mem hx,

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ (↑m !)⁻¹ʳ * x ^ m * ((↑k !)⁻¹ʳ * x ^ k) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))
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 k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

Tactic:
dpow_eq_of_mem hx,

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 k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * x ^ m * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x
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 k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * x ^ m * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

Tactic:
dpow_eq_of_mem hx,

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 k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * x ^ m * ((↑k !)⁻¹ʳ * x ^ k) = ↑((m + k).choose m) * dpow I (m + k) x
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 k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * x ^ m * ((↑k !)⁻¹ʳ * x ^ k) = ↑((m + k).choose m) * dpow I (m + k) x

Tactic:
dpow_eq_of_mem hx,

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 k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * x ^ m * ((↑k !)⁻¹ʳ * x ^ k) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))
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)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ (↑m !)⁻¹ʳ * dpow I k x ^ m = ↑(m.uniformBell k) * ((↑(m * k)!)⁻¹ʳ * x ^ (m * k))

Tactic:
dpow_eq_of_mem hx,

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)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ * x ^ k) ^ m = ↑(m.uniformBell k) * ((↑(m * k)!)⁻¹ʳ * x ^ (m * k))
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 k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
⊢ (↑m !)⁻¹ʳ * dpow I k x ^ m = ↑(m.uniformBell k) * dpow I (m * k) x

Tactic:
dpow_eq_of_mem hx,

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 k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ * x ^ k) ^ m = ↑(m.uniformBell k) * dpow I (m * k) x
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 k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ * x ^ k) ^ m = ↑(m.uniformBell k) * dpow I (m * k) x

Tactic:
dpow_eq_of_mem hx,

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 k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ * x ^ k) ^ m = ↑(m.uniformBell k) * ((↑(m * k)!)⁻¹ʳ * x ^ (m * k))
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ ↑(if hx : x ∈ Ideal.span {↑p} then ⟨(↑n !)⁻¹ * ↑x ^ n, ⋯⟩ else 0) =
    if x ∈ Ideal.span {↑p} then (↑n !)⁻¹ * ↑x ^ n else 0

Tactic:
split_ifs

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h✝ : x ∈ Ideal.span {↑p}
⊢ ↑⟨(↑n !)⁻¹ * ↑x ^ n, ⋯⟩ = (↑n !)⁻¹ * ↑x ^ n

case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h✝ : x ∉ Ideal.span {↑p}
⊢ ↑0 = 0
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case inr.inr.inr
K : Type u_2
inst✝ : DivisionRing K
x y : K[ε]
hx : fst x ≠ 0
⊢ fst x * (inl ((fst x)⁻¹ * fst y)).fst = fst y ∨ fst y * (inl ((fst x)⁻¹ * fst y)).fst = fst x

Tactic:
simp [← mul_assoc, mul_inv_cancel₀ hx]

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: case zero
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑0
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
use R, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance
    let e : R ⊗[R] S ≃ₐ[R] S := TensorProduct.lid R S
    have : IsFiniteSplit R S := by
      rw [Nat.cast_zero, Module.rankAtStalk_eq_zero_iff_subsingleton] at hn
      exact of_subsingleton_top
    apply IsFiniteSplit.of_algEquiv e.symm

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
⊢ WeaklyEtale (ULift.{u₁, u_1} R) (ULift.{u₂, u_2} S) ↔ WeaklyEtale R S

Tactic:
rw [weaklyEtale_iff, weaklyEtale_iff, Module.Flat.ulift_left_iff, Module.Flat.ulift_right_iff]
  congr!
  conv_rhs => rw [← RingHom.Flat.ulift_iff.{u₁, u₂}]
  rw [TensorProduct.lmul'_ulift, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom]
  exact RingHom.Flat.comp_iff_of_bijective_right (Equiv.bijective _)

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

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] (S ⊗[R] S) :=
  (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S).trans (TensorProduct.assoc R R T T S S)
x✝ : S
⊢ ((AlgHom.restrictScalars R ((TensorProduct.lmul' T).comp TensorProduct.includeLeft)).comp TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            (((TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R)).comp ↑e).comp TensorProduct.includeLeft)).comp
        TensorProduct.includeRight)
      x✝

Tactic:
simp [e, TensorProduct.one_def]

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

Goal state before:
pp: case hb
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] (S ⊗[R] S) :=
  (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S).trans (TensorProduct.assoc R R T T S S)
x✝ : S
⊢ ((AlgHom.restrictScalars R ((AlgHom.restrictScalars T (TensorProduct.lmul' T)).comp TensorProduct.includeRight)).comp
        TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((AlgHom.restrictScalars T ((TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R)).comp ↑e)).comp
              TensorProduct.includeRight)).comp
        TensorProduct.includeRight)
      x✝

Tactic:
simp [e, TensorProduct.one_def]

Goal state after: