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

Tactic:
ext

Goal state after:
case h₁
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x✝ : ↑(shortComplexH1 A).X₁
⊢ (ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (𝟙 A)).τ₁) x✝ =
    (ModuleCat.Hom.hom (𝟙 (shortComplexH1 A)).τ₁) x✝

case h₂
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x✝ : ↑(shortComplexH1 A).X₂
⊢ (ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (𝟙 A)).τ₂) x✝ =
    (ModuleCat.Hom.hom (𝟙 (shortComplexH1 A)).τ₂) x✝

case h₃
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x✝ : ↑(shortComplexH1 A).X₃
⊢ (ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (𝟙 A)).τ₃) x✝ =
    (ModuleCat.Hom.hom (𝟙 (shortComplexH1 A)).τ₃) x✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_1
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
⊢ (mapShortComplexH1 (g.comp f) (φ ≫ resMap f ψ)).τ₁ = (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₁

Tactic:
ext

Goal state after:
case refine_1
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
a✝¹ : G × G
x✝ : ↑A
a✝ : K × K
⊢ ((ModuleCat.Hom.hom (mapShortComplexH1 (g.comp f) (φ ≫ resMap f ψ)).τ₁ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₁ ∘ₗ lsingle a✝¹) x✝) a✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_2
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
⊢ (mapShortComplexH1 (g.comp f) (φ ≫ resMap f ψ)).τ₂ = (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₂

Tactic:
ext

Goal state after:
case refine_2
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
a✝¹ : G
x✝ : ↑A
a✝ : K
⊢ ((ModuleCat.Hom.hom (mapShortComplexH1 (g.comp f) (φ ≫ resMap f ψ)).τ₂ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₂ ∘ₗ lsingle a✝¹) x✝) a✝
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_2
τ : Type u_3
inst✝¹ : CommSemiring R
f : σ → τ
inst✝ : TendstoCofinite f
a : σ
⊢ (rename f).comp (toMvPowerSeries a) = toMvPowerSeries (f a)

Tactic:
ext

Goal state after:
R : Type u_1
σ : Type u_2
τ : Type u_3
inst✝¹ : CommSemiring R
f : σ → τ
inst✝ : TendstoCofinite f
a : σ
x✝ : R⟦X⟧
n✝ : τ →₀ ℕ
⊢ (coeff n✝) (((rename f).comp (toMvPowerSeries a)) x✝) = (coeff n✝) ((toMvPowerSeries (f a)) x✝)
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
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
⊢ (factorPow I hle).comp ((factorPow I ⋯).comp (f n✝)) = (factorPow I ⋯).comp (f m✝)

Tactic:
ext

Goal state after:
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
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
x✝ : R
⊢ ((factorPow I hle).comp ((factorPow I ⋯).comp (f n✝))) x✝ = ((factorPow I ⋯).comp (f m✝)) x✝
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
n : ℕ
⊢ (Ideal.Quotient.mk (I ^ a n)).comp (liftRingHom I ha f ⋯) = f n

Tactic:
ext

Goal state after:
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
n : ℕ
x✝ : R
⊢ ((Ideal.Quotient.mk (I ^ a n)).comp (liftRingHom I ha f ⋯)) x✝ = (f n) x✝
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:
ext

Goal state after:
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
i✝ : ι
a✝ : AdicCauchySequence I M
n✝ : ℕ
⊢ ↑(((((lsum (AdicCompletion I R)) fun i ↦ (algebraMap R (AdicCompletion I R)) (f i) • LinearMap.id) ∘ₗ
              ↑(finsuppLEquivDirectSum (AdicCompletion I R) (AdicCompletion I M) ι).symm) ∘ₗ
            DirectSum.lof (AdicCompletion I R) ι (fun i ↦ AdicCompletion I M) i✝)
          ((mk I M) a✝))
      n✝ =
    ↑((((map I ((lsum R) fun i ↦ f i • LinearMap.id) ∘ₗ map I ↑(finsuppLEquivDirectSum R M ι).symm) ∘ₗ
              ↑(sumEquivOfFintype I fun x ↦ M)) ∘ₗ
            DirectSum.lof (AdicCompletion I R) ι (fun i ↦ AdicCompletion I M) i✝)
          ((mk I M) a✝))
      n✝
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:
ext

Goal state after:
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
x✝ : A
⊢ x✝ ∈ IsUnit.submonoid A ↔ x✝ ∈ A⁰
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ Coalgebra R (C ⧸ I)

Tactic:
constructor

Goal state after:
case coassoc
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ ↑(TensorProduct.assoc R (C ⧸ I) (C ⧸ I) (C ⧸ I)) ∘ₗ rTensor (C ⧸ I) comul ∘ₗ comul = lTensor (C ⧸ I) comul ∘ₗ comul

case rTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ rTensor (C ⧸ I) counit ∘ₗ comul = (TensorProduct.mk R R (C ⧸ I)) 1

case lTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ lTensor (C ⧸ I) counit ∘ₗ comul = (TensorProduct.mk R (C ⧸ I) R).flip 1
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:
constructor

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

case mpr
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ C r ∣ p → p.contentIdeal ≤ span {r}
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:
ext

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

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

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

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

Goal state after:
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.comp g)) x✝).coeff a✝ = (((mapDomainBialgHom R f).comp (mapDomainBialgHom R g)) x✝).coeff a✝
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:
ext

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

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

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

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✝
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:
ext

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : K
⊢ x✝ ∈ Set.univ.integer K ↔ x✝ ∈ ⊤
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case neg
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
⊢ (p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)) < 1 ↔ ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1

Tactic:
constructor

Goal state after:
case neg.mp
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
⊢ (p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)) < 1 → ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1

case neg.mpr
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 ∈ p.coeffs, (v.intAdicAbv hb) x < 1) → (p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)) < 1
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:
ext

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

Goal state after:
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 := ⋯ })
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:
ext

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

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

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✝
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
⊢ (mapShortComplexH2 f 0).τ₁ = Hom.τ₁ 0

Tactic:
ext

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

Goal state after:
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✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
f g : M →* A
m✝ : M
⊢ (((lift R A M).trans (WithConv.equiv (R[M] →ₐ[R] A)).symm).toFun (f * g)).ofConv (single m✝ 1) =
    (((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).ofConv
      (single m✝ 1)
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
⊢ (mapShortComplexH2 f 0).τ₂ = Hom.τ₂ 0

Tactic:
ext

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