mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G → ↑A
g : G × G
⊢ (A.ρ g.1) ((r • x) g.2) - (r • x) (g.1 * g.2) + (r • x) g.1 =
    ((RingHom.id k) r • fun g ↦ (A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1) g

Tactic:
dsimp; rw [map_smul, smul_add, smul_sub]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
x : σ →₀ ℕ
r : R
h : r ≠ 0
⊢ (monomial x) r ∈ idealOfVars σ R ^ n ↔ n ≤ degree x

Tactic:
grind only [mem_pow_idealOfVars_iff, mem_support_iff, coeff_monomial]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
hzero : 0 ∉ closure {r | Prime r}
⊢ span {a} ∉ kaplanskySet (closure {r | Prime r}).toSubsemigroup

Tactic:
intro h

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
hzero : 0 ∉ closure {r | Prime r}
h : span {a} ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : span {a} ∉ kaplanskySet (closure {r | Prime r}).toSubsemigroup
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a

Tactic:
mem_kaplanskySet_iff

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬↑(span {a}) ∩ ↑(closure {r | Prime r}).toSubsemigroup = ∅
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case refine_2
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
⊢ ∀ x ∈ ⋯.toFinset \ Set.Finite.toFinset ⋯, (coeff x) p = 0

pp: case refine_3
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
x : σ →₀ ℕ
hx : x ∈ Set.Finite.toFinset ⋯
⊢ (coeff x) p • (coeff n) (x.prod fun s e ↦ (X ∘ f) s ^ e) = (coeff x) p

Tactic:
· simp +contextual [← monomial_mapDomain_apply_one]

Goal state after:
case refine_3
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
x : σ →₀ ℕ
hx : x ∈ Set.Finite.toFinset ⋯
⊢ (coeff x) p • (coeff n) (x.prod fun s e ↦ (X ∘ f) s ^ e) = (coeff x) p
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case neg.mpr
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.coeffs, (v.intAdicAbv hb) x < 1) → (p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)) < 1

Tactic:
intro h

Goal state after:
case neg.mpr
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
h : ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1
⊢ (p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)) < 1
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case convert_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
b : NNReal
hb : 1 < b
p : R[X]
hR : ¬IsField R
⊢ p.contentIdeal = ⊤ ↔ ∀ (x : HeightOneSpectrum R), 1 ≤ gaussNorm (x.intAdicAbv hb) 1 p

Tactic:
simp [← not_iff_not, gaussNorm_lt_one_iff_contentIdeal_le, ideal_ne_top_iff_exists hR]

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

Goal state before:
pp: case cons
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
h : f.comp ((toAddMonoidEnd R M) r) = AddMonoidHom.comp ((toAddMonoidEnd S M₂) s) f
⊢ AddSubgroup.map ((toAddMonoidEnd S M₂) s) (AddSubgroup.map f ⊤) ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup =
    AddSubgroup.map ((toAddMonoidEnd S M₂) s) ⊤ ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup

Tactic:
map_top_of_surjective f hf

Goal state after:
case cons
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
h : f.comp ((toAddMonoidEnd R M) r) = AddMonoidHom.comp ((toAddMonoidEnd S M₂) s) f
⊢ AddSubgroup.map ((toAddMonoidEnd S M₂) s) ⊤ ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup =
    AddSubgroup.map ((toAddMonoidEnd S M₂) s) ⊤ ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
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
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
n : ℕ
m : M
⊢ (lift hI g hg) (dp R n m) = hI.dpow n (g m)

Tactic:
rw [lift, lift'_apply_dp]

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

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec : s.Nonempty → (∀ i ∈ s, r i ∈ I) → hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
⊢ r a ^ n * hI.dpow n (∏ x ∈ s, r x) = n ! ^ (#(insert a s) - 1) • ∏ i ∈ insert a s, hI.dpow n (r i)

Tactic:
simp only [Finset.card_insert_of_notMem has, add_tsub_cancel_right, nsmul_eq_mul,
          Nat.cast_pow, Finset.prod_insert has,
          hrec h (fun i hi ↦ hs' i (mem_insert_of_mem hi)), ← mul_assoc]

Goal state after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec : s.Nonempty → (∀ i ∈ s, r i ∈ I) → hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
⊢ r a ^ n * ↑n ! ^ (#s - 1) * ∏ i ∈ s, hI.dpow n (r i) = ↑n ! ^ #s * hI.dpow n (r a) * ∏ i ∈ s, hI.dpow n (r i)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
⊢ Ideal.map e.symm (Ideal.map e I) = I

Tactic:
exact I.map_of_equiv e

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
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
n✝ : ℕ
x✝ : A
hx : x✝ ∉ J
⊢ (if x✝ ∈ J then hI.dpow n✝ x✝ else 0) = 0

Tactic:
by simp [if_neg hx]

Goal state after:
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)!
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
⊢ dpow I m (dpow I k x) = ↑(m.uniformBell k) * dpow I (m * k) x

Tactic:
by
  by_cases! hmk : m * k < n
  · exact dpow_comp_of_mul_lt hn_fac hk hmk hx
  · have hxmk : x ^ (m * k) = 0 := Ideal.pow_eq_zero_of_mem hnI hmk hx
    rw [dpow_eq_of_mem (dpow_mem hk hx), dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_pow, ← pow_mul, ← mul_assoc, mul_comm k, hxmk, mul_zero, mul_zero, mul_zero]

Goal state after:
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
rs : List R
h✝ : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K := torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ rs₀ : List R
h₁₂ : rs₁ ~ rs₂
H₁ : rs₀ ++ rs₁ <+~ rs
H₃ : rs₀ ++ rs₂ <+~ rs
h : IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) rs₁
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) rs₂

Tactic:
{
  induction h₁₂ generalizing rs₀ with
  | nil => exact .nil R _
  | cons r _ ih =>
    let e := quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
    rw [isWeaklyRegular_cons_iff, ← e.isWeaklyRegular_congr] at h ⊢
    refine h.imp_right (ih (r :: rs₀) ?_ ?_) <;>
      exact List.perm_middle.subperm_right.mp ‹_›
  | swap a b t =>
    rw [show ∀ x y z, x :: y :: z = [x, y] ++ z from fun _ _ _ => rfl,
      isWeaklyRegular_append_iff] at h ⊢
    have : Ideal.ofList [b, a] = Ideal.ofList [a, b] :=
      congrArg Ideal.span <| Set.ext fun _ => (List.Perm.swap a b []).mem_iff
    rw [(quotEquivOfEq _ _ (congrArg₂ _ this rfl)).isWeaklyRegular_congr] at h
    rw [List.append_cons, List.append_cons, List.append_assoc _ [b] [a]] at H₁
    apply (List.sublist_append_left (rs₀ ++ [b, a]) _).subperm.trans at H₁
    apply List.perm_append_comm.subperm.trans at H₁
    exact h.imp_left (swap · (h' b a rs₀ H₁))
  | trans h₁₂ _ ih₁₂ ih₂₃ =>
    have H₂ := (h₁₂.append_left rs₀).subperm_right.mp H₁
    exact ih₂₃ rs₀ H₂ H₃ (ih₁₂ rs₀ H₁ H₂ h) }

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⨆ a ∈ S, ↑a = ⨆ i, ↑(⨆ (_ : i ∈ S), ⟨i.carrier, ⋯⟩)

Tactic:
have (J : hI.SubDPIdeal) :
      ((⨆ (_ : J ∈ S), (J : Set.Iic I) : Set.Iic I) : Ideal A) = ⨆ (_ : J ∈ S), (J : Ideal A) := by
      by_cases hJ : J ∈ S
      · simp [ciSup_pos hJ]
      · simp [hJ, not_false_eq_true, iSup_neg, Set.Iic.coe_bot]

Goal state after:
case refine_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
this : ∀ (J : hI.SubDPIdeal), ↑(⨆ (_ : J ∈ S), ⟨J.carrier, ⋯⟩) = ⨆ (_ : J ∈ S), ↑⟨J.carrier, ⋯⟩
⊢ ⨆ a ∈ S, ↑a = ⨆ i, ↑(⨆ (_ : i ∈ S), ⟨i.carrier, ⋯⟩)
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
⊢ (Ideal.span {ε}).IsMaximal

Tactic:
refine ⟨?_, fun I hI ↦ ?_⟩
  · simp [ne_eq, Ideal.eq_top_iff_one, Ideal.mem_span_singleton', TrivSqZeroExt.ext_iff]
  · rcases ideal_trichotomy I with rfl | rfl | rfl <;>
    first | simp at hI | simp

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

Goal state before:
pp: case inl
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal :=
  { carrier := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}, isSubideal := ⋯, dpow_mem := ⋯ }
⊢ S ⊆ ↑⊤

pp: case inr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal :=
  { carrier := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}, isSubideal := ⋯, dpow_mem := ⋯ }
K : hI.SubDPIdeal
hKS : S ⊆ ↑K.carrier
⊢ S ⊆ ↑K

Tactic:
exacts [hS, hKS]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a b : A
ha : a ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
hb : b ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
n : ℕ
⊢ ∑ k ∈ Finset.antidiagonal n, hI.dpow k.1 a * hI.dpow k.2 b = hI'.dpow n (a + b)

Tactic:
hI'.dpow_add ha.1 hb.1

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a b : A
ha : a ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
hb : b ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
n : ℕ
⊢ ∑ k ∈ Finset.antidiagonal n, hI.dpow k.1 a * hI.dpow k.2 b =
    ∑ k ∈ Finset.antidiagonal n, hI'.dpow k.1 a * hI'.dpow k.2 b
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
s : SummableFamily Γ R α
g : Γ
⊢ (∀ (x : α), (s x).coeff g = 0) → ∑ᶠ (i : α), (s i).coeff g = 0

Tactic:
intro h

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
s : SummableFamily Γ R α
g : Γ
h : ∀ (x : α), (s x).coeff g = 0
⊢ ∑ᶠ (i : α), (s i).coeff g = 0
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
⊢ (coeff n) f * ((powers x) n).coeff 0 = 0

Tactic:
refine mul_eq_zero_of_right (coeff n f) (coeff_eq_zero_of_lt_orderTop ?_)

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
⊢ ↑0 < ((powers x) n).orderTop
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✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
x✝³ x✝² : R⟦Γ⟧
x✝¹ : SummableFamily Γ' V α
x✝ : α
⊢ ((x✝³ * x✝²) • x✝¹) x✝ = (x✝³ • x✝² • x✝¹) x✝

Tactic:
simp [HahnModule.instModule.mul_smul]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
⊢ (sum fun a ↦ ((SummableFamily.powers x) a).cardSupp) ≤ sum fun n ↦ x.cardSupp ^ n

Tactic:
sum_le_sum

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
⊢ sum ?g ≤ sum fun n ↦ x.cardSupp ^ n

case g
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
⊢ ℕ → Cardinal.{u_1}

case H
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
⊢ ∀ (i : ℕ), ((SummableFamily.powers x) i).cardSupp ≤ ?g i
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv (antipode R) * toConv LinearMap.id).ofConv ∘ₗ f.toLinearMap =
    (toConv (f.toLinearMap ∘ₗ antipode R) * toConv f.toLinearMap).ofConv

Tactic:
rw [convMul_comp_coalgHom_distrib, hS]

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv (f.toLinearMap ∘ₗ antipode R) * toConv ((toConv LinearMap.id).ofConv ∘ₗ f.toLinearMap)).ofConv =
    (toConv (f.toLinearMap ∘ₗ antipode R) * toConv f.toLinearMap).ofConv
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ HasGoingUp R S → SpecializingMap (PrimeSpectrum.comap (algebraMap R S))

Tactic:
intro h

Goal state after:
case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : HasGoingUp R S
⊢ SpecializingMap (PrimeSpectrum.comap (algebraMap R S))
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv LinearMap.id * toConv (antipode R)).ofConv ∘ₗ f.toLinearMap =
    (toConv f.toLinearMap * toConv (f.toLinearMap ∘ₗ antipode R)).ofConv

Tactic:
rw [convMul_comp_coalgHom_distrib, hS]

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv ((toConv LinearMap.id).ofConv ∘ₗ f.toLinearMap) * toConv (f.toLinearMap ∘ₗ antipode R)).ofConv =
    (toConv f.toLinearMap * toConv (f.toLinearMap ∘ₗ antipode R)).ofConv
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a (derivative f)) * (b - a) = 0
this : c * (b - a) + Polynomial.eval a (derivative f) ∈ maximalIdeal R
⊢ False

Tactic:
replace this := (maximalIdeal R).add_mem this ((maximalIdeal R).mul_mem_left c h)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a (derivative f)) * (b - a) = 0
this : c * (b - a) + Polynomial.eval a (derivative f) + c * (a - b) ∈ maximalIdeal R
⊢ False
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
⊢ F.IsTorsionQuot (L ⊓ K) K → F.IsTorsionQuot L K

Tactic:
intro h

Goal state after:
case mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot (L ⊓ K) K
⊢ F.IsTorsionQuot L K
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
⊢ F.IsTorsionQuot L K → F.IsTorsionQuot (L ⊓ K) K

Tactic:
intro h

Goal state after:
case mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot L K
⊢ F.IsTorsionQuot (L ⊓ K) K
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝³ : p.IsPrime
this✝² : (map f p).IsPrime
h : (map f p).height ≤ 1
h_lt : map f q < map f p
this✝¹ : (map f q).IsPrime
this✝ : (map f p).FiniteHeight
this : (map f q).height = 0
⊢ q ∈ (span t).minimalPrimes

Tactic:
height_eq_zero_iff

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝³ : p.IsPrime
this✝² : (map f p).IsPrime
h : (map f p).height ≤ 1
h_lt : map f q < map f p
this✝¹ : (map f q).IsPrime
this✝ : (map f p).FiniteHeight
this : map f q ∈ minimalPrimes (R ⧸ span t)
⊢ q ∈ (span t).minimalPrimes
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
⊢ (Hom.hom P.toLimit).ker = ⊥

Tactic:
Subgroup.eq_bot_iff_forall

Goal state after:
P : ProfiniteGrp.{u}
⊢ ∀ x ∈ (Hom.hom P.toLimit).ker, x = 1
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ∞
⊢ p.height ≤ n → ∃ I, p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ ↑n

Tactic:
intro h

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ∞
h : p.height ≤ n
⊢ ∃ I, p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ ↑n
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
q : LTSeries ↑(support R M)
⊢ ∃ p, q.length ≤ p.length ∧ (↑(RelSeries.last p)).asIdeal.IsMaximal

Tactic:
by
  obtain ⟨m, hmm, hm⟩ := exists_le_maximal _ q.last.1.2.1
  obtain hlt | rfl := lt_or_eq_of_le hm
  · use q.snoc ⟨⟨m, inferInstance⟩, mem_support_mono hm q.last.2⟩ hlt
    simpa
  · use q

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
this : (RelSeries.head l').asIdeal.LiesOver (RelSeries.last lp).asIdeal
lp' : LTSeries (PrimeSpectrum S)
hlp'len : lp'.length = lp.length
hlp' : RelSeries.last lp' = { asIdeal := (RelSeries.head l').asIdeal, isPrime := ⋯ }
right✝ : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList lp') = RelSeries.toList lp
⊢ (RelSeries.smash lp' l' hlp').length = lp.length + lq.length

Tactic:
simp [hlp'len, l']

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

Goal state before:
pp: case nil
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsNoetherianRing R
inst✝³ : IsLocalRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
reg : Sequence.IsRegular M []
⊢ supportDim R (M ⧸ ⊥ • ⊤) + ↑[].length = supportDim R M

Tactic:
Submodule.bot_smul

Goal state after:
case nil
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsNoetherianRing R
inst✝³ : IsLocalRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
reg : Sequence.IsRegular M []
⊢ supportDim R (M ⧸ ⊥) + ↑[].length = supportDim R M