mathlib-initiative/mathlib-tactics huggingface dataset:
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
w : G
⊢ w ∈ ↑((v.sum fun a b ↦ single ((s ↑a)⁻¹ * a) ((A.ρ (s ↑a)⁻¹) b)) + v.sum fun a ↦ single (s ↑a)).support → w ∈ ↑S

Tactic:
hw

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
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
w : G
hw : w ∈ ↑((v.sum fun a b ↦ single ((s ↑a)⁻¹ * a) ((A.ρ (s ↑a)⁻¹) b)) + v.sum fun a ↦ single (s ↑a)).support
⊢ w ∈ ↑S
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:
simp

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:
simp

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:
simp

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
⊢ (TensorProduct.map ↑f ↑f) (a ⊗ₜ[R] a) = f a ⊗ₜ[R] f a

Tactic:
simp

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

Goal state before:
pp: case empty
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
hs : ↑∅ ⊆ {a | IsGroupLikeElem R a}
⊢ LinearIndepOn R id ↑∅

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (↑((↑(Algebra.TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M))).comp
            (Bialgebra.comulAlgHom R (SymmetricAlgebra R M))) ∘ₗ
        ι R M)
      x =
    (↑(Bialgebra.comulAlgHom R (SymmetricAlgebra R M)) ∘ₗ ι R M) x

Tactic:
simp

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ 1 ⊗ₜ[R] (ι R M) x + (ι R M) x ⊗ₜ[R] 1 = (ι R M) x ⊗ₜ[R] 1 + 1 ⊗ₜ[R] (ι R M) x
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
x✝³ : M
x✝² : A
x✝¹ : M
x✝ : A
⊢ (((LinearMap.mul R A[M]).compr₂ counit ∘ₗ lsingle x✝³) x✝² ∘ₗ lsingle x✝¹) x✝ =
    (((LinearMap.mul R R).compl₁₂ counit counit ∘ₗ lsingle x✝³) x✝² ∘ₗ lsingle x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: case single_one_right
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* N
m✝ : M
⊢ ((counitAlgHom R R[N]).comp (mapDomainAlgHom R R f)) (single m✝ 1) = (counitAlgHom R R[M]) (single m✝ 1)

Tactic:
simp

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

Goal state before:
pp: case single_one_right
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* N
m✝ : M
⊢ ((Algebra.TensorProduct.map (mapDomainAlgHom R R f) (mapDomainAlgHom R R f)).comp (comulAlgHom R R[M]))
      (single m✝ 1) =
    ((comulAlgHom R R[N]).comp (mapDomainAlgHom R R f)) (single m✝ 1)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommSemiring R
inst✝ : Monoid M
x✝ : R[M]
a✝ : M
⊢ ((mapDomainBialgHom R (MonoidHom.id M)) x✝).coeff a✝ = ((BialgHom.id R R[M]) x✝).coeff a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_8
N : Type u_9
O : Type u_10
inst✝³ : CommSemiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : N →* O
g : M →* N
x : R[M]
a✝ : O
⊢ ((mapDomainBialgHom R f) ((mapDomainBialgHom R g) x)).coeff a✝ = ((mapDomainBialgHom R (f.comp g)) x).coeff a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : K
⊢ x✝ ∈ ↑(S.integer K).toSubring ↔
    x✝ ∈ ↑(⨅ v, ⨅ (_ : v ∉ S), (HeightOneSpectrum.valuation K v).valuationSubring.toSubring)

Tactic:
simp

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

Goal state before:
pp: case single_one_right
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
m✝ : M
⊢ ((counitAlgHom R A[N]).comp ↑(domCongr R A e)) (single m✝ 1) = (counitAlgHom R A[M]) (single m✝ 1)

Tactic:
simp

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

Goal state before:
pp: case single_one_left
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
x✝ : A
⊢ (((counitAlgHom R A[N]).comp ↑(domCongr R A e)).comp singleOneAlgHom) x✝ =
    ((counitAlgHom R A[M]).comp singleOneAlgHom) x✝

Tactic:
simp

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

Goal state before:
pp: case single_one_right
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
a : M
⊢ ((Algebra.TensorProduct.map ↑(domCongr R A e) ↑(domCongr R A e)).comp (comulAlgHom R A[M])) (single a 1) =
    ((comulAlgHom R A[N]).comp ↑(domCongr R A e)) (single a 1)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
⊢ ↑1 = 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
⊢ ∀ (x y : GroupLike R A), ↑(x * y) = ↑x * ↑y

Tactic:
simp

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

Goal state before:
pp: case single_one_right
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
m✝ : GroupLike R A
⊢ ((counitAlgHom R A).comp ((lift R A (GroupLike R A)) { toFun := fun g ↦ ↑g, map_one' := ⋯, map_mul' := ⋯ }))
      (single m✝ 1) =
    (counitAlgHom R R[GroupLike R A]) (single m✝ 1)

Tactic:
simp

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

Goal state before:
pp: case single_one_right
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
m✝ : GroupLike R A
⊢ ((Algebra.TensorProduct.map ((lift R A (GroupLike R A)) { toFun := fun g ↦ ↑g, map_one' := ⋯, map_mul' := ⋯ })
            ((lift R A (GroupLike R A)) { toFun := fun g ↦ ↑g, map_one' := ⋯, map_mul' := ⋯ })).comp
        (comulAlgHom R R[GroupLike R A]))
      (single m✝ 1) =
    ((comulAlgHom R A).comp ((lift R A (GroupLike R A)) { toFun := fun g ↦ ↑g, map_one' := ⋯, map_mul' := ⋯ }))
      (single m✝ 1)

Tactic:
simp

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

Goal state before:
pp: case single_one_right
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
m✝ : M
⊢ ((counitAlgHom R (AddMonoidAlgebra A (Additive M))).comp ↑(toAdditiveAlgEquiv R A M)) (single m✝ 1) =
    (counitAlgHom R A[M]) (single m✝ 1)

Tactic:
simp

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

Goal state before:
pp: case single_one_left
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
x✝ : A
⊢ (((counitAlgHom R (AddMonoidAlgebra A (Additive M))).comp ↑(toAdditiveAlgEquiv R A M)).comp singleOneAlgHom) x✝ =
    ((counitAlgHom R A[M]).comp singleOneAlgHom) x✝

Tactic:
simp

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

Goal state before:
pp: case single_one_right
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
a : M
⊢ ((Algebra.TensorProduct.map ↑(toAdditiveAlgEquiv R A M) ↑(toAdditiveAlgEquiv R A M)).comp (comulAlgHom R A[M]))
      (single a 1) =
    ((comulAlgHom R (AddMonoidAlgebra A (Additive M))).comp ↑(toAdditiveAlgEquiv R A M)) (single a 1)

Tactic:
simp

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

Goal state before:
pp: case refine_1
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✝¹ : G × G × G
x✝ : ↑A
a✝ : H × H × H
⊢ ((ModuleCat.Hom.hom (mapShortComplexH2 f 0).τ₁ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom (Hom.τ₁ 0) ∘ₗ lsingle a✝¹) x✝) a✝

Tactic:
simp

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

Goal state before:
pp: case refine_2
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✝¹ : G × G
x✝ : ↑A
a✝ : H × H
⊢ ((ModuleCat.Hom.hom (mapShortComplexH2 f 0).τ₂ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom (Hom.τ₂ 0) ∘ₗ lsingle a✝¹) x✝) a✝

Tactic:
simp

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

Goal state before:
pp: case single_one_right
R : Type u_1
M : Type u_8
N : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : M →* N
m✝ : M
a✝ : N
⊢ ((mapDomainBialgHom R (f * g)) (single m✝ 1)).coeff a✝ =
    ((toConv (mapDomainBialgHom R f) * toConv (mapDomainBialgHom R g)).ofConv (single m✝ 1)).coeff a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : R →+* S
⊢ (mapRingHom M f).comp (algebraMap R R[M]) = (algebraMap S S[M]).comp f

Tactic:
simp

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

Goal state before:
pp: case refine_3
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✝¹ : G
x✝ : ↑A
a✝ : H
⊢ ((ModuleCat.Hom.hom (mapShortComplexH2 f 0).τ₃ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom (Hom.τ₃ 0) ∘ₗ lsingle a✝¹) x✝) a✝

Tactic:
simp

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

Goal state before:
pp: case h₁
R : Type u_1
S : Type u_2
M : Type u_8
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommMonoid M
f : R →+* S
x✝ : R
⊢ (((comulAlgHom S S[M]).comp (mapRingHom M f)).comp singleOneRingHom) x✝ =
    (((Algebra.TensorProduct.mapRingHom f (mapRingHom M f) (mapRingHom M f) ⋯ ⋯).comp
            (comulAlgHom R R[M]).toRingHom).comp
        singleOneRingHom)
      x✝

Tactic:
simp

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

Goal state before:
pp: case h_of
R : Type u_1
S : Type u_2
M : Type u_8
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommMonoid M
f : R →+* S
x✝ : M
⊢ ((↑((comulAlgHom S S[M]).comp (mapRingHom M f))).comp (of R M)) x✝ =
    ((↑((Algebra.TensorProduct.mapRingHom f (mapRingHom M f) (mapRingHom M f) ⋯ ⋯).comp
              (comulAlgHom R R[M]).toRingHom)).comp
        (of R M))
      x✝

Tactic:
simp

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

Goal state before:
pp: case refine_1
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
a✝¹ : G × G × G
x✝ : ↑A
a✝ : G × G × G
⊢ ((ModuleCat.Hom.hom (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₁ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom
            (𝟙
                { X₁ := ModuleCat.of k (G × G × G →₀ ↑A), X₂ := ModuleCat.of k (G × G →₀ ↑A),
                  X₃ := ModuleCat.of k (G →₀ ↑A), f := d₃₂ A, g := d₂₁ A, zero := ⋯ }).τ₁ ∘ₗ
          lsingle a✝¹)
        x✝)
      a✝

Tactic:
simp

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

Goal state before:
pp: case h₁
R : Type u_1
S : Type u_2
M : Type u_8
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommMonoid M
f : R →+* S
x✝ : R
⊢ (((counitAlgHom S S[M]).comp (mapRingHom M f)).comp singleOneRingHom) x✝ =
    ((f.comp (counitAlgHom R R[M]).toRingHom).comp singleOneRingHom) x✝

Tactic:
simp

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

Goal state before:
pp: case h_of
R : Type u_1
S : Type u_2
M : Type u_8
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommMonoid M
f : R →+* S
x✝ : M
⊢ ((↑((counitAlgHom S S[M]).comp (mapRingHom M f))).comp (of R M)) x✝ =
    ((↑(f.comp (counitAlgHom R R[M]).toRingHom)).comp (of R M)) x✝

Tactic:
simp

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

Goal state before:
pp: case refine_2
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
a✝¹ : G × G
x✝ : ↑A
a✝ : G × G
⊢ ((ModuleCat.Hom.hom (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₂ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom
            (𝟙
                { X₁ := ModuleCat.of k (G × G × G →₀ ↑A), X₂ := ModuleCat.of k (G × G →₀ ↑A),
                  X₃ := ModuleCat.of k (G →₀ ↑A), f := d₃₂ A, g := d₂₁ A, zero := ⋯ }).τ₂ ∘ₗ
          lsingle a✝¹)
        x✝)
      a✝

Tactic:
simp

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

Goal state before:
pp: case refine_3
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
a✝¹ : G
x✝ : ↑A
a✝ : G
⊢ ((ModuleCat.Hom.hom (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₃ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom
            (𝟙
                { X₁ := ModuleCat.of k (G × G × G →₀ ↑A), X₂ := ModuleCat.of k (G × G →₀ ↑A),
                  X₃ := ModuleCat.of k (G →₀ ↑A), f := d₃₂ A, g := d₂₁ A, zero := ⋯ }).τ₃ ∘ₗ
          lsingle a✝¹)
        x✝)
      a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[G] →ₐc[R] R[H]
g₁ g₂ : G
⊢ f (single g₁ 1) * f (single g₂ 1) = single (mapDomainOfBialgHomFun f g₁) 1 * single (mapDomainOfBialgHomFun f g₂) 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f g : G →* H
⊢ (mapDomainBialgHomEquiv.trans (WithConv.equiv (R[G] →ₐc[R] R[H])).symm).toFun (f * g) =
    (mapDomainBialgHomEquiv.trans (WithConv.equiv (R[G] →ₐc[R] R[H])).symm).toFun f *
      (mapDomainBialgHomEquiv.trans (WithConv.equiv (R[G] →ₐc[R] R[H])).symm).toFun g

Tactic:
simp

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
⊢ mapCycles₂ f φ ≫ (shortComplexH2 B).moduleCatLeftHomologyData.i =
    (shortComplexH2 A).moduleCatLeftHomologyData.i ≫ chainsMap₂ f φ

Tactic:
simp

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

Goal state before:
pp: case single_zero_right
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Bialgebra R A
inst✝² : Bialgebra R B
inst✝¹ : AddMonoid M
inst✝ : AddMonoid N
m✝ : M
⊢ ((counitAlgHom R (MonoidAlgebra A (Multiplicative M))).comp ↑(toMultiplicativeAlgEquiv R A M)) (single m✝ 1) =
    (counitAlgHom R A[M]) (single m✝ 1)

Tactic:
simp

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

Goal state before:
pp: case single_zero_left
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Bialgebra R A
inst✝² : Bialgebra R B
inst✝¹ : AddMonoid M
inst✝ : AddMonoid N
x✝ : A
⊢ (((counitAlgHom R (MonoidAlgebra A (Multiplicative M))).comp ↑(toMultiplicativeAlgEquiv R A M)).comp singleZeroAlgHom)
      x✝ =
    ((counitAlgHom R A[M]).comp singleZeroAlgHom) x✝

Tactic:
simp

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

Goal state before:
pp: case single_zero_right
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Bialgebra R A
inst✝² : Bialgebra R B
inst✝¹ : AddMonoid M
inst✝ : AddMonoid N
a : M
⊢ ((Algebra.TensorProduct.map ↑(toMultiplicativeAlgEquiv R A M) ↑(toMultiplicativeAlgEquiv R A M)).comp
        (comulAlgHom R A[M]))
      (single a 1) =
    ((comulAlgHom R (MonoidAlgebra A (Multiplicative M))).comp ↑(toMultiplicativeAlgEquiv R A M)) (single a 1)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : R →+* S
x✝ : R
a✝ : M
⊢ (((mapRingHom M f).comp (algebraMap R R[M])) x✝).coeff a✝ = (((algebraMap S S[M]).comp f) x✝).coeff a✝

Tactic:
simp

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

Goal state before:
pp: case h₁
R : Type u_1
S : Type u_2
M : Type u_8
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : AddCommMonoid M
f : R →+* S
x✝ : R
⊢ (((comulAlgHom S S[M]).comp (mapRingHom M f)).comp singleZeroRingHom) x✝ =
    (((Algebra.TensorProduct.mapRingHom f (mapRingHom M f) (mapRingHom M f) ⋯ ⋯).comp
            (comulAlgHom R R[M]).toRingHom).comp
        singleZeroRingHom)
      x✝

Tactic:
simp

Goal state after: