mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[G] →ₐc[R] R[H]
g₁ g₂ : G
⊢ f (single (g₁ * g₂) 1) = single (mapDomainOfBialgHomFun f g₁ * mapDomainOfBialgHomFun f g₂) 1

Tactic:
rw [← mul_one (1 : R), ← single_mul_single, ← single_mul_single, map_mul]

Goal state after:
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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[G] →ₐc[R] R[H]
g₁ g₂ : G
⊢ f (single g₁ 1) * f (single g₂ 1) = single (mapDomainOfBialgHomFun f g₁) 1 * single (mapDomainOfBialgHomFun f g₂) 1
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 : ℕ
x : ↑(ModuleCat.of k (G × G →₀ ↑A))
x✝ : x ∈ cycles₂ A
this :
  (ConcreteCategory.hom ((mapShortComplexH2 f φ).τ₂ ≫ (shortComplexH2 B).g)) x =
    (ConcreteCategory.hom ((shortComplexH2 A).g ≫ (mapShortComplexH2 f φ).τ₃)) x
⊢ (ModuleCat.Hom.hom (chainsMap₂ f φ)) x ∈ cycles₂ B

Tactic:
simp_all [cycles₂, shortComplexH2]

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

Goal state before:
pp: case insert
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
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∑ x_1, ∑ i ∈ s.sym (n - ↑x_1), dpow (↑x_1) (x a) * ∏ i_1 ∈ s, dpow (Multiset.count i_1 ↑i) (x i_1) =
    ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i)

Tactic:
sum_sigma',

Goal state after:
case insert
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
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∑ x_1 ∈ univ.sigma fun a ↦ s.sym (n - ↑a), dpow (↑x_1.fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑x_1.snd) (x i) =
    ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i)
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 • ⊤ < ⊤
ntrQ : Nontrivial (R ⧸ I)
suppQ : Module.support R (Shrink.{v, u} (R ⧸ I)) = PrimeSpectrum.zeroLocus ↑I
tfae_1_to_2 :
  (∀ (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)
tfae_2_to_3 :
  (∀ 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)
⊢ [∀ (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:
tfae_have 3 → 4 := fun ⟨N, _, _, h_supp, h_ext⟩ ↦
    exists_isRegular_of_exists_subsingleton_ext I n M smul_lt N h_supp h_ext

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)
suppQ : Module.support R (Shrink.{v, u} (R ⧸ I)) = PrimeSpectrum.zeroLocus ↑I
tfae_1_to_2 :
  (∀ (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)
tfae_2_to_3 :
  (∀ 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)
tfae_3_to_4 :
  (∃ 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
⊢ [∀ (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.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h1 : IsWeaklyRegular M [a, b]
h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥
⊢ IsWeaklyRegular M [b, a]

Tactic:
by
  rw [isWeaklyRegular_cons_iff, isWeaklyRegular_singleton_iff] at h1 ⊢
  obtain ⟨ha, hb⟩ := h1
  rw [← isSMulRegular_iff_torsionBy_eq_bot] at h2
  specialize h2 (le_antisymm ?_ (smul_le_self_of_tower a (torsionBy R M b)))
  · refine le_of_eq_of_le ?_ <| smul_top_inf_eq_smul_of_isSMulRegular_on_quot <|
      ha.of_injective _ <| ker_eq_bot.mp <| ker_liftQ_eq_bot' _ (lsmul R M b) rfl
    rw [← (isSMulRegular_on_quot_iff_lsmul_comap_eq _ _).mp hb]
    exact (inf_eq_right.mpr (ker_le_comap _)).symm
  · rwa [ha.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, inf_comm, smul_comm,
      ← h2.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, and_iff_left hb]

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
S : Set hI.SubDPIdeal
h : ⋃ i ∈ (fun J ↦ J.carrier) '' S, ↑i ⊆ ↑I
⊢ hI.IsSubDPIdeal (span (⋃ i ∈ (fun J ↦ J.carrier) '' S, ↑i))

Tactic:
span_isSubDPIdeal_iff h

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
h : ⋃ i ∈ (fun J ↦ J.carrier) '' S, ↑i ⊆ ↑I
⊢ ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ ⋃ i ∈ (fun J ↦ J.carrier) '' S, ↑i, hI.dpow n s ∈ span (⋃ i ∈ (fun J ↦ J.carrier) '' S, ↑i)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⨅ s ∈ insert ⊤ S, s.carrier = ⨅ x, I ⊓ ↑(⨅ (_ : x ∈ S), ⟨x.carrier, ⋯⟩)

Tactic:
iInf_insert,

Goal state after:
case refine_2
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⊤.carrier ⊓ ⨅ x ∈ S, x.carrier = ⨅ x, I ⊓ ↑(⨅ (_ : x ∈ S), ⟨x.carrier, ⋯⟩)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ (sInf S).carrier = I ⊓ sInf (val '' Set.range fun a ↦ ⨅ (_ : a ∈ S), ⟨a.carrier, ⋯⟩)

Tactic:
rw [sInf_carrier_def, sInf_image, iInf_range, inf_iInf, iInf_insert, inf_iInf]

Goal state after:
case refine_2
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⨅ x, ⊤.carrier ⊓ ⨅ (_ : x ∈ S), x.carrier = ⨅ x, I ⊓ ↑(⨅ (_ : x ∈ S), ⟨x.carrier, ⋯⟩)
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case inl
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsUnit a
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
lift a to K[ε]ˣ using ha
    exact ⟨a⁻¹ * b, by simp⟩

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
⊢ Q ≤ Ideal.comap φ Q

Tactic:
by
  intro x hx
  simp_all only [Ideal.mem_comap, ← Ideal.Quotient.eq_zero_iff_mem (I := Q), H.mk_apply,
    zero_pow_eq, ite_eq_right_iff, H.card_pos.ne', false_implies]

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
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ φ (ζ ^ j) - (ζ ^ j) ^ q ∈ Q

Tactic:
exact H _

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: case intro
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝¹ : Algebra.IsIntegral R S
this✝ : Q.IsMaximal
p : ℕ
hc : CharP (R ⧸ P) p
this : Finite (R ⧸ P)
val✝ : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card (R ⧸ P) = p ^ ↑k
⊢ ∃ σ, IsArithFrobAt R σ Q

Tactic:
have := CharP.of_ringHom_of_ne_zero (algebraMap (R ⧸ P) (S ⧸ Q)) p hp.ne_zero

Goal state after:
case intro
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝² : Algebra.IsIntegral R S
this✝¹ : Q.IsMaximal
p : ℕ
hc : CharP (R ⧸ P) p
this✝ : Finite (R ⧸ P)
val✝ : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card (R ⧸ P) = p ^ ↑k
this : CharP (S ⧸ Q) p
⊢ ∃ σ, IsArithFrobAt R σ Q
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
n : ℕ
⊢ (coeff n) ((1 - X) * mk 1) = (coeff n) 1

Tactic:
cases n with
  | zero => simp
  | succ n => simp [sub_mul]

Goal state after:
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [coeff_index_single_X]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x y : SummableFamily Γ R α
g : Γ
a : α
ha : (x a).coeff g + (y a).coeff g ≠ 0
⊢ a ∈ (Function.support fun a ↦ (x a).coeff g) ∪ Function.support fun a ↦ (y a).coeff g

Tactic:
rw [Set.mem_union, Function.mem_support, Function.mem_support]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x y : SummableFamily Γ R α
g : Γ
a : α
ha : (x a).coeff g + (y a).coeff g ≠ 0
⊢ (x a).coeff g ≠ 0 ∨ (y a).coeff g ≠ 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ (PowerSeries.coeff 1) F.Xzero = 1

Tactic:
PowerSeries.coeff,

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ (coeff (single () 1)) F.Xzero = 1
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ F.Xzero = PowerSeries.X

Tactic:
by
  have : Invertible (F.Xzero.coeff 1) := (coeff_one_Xzero F) ▸ invertibleOne
  calc
    _ = F.Xzero.substInv.subst (F.Xzero.subst F.Xzero) := by
      have aux₀ : PowerSeries.HasSubst F.Xzero :=
        PowerSeries.HasSubst.of_constantCoeff_zero' <| constantCoeff_Xzero F
      rw [← PowerSeries.subst_comp_subst_apply aux₀ aux₀, PowerSeries.subst_substInv_left _
        F.constantCoeff_Xzero , PowerSeries.subst_X aux₀, Xzero]
    _ = _ := by
      rw [Xzero_subst_Xzero, F.Xzero.subst_substInv_left F.constantCoeff_Xzero]

Goal state after:
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ (PowerSeries.coeff 1) F.zeroX = 1

Tactic:
PowerSeries.coeff,

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ (coeff (single () 1)) F.zeroX = 1
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : Invertible ((PowerSeries.coeff 1) F.zeroX)
⊢ PowerSeries.subst (PowerSeries.subst F.zeroX F.zeroX) F.zeroX.substInv = PowerSeries.X

Tactic:
zeroX_subst_zeroX,

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : Invertible ((PowerSeries.coeff 1) F.zeroX)
⊢ PowerSeries.subst F.zeroX F.zeroX.substInv = PowerSeries.X
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f g : R⟦ℕ⟧
n : ℕ
m : ℕ × ℕ
h : f.coeff m.1 * g.coeff m.2 ≠ 0
⊢ f.coeff m.1 ≠ 0 ∧ g.coeff m.2 ≠ 0 ∧ m.1 + m.2 = n ↔ m.1 + m.2 = n

Tactic:
and_iff_right (left_ne_zero_of_mul h),

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f g : R⟦ℕ⟧
n : ℕ
m : ℕ × ℕ
h : f.coeff m.1 * g.coeff m.2 ≠ 0
⊢ g.coeff m.2 ≠ 0 ∧ m.1 + m.2 = n ↔ m.1 + m.2 = n
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f g : R⟦σ →₀ ℕ⟧
n : σ →₀ ℕ
m : (σ →₀ ℕ) × (σ →₀ ℕ)
h : f.coeff m.1 * g.coeff m.2 ≠ 0
⊢ f.coeff m.1 ≠ 0 ∧ g.coeff m.2 ≠ 0 ∧ m.1 + m.2 = n ↔ m.1 + m.2 = n

Tactic:
and_iff_right (left_ne_zero_of_mul h),

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f g : R⟦σ →₀ ℕ⟧
n : σ →₀ ℕ
m : (σ →₀ ℕ) × (σ →₀ ℕ)
h : f.coeff m.1 * g.coeff m.2 ≠ 0
⊢ g.coeff m.2 ≠ 0 ∧ m.1 + m.2 = n ↔ m.1 + m.2 = n
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
⊢ (1 - x) * (powers x).hsum = 1

Tactic:
rw [← hsum_smul, sub_smul 1 x (powers x), one_smul, hsum_sub, ←
    hsum_embDomain (x • powers x) ⟨Nat.succ, Nat.succ_injective⟩, embDomain_succ_smul_powers hx]
  simp

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := x - (single x.order) x.leadingCoeff
hy : y = 0
⊢ 0 < (1 - (single oinv) r * x).orderTop

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
⊢ 0 < (1 - (single oinv) r * x).orderTop

Tactic:
· have hrx : (single oinv) r * x = 1 := by
      rw [eq_of_sub_eq_zero hy, single_mul_single, hxo, hr, single_zero_one]
    simp only [hrx, sub_self, orderTop_zero, WithTop.top_pos]

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
⊢ 0 < (1 - (single oinv) r * x).orderTop
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1.FG → Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype I_1))

Tactic:
intro J

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
J : Ideal R
⊢ J.FG → Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J))
Module: Mathlib.RingTheory.Spectrum.Prime.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ Subsingleton (LocalizedModule.Away f M) ↔ Disjoint (↑(PrimeSpectrum.basicOpen f)) (Module.support R M)

Tactic:
by
  rw [subsingleton_iff_support_subset, PrimeSpectrum.basicOpen_eq_zeroLocus_compl,
    disjoint_compl_left_iff]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
this✝ : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (algebraMap R Rₚ) p
this : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (algebraMap R[X] Rₚ[X]) P
a : R[X]
x✝ : a ∈ ↑(Submonoid.map C p.primeCompl)
ha : a ∈ ↑P
b : R
hb : b ∈ ↑p.primeCompl ∧ C b = a
⊢ b ∈ ↑p

Tactic:
rwa [SetLike.mem_coe, LiesOver.over (P := P) (p := p), mem_comap, algebraMap_eq, hb.2]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this✝ : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset
⊢ map (Quotient.mk I) p ∈ (map (Quotient.mk I) (span ↑o)).minimalPrimes

Tactic:
convert! hps

Goal state after:
case e'_4.e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := ⋯
this✝ : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := ⋯
e_2✝ : Quotient.commSemiring I = CommRing.toCommSemiring
⊢ map (Quotient.mk I) (span ↑o) = span ↑s
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
⊢ ∀ a ∈ s, ({I ∈ s | (I.colon Set.univ).radical = (a.colon Set.univ).radical}.inf id).IsPrimary

Tactic:
intro J

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
J : Submodule R M
⊢ J ∈ s → ({I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}.inf id).IsPrimary
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro.mk
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
⊢ eval (↑q) Φₙ ∣ ↑(card ↑(ConjClasses.mk x).carrier)

Tactic:
ConjClasses.card_carrier,

Goal state after:
case intro.mk
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
⊢ eval (↑q) Φₙ ∣ ↑(card Dˣ / card ↥(MulAction.stabilizer (ConjAct Dˣ) x))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
z : R⸨X⸩
h : order z < 0
⊢ (ofPowerSeries ℤ R) (PowerSeries.X ^ (order z).natAbs) = (single (-order z)) 1

Tactic:
rw [ofPowerSeries_X_pow, Int.ofNat_natAbs_of_nonpos]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
z : R⸨X⸩
h : order z < 0
⊢ order z ≤ 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
⊢ ∃ a, Valued.v a = n

Tactic:
· use ((HahnSeries.single (-WithZero.log n)) 1)
    simp [LaurentSeries.valuation_single_zpow, exp_log hn0]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2.refine_1
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
k : Fin m
hk : (fun x1 x2 ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
⊢ (if hi : k ∈ t then 1 else 0) = if hi : k ∈ Iic ⟨i, him⟩ then 1 else 0

Tactic:
have hki := mem_Iic.2 (hk.le.trans <| mem_Iic.1 hkm.1)
    rw [dif_pos hki, dif_pos]
    by_contra h
    exact lt_irrefl k <| ((lt_min'_iff _ _).1 hk) _ <| mem_sdiff.2 ⟨hki, h⟩

Goal state after:
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 →₀ ℕ := { 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

Tactic:
Finset.map_nontrivial

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
⊢ c.support.Nontrivial