mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (((↑(Algebra.TensorProduct.assoc R R R (A ⧸ I) (A ⧸ I) (A ⧸ I))).comp
            ((Algebra.TensorProduct.map (comulAlgHom I) (AlgHom.id R (A ⧸ I))).comp (comulAlgHom I))).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap =
    (((Algebra.TensorProduct.map (AlgHom.id R (A ⧸ I)) (comulAlgHom I)).comp (comulAlgHom I)).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap

pp: case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (((Algebra.TensorProduct.map (counitAlgHom I) (AlgHom.id R (A ⧸ I))).comp (comulAlgHom I)).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap =
    ((↑(Algebra.TensorProduct.lid R (A ⧸ I)).symm).comp (Ideal.Quotient.mkₐ R I)).toLinearMap

pp: case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (((Algebra.TensorProduct.map (AlgHom.id R (A ⧸ I)) (counitAlgHom I)).comp (comulAlgHom I)).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap =
    ((↑(Algebra.TensorProduct.rid R R (A ⧸ I)).symm).comp (Ideal.Quotient.mkₐ R I)).toLinearMap

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (((↑(Algebra.TensorProduct.assoc R R R (A ⧸ I) (A ⧸ I) (A ⧸ I))).comp
            ((Algebra.TensorProduct.map (comulAlgHom I) (AlgHom.id R (A ⧸ I))).comp (comulAlgHom I))).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap =
    (((Algebra.TensorProduct.map (AlgHom.id R (A ⧸ I)) (comulAlgHom I)).comp (comulAlgHom I)).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap

case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (((Algebra.TensorProduct.map (counitAlgHom I) (AlgHom.id R (A ⧸ I))).comp (comulAlgHom I)).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap =
    ((↑(Algebra.TensorProduct.lid R (A ⧸ I)).symm).comp (Ideal.Quotient.mkₐ R I)).toLinearMap

case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (((Algebra.TensorProduct.map (AlgHom.id R (A ⧸ I)) (counitAlgHom I)).comp (comulAlgHom I)).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap =
    ((↑(Algebra.TensorProduct.rid R R (A ⧸ I)).symm).comp (Ideal.Quotient.mkₐ R I)).toLinearMap
Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (Algebra.TensorProduct.map algebraMapInv (AlgHom.id R (SymmetricAlgebra R M))).comp
      (lift
        ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)).flip 1 ∘ₗ ι R M +
          (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) 1 ∘ₗ ι R M)) =
    ↑(Algebra.TensorProduct.lid R (SymmetricAlgebra R M)).symm

Tactic:
by ext x; simp [algebraMapInv_ι]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (Algebra.TensorProduct.map (AlgHom.id R (SymmetricAlgebra R M)) algebraMapInv).comp
      (lift
        ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)).flip 1 ∘ₗ ι R M +
          (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) 1 ∘ₗ ι R M)) =
    ↑(Algebra.TensorProduct.rid R R (SymmetricAlgebra R M)).symm

Tactic:
by ext x; simp [algebraMapInv_ι]

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

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

pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
h : ¬r = 0
⊢ ((monomial n) r).contentIdeal = span {r}

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
h : r = 0
⊢ ((monomial n) r).contentIdeal = span {r}

case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
h : ¬r = 0
⊢ ((monomial n) r).contentIdeal = span {r}
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: case zero
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
⊢ counit ((domCongr R A e) 0) = counit 0

pp: case add
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✝ y✝ : A[M]
a✝¹ : counit ((domCongr R A e) x✝) = counit x✝
a✝ : counit ((domCongr R A e) y✝) = counit y✝
⊢ counit ((domCongr R A e) (x✝ + y✝)) = counit (x✝ + y✝)

pp: case single
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
m✝ : M
r✝ : A
⊢ counit ((domCongr R A e) (single m✝ r✝)) = counit (single m✝ r✝)

Tactic:
<;>

Goal state after:
case zero
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
⊢ counit ((domCongr R A e) 0) = counit 0

case add
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✝ y✝ : A[M]
a✝¹ : counit ((domCongr R A e) x✝) = counit x✝
a✝ : counit ((domCongr R A e) y✝) = counit y✝
⊢ counit ((domCongr R A e) (x✝ + y✝)) = counit (x✝ + y✝)

case single
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
m✝ : M
r✝ : A
⊢ counit ((domCongr R A e) (single m✝ r✝)) = counit (single m✝ r✝)
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
e : M ≃* N
m✝ : M
⊢ ((counitAlgHom R A[N]).comp ↑(domCongr R A e)) (single m✝ 1) = (counitAlgHom R A[M]) (single m✝ 1)

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

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
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.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✝ : M
⊢ ((counitAlgHom R (AddMonoidAlgebra A (Additive M))).comp ↑(toAdditiveAlgEquiv R A M)) (single m✝ 1) =
    (counitAlgHom R A[M]) (single m✝ 1)

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

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

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

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

Tactic:
<;>

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

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

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

Tactic:
<;>

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.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✝⁵ : 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)

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

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

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

Tactic:
<;>

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

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

Tactic:
<;>

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.DedekindDomain.SelmerGroup

Goal state before:
pp: 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

Tactic:
intro hx'

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
hx' : ⟨val✝, hx⟩ ∈ valuation.ker
⊢ ⟨val✝, hx⟩ ∈ selmerGroup.subgroupOf selmerGroup
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n 0 = 0

Tactic:
← MulZeroClass.mul_zero (0 : A),

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n (0 * 0) = 0 * 0
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case e'_2
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
⊢ AddSubgroup.map f (Ideal.ofList [] • ⊤).toAddSubgroup = AddSubgroup.map f ⊥

pp: case e'_3
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
⊢ (Ideal.ofList [] • ⊤).toAddSubgroup = ⊥

Tactic:
<;>

Goal state after:
case e'_2
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
⊢ AddSubgroup.map f (Ideal.ofList [] • ⊤).toAddSubgroup = AddSubgroup.map f ⊥

case e'_3
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
⊢ (Ideal.ofList [] • ⊤).toAddSubgroup = ⊥
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case pos
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))
h✝ : k = 0
⊢ x * 1 ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

pp: case neg
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))
h✝ : ¬k = 0
⊢ x * 0 ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
<;>

Goal state after:
case pos
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))
h✝ : k = 0
⊢ x * 1 ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

case neg
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))
h✝ : ¬k = 0
⊢ x * 0 ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))