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
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↥(cycles₁ (res S.subtype (A.toCoinvariants S)))
hz :
  (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
w : ↑(ModuleCat.of k (G × G →₀ ↑(A.toCoinvariants S)))
hzw :
  (ModuleCat.Hom.hom (d₂₁ (A.toCoinvariants S))) w =
    ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) -
      ↑((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
Z : ↥S →₀ ↑A
hZ : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Z = ↑z
W : G × G →₀ ↑A
hW : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ W = w
b : G →₀ ↑A := ↑x + (ConcreteCategory.hom (d₂₁ A)) W - (lmapDomain (↑A) k ⇑S.subtype) Z
hb : ∀ (g : G), b g ∈ Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)
β : G →₀ ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)) :=
  mapRange (Function.invFun ⇑(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype) ⋯ b
hβb : mapRange Subtype.val ⋯ β = b
α : ↥S →₀ ↑A
hα :
  (ModuleCat.Hom.hom (shortComplexH1 A).pOpcycles ∘ₗ
        ModuleCat.Hom.hom (mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂)
      α =
    (ModuleCat.Hom.hom (shortComplexH1 A).pOpcycles ∘ₗ
        ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂)
      β
δ : G × G →₀ ↑A
hβ :
  (ModuleCat.Hom.hom (shortComplexH1 A).f) δ =
    (ModuleCat.Hom.hom (mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂) α -
      (ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂) β
⊢ (ConcreteCategory.hom (d₂₁ A)) (W + δ) = mapDomain Subtype.val (α + Z) - ↑x

Tactic:
by

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
α : (FractionRing A)ˣ
⊢ (IsFractionRing.map ⋯) ↑α ≠ 0

Tactic:
by

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
⊢ (toPrincipalIdeal A (FractionRing A)).range ≤
    Subgroup.comap (Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B))
      (toPrincipalIdeal B (FractionRing B)).range

Tactic:
by

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
α : (FractionalIdeal A⁰ (FractionRing A))ˣ
⊢ (extendedHom A B) ↑α = ↑((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) α)

Tactic:
by

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

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
C : Type u_3
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra B C
inst✝³ : Algebra A C
inst✝² : IsScalarTower A B C
inst✝¹ : Module.IsTorsionFree B C
inst✝ : Module.IsTorsionFree A C
I : ↥(Ideal A)⁰
⊢ extendedIdeal B C (extendedIdeal A B I) = extendedIdeal A C I

Tactic:
by

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✝ : IsDomain B
I : ↥(Ideal A)⁰
⊢ (extendedHom A B) (mk0 I) =
    (mk (FractionRing B))
      ((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) ((FractionalIdeal.mk0 (FractionRing A)) I))

Tactic:
by

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

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
C : Type u_3
inst✝⁷ : CommRing C
inst✝⁶ : Algebra B C
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A B C
inst✝³ : Module.IsTorsionFree B C
inst✝² : Module.IsTorsionFree A C
inst✝¹ : IsDedekindDomain C
inst✝ : IsDedekindDomain B
x : ClassGroup A
⊢ (extendedHom B C) ((extendedHom A B) x) = (extendedHom A C) x

Tactic:
by

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
C : Type u_3
inst✝⁷ : CommRing C
inst✝⁶ : Algebra B C
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A B C
inst✝³ : Module.IsTorsionFree B C
inst✝² : Module.IsTorsionFree A C
inst✝¹ : IsDedekindDomain C
inst✝ : IsDedekindDomain B
⊢ (extendedHom B C).comp (extendedHom A B) = extendedHom A C

Tactic:
by

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
h : ∀ (I : Ideal A), Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
I : ↥(Ideal A)⁰
⊢ Submodule.IsPrincipal ↑(extendedIdeal A B I)

Tactic:
by

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
h : ∀ (I : Ideal A), Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
⊢ extendedHom A B = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ contentIdeal 0 = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
h : p = 0
⊢ ∀ x ∈ ↑p.coeffs, x = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.contentIdeal = ⊥ ↔ p = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.coeff n ∈ p.contentIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ ((monomial n) r).contentIdeal = span {r}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
⊢ (C r).contentIdeal = span {r}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ contentIdeal 1 = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
this : span (↑(map f p).coeffs ∪ {0}) = span (⇑f '' ↑p.coeffs ∪ {0})
⊢ (map f p).contentIdeal = Ideal.map f p.contentIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ (map f p).contentIdeal = Ideal.map f p.contentIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).contentIdeal ≤ p.contentIdeal * q.contentIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p q : R[X]
hpq : p ∣ q
⊢ q.contentIdeal ≤ p.contentIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ C (Submodule.IsPrincipal.generator p.contentIdeal) ∣ p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
a✝ : span {Submodule.IsPrincipal.generator p.contentIdeal} ≤ span {r}
⊢ C r ∣ C (Submodule.IsPrincipal.generator p.contentIdeal)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ p.contentIdeal ≤ span {r} ↔ C r ∣ p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h : p.contentIdeal = ⊤
⊢ Submodule.IsPrincipal p.contentIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h : p.contentIdeal = ⊤
⊢ p.IsPrimitive

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ p.IsPrimitive ↔ p.contentIdeal = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p q : R[X]
h : (p * q).contentIdeal = ⊤
⊢ p.contentIdeal = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p q : R[X]
⊢ p.contentIdeal * q.contentIdeal ≤ (p * q).contentIdeal.radical

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
⊢ ⊤ = p.contentIdeal * q.contentIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
⊢ (p * q).contentIdeal = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.contentIdeal ≤ span {p.content}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ span {p.content} ≤ p.contentIdeal

Tactic:
rw [← p.contentIdeal.span_singleton_generator, span_singleton_le_span_singleton, content,
    Finset.dvd_gcd_iff]

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ ∀ b ∈ p.support, Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff b
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ p.contentIdeal = span {p.content}

Tactic:
by

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

Goal state after:
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
⊢ comul (single g 1) = single g 1 ⊗ₜ[R] single g 1

Tactic:
by

Goal state after:
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
x : A[G]
⊢ (Finsupp.linearCombination A fun y ↦ single y 1) x.coeff = x

Tactic:
by

Goal state after:
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
⊢ Submodule.span A (Set.range fun y ↦ single y 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✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
⊢ counit 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✝⁸ : 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
⊢ (LinearMap.mul R A[M]).compr₂ counit = (LinearMap.mul R R).compl₁₂ counit counit

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
⊢ comul 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✝⁸ : 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
⊢ (LinearMap.mul R A[M]).compr₂ comul = (LinearMap.mul R (A[M] ⊗[R] A[M])).compl₁₂ comul comul

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
f : M →* N
⊢ (counitAlgHom R R[N]).comp (mapDomainAlgHom R R f) = counitAlgHom R R[M]

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
f : M →* N
⊢ (Algebra.TensorProduct.map (mapDomainAlgHom R R f) (mapDomainAlgHom R R f)).comp (comulAlgHom R R[M]) =
    (comulAlgHom R R[N]).comp (mapDomainAlgHom R R f)

Tactic:
by

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
⊢ mapDomainBialgHom R (MonoidHom.id M) = BialgHom.id R R[M]

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
O : Type u_10
inst✝³ : CommSemiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : N →* O
g : M →* N
⊢ mapDomainBialgHom R (f.comp g) = (mapDomainBialgHom R f).comp (mapDomainBialgHom R g)

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
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]
⊢ (mapDomainBialgHom R f) ((mapDomainBialgHom R g) x) = (mapDomainBialgHom R (f.comp g)) x

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

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✝ : K
⊢ x✝ ∈ {x | ∀ v ∉ S, (HeightOneSpectrum.valuation K v) x ≤ 1} ↔
    x✝ ∈ ↑(⨅ v, ⨅ (_ : v ∉ S), (HeightOneSpectrum.valuation K v).valuationSubring.toSubring)

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
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:
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]
hp0 : ¬p = 0
⊢ p.support.Nonempty

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
⊢ ↑(S.integer K).toSubring = ↑(⨅ v, ⨅ (_ : v ∉ S), (HeightOneSpectrum.valuation K v).valuationSubring.toSubring)

Tactic:
by

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

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
⊢ Set.univ.integer K = ⊤

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
e : M ≃* N
⊢ (counitAlgHom R A[N]).comp ↑(domCongr R A e) = counitAlgHom R A[M]

Tactic:
by

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

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
⊢ ∅.integer K = ⊥

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
⊢ (H1CoresCoinf A S).Exact

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✝ : Kˣ
⊢ x✝ ∈ {x | ∀ v ∉ S, (HeightOneSpectrum.valuation K v) ↑x = 1} ↔
    x✝ ∈ ↑(⨅ v, ⨅ (_ : v ∉ S), (HeightOneSpectrum.valuation K v).valuationSubring.unitGroup)

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
e : M ≃* N
⊢ (Algebra.TensorProduct.map ↑(domCongr R A e) ↑(domCongr R A e)).comp (comulAlgHom R A[M]) =
    (comulAlgHom R A[N]).comp ↑(domCongr R A e)

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
inst✝ : Subsingleton M
r : R[M]
⊢ (algebraMap R R[M]) ((counitBialgHom R R[M]).toFun r) = r

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
⊢ ↑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✝⁸ : 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:
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]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
x✝ : ℕ
h1 : p.coeff x✝ ≠ 0
h2 : 1 ≤ (v.intAdicAbv hb) (p.coeff x✝)
⊢ x✝ ∈ p.support

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 : (↥(S.integer K))ˣ
v : HeightOneSpectrum R
hv : v ∉ S
⊢ (HeightOneSpectrum.valuation K v) ↑(Units.mk0 ↑↑x ⋯) * (HeightOneSpectrum.valuation K v) ↑x.inv = 1

Tactic:
by

Goal state after: