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
f : G → ↑A
⊢ (∀ (x : G × G), (A.ρ x.1) (f x.2) - f (x.1 * x.2) + f x.1 = 0 x) ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0

Tactic:
Prod.forall

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G → ↑A
⊢ (∀ (a b : G), (A.ρ a) (f b) - f (a * b) + f a = 0 (a, b)) ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A
⊢ (∀ (x : G × G × G), (A.ρ x.1) (f x.2) - f (x.1 * x.2.1, x.2.2) + f (x.1, x.2.1 * x.2.2) - f (x.1, x.2.1) = 0 x) ↔
    ∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0

Tactic:
Prod.forall

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A
⊢ (∀ (a a_1 b : G), (A.ρ a) (f (a_1, b)) - f (a * a_1, b) + f (a, a_1 * b) - f (a, a_1) = 0 (a, a_1, b)) ↔
    ∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
⊢ (ConcreteCategory.hom ((inhomogeneousChains X.X₃).d 1 0)) ((ConcreteCategory.hom (chainsIso₁ X.X₃).inv) ↑z) = 0

Tactic:
by
    rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]; simp

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

Goal state before:
pp: case h.refine_4
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
⊢ ⇑x -
      ⇑((ConcreteCategory.hom (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S))))
          ⟨fun g ↦ Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯, ⋯⟩) ∈
    coboundaries₁ A

Tactic:
use y

Goal state after:
case h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
⊢ (ModuleCat.Hom.hom (d₀₁ A)) y =
    ⇑x -
      ⇑((ConcreteCategory.hom (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S))))
          ⟨fun g ↦ Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯, ⋯⟩)
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
h : r = 0
⊢ C r ∈ idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0

Tactic:
simp [h]

Goal state after:
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I | ¬I.FG}
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span ↑G = sSup C
J : Ideal R
J_mem_C : J ∈ C
G_subset_J : ↑G ⊆ ↑J
⊢ sSup C ∈ C

Tactic:
suffices J_eq_sSup : J = sSup C from J_eq_sSup ▸ J_mem_C

Goal state after:
R : Type u_1
inst✝ : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I | ¬I.FG}
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span ↑G = sSup C
J : Ideal R
J_mem_C : J ∈ C
G_subset_J : ↑G ⊆ ↑J
⊢ J = sSup C
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
⊢ IsBoundary₀ G a ↔ ∃ x, (x.sum fun g z ↦ g • z - z) = a

Tactic:
constructor
  · rintro ⟨x, hx⟩
    use x.sum (fun g a => single g (-(g⁻¹ • a)))
    simp_all [sum_neg_index, sum_sum_index, neg_add_eq_sub]
  · rintro ⟨x, hx⟩
    use x.sum (fun g a => single g (-(g • a)))
    simp_all [sum_neg_index, sum_sum_index, neg_add_eq_sub]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : span S = Ideal.map constantCoeff I
⊢ I = span (insert X (⇑C '' S))

Tactic:
rw [Ideal.span_insert, ← Ideal.map_span, hSI, Ideal.map_map]
  refine le_antisymm ?_ (by simp [Ideal.span_le, hXI, map_constantCoeff_le_self_of_X_mem])
  exact fun f hf ↦ mem_span_singleton_sup.mpr
    ⟨_, _, mem_map_of_mem _ hf, f.eq_shift_mul_X_add_const.symm⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I) + 1

Tactic:
by_cases hfg : I.FG

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : I.FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I) + 1

case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : ¬I.FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I) + 1
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : I.FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I) + 1

pp: case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : ¬I.FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I) + 1

Tactic:
swap

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : ¬I.FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I) + 1

case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : I.FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I) + 1
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
⊢ Ideal.map constantCoeff I ≤ Ideal.map constantCoeff (span T)

Tactic:
rw [map_le_iff_le_comap]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
⊢ I ≤ comap constantCoeff (Ideal.map constantCoeff (span T))
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ π A 1 ≫ (H1Iso A).hom = (isoCycles₁ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.π

Tactic:
simp [H1Iso, isoCycles₁, π, HomologicalComplex.homologyπ, leftHomologyπ]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
hfg : I.FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I)

pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
hfg : I.FG
⊢ spanFinrank (Ideal.map constantCoeff I) ≤ spanFinrank I

Tactic:
swap

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
hfg : I.FG
⊢ spanFinrank (Ideal.map constantCoeff I) ≤ spanFinrank I

case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
hfg : I.FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I)
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : P.FG
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : ¬P.FG
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1

Tactic:
swap

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : ¬P.FG
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1

case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : P.FG
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
hn : 0 < 0
⊢ ↑((J ^ 0) ^ m) ⊆ ↑(J ^ m)

Tactic:
exfalso
      exact Nat.not_succ_le_zero 0 hn

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ b ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x,
    ∃ a, ∃ (_ : a ∈ antidiagonal (optionElim k x)), ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩ = b

Tactic:
rintro ⟨⟨m, n⟩, ⟨u, v⟩⟩ h

Goal state after:
case refine_3
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
⊢ ∃ a, ∃ (_ : a ∈ antidiagonal (optionElim k x)), ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩ = ⟨(m, n), (u, v)⟩
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
h : n = 0
⊢ MvPolynomial.idealOfVars σ R ^ n = ⊤

Tactic:
simp [h]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
inj : Function.Injective ⇑f
m : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
m' : ↥(maximalIdeal (AdicCompletion (maximalIdeal R) R))
hm' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).toCotangent m' = m
l : R
hl : Submodule.Quotient.mk l = ↑↑m' 2
lmem : l ∈ maximalIdeal R
⊢ (algebraMap R (AdicCompletion (maximalIdeal R) R)) l - ↑m' ∈ maximalIdeal (AdicCompletion (maximalIdeal R) R) ^ 2

Tactic:
change (of (maximalIdeal R) R l) - m' ∈ _

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
inj : Function.Injective ⇑f
m : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
m' : ↥(maximalIdeal (AdicCompletion (maximalIdeal R) R))
hm' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).toCotangent m' = m
l : R
hl : Submodule.Quotient.mk l = ↑↑m' 2
lmem : l ∈ maximalIdeal R
⊢ (of (maximalIdeal R) R) l - ↑m' ∈ maximalIdeal (AdicCompletion (maximalIdeal R) R) ^ 2
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
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
⊢ mapDomain (s ∘ QuotientGroup.mk) v = 0

Tactic:
mapDomain_comp

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
⊢ mapDomain s (mapDomain QuotientGroup.mk v) = 0
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
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
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ y ∈ s, y ≠ x → c y = 0
⊢ False

Tactic:
have hcxa : d = c x := mul_left_injective₀ hcx (by simpa using (key (x, x) (by simp [*])))

Goal state after:
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
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
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ y ∈ s, y ≠ x → c y = 0
hcxa : d = c x
⊢ False
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
h : p = 0
⊢ ∀ x ∈ ↑p.coeffs, x = 0

Tactic:
simp [h]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.coeff n ∈ p.contentIdeal

Tactic:
simp [h]

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 ≤ P ∨ q.contentIdeal ≤ P

Tactic:
rw [← Ideal.mk_ker (I := P)] at hpq ⊢

Goal state after:
R : Type u_3
inst✝ : CommRing R
p q : R[X]
P : Ideal R
hpq : (p * q).contentIdeal ≤ RingHom.ker (Ideal.Quotient.mk P)
hPprime : P.IsPrime
⊢ p.contentIdeal ≤ RingHom.ker (Ideal.Quotient.mk P) ∨ q.contentIdeal ≤ RingHom.ker (Ideal.Quotient.mk P)
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
G : Type u_5
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
g : G
⊢ comul (single g 1) = single g 1 ⊗ₜ[R] single g 1

Tactic:
simp [Algebra.TensorProduct.one_def]

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case h
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
e : ↥T → ℕ
g : ↥T → ↥S
hg : ∀ (a : ↥T), g a • ↑a ^ e a • m = 0
a : R
ha : a ∈ ↑T
u : ↥S
hu : ∏ a, g a = g ⟨a, ha⟩ * u
⊢ ↑u • ↑(g ⟨a, ha⟩) • a ^ e ⟨a, ha⟩ • m = 0

Tactic:
exact smul_eq_zero_of_right u.1 (hg ⟨a, ha⟩)

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

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
⊢ False

Tactic:
let _ := pass.isPrime

Goal state after:
case inr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝ : p.IsPrime := IsAssociatedPrime.isPrime pass
⊢ False
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n✝ : ℕ
x✝ y✝ : A
ha : x✝ ∈ ⊥
hb : y✝ ∈ ⊥
h : n✝ = 0
⊢ 1 = ∑ x ∈ antidiagonal n✝, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0

Tactic:
simp [h]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
⊢ ‖dpow' p n ↑x‖ ≤ 1

Tactic:
unfold dpow'
  by_cases hn : n = 0
  · simp [hn]
  · apply le_trans (dpow'_norm_le_of_ne_zero p hn hx)
    rw [← zpow_neg_one, ← zpow_zero ↑p]
    gcongr
    · exact_mod_cast Nat.Prime.one_le hp.elim
    · norm_num

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 A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
⊢ hI.dpow k z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
let J := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
⊢ hI.dpow k z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
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 A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
y : A
m : ℕ
hm : m ≠ 0
x : A
hxS : x ∈ S
hxy : y = hI.dpow m x
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n (hI.dpow m x) ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
hI.dpow_comp hm (hS hxS)

Goal state after:
case refine_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
y : A
m : ℕ
hm : m ≠ 0
x : A
hxS : x ∈ S
hxy : y = hI.dpow m x
n : ℕ
hn : n ≠ 0
⊢ ↑(n.uniformBell m) * hI.dpow (n * m) x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit k R
p : PrimeSpectrum R
⊢ RingHom.ker ((↑(AlgEquiv.ofBijective (ofId k (R ⧸ p.asIdeal)) ⋯).symm).comp (Ideal.Quotient.mkₐ k p.asIdeal)) =
    p.asIdeal

Tactic:
rw [← AlgHom.comap_ker, ← RingHom.ker_coe_toRingHom, AlgEquiv.toAlgHom_toRingHom,
      AlgHom.ker_coe_equiv, ← RingHom.ker_eq_comap_bot, ← RingHom.ker_coe_toRingHom,
      Ideal.Quotient.mkₐ_ker]

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
P : Extension R S
x : P.Ring
x_in : x ∈ P.ker
property✝ : Cotangent.mk ⟨x, x_in⟩ ∈ P.extendScalars.cotangentComplex.ker
⊢ (P.cotangentComplex ∘ₗ ↑P.cotangentExtendScalarsEquiv ∘ₗ h1Cotangentι) ⟨Cotangent.mk ⟨x, x_in⟩, property✝⟩ =
    1 ⊗ₜ[P.Ring] (D R P.Ring) x

Tactic:
exact cotangentComplex_mk P ⟨x, x_in⟩

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
⊢ φ ζ = ζ ^ q

Tactic:
obtain ⟨k, hk, hζ⟩ := IsPrimitiveRoot.exists_pos hζ hm

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✝ : 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
⊢ φ ζ = ζ ^ q
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n✝ : ℕ
a : A
ha : a ∈ I
⊢ (dividedPowers hI hf hIJ hIf).dpow n✝ (f a) = f (hI.dpow n✝ a)

Tactic:
rw [dpow_apply hI hf hIJ hIf ha]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
x✝¹ x✝ : HomogeneousSubsemiring 𝒜
x : Subsemiring A
hx : IsHomogeneous 𝒜 x
y : Subsemiring A
hy : IsHomogeneous 𝒜 y
h : x = y
⊢ { toSubsemiring := x, is_homogeneous' := hx } = { toSubsemiring := y, is_homogeneous' := hy }

Tactic:
simp [h]

Goal state after: