mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case insert.e_a
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
n : ι → ℕ
m : M
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, dp R (n i) m = ↑(multinomial s✝ n) * dp R (s✝.sum n) m
⊢ ↑(multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) = ↑(multinomial (insert a✝ s✝) n)

Tactic:
multinomial_insert hi,

Goal state after:
case insert.e_a
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
n : ι → ℕ
m : M
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, dp R (n i) m = ↑(multinomial s✝ n) * dp R (s✝.sum n) m
⊢ ↑(multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) =
    ↑((n a✝ + ∑ i ∈ s✝, n i).choose (n a✝) * multinomial s✝ n)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ dpow n 0 = ↑(#(∅.sym n))

Tactic:
rw [dpow_eval_zero hn, eq_comm, ← cast_zero]
      apply congr_arg
      rw [card_eq_zero, sym_eq_empty]
      exact ⟨hn, rfl⟩

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 : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
⊢ [∀ (N : ModuleCat R),
        Nontrivial ↑N →
          Module.Finite R ↑N → Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I → ∀ i < n, Subsingleton (Ext N M i),
      ∀ i < n, Subsingleton (Ext (of R (Shrink.{v, u} (R ⧸ I))) M i),
      ∃ N,
        Nontrivial ↑N ∧
          Module.Finite R ↑N ∧ Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I ∧ ∀ i < n, Subsingleton (Ext N M i),
      ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs].TFAE

Tactic:
have ntrQ : Nontrivial (R ⧸ I) := by
    apply Submodule.Quotient.nontrivial_iff.mpr
    by_contra eq
    simp [eq] at smul_lt

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
ntrQ : Nontrivial (R ⧸ I)
⊢ [∀ (N : ModuleCat R),
        Nontrivial ↑N →
          Module.Finite R ↑N → Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I → ∀ i < n, Subsingleton (Ext N M i),
      ∀ i < n, Subsingleton (Ext (of R (Shrink.{v, u} (R ⧸ I))) M i),
      ∃ N,
        Nontrivial ↑N ∧
          Module.Finite R ↑N ∧ Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I ∧ ∀ i < n, Subsingleton (Ext N M i),
      ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs].TFAE
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case hdp
A : Type u_3
B : Type u_4
C : Type u_5
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
n : ℕ
a : A
ha : a ∈ ↑I
⊢ g (hJ.dpow n (f a)) = hK.dpow n (g (f a))

Tactic:
rw [← RingHom.comp_apply, hh.2 a ha, RingHom.comp_apply, hf.2 a ha]

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

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ ((↑k.1!)⁻¹ʳ * x ^ k.1 * if y ∈ I then (↑k.2!)⁻¹ʳ * y ^ k.2 else 0) = 0

Tactic:
if_pos 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
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ (↑k.1!)⁻¹ʳ * x ^ k.1 * ((↑k.2!)⁻¹ʳ * y ^ k.2) = 0
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 !)⁻¹ʳ * ((↑k !)⁻¹ʳ * x ^ m * x ^ k) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))

Tactic:
mul_assoc _ (x ^ m),

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 !)⁻¹ʳ * ((↑k !)⁻¹ʳ * (x ^ m * x ^ k)) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))
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✝ y✝ : A
hx : x✝ ∈ J
hy : y✝ ∈ J
⊢ (if x✝ + y✝ ∈ J then hI.dpow n✝ (x✝ + y✝) else 0) =
    ∑ x ∈ Finset.antidiagonal n✝, hI.dpow x.1 x✝ * if y✝ ∈ J then hI.dpow x.2 y✝ else 0

Tactic:
if_pos hy,

Goal state after:
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✝ y✝ : A
hx : x✝ ∈ J
hy : y✝ ∈ J
⊢ (if x✝ + y✝ ∈ J then hI.dpow n✝ (x✝ + y✝) else 0) = ∑ x ∈ Finset.antidiagonal n✝, hI.dpow x.1 x✝ * hI.dpow x.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 k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ * x ^ m * x ^ k) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))

Tactic:
mul_assoc _ (x ^ m),

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 !)⁻¹ʳ * ((↑k !)⁻¹ʳ * (x ^ m * x ^ k)) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))
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
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherian R M
rs rs' : List R
h1 : IsRegular M rs
h2 : rs ~ rs'
⊢ IsRegular M rs'

Tactic:
by
  obtain ⟨h3, h4⟩ := h1
  refine ⟨IsLocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdeal h3 h2 ?_, ?_⟩
  · intro x (h6 : x ∈ { r | r ∈ rs })
    refine IsLocalRing.le_maximalIdeal ?_ (Ideal.subset_span h6)
    exact h4 ∘ Eq.trans (top_smul _).symm ∘ Eq.symm ∘ congrArg (· • ⊤)
  · refine ne_of_ne_of_eq h4 (congrArg (Ideal.span · • ⊤) ?_)
    exact Set.ext fun _ => h2.mem_iff

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case inl
R : Type u_1
K : Type u_2
inst✝ : DivisionRing K
⊢ Submodule.IsPrincipal ⊥

Tactic:
exact bot_isPrincipal

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✝
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
h : Function.Surjective ⇑(algebraMap R P.Ring)
x : P.Cotangent
this : Subsingleton Ω[P.Ring⁄R]
⊢ x ∈ P.cotangentComplex.ker

Tactic:
exact Subsingleton.elim _ _

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
h : Infinite (R ⧸ Ideal.under R Q)
⊢ False

Tactic:
obtain rfl : Q = ⊤ := by simpa [Nat.card_eq_zero_of_infinite, ← Ideal.eq_top_iff_one] using H 0

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
H : φ.IsArithFrobAt ⊤
h : Infinite (R ⧸ Ideal.under R ⊤)
⊢ False
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : S
s : ↥Q.primeCompl
⊢ IsLocalization.mk' (Localization.AtPrime Q)
      (φ x * ↑(s ^ Nat.card (R ⧸ Ideal.under R Q)) - x ^ Nat.card (R ⧸ Ideal.under R Q) * ↑⟨φ ↑s, ⋯⟩)
      (⟨φ ↑s, ⋯⟩ * s ^ Nat.card (R ⧸ Ideal.under R Q)) ∈
    maximalIdeal (Localization.AtPrime Q)

Tactic:
IsLocalization.AtPrime.mk'_mem_maximal_iff (Localization.AtPrime Q) Q

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : S
s : ↥Q.primeCompl
⊢ φ x * ↑(s ^ Nat.card (R ⧸ Ideal.under R Q)) - x ^ Nat.card (R ⧸ Ideal.under R Q) * ↑⟨φ ↑s, ⋯⟩ ∈ Q
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
hn : n ≠ k
⊢ k • g ≠ n • g

Tactic:
contrapose hn
    apply (StrictMono.injective (nsmul_left_strictMono hg)) hn.symm

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g g' : Γ
hg : ∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g'
hg' : g' ∈ s.hsum.support
⊢ g ≤ g'

Tactic:
rw [mem_support, coeff_hsum_eq_sum] at hg'

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g g' : Γ
hg : ∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g'
hg' : ∑ i ∈ (s.coeff g').support, (s i).coeff g' ≠ 0
⊢ g ≤ g'
Module: Mathlib.RingTheory.HahnSeries.Cardinal

Goal state before:
pp: Γ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero S
x : R⟦Γ⟧
y : S⟦Γ⟧
h : x.support = y.support
⊢ x.cardSupp = y.cardSupp

Tactic:
cardSupp,

Goal state after:
Γ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero S
x : R⟦Γ⟧
y : S⟦Γ⟧
h : x.support = y.support
⊢ #↑x.support = #↑y.support
Module: Mathlib.RingTheory.HahnSeries.Cardinal

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ ((single a) r).cardSupp = 1

Tactic:
cardSupp,

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ #↑((single a) r).support = 1
Module: Mathlib.RingTheory.HahnSeries.Cardinal

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x : R⟦Γ⟧
a : Γ
r : R
⊢ (x * (single a) r).cardSupp ≤ x.cardSupp

Tactic:
by
  simpa using (cardSupp_mul_le ..).trans (mul_le_mul_right (cardSupp_single_le ..) _)

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
⊢ ⇑(powers x) = HPow.hPow x

Tactic:
ext1 n
  simp [hx]

Goal state after:
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
⊢ SpecializingMap (PrimeSpectrum.comap (algebraMap R S) ∘ PrimeSpectrum.comap (algebraMap S T))

Tactic:
apply SpecializingMap.comp

Goal state after:
case hf
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
⊢ SpecializingMap (PrimeSpectrum.comap (algebraMap S T))

case hg
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
⊢ SpecializingMap (PrimeSpectrum.comap (algebraMap R S))
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : n = 0
h1 : 1 = Fin.last p.length
⊢ x ∈ (p.toFun 1).asIdeal ∧ n + 1 = p.length ∧ RelSeries.head p = RelSeries.head p ∧ RelSeries.last p = RelSeries.last p

Tactic:
simpa [h1, hp] using! hx

Goal state after:
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
inst✝² : IsInvariant A B G
P Q : Ideal B
inst✝¹ : P.IsPrime
inst✝ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
N N' : OpenNormalSubgroup G
f : N ⟶ N'
h : B' ↥↑N'.toOpenSubgroup ≤ B' ↥↑N.toOpenSubgroup
x : G
hx : Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) Q = ↑x • Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) P
⊢ Ideal.under (↥(B' ↥↑N'.toOpenSubgroup)) Q =
    (QuotientGroup.map (↑N.toOpenSubgroup) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑⟨↑x, hx⟩ •
      Ideal.under (↥(B' ↥↑N'.toOpenSubgroup)) P

Tactic:
simpa only [Ideal.comap_comap, Ideal.pointwise_smul_eq_comap, ← Ideal.comap_coe
        (F := RingEquiv _ _)] using! congr(Ideal.comap (Subalgebra.inclusion h).toRingHom $hx)

Goal state after:
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → CommRing (S i)
inst✝² : (i : ι) → Algebra R (S i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsLocalIso R (S i)
this✝ : (i : ι) → Algebra ((i : ι) → S i) (S i) := ⋯
this : ∀ (i : ι), IsLocalization.Away (Pi.single i 1) (S i)
⊢ Ideal.span (Set.range fun i ↦ Pi.single i 1) = ⊤

Tactic:
exact Ideal.span_single_eq_top _

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
X : ModuleCat R
proj : Projective X
this : Small.{v, u} (Localization S)
⊢ Projective ((localizedModuleFunctor S).obj X)

Tactic:
rw [← IsProjective.iff_projective] at proj ⊢

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
X : ModuleCat R
proj : Module.Projective R ↑X
this : Small.{v, u} (Localization S)
⊢ Module.Projective (Localization S) ↑((localizedModuleFunctor S).1 X)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x = 0 → x.powerSeriesPart = 0

Tactic:
rintro rfl
    simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : MvPolynomial n R
i : n
hf0 : f ≠ 0
hif : i ∉ f.vars
hig : i ∉ g.vars
h : IsRelPrime f g
S : Type (max u_4 u_3) := MvPolynomial { j // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  (renameEquiv R (Equiv.optionSubtypeNe i).symm).trans (optionEquivLeft R { b // b ≠ i })
he : (↑e.symm).comp Polynomial.CAlgHom = rename Subtype.val
⊢ Irreducible (f * X i + g)

Tactic:
obtain ⟨f, rfl⟩ : f ∈ (e.symm.toAlgHom.comp Polynomial.CAlgHom).range :=
    he ▸ exists_rename_eq_of_vars_subset_range _ _ Subtype.val_injective (by simpa [Set.subset_def])

Goal state after:
n : Type u_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : MvPolynomial n R
i : n
hig : i ∉ g.vars
S : Type (max u_4 u_3) := MvPolynomial { j // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  (renameEquiv R (Equiv.optionSubtypeNe i).symm).trans (optionEquivLeft R { b // b ≠ i })
he : (↑e.symm).comp Polynomial.CAlgHom = rename Subtype.val
f : S
hf0 : ((↑e.symm).comp Polynomial.CAlgHom).toRingHom f ≠ 0
hif : i ∉ (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f).vars
h : IsRelPrime (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f) g
⊢ Irreducible (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f * X i + g)
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case nontrivial
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := ⋯
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ (sumSMulXSMulY c).support.Nontrivial

Tactic:
hsupp,

Goal state after:
case nontrivial
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ (Finset.map ι c.support).Nontrivial
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case disjoint
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := ⋯
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ (↑(sumSMulXSMulY c).support).PairwiseDisjoint Finsupp.support

Tactic:
hsupp,

Goal state after:
case disjoint
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ (↑(Finset.map ι c.support)).PairwiseDisjoint Finsupp.support
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case disjoint
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := ⋯
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ (↑(sumSMulXSMulY c).support).PairwiseDisjoint Finsupp.support

Tactic:
rw [hsupp, Finset.coe_map, ι.injective.injOn.pairwiseDisjoint_image]

Goal state after:
case disjoint
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ (↑c.support).PairwiseDisjoint (Finsupp.support ∘ ⇑ι)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ

Tactic:
obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (Int.neg_nonpos_of_nonneg ord_nonpos)

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
⊢ (coeff m) φ * (coeff (p • m)) ((monomial (p • m)) 1) = (coeff m) φ

Tactic:
coeff_monomial,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
⊢ ((coeff m) φ * if p • m = p • m then 1 else 0) = (coeff m) φ
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
d : σ →₀ ℕ
hd : d ≠ m
⊢ (coeff d) φ * (coeff (p • m)) ((monomial (p • d)) 1) = 0

Tactic:
coeff_monomial,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
d : σ →₀ ℕ
hd : d ≠ m
⊢ ((coeff d) φ * if p • m = p • d then 1 else 0) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : (coeff m) ((expand p hp) φ) ≠ 0
⊢ p ∣ m i

Tactic:
simp only [expand, substAlgHom_apply, coeff_subst (HasSubst.X_pow hp)] at h

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ∑ᶠ (d : σ →₀ ℕ), (coeff d) φ • (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) ≠ 0
⊢ p ∣ m i
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: case e_a
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : ↑M
i : ι
this✝ : Module R ↑M := Module.compHom (↑M) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) ↑M
i1 j1 : ι
⊢ (single j i 1 * x) i1 j1 = (∑ i_1, x i i_1 • single j i_1 1) i1 j1

Tactic:
simp only [mul_apply, smul_single, smul_eq_mul, mul_one, sum_apply]

Goal state after:
case e_a
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : ↑M
i : ι
this✝ : Module R ↑M := Module.compHom (↑M) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) ↑M
i1 j1 : ι
⊢ ∑ j_1, single j i 1 i1 j_1 * x j_1 j1 = ∑ c, single j c (x i c) i1 j1