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

Goal state before:
pp: S : Type u_1
R : Type u
M : Type v
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring 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
x : tsze R M
hx : x ∈ ⊤
⊢ x ∈ (inlAlgHom S R M).range ⊔ Algebra.adjoin S (Set.range inr)

Tactic:
;

Goal state after:
S : Type u_1
R : Type u
M : Type v
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring 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
x : tsze R M
hx : x ∈ ⊤
⊢ x ∈ (inlAlgHom S R M).range ⊔ Algebra.adjoin S (Set.range inr)
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
x✝¹ x✝ : A
⊢ (((LinearMap.mul R A).compr₂ counit) x✝¹) x✝ = (((LinearMap.mul R R).compl₁₂ counit counit) x✝¹) x✝

Tactic:
;

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
x✝¹ x✝ : A
⊢ (((LinearMap.mul R A).compr₂ comul) x✝¹) x✝ = (((LinearMap.mul R (A ⊗[R] A)).compl₁₂ comul comul) x✝¹) x✝

Tactic:
;

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) 1) 1 =
    (((LinearMap.mul R R).compl₁₂ CoalgebraStruct.counit CoalgebraStruct.counit) 1) 1

Tactic:
;

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) 1) 1 =
    (((LinearMap.mul R (R ⊗[R] R)).compl₁₂ CoalgebraStruct.comul CoalgebraStruct.comul) 1) 1

Tactic:
;

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

Tactic:
;

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 : ι
x✝ : A i
⊢ (counit ∘ₗ lsingle i) x✝ = counit x✝

Tactic:
;

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)
i✝ : ι
x✝ : A i✝
⊢ ((↑(TensorProduct.comm R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ comul) ∘ₗ lsingle i✝) x✝ = (comul ∘ₗ lsingle i✝) x✝

Tactic:
;

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 : ι
x✝ : A
⊢ (comul ∘ₗ lsingle i) x✝ = (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) x✝

Tactic:
;

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 j : ι
x✝ : A
⊢ ((comul ∘ₗ lapply i) ∘ₗ lsingle j) x✝ = ((TensorProduct.map (lapply i) (lapply i) ∘ₗ comul) ∘ₗ lsingle j) x✝

Tactic:
;

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 j : ι
x✝ : A
⊢ ((comul ∘ₗ lapply i) ∘ₗ lsingle j) x✝ = ((TensorProduct.map (lapply i) (lapply i) ∘ₗ comul) ∘ₗ lsingle j) 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 : ι
x✝ : A
⊢ (counit ∘ₗ lsingle i) x✝ = counit x✝

Tactic:
;

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
a✝ : ι
x✝ : A
⊢ ((↑(TensorProduct.comm R (ι →₀ A) (ι →₀ A)) ∘ₗ comul) ∘ₗ lsingle a✝) x✝ = (comul ∘ₗ lsingle a✝) x✝

Tactic:
;

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
x✝ : A i
⊢ (comul ∘ₗ LinearMap.single R A i) x✝ = (map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul) x✝

Tactic:
;

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 j : n
x✝ : A j
⊢ ((comul ∘ₗ proj i) ∘ₗ LinearMap.single R A j) x✝ = ((map (proj i) (proj i) ∘ₗ comul) ∘ₗ LinearMap.single R A j) x✝

Tactic:
;

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 j : n
x✝ : A j
⊢ ((comul ∘ₗ proj i) ∘ₗ LinearMap.single R A j) x✝ = ((map (proj i) (proj i) ∘ₗ comul) ∘ₗ LinearMap.single R A j) 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
x✝ : A i
⊢ (counit ∘ₗ LinearMap.single R A i) x✝ = counit x✝

Tactic:
;

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

Tactic:
;

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

Tactic:
;

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) 1 = ((fun x ↦ ↑x) g) 1

Tactic:
;

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.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
x✝¹ : R
x✝ : ↑((restrictScalars f).obj X)
⊢ (AddEquiv.refl ↑((restrictScalars f).obj X)).toFun (x✝¹ • x✝) =
    (RingHom.id R) x✝¹ • (AddEquiv.refl ↑((restrictScalars f).obj X)).toFun x✝

Tactic:
;

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
x✝¹ : R
x✝ : ↑((restrictScalars f).obj X)
⊢ (AddEquiv.refl ↑((restrictScalars f).obj X)).toFun (x✝¹ • x✝) =
    (RingHom.id R) x✝¹ • (AddEquiv.refl ↑((restrictScalars f).obj X)).toFun x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X✝ Y✝ : ModuleCat S
x✝ : X✝ ⟶ Y✝
⊢ (restrictScalars f).map x✝ ≫
      (let __spread.0 := AddEquiv.refl ↑((restrictScalars f).obj Y✝);
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ }).toModuleIso.hom =
    (let __spread.0 := AddEquiv.refl ↑((restrictScalars f).obj X✝);
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ }).toModuleIso.hom ≫
      (restrictScalars f).map x✝

Tactic:
;

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X✝ Y✝ : ModuleCat S
x✝ : X✝ ⟶ Y✝
⊢ (restrictScalars f).map x✝ ≫
      (let __spread.0 := AddEquiv.refl ↑((restrictScalars f).obj Y✝);
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ }).toModuleIso.hom =
    (let __spread.0 := AddEquiv.refl ↑((restrictScalars f).obj X✝);
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ }).toModuleIso.hom ≫
      (restrictScalars f).map x✝
Module: Mathlib.RingTheory.Bialgebra.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✝¹¹ : Semiring A
inst✝¹⁰ : Semiring B
inst✝⁹ : Semiring C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra 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✝ y✝ : A
⊢ ((↑f).copy f' h).toFun (x✝ * y✝) = ((↑f).copy f' h).toFun x✝ * ((↑f).copy f' h).toFun y✝

Tactic:
;

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✝¹¹ : Semiring A
inst✝¹⁰ : Semiring B
inst✝⁹ : Semiring C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra 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✝ y✝ : A
⊢ ((↑f).copy f' h).toFun (x✝ * y✝) = ((↑f).copy f' h).toFun x✝ * ((↑f).copy f' h).toFun y✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
inst✝ : Ring R
M : ModuleCat R
r : R
x : ↑((restrictScalars (RingHom.id R)).obj M)
⊢ (AddEquiv.refl ↑((restrictScalars (RingHom.id R)).obj M)) (r • x) =
    r • (AddEquiv.refl ↑((restrictScalars (RingHom.id R)).obj M)) x

Tactic:
;

Goal state after:
R : Type u₁
inst✝ : Ring R
M : ModuleCat R
r : R
x : ↑((restrictScalars (RingHom.id R)).obj M)
⊢ (AddEquiv.refl ↑((restrictScalars (RingHom.id R)).obj M)) (r • x) =
    r • (AddEquiv.refl ↑((restrictScalars (RingHom.id R)).obj M)) x
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ : Type u₁
R₂ : Type u₂
R₃ : Type u₃
inst✝² : Ring R₁
inst✝¹ : Ring R₂
inst✝ : Ring R₃
f : R₁ →+* R₂
g : R₂ →+* R₃
M : ModuleCat R₃
r : R₁
x : ↑((restrictScalars (g.comp f)).obj M)
⊢ (AddEquiv.refl ↑((restrictScalars (g.comp f)).obj M)) (r • x) =
    r • (AddEquiv.refl ↑((restrictScalars (g.comp f)).obj M)) x

Tactic:
;

Goal state after:
R₁ : Type u₁
R₂ : Type u₂
R₃ : Type u₃
inst✝² : Ring R₁
inst✝¹ : Ring R₂
inst✝ : Ring R₃
f : R₁ →+* R₂
g : R₂ →+* R₃
M : ModuleCat R₃
r : R₁
x : ↑((restrictScalars (g.comp f)).obj M)
⊢ (AddEquiv.refl ↑((restrictScalars (g.comp f)).obj M)) (r • x) =
    r • (AddEquiv.refl ↑((restrictScalars (g.comp f)).obj M)) x
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : Algebra R₀ R
inst✝ : Algebra R₀ S
f : R →ₐ[R₀] S
M N : ModuleCat S
g : M ⟶ N
r₀ : R₀
m : ↑((restrictScalars f.toRingHom).obj M)
⊢ (Hom.hom ((restrictScalars f.toRingHom).map (r₀ • g))) m = (Hom.hom (r₀ • (restrictScalars f.toRingHom).map g)) m

Tactic:
;

Goal state after:
R₀ : Type u_1
R : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : Algebra R₀ R
inst✝ : Algebra R₀ S
f : R →ₐ[R₀] S
M N : ModuleCat S
g : M ⟶ N
r₀ : R₀
m : ↑((restrictScalars f.toRingHom).obj M)
⊢ (Hom.hom ((restrictScalars f.toRingHom).map (r₀ • g))) m = (Hom.hom (r₀ • (restrictScalars f.toRingHom).map g)) m
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case add
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑M₁
ihx : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x✝
ihy : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) y✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) y✝
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x✝ + (Hom.hom (map' f (l₁₂ ≫ l₂₃))) y✝ =
    (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x✝ + (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) y✝

Tactic:
;

Goal state after:
case add
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑M₁
ihx : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x✝
ihy : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) y✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) y✝
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x✝ + (Hom.hom (map' f (l₁₂ ≫ l₂₃))) y✝ =
    (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x✝ + (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) y✝
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
x✝ : A
⊢ ((counitAlgHom R B).comp ↑(AlgEquiv.ofBijective (↑f) hf)) x✝ = (counitAlgHom R A) x✝

Tactic:
;

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✝
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
x✝ : A
⊢ ((Algebra.TensorProduct.map ↑(AlgEquiv.ofBijective (↑f) hf) ↑(AlgEquiv.ofBijective (↑f) hf)).comp (comulAlgHom R A))
      x✝ =
    ((comulAlgHom R B).comp ↑(AlgEquiv.ofBijective (↑f) hf)) x✝

Tactic:
;

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
⊢ ((Algebra.TensorProduct.map ↑(AlgEquiv.ofBijective (↑f) hf) ↑(AlgEquiv.ofBijective (↑f) hf)).comp (comulAlgHom R A))
      x✝ =
    ((comulAlgHom R B).comp ↑(AlgEquiv.ofBijective (↑f) hf)) x✝
Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : CoalgCat R
f : Y ⟶ Z
x✝ : ↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X ⊗ Y))
⊢ (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (X ◁ f))) x✝ =
    (ModuleCat.Hom.hom
        ((Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X ⊗ (forget₂ (CoalgCat R) (ModuleCat R)).obj Y)).inv ≫
          (forget₂ (CoalgCat R) (ModuleCat R)).obj X ◁ (forget₂ (CoalgCat R) (ModuleCat R)).map f ≫
            (Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X ⊗ (forget₂ (CoalgCat R) (ModuleCat R)).obj Z)).hom))
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
X Y Z : CoalgCat R
f : Y ⟶ Z
x✝ : ↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X ⊗ Y))
⊢ (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (X ◁ f))) x✝ =
    (ModuleCat.Hom.hom
        ((Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X ⊗ (forget₂ (CoalgCat R) (ModuleCat R)).obj Y)).inv ≫
          (forget₂ (CoalgCat R) (ModuleCat R)).obj X ◁ (forget₂ (CoalgCat R) (ModuleCat R)).map f ≫
            (Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X ⊗ (forget₂ (CoalgCat R) (ModuleCat R)).obj Z)).hom))
      x✝
Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ X₂✝ : CoalgCat R
X : X₁✝ ⟶ X₂✝
f : CoalgCat R
x✝ : ↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X₁✝ ⊗ f))
⊢ (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (X ▷ f))) x✝ =
    (ModuleCat.Hom.hom
        ((Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X₁✝ ⊗ (forget₂ (CoalgCat R) (ModuleCat R)).obj f)).inv ≫
          (forget₂ (CoalgCat R) (ModuleCat R)).map X ▷ (forget₂ (CoalgCat R) (ModuleCat R)).obj f ≫
            (Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X₂✝ ⊗ (forget₂ (CoalgCat R) (ModuleCat R)).obj f)).hom))
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
X₁✝ X₂✝ : CoalgCat R
X : X₁✝ ⟶ X₂✝
f : CoalgCat R
x✝ : ↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X₁✝ ⊗ f))
⊢ (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (X ▷ f))) x✝ =
    (ModuleCat.Hom.hom
        ((Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X₁✝ ⊗ (forget₂ (CoalgCat R) (ModuleCat R)).obj f)).inv ≫
          (forget₂ (CoalgCat R) (ModuleCat R)).map X ▷ (forget₂ (CoalgCat R) (ModuleCat R)).obj f ≫
            (Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X₂✝ ⊗ (forget₂ (CoalgCat R) (ModuleCat R)).obj f)).hom))
      x✝