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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
⊢ (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d 1 (1 + 1)) ∘ₗ ConcreteCategory.hom (cochainsIso₁ X.X₃).inv) ⇑z =
    0

Tactic:
← ModuleCat.hom_comp,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
⊢ (ModuleCat.Hom.hom ((cochainsIso₁ X.X₃).inv ≫ (inhomogeneousCochains X.X₃).d 1 (1 + 1))) ⇑z = 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
g : Fin (1 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₂ X.X₁).inv) x) g =
    (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d 1 (1 + 1)) ∘ₗ ConcreteCategory.hom (cochainsIso₁ X.X₂).inv) y
      g

Tactic:
← ModuleCat.hom_comp,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
g : Fin (1 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₂ X.X₁).inv) x) g =
    (ModuleCat.Hom.hom ((cochainsIso₁ X.X₂).inv ≫ (inhomogeneousCochains X.X₂).d 1 (1 + 1))) y g
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)
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d A 1) ∘ₗ ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x = 0

Tactic:
← ModuleCat.hom_comp,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
⊢ (ModuleCat.Hom.hom ((cochainsIso₁ A).inv ≫ inhomogeneousCochains.d A 1)) ⇑x = 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
x : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d A 2) ∘ₗ ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x = 0

Tactic:
← ModuleCat.hom_comp,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ (ModuleCat.Hom.hom ((cochainsIso₂ A).inv ≫ inhomogeneousCochains.d A 2)) ⇑x = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

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

Tactic:
groupHomologyπOdd_eq_zero_iff,

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
A : Rep k G
i : ℕ
hi : Odd i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ ↑(x - y) ∈ LinearMap.range A.ρ.norm ↔ ↑x - ↑y ∈ LinearMap.range A.ρ.norm
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:
← ModuleCat.hom_comp,

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 ((chainsIso₁ X.X₃).inv ≫ (inhomogeneousChains X.X₃).d 1 0)) ↑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
| ((ConcreteCategory.hom ((inhomogeneousChains X.X₂).d 1 0) ∘ₗ ConcreteCategory.hom (chainsIso₁ X.X₂).inv) y) x✝

Tactic:
← ModuleCat.hom_comp,

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 ((chainsIso₁ X.X₂).inv ≫ (inhomogeneousChains X.X₂).d 1 0)) y) x✝
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 × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
⊢ (ConcreteCategory.hom ((inhomogeneousChains X.X₃).d 2 1) ∘ₗ ConcreteCategory.hom (chainsIso₂ X.X₃).inv) ↑z = 0

Tactic:
← ModuleCat.hom_comp,

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 × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
⊢ (ModuleCat.Hom.hom ((chainsIso₂ X.X₃).inv ≫ (inhomogeneousChains X.X₃).d 2 1)) ↑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 × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
x✝ : Fin 1 → G
| ((ConcreteCategory.hom ((inhomogeneousChains X.X₂).d 2 1) ∘ₗ ConcreteCategory.hom (chainsIso₂ X.X₂).inv) y) x✝

Tactic:
← ModuleCat.hom_comp,

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 × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
x✝ : Fin 1 → G
| ((ModuleCat.Hom.hom ((chainsIso₂ X.X₂).inv ≫ (inhomogeneousChains X.X₂).d 2 1)) y) x✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A✝ : Rep k H
B : Rep k G
f : G →* H
φ : res f A✝ ⟶ B
n : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ Function.Injective ⇑(ConcreteCategory.hom (H1InfRes A S).f)

Tactic:
injective_iff_map_eq_zero

Goal state after:
k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A✝ : Rep k H
B : Rep k G
f : G →* H
φ : res f A✝ ⟶ B
n : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ ∀ (a : ↑(H1InfRes A S).X₁), (ConcreteCategory.hom (H1InfRes A S).f) a = 0 → a = 0
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
⊢ map 0 = 0

Tactic:
cat_disch

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ^ n = restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯

Tactic:
apply Submodule.restrictScalars_injective R

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ^ n) =
    Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯)
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : TendstoCofinite g
p : MvPowerSeries σ R
⊢ (rename g) ((rename f) p) = (rename (g ∘ f)) p

Tactic:
ext y; simp only [coeff_rename]
  rw [← Finset.sum_finset_product' ((TendstoCofinite.finite_preimage_singleton
    (Finsupp.mapDomain (g ∘ f)) y).toFinset.image (fun u ↦ (Finsupp.mapDomain f u, u))) _ _
      (by simp; grind [mapDomain_comp]), Finset.sum_image (by simp)]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.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
x : A
hx : x ∈ Coinvariants.ker (Representation.ofDistribMulAction k G A)
r : k
x✝² : A
x✝¹ : x✝² ∈ Submodule.span k (Set.range fun gv ↦ ((Representation.ofDistribMulAction k G A) gv.1) gv.2 - gv.2)
x✝ : IsBoundary₀ G x✝²
X : G →₀ A
hX : (X.sum fun g z ↦ g⁻¹ • z - z) = x✝²
⊢ ((r • X).sum fun g z ↦ g⁻¹ • z - z) = r • x✝²

Tactic:
by simp [← hX, sum_smul_index', smul_comm, smul_sub, smul_sum]

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)
⊢ (ConcreteCategory.hom ((inhomogeneousChains A).d 1 0) ∘ₗ ConcreteCategory.hom (chainsIso₁ A).inv) ↑x = 0

Tactic:
← ModuleCat.hom_comp,

Goal state after:
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
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)
⊢ (ConcreteCategory.hom ((inhomogeneousChains A).d 2 1) ∘ₗ ConcreteCategory.hom (chainsIso₂ A).inv) ↑x = 0

Tactic:
← ModuleCat.hom_comp,

Goal state after:
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 2 1)) ↑x = 0
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case h.succ
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
n✝ : ℕ
hn : 0 < n✝ + 1
⊢ ↑(J ^ (n✝ * m + m)) ⊆ ↑(J ^ m)

Tactic:
apply Ideal.pow_le_pow_right

Goal state after:
case h.succ
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
n✝ : ℕ
hn : 0 < n✝ + 1
⊢ m ≤ n✝ * m + m
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
i✝ : ℕ
g✝ : Fin i✝ → G
x✝ : ↑(ModuleCat.of k ↑A)
a✝ : Fin i✝ → K
⊢ ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsMap (g.comp f) (φ ≫ (resFunctor f).map ψ)).f i✝)) x✝) a✝ =
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g✝) ≫ (chainsMap f φ ≫ chainsMap g ψ).f i✝)) x✝) a✝

Tactic:
simp [chainsMap_f, Function.comp_assoc]

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

Goal state before:
pp: case neg
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
n : ℕ
hn : maximalIdeal A ^ n = 0
m : ℕ
hf : f n = f m
h : ¬m ≤ n
⊢ f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]

Tactic:
rw [hf]

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
⊢ chainsMap₂ f φ ≫ (shortComplexH1 B).f = (shortComplexH1 A).f ≫ chainsMap₁ f φ

Tactic:
by
    simp only [shortComplexH1]
    ext : 3
    simpa [d₂₁, map_add, map_sub, ← map_inv] using congr(single _ $((hom_comm_apply φ _ _).symm))

Goal state after:
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 M
hxn : ↑x n = 0
i : ℕ
⊢ ↑((ofPowSMul I M n) (ofValEqZero I hxn)) i = ↑x i

Tactic:
by_cases! h : n ≤ i

Goal state after:
case pos
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 M
hxn : ↑x n = 0
i : ℕ
h : n ≤ i
⊢ ↑((ofPowSMul I M n) (ofValEqZero I hxn)) i = ↑x i

case neg
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 M
hxn : ↑x n = 0
i : ℕ
h : i < n
⊢ ↑((ofPowSMul I M n) (ofValEqZero I hxn)) i = ↑x i
Module: Mathlib.RingTheory.Algebraic.Pi

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : CommSemiring T
inst✝¹ : Algebra R S
inst✝ : Algebra S T
z : S
⊢ (algebraMap S T) ((aeval z) 0) = 0 z

Tactic:
by simp only [Pi.zero_apply, map_zero]

Goal state after:
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
a b c : ℕ
σ : Type u_3
inst✝ : Finite σ
⊢ IsAdicComplete (Ideal.span (Set.range X)) (MvPowerSeries σ R)

Tactic:
have : Ideal.map (toAdicCompletionAlgEquiv σ R).toRingEquiv (Ideal.span (Set.range X)) =
    (MvPolynomial.idealOfVars σ R).map (algebraMap ..) := by
    simp_rw [Ideal.map_span, ← Set.range_comp]
    congr 2; ext1
    simp [AdicCompletion.algebraMap_apply, ← MvPolynomial.coe_X, toAdicCompletion_coe]
  rw [← IsAdicComplete.congr_ringEquiv _ (toAdicCompletionAlgEquiv σ R).toRingEquiv, this,
    IsAdicComplete.map_algebraMap_iff]
  exact AdicCompletion.isAdicComplete (MvPolynomial.idealOfVars_fg σ R)

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
I : (FractionalIdeal A⁰ (FractionRing A))ˣ
⊢ (extendedHom A B) ((mk (FractionRing A)) I) =
    (mk (FractionRing B)) ((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) I)

Tactic:
by
  rw [← ClassGroup.Quot_mk_eq_mk, ← ClassGroup.Quot_mk_eq_mk]
  exact extendedHom_quotientMk A B I

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I : ↥(Ideal A)⁰
⊢ (extendedHom A B) (mk0 I) = mk0 (extendedIdeal A B I)

Tactic:
mk0_eq_quotientMk,

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I : ↥(Ideal A)⁰
⊢ (extendedHom A B) ↑((FractionalIdeal.mk0 (FractionRing A)) I) = mk0 (extendedIdeal A B I)
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I : ↥(Ideal A)⁰
⊢ (extendedHom A B) ↑((FractionalIdeal.mk0 (FractionRing A)) I) = mk0 (extendedIdeal A B I)

Tactic:
mk0_eq_quotientMk,

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I : ↥(Ideal A)⁰
⊢ (extendedHom A B) ↑((FractionalIdeal.mk0 (FractionRing A)) I) =
    ↑((FractionalIdeal.mk0 (FractionRing B)) (extendedIdeal A B I))
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
M : Type u_8
N : Type u_9
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Bialgebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
x : A[M]
⊢ counit ((domCongr R A e) x) = counit x

Tactic:
induction x using MonoidAlgebra.induction_linear

Goal state after:
case zero
R : Type u_1
A : Type u_3
M : Type u_8
N : Type u_9
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Bialgebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
⊢ counit ((domCongr R A e) 0) = counit 0

case add
R : Type u_1
A : Type u_3
M : Type u_8
N : Type u_9
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Bialgebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
x✝ y✝ : A[M]
a✝¹ : counit ((domCongr R A e) x✝) = counit x✝
a✝ : counit ((domCongr R A e) y✝) = counit y✝
⊢ counit ((domCongr R A e) (x✝ + y✝)) = counit (x✝ + y✝)

case single
R : Type u_1
A : Type u_3
M : Type u_8
N : Type u_9
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Bialgebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
m✝ : M
r✝ : A
⊢ counit ((domCongr R A e) (single m✝ r✝)) = counit (single m✝ r✝)
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
M : Type u_8
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Bialgebra R A
inst✝ : CommMonoid M
f g : WithConv (R[M] →ₐc[R] A)
x : M
⊢ (f * g).ofConv (single x 1) = f.ofConv (single x 1) * g.ofConv (single x 1)

Tactic:
simp only [BialgHom.convMul_def, BialgHom.coe_comp, Function.comp_apply]

Goal state after:
R : Type u_1
A : Type u_3
M : Type u_8
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Bialgebra R A
inst✝ : CommMonoid M
f g : WithConv (R[M] →ₐc[R] A)
x : M
⊢ (mulBialgHom R A) ((Bialgebra.TensorProduct.map f.ofConv g.ofConv) ((comulBialgHom R R[M]) (single x 1))) =
    f.ofConv (single x 1) * g.ofConv (single x 1)
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: 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
⊢ v.valuationOfNeZeroToFun 1 = 1

Tactic:
← WithZero.coe_inj,

Goal state after:
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
⊢ ↑(v.valuationOfNeZeroToFun 1) = ↑1
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: 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✝¹ x✝ : Kˣ
⊢ v.valuationOfNeZeroToFun (x✝¹ * x✝) = v.valuationOfNeZeroToFun x✝¹ * v.valuationOfNeZeroToFun x✝

Tactic:
← WithZero.coe_inj,

Goal state after:
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✝¹ x✝ : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun (x✝¹ * x✝)) = ↑(v.valuationOfNeZeroToFun x✝¹ * v.valuationOfNeZeroToFun x✝)
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: 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ˣ
⊢ v.valuationOfNeZero ((Units.map ↑(algebraMap R K)) x) = 1

Tactic:
← WithZero.coe_inj,

Goal state after:
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ˣ
⊢ ↑(v.valuationOfNeZero ((Units.map ↑(algebraMap R K)) x)) = ↑1
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: case inl
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✝ : Subsingleton M
⊢ ∃ r ∈ annihilator R N, IsSMulRegular M r

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
⊢ ∃ r ∈ annihilator R N, IsSMulRegular M r

Tactic:
· exact ⟨0, ⟨Submodule.zero_mem (Module.annihilator R N), IsSMulRegular.zero⟩⟩

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
⊢ ∃ r ∈ annihilator R N, IsSMulRegular M r
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: 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'
ass : p ∈ associatedPrimes R' M'
fg : (Ideal.comap (algebraMap R R') p).FG
⊢ Ideal.comap (algebraMap R R') p ∈ associatedPrimes R M

Tactic:
rcases ass with ⟨hp, x, hx⟩
  rcases fg with ⟨T, hT⟩
  rcases IsLocalizedModule.mk'_surjective S f x with ⟨⟨m, s⟩, rfl⟩
  simp only [Function.uncurry_apply_pair] at hx
  have mem (a : T) : algebraMap R R' a ∈ p := by
    simpa [← Ideal.mem_comap, ← hT] using Ideal.subset_span a.2
  simp only [hx, Ideal.mem_radical_iff, mem_bot, mem_colon_singleton, ← map_pow, algebraMap_smul,
    ← IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_eq_zero' f] at mem
  choose e g hg using mem
  refine ⟨.under R p, (∏ a, g a).1 • m, le_antisymm ?_ fun r hr ↦ ?_⟩
  · rw [← hT, Ideal.span_le]
    intro a ha
    simp only [SetLike.mem_coe, Ideal.mem_radical_iff, mem_bot, mem_colon_singleton]
    obtain ⟨u, hu⟩ : g ⟨a, ha⟩ ∣ (∏ a, g a) := by
      apply Finset.dvd_prod_of_mem g (Finset.mem_univ ⟨a, ha⟩)
    use e ⟨a, ha⟩
    rw [hu, Submonoid.coe_mul, smul_smul, ← mul_assoc, mul_comm, ← smul_smul, mul_comm, ← smul_smul]
    exact smul_eq_zero_of_right u.1 (hg ⟨a, ha⟩)
  · simp only [Ideal.mem_radical_iff, mem_bot, mem_colon_singleton, smul_smul] at hr
    obtain ⟨k, hk⟩ := hr
    have mem : r ^ k * (∏ a, g a).1 ∈ Ideal.comap (algebraMap R R') p := by
      rw [hx]
      use 1
      simp_rw [pow_one, mem_colon_singleton, algebraMap_smul, ← IsLocalizedModule.mk'_smul,
        hk, IsLocalizedModule.mk'_zero, mem_bot]
    apply hp.mem_of_pow_mem k
    rw [← map_pow]
    exact ((hp.under R).mul_mem_iff_mem_or_mem.mp mem).resolve_right
      (Set.disjoint_left.mp ((IsLocalization.disjoint_under_iff S R' p).mpr hp.1) (∏ a, g a).2)

Goal state after: