mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²³ : Monoid G
inst✝²² : Ring R
inst✝²¹ : AddCommGroup V
inst✝²⁰ : TopologicalSpace V
inst✝¹⁹ : IsTopologicalAddGroup V
inst✝¹⁸ : Module R V
inst✝¹⁷ : AddCommGroup W
inst✝¹⁶ : TopologicalSpace W
inst✝¹⁵ : IsTopologicalAddGroup W
inst✝¹⁴ : Module R W
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
S✝ : Type u_6
inst✝⁹ : Monoid S✝
inst✝⁸ : DistribMulAction S✝ W
inst✝⁷ : SMulCommClass R S✝ W
inst✝⁶ : ContinuousConstSMul S✝ W
inst✝⁵ : LinearMap.CompatibleSMul W W S✝ R
S : Type u_7
inst✝⁴ : Ring S
inst✝³ : Module S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝² x✝¹ : S
x✝ : π₁ →ⁱL π₂
⊢ (x✝² + x✝¹) • x✝ = x✝² • x✝ + x✝¹ • x✝

Tactic:
by ext; simp [add_smul]

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case refine_2
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
x✝ : Mono f
ι : Abelian.image f ⟶ V := Abelian.image.ι f
hf : Abelian.factorThruImage f ≫ ι ≠ 0
φ : V ⟶ Abelian.image f := Injective.factorThru (𝟙 (Abelian.image f)) ι
hφι : φ ≫ ι ≠ 0
⊢ Epi ι

Tactic:
obtain ⟨c, hc⟩ : ∃ c : k, c • _ = 𝟙 V := (finrank_eq_one_iff_of_nonzero' _ hφι).mp h (𝟙 V)

Goal state after:
case refine_2
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
x✝ : Mono f
ι : Abelian.image f ⟶ V := Abelian.image.ι f
hf : Abelian.factorThruImage f ≫ ι ≠ 0
φ : V ⟶ Abelian.image f := Injective.factorThru (𝟙 (Abelian.image f)) ι
hφι : φ ≫ ι ≠ 0
c : k
hc : c • φ ≫ ι = 𝟙 V
⊢ Epi ι
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↑A
g : G
⊢ (A.ρ g) (x + y) - (x + y) = ((fun g ↦ (A.ρ g) x - x) + fun g ↦ (A.ρ g) y - y) g

Tactic:
simp only [map_add, add_sub_add_comm]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↑A
g : G
⊢ (A.ρ g) x - x + ((A.ρ g) y - y) = ((fun g ↦ (A.ρ g) x - x) + fun g ↦ (A.ρ g) y - y) g
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
⊢ (ModuleCat.Hom.hom ((chainsIso₁ X.X₃).inv ≫ (inhomogeneousChains X.X₃).d 1 0)) ↑z = 0

Tactic:
eq_d₁₀_comp_inv

Goal state after:
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
⊢ (ModuleCat.Hom.hom (d₁₀ X.X₃ ≫ (chainsIso₀ X.X₃).inv)) ↑z = 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
x✝ : Fin 0 → G
| ((ModuleCat.Hom.hom ((chainsIso₁ X.X₂).inv ≫ (inhomogeneousChains X.X₂).d 1 0)) y) x✝

Tactic:
eq_d₁₀_comp_inv

Goal state after:
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
x✝ : Fin 0 → G
| ((ModuleCat.Hom.hom (d₁₀ X.X₂ ≫ (chainsIso₀ X.X₂).inv)) y) x✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : G →₀ ↑A
⊢ x ∈ cycles₁ A ↔ (x.sum fun g a ↦ (A.ρ g⁻¹) a) = x.sum fun x a ↦ a

Tactic:
change x.sum (fun g a => A.ρ g⁻¹ a - a) = 0 ↔ _
  rw [sum_sub, sub_eq_zero]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₁ A)
⊢ (ModuleCat.Hom.hom ((chainsIso₁ A).inv ≫ (inhomogeneousChains A).d 1 0)) ↑x = 0

Tactic:
eq_d₁₀_comp_inv

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₁ A)
⊢ (ModuleCat.Hom.hom (d₁₀ A ≫ (chainsIso₀ A).inv)) ↑x = 0
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
g : R⟦X⟧
⊢ g ∈ I → g ∈ Submodule.span R⟦X⟧ (Set.range F)

Tactic:
hg

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
g : R⟦X⟧
hg : g ∈ I
⊢ g ∈ Submodule.span R⟦X⟧ (Set.range F)
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ := fun t ↦ Nat.rec g (fun x G' ↦ mk fun p ↦ (coeff (p + 1)) G' - ∑ i, T G' i * (coeff (p + 1)) (F i)) t
hG : ∀ (n : ℕ), G n ∈ I
hG' : ∀ (n_1 : ℕ), G n_1 - ∑ i, C (T (G n_1) i) * F i = X * G (n_1 + 1)
H : Fin n → R⟦X⟧ := fun i ↦ mk fun n ↦ T (G n) i
⊢ g - ∑ i, ↑((trunc 0) (H i)) * F i = X ^ 0 * G 0

Tactic:
simp [G]

Goal state after:
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 2 ≫ (H2Iso A).hom = (isoCycles₂ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.π

Tactic:
by
  simp [H2Iso, isoCycles₂, π, HomologicalComplex.homologyπ, leftHomologyπ]

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
this : ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j ≤ I ^ i
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j • ⊤ ≤ I ^ i • ⊤

Tactic:
by
        simpa only [smul_top_eq_map, Algebra.algebraMap_self, map_id] using! this

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
this : ∀ (i : ℕ), ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ i)
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j • ⊤) * ↑(I ^ j • ⊤) ⊆ ↑(I ^ i • ⊤)

Tactic:
by
        simpa only [smul_top_eq_map, Algebra.algebraMap_self, map_id] using! this

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I m : Ideal R
inst✝ : m.IsMaximal
le : I ≤ m
fg : I.FG
mapeq :
  Ideal.map (algebraMap R (AdicCompletion I R)) m = comap (evalOneₐ I).toRingHom (Ideal.map (Ideal.Quotient.mk I) m)
⊢ RingHom.ker (Ideal.Quotient.mk I) ≤ m

Tactic:
simpa using le

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

Goal state before:
pp: 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
⊢ ∃ a, f a = m

Tactic:
have lmem : (transitionMap _ R (Nat.le_succ 1)) (m'.1.1 2) = m'.1.1 1 := m'.1.2 (Nat.le_succ 1)

Goal state after:
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 : (transitionMap (maximalIdeal R) R ⋯) (↑↑m' 2) = ↑↑m' 1
⊢ ∃ a, f a = m
Module: Mathlib.RingTheory.AdicCompletion.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
n : ℕ
hn : maximalIdeal A ^ n = 0
⊢ ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD maximalIdeal A ^ n • ⊤]

Tactic:
use f n

Goal state after:
case h
R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
n : ℕ
hn : maximalIdeal A ^ n = 0
⊢ ∀ (n_1 : ℕ), f n_1 ≡ f n [SMOD maximalIdeal A ^ n_1 • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
⊢ (ofPowSMul I M n).range ≤
    ((map I ((lsum R) fun i ↦ ↑i • LinearMap.id) ∘ₗ map I ↑(finsuppLEquivDirectSum R M ↥s).symm) ∘ₗ
        ↑(sumEquivOfFintype I fun x ↦ M)).range

Tactic:
LinearMap.range_comp_of_range_eq_top _ (LinearEquiv.range _),

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
⊢ (ofPowSMul I M n).range ≤
    (map I ((lsum R) fun i ↦ ↑i • LinearMap.id) ∘ₗ map I ↑(finsuppLEquivDirectSum R M ↥s).symm).range
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h
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 := ⋯
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := ⋯
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := ⋯
he : Function.Injective e
ve : G × G →₀ ↑A := ⋯
hS : ↑(v + (ConcreteCategory.hom (d₂₁ A)) ve).support ⊆ ↑S
⊢ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f)
      ((ConcreteCategory.hom (H1π (res S.subtype A)))
        ⟨comapDomain Subtype.val (v + (ConcreteCategory.hom (d₂₁ A)) ve) ⋯, ?w⟩) =
    (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩

Tactic:
simp only [H1CoresCoinfOfTrivial_f, H1CoresCoinfOfTrivial_X₁, H1π_comp_map_apply]
    refine (H1π_eq_iff _ _).2 ?_
  /- Indeed, `v + d(ve) - x = d(ve - z) ∈ B₁(G, A)`, since `v := x - dz`. -/
    use ve - z
    have := mapDomain_comapDomain (α := S) Subtype.val Subtype.val_injective
      (v + d₂₁ A ve) (fun x hx => ⟨⟨x, hS hx⟩, rfl⟩)
    simp_all [mapCycles₁_hom, v, add_sub_assoc, sub_add_sub_cancel']

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : p = 0
⊢ gaussNorm (v.intAdicAbv hb) 1 p ≤ 1

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
⊢ gaussNorm (v.intAdicAbv hb) 1 p ≤ 1

Tactic:
· simp [hp0]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
⊢ gaussNorm (v.intAdicAbv hb) 1 p ≤ 1
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : p = 0
⊢ gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
⊢ gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal

Tactic:
· simp [hp0]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
⊢ gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup M''
inst✝ : Module R M''
r : R
f : M →ₗ[R] M'
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : f.range = g.ker
h1 : IsSMulRegular M r
h2 : IsSMulRegular M'' r
x : M'
hx : r • x = 0
⊢ x = 0

Tactic:
obtain ⟨y, ⟨⟩⟩ := (congrArg (x ∈ ·) hfg).mpr <| h2.right_eq_zero_of_smul <|
    (g.map_smul r x).symm.trans <| (congrArg _ hx).trans g.map_zero

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup M''
inst✝ : Module R M''
r : R
f : M →ₗ[R] M'
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : f.range = g.ker
h1 : IsSMulRegular M r
h2 : IsSMulRegular M'' r
y : M
hx : r • f y = 0
⊢ f y = 0
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case insert
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ∏ i ∈ insert a✝ s✝, hI.dpow (n i) a = ↑(multinomial (insert a✝ s✝) n) * hI.dpow ((insert a✝ s✝).sum n) a

Tactic:
rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
      mul_assoc, hI.mul_dpow ha, ← sum_insert hi, ← mul_assoc]
    apply congr_arg₂ _ _ rfl
    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]

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

Goal state before:
pp: case empty
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 : ℕ
⊢ dpow n (∅.sum x) = ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dpow (Multiset.count i ↑k) (x i)

Tactic:
simp only [sum_empty, prod_empty, sum_const, nsmul_eq_mul, mul_one]

Goal state after:
case empty
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 : ℕ
⊢ dpow n 0 = ↑(#(∅.sym n))
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
  have suppQ : Module.support R (Shrink.{v} (R ⧸ I)) = PrimeSpectrum.zeroLocus I := by
    rw [(Shrink.linearEquiv R _).support_eq, Module.support_eq_zeroLocus, annihilator_quotient]
  tfae_have 1 → 2 := fun h1 i hi ↦ h1 (ModuleCat.of R (Shrink.{v} (R ⧸ I)))
    inferInstance inferInstance suppQ.subset i hi
  tfae_have 2 → 3 := fun h2 ↦ ⟨(ModuleCat.of R (Shrink.{v} (R ⧸ I))),
    inferInstance, Module.Finite.equiv (Shrink.linearEquiv R (R ⧸ I)).symm, suppQ, h2⟩
  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
  tfae_have 4 → 1 := fun ⟨rs, len, mem, reg⟩ N Nntr Nfin Nsupp i hi ↦
    subsingleton_ext_of_exists_isRegular I N Nsupp M smul_lt rs mem reg i (hi.trans_eq len.symm)
  tfae_finish

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

Goal state before:
pp: case succ
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
n : ℕ
a✝ : f (hI.dpow n 0) = hJ.dpow n 0
⊢ f (hI.dpow (n + 1) 0) = hJ.dpow (n + 1) 0

Tactic:
rw [hI.dpow_eval_zero n.succ_ne_zero, hJ.dpow_eval_zero n.succ_ne_zero, map_zero]

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

Goal state before:
pp: case pos.x
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
j : ι
hj : j ∈ s
⊢ ∏ x ∈ s, r x ∈ I

Tactic:
rw [Finset.prod_eq_prod_sdiff_singleton_mul hj]

Goal state after:
case pos.x
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
j : ι
hj : j ∈ s
⊢ (∏ x ∈ s \ {j}, r x) * r j ∈ I
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent x.fst

Tactic:
refine ⟨n, ?_⟩
    rw [← fst_pow, hn, fst_zero]

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case inr.inl
R : Type u_1
K : Type u_2
inst✝ : DivisionRing K
⊢ Submodule.IsPrincipal (Ideal.span {ε})

pp: case inr.inr
R : Type u_1
K : Type u_2
inst✝ : DivisionRing K
⊢ Submodule.IsPrincipal ⊤

Tactic:
· exact ⟨_, rfl⟩

Goal state after:
case inr.inr
R : Type u_1
K : Type u_2
inst✝ : DivisionRing K
⊢ Submodule.IsPrincipal ⊤
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case pos
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
x y : A
hx : x ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy : y ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hx_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
n : ℕ
hn : n ≠ 0
m : ℕ
a✝ : m ∈ Finset.range (n + 1)
hm0 : m = 0
⊢ hI.dpow 0 x * hI.dpow (n - 0) y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
exact (span _).mul_mem_left _ (hy_pow n hn)

Goal state after: