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

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupCohomologyπEven A g hg i hi)) (x - y) = 0 ↔ ↑x - ↑y ∈ (Hom.hom A.norm).range

Tactic:
groupCohomologyπEven_eq_zero_iff

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ ↑(x - y) ∈ (Hom.hom A.norm).range ↔ ↑x - ↑y ∈ (Hom.hom A.norm).range
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
hf : IsMulCocycle₁ f
z : L
hz : aux f z ≠ 0
⊢ IsMulCoboundary₁ f

Tactic:
have : aux f z = ∑ h, f h * h z := by simp [aux, Finsupp.linearCombination, Finsupp.sum_fintype]

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
hf : IsMulCocycle₁ f
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h, ↑(f h) * h z
⊢ IsMulCoboundary₁ f
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
f : ↥(cocycles₁ A)
g h : G
⊢ f h + f g = f g + f h

Tactic:
add_comm

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
f : ↥(cocycles₁ A)
g h : G
⊢ f g + f h = f g + f h
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
f : G → A
hf : f ∈ coboundaries₁ (Rep.ofDistribMulAction k G A)
⊢ IsCoboundary₁ f

Tactic:
by
  rcases hf with ⟨a, rfl⟩
  exact ⟨a, fun _ => rfl⟩

Goal state after:
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 : ↥(cocycles₁ A)
this :
  (ConcreteCategory.hom ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv)) x =
    (ConcreteCategory.hom (iCocycles A 1)) ((ConcreteCategory.hom (isoCocycles₁ A).inv) x)
⊢ (ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x =
    (ModuleCat.Hom.hom (HomologicalComplex.iCycles (inhomogeneousCochains A) 1))
      ((ConcreteCategory.hom (isoCocycles₁ A).inv) x)

Tactic:
← this

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
this :
  (ConcreteCategory.hom ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv)) x =
    (ConcreteCategory.hom (iCocycles A 1)) ((ConcreteCategory.hom (isoCocycles₁ A).inv) x)
⊢ (ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x =
    (ConcreteCategory.hom ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv)) x
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ m ∈ x.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m') ↔ ∀ xi ∈ x.support, ∃ si ∈ s, ∃ c, xi = si + c

Tactic:
add_comm

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ m ∈ x.coeff.support, ∃ m' ∈ s, ∃ d, m = m' + d) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, ∃ c, xi = si + c
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝² : TendstoCofinite f
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
x : τ →₀ ℕ
⊢ Finset.image
      (fun x ↦
        match x with
        | (fst, b) => (b.1 + b.2, b))
      ⋯.toFinset =
    ⋯.toFinset

Tactic:
ext ⟨_, _, _⟩

Goal state after:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝² : TendstoCofinite f
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
x : τ →₀ ℕ
fst✝¹ fst✝ snd✝ : σ →₀ ℕ
⊢ (fst✝¹, fst✝, snd✝) ∈
      Finset.image
        (fun x ↦
          match x with
          | (fst, b) => (b.1 + b.2, b))
        ⋯.toFinset ↔
    (fst✝¹, fst✝, snd✝) ∈ ⋯.toFinset
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w✝¹ → R
H : (∑ i, s i * r i) * a + ∑ x, s x * p x = y
⊢ ∃ y_1 ∈ span (Set.range p), ∃ z ∈ span (Set.range fun a_1 ↦ a • i a_1), y_1 + z = y

Tactic:
add_comm

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w✝¹ → R
H : ∑ x, s x * p x + (∑ i, s i * r i) * a = y
⊢ ∃ y_1 ∈ span (Set.range p), ∃ z ∈ span (Set.range fun a_1 ↦ a • i a_1), y_1 + z = y
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
f : σ → τ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : R →+* S
p : MvPowerSeries σ R
⊢ (rename f) ((map φ) p) = (map φ) ((rename f) p)

Tactic:
by
  ext; simp [coeff_rename]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
hC : ∅ ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) ∅
⊢ ⊥ ∈ kaplanskySet S ∧ ∀ J ∈ ∅, J ≤ ⊥

Tactic:
by simpa [mem_kaplanskySet_iff, eq_empty_iff_forall_notMem]

Goal state after:
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 x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : Prime z
⊢ (∀ b ∈ {z}, Prime b) ∧ Associated {z}.prod z

Tactic:
simpa

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
inst✝ : A.IsTrivial
g : G
a : ↑A
⊢ (H1ToTensorOfIsTrivial A)
      ((ConcreteCategory.hom (H1π A)) ((ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (single g a))) =
    Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a

Tactic:
simp only [H1ToTensorOfIsTrivial, H1π, AddMonoidHom.coe_toIntLinearMap, AddMonoidHom.coe_comp]

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g : G
a : ↑A
⊢ (⇑(QuotientAddGroup.lift (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup
            ((Finsupp.liftAddHom fun g ↦
                  ↑((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A) (Additive.ofMul (Abelianization.of g)))).comp
              (cycles₁ A).toAddSubgroup.subtype)
            ⋯) ∘
        ⇑↑(ModuleCat.Hom.hom (H1Iso A).hom))
      ((ConcreteCategory.hom ((isoCycles₁ A).inv ≫ π A 1))
        ((ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (single g a))) =
    Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ ((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A).compr₂ₛₗ
        (H1ToTensorOfIsTrivial A ∘ₗ TensorProduct.lift (mkH1OfIsTrivial A))).toAddMonoidHom =
    ((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A).compr₂ₛₗ LinearMap.id).toAddMonoidHom

Tactic:
ext g a
      simp [TensorProduct.mk_apply, TensorProduct.lift.tmul, mkH1OfIsTrivial_apply,
        H1ToTensorOfIsTrivial_H1π_single g a]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
m✝ n✝ : ℕ
x✝ : m✝ ≤ n✝
⊢ m✝ ∈ Finset.Iic n✝

Tactic:
simpa

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

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
i n : ℕ
hn : (Finset.Iic i).sup N ≤ n
⊢ u n - L ∈ I ^ i

Tactic:
have := Ideal.add_mem _ (hN i ((Finset.Iic i).sup N) (Finset.le_sup (by simp))
      n (.trans (Finset.le_sup (by simp)) hn)) (hL i)

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝¹ : (𝓝 0).IsCountablyGenerated
this✝ : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
i n : ℕ
hn : (Finset.Iic i).sup N ≤ n
this : u n - u ((Finset.Iic i).sup N) + (u ((Finset.Iic i).sup N) - L) ∈ I ^ i
⊢ u n - L ∈ I ^ i
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : 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
this : ∃ a b, (a none = m ∧ b none = n) ∧ a.some = u ∧ a + b = optionElim k x ∧ b.some = v
⊢ ∃ a, ∃ (_ : a ∈ antidiagonal (optionElim k x)), ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩ = ⟨(m, n), (u, v)⟩

Tactic:
simpa

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
⊢ optionFunLeft σ R (p * q) = optionFunLeft σ R p * optionFunLeft σ R q

Tactic:
ext k x
  simp only [coeff_coeff_optionFunLeft, coeff_mul, PowerSeries.coeff_mul, map_sum, sum_sigma']
  refine sum_bij (fun y _ ↦ ⟨(y.1 none, y.2 none), (y.1.some, y.2.some)⟩) ?_ ?_ ?_ ?_
  · intros; simp_all [Finsupp.ext_iff]
  · intros; ext t <;> cases t
    all_goals simp_all [Finsupp.ext_iff]
  · rintro ⟨⟨m, n⟩, ⟨u, v⟩⟩ h
    suffices ∃ a b, (a none = m ∧ b none = n) ∧ a.some = u ∧ a + b = optionElim k x ∧
      b.some = v by simpa
    use u.optionElim m, v.optionElim n
    suffices optionElim m u + optionElim n v = optionElim k x by simp_all
    ext t; cases t <;> simp_all [Finsupp.ext_iff]
  · intros; simp_all [Finsupp.ext_iff]

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this✝ : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
y : AdicCompletion (maximalIdeal R) R
hy : (residue (AdicCompletion (maximalIdeal R) R)) y = x
z : R
hz : (Ideal.Quotient.mk (maximalIdeal R ^ 1 • ⊤)) z = ↑y 1
this : (algebraMap R (AdicCompletion (maximalIdeal R) R)) z - y ∈ maximalIdeal R ^ 1 • ⊤
⊢ (algebraMap R (AdicCompletion (maximalIdeal R) R)) z - y ∈ maximalIdeal R • ⊤

Tactic:
simpa

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) ((truncTotal n) (toAdicCompletionInv σ R f)) = ↑f n

Tactic:
← Ideal.Quotient.mk_out (f.val n),

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) ((truncTotal n) (toAdicCompletionInv σ R f)) =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) (Quotient.out (↑f n))
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 : ℕ
x : AdicCompletion I ↥(I ^ n • ⊤)
i : ℕ
hx : ↑((ofPowSMul I M n) x) (i + n) = 0
⊢ i + n = ?m.71 + n

Tactic:
add_comm

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 : ℕ
x : AdicCompletion I ↥(I ^ n • ⊤)
i : ℕ
hx : ↑((ofPowSMul I M n) x) (i + n) = 0
⊢ n + i = n + i
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
y : AdicCompletion I ↥(I ^ n • ⊤)
⊢ (eval I M n) ((ofPowSMul I M n) y) = 0

Tactic:
eval_apply,

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
y : AdicCompletion I ↥(I ^ n • ⊤)
⊢ ↑((ofPowSMul I M n) y) n = 0
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
h : I.FG
x : ℕ → AdicCompletion I M
m n : ℕ
hx : (eval I M m) (x m) = (eval I M m) (x n)
h' : m ≤ n
⊢ ↑(x n) m = ↑(x m) m

Tactic:
eval_apply,

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
m n : ℕ
hx : ↑(x m) m = (eval I M m) (x n)
h' : m ≤ n
⊢ ↑(x n) m = ↑(x m) m
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
h : I.FG
x : ℕ → AdicCompletion I M
m n : ℕ
hx : ↑(x m) m = (eval I M m) (x n)
h' : m ≤ n
⊢ ↑(x n) m = ↑(x m) m

Tactic:
eval_apply,

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
m n : ℕ
hx : ↑(x m) m = ↑(x n) m
h' : m ≤ n
⊢ ↑(x n) m = ↑(x m) m
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD I ^ m • ⊤]
L : AdicCompletion I M := ⟨fun i ↦ ↑(x i) i, ⋯⟩
i : ℕ
⊢ x i ≡ L [SMOD I ^ i • ⊤]

Tactic:
rw [SModEq.sub_mem, pow_smul_top_eq_ker_eval h]

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
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD I ^ m • ⊤]
L : AdicCompletion I M := ⟨fun i ↦ ↑(x i) i, ⋯⟩
i : ℕ
⊢ x i - L ∈ (eval I M i).ker
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case right
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ ¬(valuation K v) (↑(algebraMap R K) ↑x) < ↑1

Tactic:
obtain ⟨x, _, hx, _⟩ := x
    change ¬v.valuation K (algebraMap R K x) < 1
    apply_fun v.intValuation at hx
    rw [map_one, map_mul] at hx
    rw [not_lt, ← hx, ← mul_one <| v.valuation _ _, valuation_of_algebraMap]
    gcongr
    exact v.intValuation_le_one _

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

Goal state before:
pp: case mpr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
⊢ ⟨val✝, hx⟩ ∈ selmerGroup.subgroupOf selmerGroup → ⟨val✝, hx⟩ ∈ valuation.ker

Tactic:
exact fun hx' => funext fun v => hx' v <| Set.notMem_empty v

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
p : Ideal R
hp : p ∈ (annihilator R M).minimalPrimes
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
hq : q ∈ associatedPrimes Rₚ (LocalizedModule p.primeCompl M)
q_prime : q.IsPrime
⊢ p ∈ associatedPrimes R M

Tactic:
simp only [← preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule p.primeCompl
    Rₚ (LocalizedModule.mkLinearMap p.primeCompl M), Set.mem_preimage] at hq

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
p : Ideal R
hp : p ∈ (annihilator R M).minimalPrimes
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
q_prime : q.IsPrime
hq : Ideal.comap (algebraMap R Rₚ) q ∈ associatedPrimes R M
⊢ p ∈ associatedPrimes R M
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 : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
k : ℕ
hk : x ^ k ∈ I
⊢ ∀ i < n, Subsingleton (Ext N (of R (QuotSMulTop (x ^ k) ↑M)) i)

Tactic:
intro i hi

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
k : ℕ
hk : x ^ k ∈ I
i : ℕ
hi : i < n
⊢ Subsingleton (Ext N (of R (QuotSMulTop (x ^ k) ↑M)) i)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case h
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
F : MvPolynomial (ℕ × M) R
⊢ P (Quot.mk (⇑(ringCon R M).toSetoid) F)

Tactic:
| _ F
   => 

Goal state after:
case h
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
F : MvPolynomial (ℕ × M) R
⊢ P (Quot.mk (⇑(ringCon R M).toSetoid) F)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.smul
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m✝ : M
r : R
m : M
hm : m ∈ Submodule.span R (Set.range v)
h :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k m ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ x * dp R k (r • m) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
simp [dp_smul, smul_mem _ _ (h x k hx)]

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

Goal state before:
pp: case insert.h
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∀ x_1 ∈ s, dpow (Multiset.count x_1 ↑m) (x x_1) = dpow (Multiset.count x_1 ↑(Sym.filterNe a m).snd) (x x_1)

Tactic:
intro i hi

Goal state after:
case insert.h
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ dpow (Multiset.count i ↑m) (x i) = dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝³ : CommSemiring A
ι : Type u_2
inst✝² : DecidableEq ι
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
x✝ : Sym ι n
a✝ : x✝ ∈ x.support.sym n
⊢ ∀ x_1 ∈ x.support,
    hJ.dpow (Multiset.count x_1 ↑x✝) (x x_1 • b x_1) =
      (fun i r ↦ r ^ Multiset.count i ↑x✝ • hJ.dpow (Multiset.count i ↑x✝) (b i)) x_1 (x x_1)

Tactic:
intro i hi

Goal state after:
A : Type u_1
inst✝³ : CommSemiring A
ι : Type u_2
inst✝² : DecidableEq ι
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
x✝ : Sym ι n
a✝ : x✝ ∈ x.support.sym n
i : ι
hi : i ∈ x.support
⊢ hJ.dpow (Multiset.count i ↑x✝) (x i • b i) =
    (fun i r ↦ r ^ Multiset.count i ↑x✝ • hJ.dpow (Multiset.count i ↑x✝) (b i)) i (x i)
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: 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
S : Set A
hS : I = span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
h : map f I ≤ J
n✝ : ℕ
a : A
ha : a ∈ I
⊢ hJ.dpow n✝ (f a) = f (hI.dpow n✝ a)

Tactic:
by
      rw [← fromGens_coe hI hJ hS h hdp, (fromGens hI hJ hS h hdp).dpow_comp a ha]

Goal state after: