mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
hf : ∀ {m : ℕ}, (factorPow I ⋯).comp (f (m + 1)) = f m
inst✝ : IsAdicComplete I S
F : R →+* S
hF : ∀ (n : ℕ), (Ideal.Quotient.mk (I ^ a n)).comp F = f n
⊢ F = liftRingHom I ha f ⋯

Tactic:
by

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
⊢ (ofPowSMul I M n) (ofValEqZero I hxn) = x

Tactic:
by

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 : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ ↑(A.ofQuotient S)
hx : x ∈ cycles₁ (A.ofQuotient S)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), ↑(s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
⊢ ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨mapDomain s x, ?m.110⟩) =
    ↑⟨x, hx⟩

Tactic:
by

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 : ℕ
y : AdicCompletion I ↥(I ^ n • ⊤)
⊢ n ≤ n

Tactic:
by

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 : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x✝ : G ⧸ S →₀ ↑(A.ofQuotient S)
hx : x✝ ∈ cycles₁ (A.ofQuotient S)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), ↑(s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
x y : G ⧸ S
h : s x = s y
⊢ x = y

Tactic:
by

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 : ℕ
⊢ restrictScalars R (ofPowSMul I M n).range = (eval I M n).ker

Tactic:
by

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 : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ ↑(A.ofQuotient S)
hx : x ∈ cycles₁ (A.ofQuotient S)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), ↑(s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
a✝ : G ⧸ S
b : a✝ ∈ x.support
a : G
⊢ ↑(s ↑a)⁻¹ = ↑a⁻¹

Tactic:
by

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 : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G ⧸ S →₀ ↑(A.ofQuotient S)
hx : x ∈ cycles₁ (A.ofQuotient S)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), ↑(s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
a✝ : G ⧸ S
b : a✝ ∈ x.support
a : G
⊢ (A.ρ (s ↑a)⁻¹) (x ↑a) = ((A.ρ.ofQuotient S) (↑a)⁻¹) (x ↑a)

Tactic:
by

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 : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
⊢ Epi (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)

Tactic:
by

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
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : ι → R
⊢ ((lsum (AdicCompletion I R)) fun i ↦ (algebraMap R (AdicCompletion I R)) (f i) • LinearMap.id) ∘ₗ
      ↑(finsuppLEquivDirectSum (AdicCompletion I R) (AdicCompletion I M) ι).symm =
    (map I ((lsum R) fun i ↦ f i • LinearMap.id) ∘ₗ map I ↑(finsuppLEquivDirectSum R M ι).symm) ∘ₗ
      ↑(sumEquivOfFintype I fun x ↦ M)

Tactic:
by

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 : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
⊢ map S.subtype (𝟙 (res S.subtype A)) 1 ≫ map (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv 1 = 0

Tactic:
by

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 : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
⊢ (↑(finsuppLEquivDirectSum (AdicCompletion I R) (AdicCompletion I M) ↥s).symm).range = ⊤

Tactic:
by

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 : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
x✝ : AdicCompletion I (↥s →₀ M)
⊢ (map I ↑(finsuppLEquivDirectSum R M ↥s).symm) ((map I ↑(finsuppLEquivDirectSum R M ↥s)) x✝) = x✝

Tactic:
by

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 : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
⊢ Epi (map (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv 1)

Tactic:
by

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 : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
x : AdicCompletion I ↥(I ^ n • ⊤)
x✝ : ↥s →₀ M
⊢ ((lsum R) fun i ↦ ↑i • LinearMap.id) x✝ ∈ I ^ n • ⊤

Tactic:
by

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 : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
x : AdicCompletion I ↥(I ^ n • ⊤)
⊢ Function.Surjective ⇑(LinearMap.codRestrict (I ^ n • ⊤) ((lsum R) fun i ↦ ↑i • LinearMap.id) ⋯)

Tactic:
by

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 : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
this : Function.Surjective ⇑(LinearMap.codRestrict (I ^ n • ⊤) ((lsum R) fun i ↦ ↑i • LinearMap.id) ⋯)
x : AdicCompletion I (↥s →₀ M)
⊢ (map I ((lsum R) fun i ↦ ↑i • LinearMap.id)) x =
    (ofPowSMul I M n) ((map I (LinearMap.codRestrict (I ^ n • ⊤) ((lsum R) fun i ↦ ↑i • LinearMap.id) ⋯)) x)

Tactic:
by

Goal state after:
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
⊢ (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y

Tactic:
by

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 : ℕ
h : I.FG
⊢ I ^ n • ⊤ = (eval I M n).ker

Tactic:
by

Goal state after:
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) 1) = 1 z

Tactic:
by

Goal state after:
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
x✝¹ x✝ : R[X]
z : S
⊢ (algebraMap S T) ((aeval z) (x✝¹ * x✝)) =
    ((fun z ↦ (algebraMap S T) ((aeval z) x✝¹)) * fun z ↦ (algebraMap S T) ((aeval z) x✝)) z

Tactic:
by

Goal state after:
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

Goal state after:
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
x✝¹ x✝ : R[X]
z : S
⊢ (algebraMap S T) ((aeval z) (x✝¹ + x✝)) =
    ((fun z ↦ (algebraMap S T) ((aeval z) x✝¹)) + fun z ↦ (algebraMap S T) ((aeval z) x✝)) z

Tactic:
by

Goal state after:
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
x✝¹ : R[X]
x✝ : S → T
z : S
⊢ ({ toFun := fun p z ↦ (algebraMap S T) ((aeval z) p), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
          x✝¹ *
        x✝)
      z =
    (x✝ *
        { toFun := fun p z ↦ (algebraMap S T) ((aeval z) p), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          x✝¹)
      z

Tactic:
by

Goal state after:
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
x✝¹ : R[X]
x✝ : S → T
z : S
⊢ (x✝¹ • x✝) z =
    ({ toFun := fun p z ↦ (algebraMap S T) ((aeval z) p), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
          x✝¹ *
        x✝)
      z

Tactic:
by

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
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD I ^ m • ⊤]
m n : ℕ
h' : m ≤ n
⊢ (transitionMap I M h') ((fun i ↦ ↑(x i) i) n) = (fun i ↦ ↑(x i) i) m

Tactic:
by

Goal state after:
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:
by

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
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD I ^ m • ⊤]
⊢ ∃ L, ∀ (n : ℕ), x n ≡ L [SMOD I ^ n • ⊤]

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
x : AdicCompletion I R
⊢ I ^ 1 * ⊤ = I

Tactic:
by

Goal state after:
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
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
x y : G
hxy : e x = e y
⊢ x = y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
x : AdicCompletion I R
eq : I ^ 1 * ⊤ = I
⊢ Function.Injective ⇑(Ideal.Quotient.factor ⋯)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
⊢ RingHom.ker (evalOneₐ I).toRingHom = Ideal.map (algebraMap R (AdicCompletion I R)) I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Artinian.Algebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsIntegral R A
⊢ IsUnit.submonoid A = A⁰

Tactic:
by

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 σ
⊢ Ideal.map (toAdicCompletionAlgEquiv σ R).toRingEquiv (Ideal.span (Set.range X)) =
    Ideal.map (algebraMap (MvPolynomial σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R)

Tactic:
by

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 σ
this :
  Ideal.map (toAdicCompletionAlgEquiv σ R).toRingEquiv (Ideal.span (Set.range X)) =
    Ideal.map (algebraMap (MvPolynomial σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R)
⊢ IsAdicComplete (Ideal.span (Set.range X)) (MvPowerSeries σ R)

Tactic:
rw [← IsAdicComplete.congr_ringEquiv _ (toAdicCompletionAlgEquiv σ R).toRingEquiv, this,
    IsAdicComplete.map_algebraMap_iff]

Goal state after:
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 σ
this :
  Ideal.map (toAdicCompletionAlgEquiv σ R).toRingEquiv (Ideal.span (Set.range X)) =
    Ideal.map (algebraMap (MvPolynomial σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R)
⊢ IsAdicComplete (MvPolynomial.idealOfVars σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
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:
by

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 : ℕ
⊢ IsAdicComplete (Ideal.span {X}) R⟦X⟧

Tactic:
by

Goal state after:
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
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
he : Function.Injective e
ve : G × G →₀ ↑A := mapDomain e v
⊢ ↑(v + (ConcreteCategory.hom (d₂₁ A)) ve).support ⊆ ↑S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
a b : A
ha : IsGroupLikeElem R a
hb : IsGroupLikeElem R b
⊢ counit (a * b) = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
a b : A
ha : IsGroupLikeElem R a
hb : IsGroupLikeElem R b
⊢ comul (a * b) = (a * b) ⊗ₜ[R] (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
a b : A
hab : a * b = 1
hba : b * a = 1
ha : IsGroupLikeElem R a
⊢ counit b * counit a = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
a b : A
hab : a * b = 1
hba : b * a = 1
ha : IsGroupLikeElem R a
⊢ counit a * 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
a b : A
hab : a * b = 1
hba : b * a = 1
ha : IsGroupLikeElem R a
⊢ comul b * comul a = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
a b : A
hab : a * b = 1
hba : b * a = 1
ha : IsGroupLikeElem R a
⊢ comul a * b ⊗ₜ[R] b = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
u : Aˣ
⊢ ↑u⁻¹ * ↑u = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
u : Aˣ
⊢ ↑u * ↑u⁻¹ = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : Semiring A
X : Type u_3
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x : X
a : A
⊢ comul (single x a) = (TensorProduct.map (lsingle x) (lsingle x)) (comul a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
n : ℤ
⊢ comul (C a * T n) = (TensorProduct.map (lsingle n) (lsingle n)) (comul a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
n : ℤ
⊢ comul (C a * T n) = T n ⊗ₜ[R] (C a * T n)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
n : ℤ
⊢ counit (C a * T n) = counit a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
r : R
⊢ IsGroupLikeElem R r ↔ r = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
a : A
inst✝ : Nontrivial R
ha : IsGroupLikeElem R a
⊢ a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
inst✝³ : Module R B
inst✝² : Coalgebra R B
a : A
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
⊢ counit (f a) = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
inst✝³ : Module R B
inst✝² : Coalgebra R B
a : A
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
⊢ comul (f a) = f a ⊗ₜ[R] f a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
⊢ Injective val

Tactic:
by

Goal state after:
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
hc : ∑ a ∈ s, c a • a = d • a
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
⊢ ∑ x ∈ s, ∑ y ∈ s, (if x = y then d * c x else 0) • x ⊗ₜ[R] y = d • ∑ x ∈ s, c x • x ⊗ₜ[R] x

Tactic:
by

Goal state after: