mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (counitAlgHom R A).comp ((lift R A (GroupLike R A)) { toFun := fun g ↦ ↑g, map_one' := ⋯, map_mul' := ⋯ }) =
    counitAlgHom R R[GroupLike R A]

Tactic:
by

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✝¹ x✝ : ↥(S.unit K)
⊢ { val := ⟨↑↑(x✝¹ * x✝), ⋯⟩, inv := ⟨↑(↑(x✝¹ * x✝))⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ } =
    { val := ⟨↑↑x✝¹, ⋯⟩, inv := ⟨↑(↑x✝¹)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ } *
      { val := ⟨↑↑x✝, ⋯⟩, inv := ⟨↑(↑x✝)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }

Tactic:
by

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
⊢ (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]) =
    (comulAlgHom R A).comp ((lift R A (GroupLike R A)) { toFun := fun g ↦ ↑g, map_one' := ⋯, map_mul' := ⋯ })

Tactic:
by

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
⊢ (counitAlgHom R (AddMonoidAlgebra A (Additive M))).comp ↑(toAdditiveAlgEquiv R A M) = counitAlgHom R A[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 : ℕ
⊢ chainsMap₃ f φ ≫ (shortComplexH2 B).f = (shortComplexH2 A).f ≫ chainsMap₂ f φ

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 : ℕ
⊢ chainsMap₂ f φ ≫ (shortComplexH2 B).g = (shortComplexH2 A).g ≫ chainsMap₁ f φ

Tactic:
by

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

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

Tactic:
by

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
⊢ (Algebra.TensorProduct.map ↑(toAdditiveAlgEquiv R A M) ↑(toAdditiveAlgEquiv R A M)).comp (comulAlgHom R A[M]) =
    (comulAlgHom R (AddMonoidAlgebra A (Additive M))).comp ↑(toAdditiveAlgEquiv R A M)

Tactic:
by

Goal state after:
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✝² : Semiring A
inst✝¹ : Bialgebra R A
inst✝ : Monoid M
m : M
a : A
⊢ (toAdditiveBialgEquiv R A M) (single m a) = AddMonoidAlgebra.single (Additive.ofMul m) a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
b : NNReal
hb : 1 < b
p : R[X]
hR : ¬IsField R
⊢ p.contentIdeal = ⊤ ↔ ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1

Tactic:
by

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✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
f g : M →* A
⊢ ((lift R A M).trans (WithConv.equiv (R[M] →ₐ[R] A)).symm).toFun (f * g) =
    ((lift R A M).trans (WithConv.equiv (R[M] →ₐ[R] A)).symm).toFun f *
      ((lift R A M).trans (WithConv.equiv (R[M] →ₐ[R] A)).symm).toFun g

Tactic:
by

Goal state after:
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✝¹ : Algebra R A
inst✝ : Monoid M
f g : WithConv (R[M] →ₐ[R] A)
x : M
⊢ (f * g).ofConv (single x 1) = f.ofConv (single x 1) * g.ofConv (single x 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
hR : ¬IsField R
b : NNReal
hb : 1 < b
p : R[X]
⊢ p.IsPrimitive ↔ ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1

Tactic:
by

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

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

Goal state before:
pp: 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
⊢ mapDomainBialgHom R (f * g) = (toConv (mapDomainBialgHom R f) * toConv (mapDomainBialgHom R g)).ofConv

Tactic:
by

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:
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
⊢ mapShortComplexH2 f 0 = 0

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Regular.Category

Goal state before:
pp: R : Type u
inst✝² : CommRing R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
⊢ Function.Exact ⇑((lsmul R M) r) ⇑(r • ⊤).mkQ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Regular.Category

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
r : R
⊢ Epi (M.smulShortComplex r).g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Regular.Category

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
r : R
reg : IsSMulRegular (↑M) r
⊢ Mono (M.smulShortComplex r).f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
h : x ∉ Set.range fun x ↦ single x 1
⊢ insert x (Set.range fun x ↦ single x 1) ⊆ {a | IsGroupLikeElem R a}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
h : x ∉ Set.range fun x ↦ single x 1
this : LinearIndepOn R id (insert x (Set.range fun x ↦ single x 1))
⊢ x.coeff.sum single ∉ span R (Set.range fun x ↦ single x 1)

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
⊢ mapShortComplexH2 (MonoidHom.id G) (𝟙 A) = 𝟙 (shortComplexH2 A)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
⊢ x ∈ Set.range fun x ↦ single x 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
⊢ (x ∈ Set.range fun x ↦ single x 1) → IsGroupLikeElem R x

Tactic:
by

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]
⊢ (fun m ↦ single m 1) (mapDomainOfBialgHomFun f 1) = (fun m ↦ single m 1) 1

Tactic:
by

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
⊢ mapDomainOfBialgHomFun f (g₁ * g₂) = mapDomainOfBialgHomFun f g₁ * mapDomainOfBialgHomFun f g₂

Tactic:
by

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

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
g : G
r : R
⊢ single ((mapDomainOfBialgHom f) g) r = f (single g r)

Tactic:
by

Goal state after:
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
⊢ mapShortComplexH2 (g.comp f) (φ ≫ (resFunctor f).map ψ) = mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
⊢ mapDomainBialgHom R (mapDomainOfBialgHom f) = f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ mapDomainOfBialgHom (mapDomainBialgHom R f) = f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
G : Type u_5
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Group G
⊢ mapDomainOfBialgHom (BialgHom.id R R[G]) = MonoidHom.id G

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 : ℕ
x : ↑(ModuleCat.of k (G × G →₀ ↑A))
x✝ : x ∈ cycles₂ A
⊢ (ModuleCat.Hom.hom (chainsMap₂ f φ)) x ∈ cycles₂ B

Tactic:
by

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

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[H] →ₐc[R] R[I]
g : R[G] →ₐc[R] R[H]
⊢ mapDomainOfBialgHom (f.comp g) = (mapDomainOfBialgHom f).comp (mapDomainOfBialgHom g)

Tactic:
by

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

Goal state after:
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
⊢ mapCycles₂ (g.comp f) (φ ≫ (resFunctor f).map ψ) = mapCycles₂ f φ ≫ mapCycles₂ g ψ

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

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
⊢ cyclesMap f φ 2 ≫ (isoCycles₂ B).hom = (isoCycles₂ A).hom ≫ mapCycles₂ f φ

Tactic:
by

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✝¹ : AddMonoid M
inst✝ : AddMonoid N
⊢ (counitAlgHom R (MonoidAlgebra A (Multiplicative M))).comp ↑(toMultiplicativeAlgEquiv R A M) = counitAlgHom R A[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
⊢ H2π A ≫ map f φ 2 = mapCycles₂ f φ ≫ H2π B

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✝ n : ℕ
A : Rep k G
⊢ map (MonoidHom.id G) (𝟙 A) n = 𝟙 (groupHomology A n)

Tactic:
by

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✝¹ : AddMonoid M
inst✝ : AddMonoid N
⊢ (Algebra.TensorProduct.map ↑(toMultiplicativeAlgEquiv R A M) ↑(toMultiplicativeAlgEquiv R A M)).comp
      (comulAlgHom R A[M]) =
    (comulAlgHom R (MonoidAlgebra A (Multiplicative M))).comp ↑(toMultiplicativeAlgEquiv R A 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✝ n : ℕ
X✝ Y✝ Z✝ : Rep k G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ map (MonoidHom.id G) (f ≫ g) n = map (MonoidHom.id G) f n ≫ map (MonoidHom.id G) g n

Tactic:
by

Goal state after:
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✝² : Semiring A
inst✝¹ : Bialgebra R A
inst✝ : AddMonoid M
m : M
a : A
⊢ (toMultiplicativeBialgEquiv R A M) (single m a) = MonoidAlgebra.single (Multiplicative.ofAdd m) 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✝ n : ℕ
x✝¹ x✝ : Rep k G
⊢ (functor k G n).map 0 = 0

Tactic:
by

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✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : AddMonoid M
f g : Multiplicative M →* A
⊢ ((lift R A M).trans (WithConv.equiv (R[M] →ₐ[R] A)).symm).toFun (f * g) =
    ((lift R A M).trans (WithConv.equiv (R[M] →ₐ[R] A)).symm).toFun f *
      ((lift R A M).trans (WithConv.equiv (R[M] →ₐ[R] A)).symm).toFun g

Tactic:
by

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
⊢ (mapRingHom M f).comp (algebraMap R R[M]) = (algebraMap S S[M]).comp f

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✝ n : ℕ
X Y : Rep k H
φ : X ⟶ Y
⊢ (resFunctor f ⋙ functor k G n).map φ ≫ map f (𝟙 (res f Y)) n = map f (𝟙 (res f X)) n ≫ (functor k H n).map φ

Tactic:
by

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

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

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
n : ℕ
X Y : Rep k G
φ : X ⟶ Y
⊢ (functor k G n).map φ ≫ map (QuotientGroup.mk' S) (Y.toCoinvariantsMkQ S) n =
    map (QuotientGroup.mk' S) (X.toCoinvariantsMkQ S) n ≫
      (quotientToCoinvariantsFunctor k S ⋙ functor k (G ⧸ S) n).map φ

Tactic:
by

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

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

Tactic:
by

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✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
f g : G →+ H
⊢ (mapDomainBialgHomEquiv.trans ((WithConv.equiv (R[G] →ₐc[R] R[H])).symm.trans Additive.ofMul)).toFun (f + g) =
    (mapDomainBialgHomEquiv.trans ((WithConv.equiv (R[G] →ₐc[R] R[H])).symm.trans Additive.ofMul)).toFun f +
      (mapDomainBialgHomEquiv.trans ((WithConv.equiv (R[G] →ₐc[R] R[H])).symm.trans Additive.ofMul)).toFun g

Tactic:
by

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

Goal state before:
pp: R : Type u_11
inst✝² : CommSemiring R
A : Type u_12
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
n : ℤ
⊢ comul (T n) = T n ⊗ₜ[R] T n

Tactic:
by

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

Goal state before:
pp: R : Type u_11
inst✝² : CommSemiring R
A : Type u_12
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
n : ℤ
⊢ counit (T n) = 1

Tactic:
by

Goal state after:
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 : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) = (valuation K v) ↑x

Tactic:
by

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

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

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

Goal state after:
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:
by
  rw [← WithZero.coe_inj, valuationOfNeZero_eq, Units.coe_map, eq_iff_le_not_lt]
  constructor
  · exact v.valuation_le_one x
  · 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: 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
n : ℕ
x : Kˣ
⊢ (fun x ↦ x • ↑n) (v.valuationOfNeZero x) = Multiplicative.toAdd (v.valuationOfNeZero ((powMonoidHom n) x))

Tactic:
by

Goal state after:
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
n : ℕ
⊢ (powMonoidHom n).range ≤ Subgroup.comap v.valuationOfNeZero (AddSubgroup.toSubgroup (AddSubgroup.zmultiples ↑n))

Tactic:
by

Goal state after: