mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
ext

Goal state after:
case h1
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ (a * b)⁻¹.fst = (b⁻¹ * a⁻¹).fst

case h2
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ (a * b)⁻¹.snd = (b⁻¹ * a⁻¹).snd
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ counit ∘ₗ inr R A B = counit

Tactic:
ext

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : B
⊢ (counit ∘ₗ inr R A B) x✝ = counit x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ counit ∘ₗ inl R A B = counit

Tactic:
ext

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (counit ∘ₗ inl R A B) x✝ = counit x✝
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
⊢ (-x)⁻¹ = -x⁻¹

Tactic:
ext

Goal state after:
case h1
R : Type u
M : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
⊢ (-x)⁻¹.fst = (-x⁻¹).fst

case h2
R : Type u
M : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
⊢ (-x)⁻¹.snd = (-x⁻¹).snd
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
f g : R →ₗc[R] A
h : f 1 = g 1
⊢ (fun x ↦ ↑x) f = (fun x ↦ ↑x) g

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
f g : R →ₗc[R] A
h : f 1 = g 1
⊢ ((fun x ↦ ↑x) f) 1 = ((fun x ↦ ↑x) g) 1
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
f : A →ₗc[R] B
f' : A → B
h : f' = ⇑f
⊢ counit ∘ₗ (↑f).copy f' h = counit

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
f : A →ₗc[R] B
f' : A → B
h : f' = ⇑f
x✝ : A
⊢ (counit ∘ₗ (↑f).copy f' h) x✝ = counit x✝
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
⊢ counit ∘ₗ LinearMap.id = counit

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
x✝ : A
⊢ (counit ∘ₗ LinearMap.id) x✝ = counit x✝
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ₁ : B →ₗc[R] C
φ₂ : A →ₗc[R] B
⊢ counit ∘ₗ ↑φ₁ ∘ₗ ↑φ₂ = counit

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ₁ : B →ₗc[R] C
φ₂ : A →ₗc[R] B
x✝ : A
⊢ (counit ∘ₗ ↑φ₁ ∘ₗ ↑φ₂) x✝ = counit x✝
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ₁ : B →ₗc[R] C
φ₂ : A →ₗc[R] B
⊢ map (↑φ₁ ∘ₗ ↑φ₂) (↑φ₁ ∘ₗ ↑φ₂) ∘ₗ comul = comul ∘ₗ ↑φ₁ ∘ₗ ↑φ₂

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ₁ : B →ₗc[R] C
φ₂ : A →ₗc[R] B
x✝ : A
⊢ (map (↑φ₁ ∘ₗ ↑φ₂) (↑φ₁ ∘ₗ ↑φ₂) ∘ₗ comul) x✝ = (comul ∘ₗ ↑φ₁ ∘ₗ ↑φ₂) x✝
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ counit ∘ₗ counit = counit

Tactic:
ext

Goal state after:
R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (counit ∘ₗ counit) x✝ = counit x✝
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ map counit counit ∘ₗ comul = comul ∘ₗ counit

Tactic:
ext

Goal state after:
R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (map counit counit ∘ₗ comul) x✝ = (comul ∘ₗ counit) x✝
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ f (r₁ * r₂) + (g (m₁ <• r₂) + g (r₁ •> m₂)) = f (r₁ * r₂) + (g m₁ * f r₂ + f r₁ * g m₂)

Tactic:
hfg,

Goal state after:
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ f (r₁ * r₂) + (g (m₁ <• r₂) + f r₁ * g m₂) = f (r₁ * r₂) + (g m₁ * f r₂ + f r₁ * g m₂)
Module: Mathlib.RingTheory.Bialgebra.Basic

Goal state before:
pp: R✝ : Type u
A✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Bialgebra R✝ A✝
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : Coalgebra R A
counit_one : counit 1 = 1
counit_mul : ∀ {a b : A}, counit (a * b) = counit a * counit b
comul_one : comul 1 = 1
comul_mul : ∀ {a b : A}, comul (a * b) = comul a * comul b
⊢ (LinearMap.mul R A).compr₂ counit = (LinearMap.mul R R).compl₁₂ counit counit

Tactic:
ext

Goal state after:
R✝ : Type u
A✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Bialgebra R✝ A✝
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : Coalgebra R A
counit_one : counit 1 = 1
counit_mul : ∀ {a b : A}, counit (a * b) = counit a * counit b
comul_one : comul 1 = 1
comul_mul : ∀ {a b : A}, comul (a * b) = comul a * comul b
x✝¹ x✝ : A
⊢ (((LinearMap.mul R A).compr₂ counit) x✝¹) x✝ = (((LinearMap.mul R R).compl₁₂ counit counit) x✝¹) x✝
Module: Mathlib.RingTheory.Bialgebra.Basic

Goal state before:
pp: R✝ : Type u
A✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Bialgebra R✝ A✝
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : Coalgebra R A
counit_one : counit 1 = 1
counit_mul : ∀ {a b : A}, counit (a * b) = counit a * counit b
comul_one : comul 1 = 1
comul_mul : ∀ {a b : A}, comul (a * b) = comul a * comul b
⊢ (LinearMap.mul R A).compr₂ comul = (LinearMap.mul R (A ⊗[R] A)).compl₁₂ comul comul

Tactic:
ext

Goal state after:
R✝ : Type u
A✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Bialgebra R✝ A✝
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : Coalgebra R A
counit_one : counit 1 = 1
counit_mul : ∀ {a b : A}, counit (a * b) = counit a * counit b
comul_one : comul 1 = 1
comul_mul : ∀ {a b : A}, comul (a * b) = comul a * comul b
x✝¹ x✝ : A
⊢ (((LinearMap.mul R A).compr₂ comul) x✝¹) x✝ = (((LinearMap.mul R (A ⊗[R] A)).compl₁₂ comul comul) x✝¹) x✝
Module: Mathlib.RingTheory.Bialgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.mul R R).compr₂ CoalgebraStruct.counit =
    (LinearMap.mul R R).compl₁₂ CoalgebraStruct.counit CoalgebraStruct.counit

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ (((LinearMap.mul R R).compr₂ CoalgebraStruct.counit) 1) 1 =
    (((LinearMap.mul R R).compl₁₂ CoalgebraStruct.counit CoalgebraStruct.counit) 1) 1
Module: Mathlib.RingTheory.Bialgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.mul R R).compr₂ CoalgebraStruct.comul =
    (LinearMap.mul R (R ⊗[R] R)).compl₁₂ CoalgebraStruct.comul CoalgebraStruct.comul

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ (((LinearMap.mul R R).compr₂ CoalgebraStruct.comul) 1) 1 =
    (((LinearMap.mul R (R ⊗[R] R)).compl₁₂ CoalgebraStruct.comul CoalgebraStruct.comul) 1) 1
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
inst✝¹ : IsCocomm R A
inst✝ : IsCocomm R B
⊢ ↑(TensorProduct.comm R (A × B) (A × B)) ∘ₗ comul = comul

Tactic:
ext

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
inst✝¹ : IsCocomm R A
inst✝ : IsCocomm R B
x✝ : A
⊢ ((↑(TensorProduct.comm R (A × B) (A × B)) ∘ₗ comul) ∘ₗ inl R A B) x✝ = (comul ∘ₗ inl R A B) x✝

case hr
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
inst✝¹ : IsCocomm R A
inst✝ : IsCocomm R B
x✝ : B
⊢ ((↑(TensorProduct.comm R (A × B) (A × B)) ∘ₗ comul) ∘ₗ inr R A B) x✝ = (comul ∘ₗ inr R A B) x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → CoalgebraStruct R (A i)
i : ι
⊢ comul ∘ₗ lsingle i = TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → CoalgebraStruct R (A i)
i : ι
x✝ : A i
⊢ (comul ∘ₗ lsingle i) x✝ = (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → CoalgebraStruct R (A i)
i : ι
⊢ counit ∘ₗ lsingle i = counit

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → CoalgebraStruct R (A i)
i : ι
x✝ : A i
⊢ (counit ∘ₗ lsingle i) x✝ = counit x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : (i : ι) → Coalgebra R (A i)
inst✝ : ∀ (i : ι), IsCocomm R (A i)
⊢ ↑(TensorProduct.comm R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ comul = comul

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : (i : ι) → Coalgebra R (A i)
inst✝ : ∀ (i : ι), IsCocomm R (A i)
i✝ : ι
x✝ : A i✝
⊢ ((↑(TensorProduct.comm R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ comul) ∘ₗ lsingle i✝) x✝ = (comul ∘ₗ lsingle i✝) x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
i : ι
⊢ comul ∘ₗ lsingle i = TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
i : ι
x✝ : A
⊢ (comul ∘ₗ lsingle i) x✝ = (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
i : ι
⊢ counit ∘ₗ lsingle i = counit

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
i : ι
x✝ : A
⊢ (counit ∘ₗ lsingle i) x✝ = counit x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsCocomm R A
⊢ ↑(TensorProduct.comm R (ι →₀ A) (ι →₀ A)) ∘ₗ comul = comul

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsCocomm R A
a✝ : ι
x✝ : A
⊢ ((↑(TensorProduct.comm R (ι →₀ A) (ι →₀ A)) ∘ₗ comul) ∘ₗ lsingle a✝) x✝ = (comul ∘ₗ lsingle a✝) x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
i : n
⊢ comul ∘ₗ LinearMap.single R A i = map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul

Tactic:
ext

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
i : n
x✝ : A i
⊢ (comul ∘ₗ LinearMap.single R A i) x✝ = (map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul) x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
i : n
⊢ counit ∘ₗ LinearMap.single R A i = counit

Tactic:
ext

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
i : n
x✝ : A i
⊢ (counit ∘ₗ LinearMap.single R A i) x✝ = counit x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
A : n → Type u_3
inst✝³ : (i : n) → AddCommMonoid (A i)
inst✝² : (i : n) → Module R (A i)
inst✝¹ : (i : n) → Coalgebra R (A i)
inst✝ : ∀ (i : n), IsCocomm R (A i)
⊢ ↑(TensorProduct.comm R ((i : n) → A i) ((i : n) → A i)) ∘ₗ comul = comul

Tactic:
ext

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
A : n → Type u_3
inst✝³ : (i : n) → AddCommMonoid (A i)
inst✝² : (i : n) → Module R (A i)
inst✝¹ : (i : n) → Coalgebra R (A i)
inst✝ : ∀ (i : n), IsCocomm R (A i)
i✝ : n
x✝ : A i✝
⊢ ((↑(TensorProduct.comm R ((i : n) → A i) ((i : n) → A i)) ∘ₗ comul) ∘ₗ LinearMap.single R A i✝) x✝ =
    (comul ∘ₗ LinearMap.single R A i✝) x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : Coalgebra R B
e : A ≃ B
this✝ : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
⊢ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul = LinearMap.lTensor A comul ∘ₗ comul

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : Coalgebra R B
e : A ≃ B
this✝ : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
x✝ : A
⊢ (↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul) x✝ = (LinearMap.lTensor A comul ∘ₗ comul) x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : Coalgebra R B
e : A ≃ B
this✝ : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
⊢ LinearMap.rTensor A counit ∘ₗ comul = (TensorProduct.mk R R A) 1

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : Coalgebra R B
e : A ≃ B
this✝ : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
x✝ : A
⊢ (LinearMap.rTensor A counit ∘ₗ comul) x✝ = ((TensorProduct.mk R R A) 1) x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : Coalgebra R B
e : A ≃ B
this✝ : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
⊢ LinearMap.lTensor A counit ∘ₗ comul = (TensorProduct.mk R A R).flip 1

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : Coalgebra R B
e : A ≃ B
this✝ : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
x✝ : A
⊢ (LinearMap.lTensor A counit ∘ₗ comul) x✝ = ((TensorProduct.mk R A R).flip 1) x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid B
inst✝² : Module R B
inst✝¹ : Coalgebra R B
inst✝ : IsCocomm R B
e : A ≃ B
this✝¹ : AddCommMonoid A := e.addCommMonoid
this✝ : Module R A := Equiv.module R e
this : Coalgebra R A := coalgebra R e
⊢ ↑(TensorProduct.comm R A A) ∘ₗ comul = comul

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid B
inst✝² : Module R B
inst✝¹ : Coalgebra R B
inst✝ : IsCocomm R B
e : A ≃ B
this✝¹ : AddCommMonoid A := e.addCommMonoid
this✝ : Module R A := Equiv.module R e
this : Coalgebra R A := coalgebra R e
x✝ : A
⊢ (↑(TensorProduct.comm R A A) ∘ₗ comul) x✝ = comul x✝
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : CoalgebraStruct R A
f g : R →ₐc[R] A
h : f 1 = g 1
⊢ (fun x ↦ ↑x) f = (fun x ↦ ↑x) g

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : CoalgebraStruct R A
f g : R →ₐc[R] A
h : f 1 = g 1
⊢ ((fun x ↦ ↑x) f) 1 = ((fun x ↦ ↑x) g) 1
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
⊢ (counitAlgHom R A).comp (Algebra.ofId R A) = counitAlgHom R R

Tactic:
ext

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
⊢ (Algebra.TensorProduct.map (Algebra.ofId R A) (Algebra.ofId R A)).comp (comulAlgHom R R) =
    (comulAlgHom R A).comp (Algebra.ofId R A)

Tactic:
ext

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
C : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
f : A →ₐc[R] B
hf : Bijective ⇑f
⊢ (counitAlgHom R B).comp ↑(AlgEquiv.ofBijective (↑f) hf) = counitAlgHom R A

Tactic:
ext

Goal state after:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
f : A →ₐc[R] B
hf : Bijective ⇑f
x✝ : A
⊢ ((counitAlgHom R B).comp ↑(AlgEquiv.ofBijective (↑f) hf)) x✝ = (counitAlgHom R A) x✝