mathlib-initiative/mathlib-tactics huggingface dataset:
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:
ext

Goal state after:
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✝
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
⊢ (mapShortComplexH2 f 0).τ₃ = Hom.τ₃ 0

Tactic:
ext

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

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

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✝
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
⊢ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₁ =
    (𝟙
        { 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 := ⋯ }).τ₁

Tactic:
ext

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

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

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✝
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:
simpa [smulShortComplex, ModuleCat.epi_iff_surjective] using Submodule.mkQ_surjective _

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
⊢ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₂ =
    (𝟙
        { 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 := ⋯ }).τ₂

Tactic:
ext

Goal state after:
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✝
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
⊢ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₃ =
    (𝟙
        { 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 := ⋯ }).τ₃

Tactic:
ext

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

Goal state before:
pp: case refine_3
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) (φ ≫ resMap f ψ)).τ₃ = (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃

Tactic:
ext

Goal state after:
case refine_3
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 (mapShortComplexH2 (g.comp f) (φ ≫ resMap f ψ)).τ₃ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃ ∘ₗ lsingle a✝¹) x✝) a✝
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: case single_one_left
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))).comp singleOneAlgHom = (↑f).comp singleOneAlgHom

Tactic:
ext

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

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

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

Goal state after:
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✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : AddMonoid M
f g : Multiplicative 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.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:
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✝¹ : 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✝
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:
ext

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

case h_of
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✝ : M
⊢ Additive.toMul ((MonoidHom.toAdditiveRight ((↑((comulAlgHom S S[M]).comp (mapRingHom M f))).comp (of R M))) x✝) =
    Additive.toMul
      ((MonoidHom.toAdditiveRight
          ((↑((Algebra.TensorProduct.mapRingHom f (mapRingHom M f) (mapRingHom M f) ⋯ ⋯).comp
                  (comulAlgHom R R[M]).toRingHom)).comp
            (of R M)))
        x✝)
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:
ext

Goal state after:
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
⊢ (((counitAlgHom S S[M]).comp (mapRingHom M f)).comp singleZeroRingHom) x✝ =
    ((f.comp (counitAlgHom R R[M]).toRingHom).comp singleZeroRingHom) x✝

case h_of
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✝ : M
⊢ Additive.toMul ((MonoidHom.toAdditiveRight ((↑((counitAlgHom S S[M]).comp (mapRingHom M f))).comp (of R M))) x✝) =
    Additive.toMul ((MonoidHom.toAdditiveRight ((↑(f.comp (counitAlgHom R R[M]).toRingHom)).comp (of R M))) x✝)
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
⊢ p ∈ associatedPrimes R' M'

Tactic:
constructor

Goal state after:
case toIsPrime
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
⊢ p.IsPrime

case eq_radical_colon
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
⊢ ∃ x, p = (⊥.colon {x}).radical
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ˣ
⊢ (valuation K v) (↑(algebraMap R K) ↑x) ≤ ↑1 ∧ ¬(valuation K v) (↑(algebraMap R K) ↑x) < ↑1

Tactic:
constructor

Goal state after:
case left
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ˣ
⊢ (valuation K v) (↑(algebraMap R K) ↑x) ≤ ↑1

case right
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ˣ
⊢ ¬(valuation K v) (↑(algebraMap R K) ↑x) < ↑1
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
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
⊢ ⟨val✝, hx⟩ ∈ valuation.ker ↔ ⟨val✝, hx⟩ ∈ selmerGroup.subgroupOf selmerGroup

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
⊢ ⟨val✝, hx⟩ ∈ valuation.ker → ⟨val✝, hx⟩ ∈ selmerGroup.subgroupOf selmerGroup

case mpr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
⊢ ⟨val✝, hx⟩ ∈ selmerGroup.subgroupOf selmerGroup → ⟨val✝, hx⟩ ∈ valuation.ker
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
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker ↔
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker →
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range

case mpr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range →
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ dpow n 0 = ↑(#(∅.sym n))

Tactic:
· rw [dpow_eval_zero hn, eq_comm, ← cast_zero]
      apply congr_arg
      rw [card_eq_zero, sym_eq_empty]
      exact ⟨hn, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ (fun g ↦ g ∘ ⇑(RingCon.mkₐ R (ringCon R M))) ⇑f = (fun g ↦ g ∘ ⇑(RingCon.mkₐ R (ringCon R M))) ⇑g

Tactic:
simpa [← AlgHom.coe_comp] using MvPolynomial.algHom_ext fun ⟨n, m⟩ ↦ h n m

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case mk.mk
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
toRingHom✝¹ : A →+* B
ideal_comp✝¹ : map toRingHom✝¹ I ≤ J
dpow_comp✝¹ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝¹ a) = toRingHom✝¹ (hI.dpow n a)
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' : ⇑toRingHom✝¹ = ⇑toRingHom✝
⊢ toRingHom✝¹ = toRingHom✝

Tactic:
ext

Goal state after:
case mk.mk
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
toRingHom✝¹ : A →+* B
ideal_comp✝¹ : map toRingHom✝¹ I ≤ J
dpow_comp✝¹ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝¹ a) = toRingHom✝¹ (hI.dpow n a)
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' : ⇑toRingHom✝¹ = ⇑toRingHom✝
x✝ : A
⊢ toRingHom✝¹ x✝ = toRingHom✝ x✝
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
⊢ (lift hI g hg).toLinearMap ∘ₗ embed R M = g

Tactic:
ext

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
x✝ : M
⊢ ((lift hI g hg).toLinearMap ∘ₗ embed R M) x✝ = g x✝
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_4
inst✝⁵ : CommSemiring S
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module S N
f : M →ₗ[R] N
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S N
⊢ (map S f).toLinearMap ∘ₗ embed R M = ↑R (embed S N) ∘ₗ f

Tactic:
ext

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_4
inst✝⁵ : CommSemiring S
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module S N
f : M →ₗ[R] N
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S N
x✝ : M
⊢ ((map S f).toLinearMap ∘ₗ embed R M) x✝ = (↑R (embed S N) ∘ₗ f) x✝
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hn : ¬n = 0
⊢ 1 ≤ ↑p

Tactic:
exact_mod_cast Nat.Prime.one_le hp.elim

Goal state after: