mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

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

Tactic:
intro r

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h : p.contentIdeal = ⊤
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ C r ∣ p → IsUnit 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
x✝³ : M
x✝² : A
x✝¹ : M
x✝ : A
⊢ (((LinearMap.mul R A[M]).compr₂ counit ∘ₗ lsingle x✝³) x✝² ∘ₗ lsingle x✝¹) x✝ =
    (((LinearMap.mul R R).compl₁₂ counit counit ∘ₗ lsingle x✝³) x✝² ∘ₗ lsingle x✝¹) x✝

Tactic:
;

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

Tactic:
;

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

Tactic:
;

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

Tactic:
;

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
x✝ : R[M]
a✝ : O
⊢ ((mapDomainBialgHom R (f.comp g)) x✝).coeff a✝ = (((mapDomainBialgHom R f).comp (mapDomainBialgHom R g)) x✝).coeff a✝

Tactic:
;

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

Tactic:
;

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

Tactic:
;

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

Tactic:
;

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

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

Tactic:
;

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

Tactic:
;

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.RingTheory.Bialgebra.MonoidAlgebra

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

Tactic:
;

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.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : M
⊢ IsGroupLikeElem R ((fun x ↦ single x 1) g)

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : M
⊢ IsGroupLikeElem R ((fun x ↦ single x 1) g)
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
g : G
⊢ (mapDomainOfBialgHom (mapDomainBialgHom R f)) g = f g

Tactic:
;

Goal state after:
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
g : G
⊢ (mapDomainOfBialgHom (mapDomainBialgHom R f)) g = f g
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
g : G
⊢ (fun m ↦ single m 1) ((mapDomainOfBialgHom (mapDomainBialgHom R f)) g) = (fun m ↦ single m 1) (f g)

Tactic:
;

Goal state after:
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
g : G
⊢ (fun m ↦ single m 1) ((mapDomainOfBialgHom (mapDomainBialgHom R f)) g) = (fun m ↦ single m 1) (f g)
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
this :
  (ConcreteCategory.hom ((mapShortComplexH2 f φ).τ₂ ≫ (shortComplexH2 B).g)) x =
    (ConcreteCategory.hom ((shortComplexH2 A).g ≫ (mapShortComplexH2 f φ).τ₃)) x
⊢ (ModuleCat.Hom.hom (chainsMap₂ f φ)) x ∈ cycles₂ B

Tactic:
;

Goal state after:
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
this :
  (ConcreteCategory.hom ((mapShortComplexH2 f φ).τ₂ ≫ (shortComplexH2 B).g)) x =
    (ConcreteCategory.hom ((shortComplexH2 A).g ≫ (mapShortComplexH2 f φ).τ₃)) x
⊢ (ModuleCat.Hom.hom (chainsMap₂ f φ)) x ∈ cycles₂ B
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: case single_zero_right
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : 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)

Tactic:
;

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

Tactic:
;

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.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.intValuation.extendToLocalization ⋯ K) ↑x = ?m.34 * ?m.36

Tactic:
;

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
v : HeightOneSpectrum R
x : Kˣ
⊢ (v.intValuation.extendToLocalization ⋯ K) ↑x = ?m.34 * ?m.36
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
⊢ (valuation K v) ↑1 = ↑1

Tactic:
;

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
v : HeightOneSpectrum R
⊢ (valuation K v) ↑1 = ↑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
v : HeightOneSpectrum R
x✝¹ x✝ : Kˣ
⊢ (valuation K v) ↑(x✝¹ * x✝) = (valuation K v) ↑x✝¹ * (valuation K v) ↑x✝

Tactic:
;

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
v : HeightOneSpectrum R
x✝¹ x✝ : Kˣ
⊢ (valuation K v) ↑(x✝¹ * x✝) = (valuation K v) ↑x✝¹ * (valuation K v) ↑x✝
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ˣ
⊢ v.valuationOfNeZero x • ↑n = Multiplicative.toAdd (v.valuationOfNeZero x) * ↑n

Tactic:
;

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
v : HeightOneSpectrum R
n : ℕ
x : Kˣ
⊢ v.valuationOfNeZero x • ↑n = Multiplicative.toAdd (v.valuationOfNeZero x) * ↑n
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
        rintro _ ⟨x, rfl⟩
        exact
          ⟨v.valuationOfNeZero x, by simp only [powMonoidHom_apply, map_pow, Int.toAdd_pow]; rfl⟩

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
S S' : Set (HeightOneSpectrum R)
n : ℕ
x y : ↥selmerGroup
⊢ (fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑x * ((↑v).valuationOfNeZeroMod n) ↑y) =
    (fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑x) * fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑y

Tactic:
;

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
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x y : ↥selmerGroup
⊢ (fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑x * ((↑v).valuationOfNeZeroMod n) ↑y) =
    (fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑x) * fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑y
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribSMul.toLinearMap R M r)
⊢ map ((LinearMap.lsmul R M) r) ⊤ ⊓ N ≤ map ((LinearMap.lsmul R M) r) N ↔ r • ⊤ ⊓ N ≤ r • N

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribSMul.toLinearMap R M r)
⊢ map ((LinearMap.lsmul R M) r) ⊤ ⊓ N ≤ map ((LinearMap.lsmul R M) r) N ↔ r • ⊤ ⊓ N ≤ r • N
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M''
M''' : Type u_6
inst✝¹ : AddCommGroup M'''
inst✝ : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h : IsSMulRegular M''' r
this : IsSMulRegular (M'' ⧸ f₂.range) r
⊢ f₂.range ⊓ r • ⊤ ≤ r • f₂.range

Tactic:
inf_comm

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M''
M''' : Type u_6
inst✝¹ : AddCommGroup M'''
inst✝ : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h : IsSMulRegular M''' r
this : IsSMulRegular (M'' ⧸ f₂.range) r
⊢ r • ⊤ ⊓ f₂.range ≤ r • f₂.range
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < 0, Subsingleton (Ext N M i)
this : Nontrivial ↑M
⊢ [].length = 0 ∧ (∀ r ∈ [], r ∈ I) ∧ RingTheory.Sequence.IsRegular ↑M []

Tactic:
simp [isRegular_iff]

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
m : M
⊢ dp R 0 m = 1

Tactic:
by
  rw [dp_def, ← RingCon.coe_one]
  exact Quotient.sound <| RingCon.le_ringConGen _ _ Rel.zero

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

Goal state before:
pp: case dp.zero
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ (x * if k = 0 then 1 else 0) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
;

Goal state after:
case dp.zero
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ (x * if k = 0 then 1 else 0) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))