mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (Algebra.TensorProduct.map ↑(AlgEquiv.ofBijective (↑f) hf) ↑(AlgEquiv.ofBijective (↑f) hf)).comp (comulAlgHom R A) =
    (comulAlgHom R B).comp ↑(AlgEquiv.ofBijective (↑f) hf)

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
⊢ ((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
⊢ (forget₂ (CoalgCat R) (ModuleCat R)).map (X ◁ f) =
    (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

Tactic:
ext

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
⊢ (forget₂ (CoalgCat R) (ModuleCat R)).map (X ▷ f) =
    (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

Tactic:
ext

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✝
Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

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

Tactic:
ext

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : CoalgCat R
⊢ (TensorProduct.mk R ↑(𝟙_ (CoalgCat R)).toModuleCat ↑X.toModuleCat).compr₂ₛₗ
      (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (λ_ X).hom)) =
    (TensorProduct.mk R ↑(𝟙_ (CoalgCat R)).toModuleCat ↑X.toModuleCat).compr₂ₛₗ
      (ModuleCat.Hom.hom
        (((Iso.refl
                  ((forget₂ (CoalgCat R) (ModuleCat R)).obj (𝟙_ (CoalgCat R)) ⊗
                    (forget₂ (CoalgCat R) (ModuleCat R)).obj X)).symm ≪≫
              ((Iso.refl (𝟙_ (ModuleCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X))) ≪≫
            λ_ ((forget₂ (CoalgCat R) (ModuleCat R)).obj X)).hom)

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
X : CoalgCat R
x✝ : ↑X.toModuleCat
⊢ (((TensorProduct.mk R ↑(𝟙_ (CoalgCat R)).toModuleCat ↑X.toModuleCat).compr₂ₛₗ
          (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (λ_ X).hom)))
        1)
      x✝ =
    (((TensorProduct.mk R ↑(𝟙_ (CoalgCat R)).toModuleCat ↑X.toModuleCat).compr₂ₛₗ
          (ModuleCat.Hom.hom
            (((Iso.refl
                      ((forget₂ (CoalgCat R) (ModuleCat R)).obj (𝟙_ (CoalgCat R)) ⊗
                        (forget₂ (CoalgCat R) (ModuleCat R)).obj X)).symm ≪≫
                  ((Iso.refl (𝟙_ (ModuleCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X))) ≪≫
                λ_ ((forget₂ (CoalgCat R) (ModuleCat R)).obj X)).hom))
        1)
      x✝
Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : CoalgCat R
⊢ (TensorProduct.mk R ↑X.toModuleCat ↑(𝟙_ (CoalgCat R)).toModuleCat).compr₂ₛₗ
      (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (ρ_ X).hom)) =
    (TensorProduct.mk R ↑X.toModuleCat ↑(𝟙_ (CoalgCat R)).toModuleCat).compr₂ₛₗ
      (ModuleCat.Hom.hom
        (((Iso.refl
                  ((forget₂ (CoalgCat R) (ModuleCat R)).obj X ⊗
                    (forget₂ (CoalgCat R) (ModuleCat R)).obj (𝟙_ (CoalgCat R)))).symm ≪≫
              (Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X) ⊗ᵢ (Iso.refl (𝟙_ (ModuleCat R))).symm)) ≪≫
            ρ_ ((forget₂ (CoalgCat R) (ModuleCat R)).obj X)).hom)

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
X : CoalgCat R
x✝ : ↑X.toModuleCat
⊢ (((TensorProduct.mk R ↑X.toModuleCat ↑(𝟙_ (CoalgCat R)).toModuleCat).compr₂ₛₗ
          (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (ρ_ X).hom)))
        x✝)
      1 =
    (((TensorProduct.mk R ↑X.toModuleCat ↑(𝟙_ (CoalgCat R)).toModuleCat).compr₂ₛₗ
          (ModuleCat.Hom.hom
            (((Iso.refl
                      ((forget₂ (CoalgCat R) (ModuleCat R)).obj X ⊗
                        (forget₂ (CoalgCat R) (ModuleCat R)).obj (𝟙_ (CoalgCat R)))).symm ≪≫
                  (Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X) ⊗ᵢ (Iso.refl (𝟙_ (ModuleCat R))).symm)) ≪≫
                ρ_ ((forget₂ (CoalgCat R) (ModuleCat R)).obj X)).hom))
        x✝)
      1
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
M✝ : ModuleCat R
M M' : ModuleCat R
g : M ⟶ M'
s : S
h : ↑((restrictScalars f).obj (of S S)) →ₗ[R] ↑M
⊢ Hom.hom g ∘ₗ (s • h) = (RingHom.id S) s • Hom.hom g ∘ₗ h

Tactic:
ext

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
M✝ : ModuleCat R
M M' : ModuleCat R
g : M ⟶ M'
s : S
h : ↑((restrictScalars f).obj (of S S)) →ₗ[R] ↑M
x✝ : ↑((restrictScalars f).obj (of S S))
⊢ (Hom.hom g ∘ₗ (s • h)) x✝ = ((RingHom.id S) s • Hom.hom g ∘ₗ h) x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
x✝ : ModuleCat R
⊢ CoextendScalars.map' f (𝟙 x✝) = 𝟙 (CoextendScalars.obj' f x✝)

Tactic:
ext

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
x✝¹ : ModuleCat R
x✝ : ↑(CoextendScalars.obj' f x✝¹)
⊢ (Hom.hom (CoextendScalars.map' f (𝟙 x✝¹))) x✝ = (Hom.hom (𝟙 (CoextendScalars.obj' f x✝¹))) x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X✝ Y✝ Z✝ : ModuleCat R
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ CoextendScalars.map' f (x✝¹ ≫ x✝) = CoextendScalars.map' f x✝¹ ≫ CoextendScalars.map' f x✝

Tactic:
ext

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X✝ Y✝ Z✝ : ModuleCat R
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ↑(CoextendScalars.obj' f X✝)
⊢ (Hom.hom (CoextendScalars.map' f (x✝² ≫ x✝¹))) x✝ =
    (Hom.hom (CoextendScalars.map' f x✝² ≫ CoextendScalars.map' f x✝¹)) x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : (restrictScalars f).obj X ⟶ Y
⊢ RestrictionCoextensionAdj.HomEquiv.toRestriction f (RestrictionCoextensionAdj.HomEquiv.fromRestriction f g) = g

Tactic:
ext

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : (restrictScalars f).obj X ⟶ Y
x✝ : ↑((restrictScalars f).obj X)
⊢ (Hom.hom
        (RestrictionCoextensionAdj.HomEquiv.toRestriction f (RestrictionCoextensionAdj.HomEquiv.fromRestriction f g)))
      x✝ =
    (Hom.hom g) x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : X ⟶ (coextendScalars f).obj Y
⊢ RestrictionCoextensionAdj.HomEquiv.fromRestriction f (RestrictionCoextensionAdj.HomEquiv.toRestriction f g) = g

Tactic:
ext

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : X ⟶ (coextendScalars f).obj Y
x✝¹ : ↑X
x✝ : ↑((restrictScalars f).obj (of S S))
⊢ ((CoextendScalars.equiv f Y)
        ((Hom.hom
            (RestrictionCoextensionAdj.HomEquiv.fromRestriction f
              (RestrictionCoextensionAdj.HomEquiv.toRestriction f g)))
          x✝¹))
      x✝ =
    ((CoextendScalars.equiv f Y) ((Hom.hom g) x✝¹)) x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : X ⟶ (coextendScalars f).obj Y
⊢ { toFun := RestrictionCoextensionAdj.HomEquiv.fromRestriction f,
          invFun := RestrictionCoextensionAdj.HomEquiv.toRestriction f, left_inv := ⋯, right_inv := ⋯ }.symm
      g =
    (restrictScalars f).map g ≫ (RestrictionCoextensionAdj.counit' f).app Y

Tactic:
ext

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : X ⟶ (coextendScalars f).obj Y
x✝ : ↑((restrictScalars f).obj X)
⊢ (Hom.hom
        ({ toFun := RestrictionCoextensionAdj.HomEquiv.fromRestriction f,
              invFun := RestrictionCoextensionAdj.HomEquiv.toRestriction f, left_inv := ⋯, right_inv := ⋯ }.symm
          g))
      x✝ =
    (Hom.hom ((restrictScalars f).map g ≫ (RestrictionCoextensionAdj.counit' f).app Y)) x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case refine_1.refine_1
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
s₁ s₂ : S
⊢ evalAt f (s₁ + s₂) g = evalAt f s₁ g + evalAt f s₂ g

Tactic:
ext

Goal state after:
case refine_1.refine_1
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
s₁ s₂ : S
x✝ : ↑X
⊢ (evalAt f (s₁ + s₂) g) x✝ = (evalAt f s₁ g + evalAt f s₂ g) x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ R₃ : Type u₁
inst✝² : CommRing R₁
inst✝¹ : CommRing R₂
inst✝ : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
⊢ ((extendRestrictScalarsAdj (f₂₃.comp f₁₂)).homEquiv M ((extendScalars f₁₂ ⋙ extendScalars f₂₃).obj M))
      ((extendScalarsComp f₁₂ f₂₃).hom.app M) =
    (extendRestrictScalarsAdj f₁₂).unit.app M ≫
      (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app (ExtendScalars.obj' f₁₂ M)) ≫
        (restrictScalarsComp f₁₂ f₂₃).inv.app ((extendScalars f₂₃).obj (ExtendScalars.obj' f₁₂ M))

Tactic:
dsimp [extendScalarsComp, conjugateIsoEquiv, conjugateEquiv]
  simp only [Functor.comp_obj, Category.assoc, Category.id_comp,
    Category.comp_id, Adjunction.comp_unit_app, Adjunction.homEquiv_unit,
    Functor.map_comp, Adjunction.unit_naturality_assoc,
    Adjunction.right_triangle_components]
  rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
f : M →ₗc[S] N
g : P →ₗc[R] Q
⊢ counit ∘ₗ AlgebraTensorModule.map f.toLinearMap g.toLinearMap = counit

Tactic:
ext

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
f : M →ₗc[S] N
g : P →ₗc[R] Q
x✝¹ : M
x✝ : P
⊢ ((AlgebraTensorModule.curry (counit ∘ₗ AlgebraTensorModule.map f.toLinearMap g.toLinearMap)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry counit) x✝¹) x✝
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
⊢ counit ∘ₗ ↑(AlgebraTensorModule.assoc R S S M N P) = counit

Tactic:
ext

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
x✝² : M
x✝¹ : N
x✝ : P
⊢ (((AlgebraTensorModule.curry (AlgebraTensorModule.curry (counit ∘ₗ ↑(AlgebraTensorModule.assoc R S S M N P)))) x✝²)
        x✝¹)
      x✝ =
    (((AlgebraTensorModule.curry (AlgebraTensorModule.curry counit)) x✝²) x✝¹) x✝
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝³ x✝² x✝¹ : BialgCat R
x✝ : x✝² ⟶ x✝¹
⊢ (forget₂ (BialgCat R) (AlgCat R)).map (x✝³ ◁ x✝) =
    (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝²)).inv ≫
      (forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ◁ (forget₂ (BialgCat R) (AlgCat R)).map x✝ ≫
        (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).hom

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
x✝⁴ x✝³ x✝² : BialgCat R
x✝¹ : x✝³ ⟶ x✝²
x✝ : ↑((forget₂ (BialgCat R) (AlgCat R)).obj (x✝⁴ ⊗ x✝³))
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (x✝⁴ ◁ x✝¹))) x✝ =
    (AlgCat.Hom.hom
        ((Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝⁴ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝³)).inv ≫
          (forget₂ (BialgCat R) (AlgCat R)).obj x✝⁴ ◁ (forget₂ (BialgCat R) (AlgCat R)).map x✝¹ ≫
            (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝⁴ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝²)).hom))
      x✝
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ X₂✝ : BialgCat R
x✝¹ : X₁✝ ⟶ X₂✝
x✝ : BialgCat R
⊢ (forget₂ (BialgCat R) (AlgCat R)).map (x✝¹ ▷ x✝) =
    (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝)).inv ≫
      (forget₂ (BialgCat R) (AlgCat R)).map x✝¹ ▷ (forget₂ (BialgCat R) (AlgCat R)).obj x✝ ≫
        (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₂✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝)).hom

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
X₁✝ X₂✝ : BialgCat R
x✝² : X₁✝ ⟶ X₂✝
x✝¹ : BialgCat R
x✝ : ↑((forget₂ (BialgCat R) (AlgCat R)).obj (X₁✝ ⊗ x✝¹))
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (x✝² ▷ x✝¹))) x✝ =
    (AlgCat.Hom.hom
        ((Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).inv ≫
          (forget₂ (BialgCat R) (AlgCat R)).map x✝² ▷ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹ ≫
            (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₂✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).hom))
      x✝
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ Y₁✝ X₂✝ Y₂✝ : BialgCat R
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
⊢ (forget₂ (BialgCat R) (AlgCat R)).map (x✝¹ ⊗ₘ x✝) =
    (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj X₂✝)).inv ≫
      ((forget₂ (BialgCat R) (AlgCat R)).map x✝¹ ⊗ₘ (forget₂ (BialgCat R) (AlgCat R)).map x✝) ≫
        (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj Y₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj Y₂✝)).hom

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
X₁✝ Y₁✝ X₂✝ Y₂✝ : BialgCat R
x✝² : X₁✝ ⟶ Y₁✝
x✝¹ : X₂✝ ⟶ Y₂✝
x✝ : ↑((forget₂ (BialgCat R) (AlgCat R)).obj (X₁✝ ⊗ X₂✝))
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (x✝² ⊗ₘ x✝¹))) x✝ =
    (AlgCat.Hom.hom
        ((Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj X₂✝)).inv ≫
          ((forget₂ (BialgCat R) (AlgCat R)).map x✝² ⊗ₘ (forget₂ (BialgCat R) (AlgCat R)).map x✝¹) ≫
            (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj Y₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj Y₂✝)).hom))
      x✝