mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ LinearMap.rTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R) 1 = (TensorProduct.mk R R R) 1

Tactic:
by ext; rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ LinearMap.lTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R) 1 = (TensorProduct.mk R R R).flip 1

Tactic:
by ext; rfl

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

Goal state before:
pp: 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
x : A
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
        ((TensorProduct.map (inl R A B) (inl R A B)) (comul x))) =
    (lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
      ((TensorProduct.map (inl R A B) (inl R A B)) (comul x))

Tactic:
simp_rw [← comp_apply, ← comp_assoc, rTensor_comp_map, lTensor_comp_map, coprod_inl,
        ← map_comp_rTensor, ← map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc,
        TensorProduct.map_map_comp_assoc_eq, comp_apply, LinearEquiv.coe_coe]

Goal state after:
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:
by ext; rfl

Goal state after:
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)
⊢ counit ∘ₗ DFinsupp.coeFnLinearMap R = counit

Tactic:
apply LinearMap.ext fun x ↦ ?_

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)
x : Π₀ (i : n), A i
⊢ (counit ∘ₗ DFinsupp.coeFnLinearMap R) 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) → CoalgebraStruct R (A i)
⊢ comul ∘ₗ coeFnLinearMap R = map (coeFnLinearMap R) (coeFnLinearMap R) ∘ₗ comul

Tactic:
apply LinearMap.ext fun x ↦ ?_

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)
x : Π₀ (i : n), A i
⊢ (comul ∘ₗ coeFnLinearMap R) x = (map (coeFnLinearMap R) (coeFnLinearMap R) ∘ₗ 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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CoalgebraStruct R M
⊢ counit ∘ₗ Finsupp.lcoeFun = counit

Tactic:
apply LinearMap.ext fun x ↦ ?_

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CoalgebraStruct R M
x : n →₀ M
⊢ (counit ∘ₗ Finsupp.lcoeFun) 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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CoalgebraStruct R M
⊢ comul ∘ₗ lcoeFun = map lcoeFun lcoeFun ∘ₗ comul

Tactic:
apply LinearMap.ext fun x ↦ ?_

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CoalgebraStruct R M
x : n →₀ M
⊢ (comul ∘ₗ lcoeFun) x = (map lcoeFun lcoeFun ∘ₗ comul) 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:
by ext; rfl

Goal state after:
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:
by ext; rfl

Goal state after:
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:
by ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

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

Tactic:
by ext; rfl

Goal state after:
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:
by ext; rfl

Goal state after:
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:
by ext; rfl

Goal state after:
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:
by ext; rfl

Goal state after:
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:
by ext; rfl

Goal state after:
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:
by ext; rfl

Goal state after:
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:
by ext; rfl

Goal state after:
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:
by ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ x✝ : BialgCat R
⊢ ((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝² x✝¹ x✝).hom)).comp
          Algebra.TensorProduct.includeLeft).comp
      Algebra.TensorProduct.includeLeft =
    ((AlgCat.Hom.hom
              (((Iso.refl
                        ((forget₂ (BialgCat R) (AlgCat R)).obj (x✝² ⊗ x✝¹) ⊗
                          (forget₂ (BialgCat R) (AlgCat R)).obj x✝)).symm ≪≫
                    ((Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗
                            (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ⊗ᵢ
                      Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝))) ≪≫
                  α_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²) ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)
                      ((forget₂ (BialgCat R) (AlgCat R)).obj x✝) ≪≫
                    (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²) ⊗ᵢ
                        Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝)) ≪≫
                      Iso.refl
                        ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗
                          (forget₂ (BialgCat R) (AlgCat R)).obj (x✝¹ ⊗ x✝))).hom).comp
          Algebra.TensorProduct.includeLeft).comp
      Algebra.TensorProduct.includeLeft

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ x✝ : BialgCat R
⊢ (AlgHom.restrictScalars R
          ((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝² x✝¹ x✝).hom)).comp
            Algebra.TensorProduct.includeLeft)).comp
      Algebra.TensorProduct.includeRight =
    (AlgHom.restrictScalars R
          ((AlgCat.Hom.hom
                (((Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj (x✝² ⊗ x✝¹) ⊗
                            (forget₂ (BialgCat R) (AlgCat R)).obj x✝)).symm ≪≫
                      ((Iso.refl
                            ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗
                              (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ⊗ᵢ
                        Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝))) ≪≫
                    α_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²) ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)
                        ((forget₂ (BialgCat R) (AlgCat R)).obj x✝) ≪≫
                      (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²) ⊗ᵢ
                          Iso.refl
                            ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝)) ≪≫
                        Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗
                            (forget₂ (BialgCat R) (AlgCat R)).obj (x✝¹ ⊗ x✝))).hom).comp
            Algebra.TensorProduct.includeLeft)).comp
      Algebra.TensorProduct.includeRight

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ x✝ : BialgCat R
⊢ (AlgHom.restrictScalars R (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝² x✝¹ x✝).hom))).comp
      Algebra.TensorProduct.includeRight =
    (AlgHom.restrictScalars R
          (AlgCat.Hom.hom
            (((Iso.refl
                      ((forget₂ (BialgCat R) (AlgCat R)).obj (x✝² ⊗ x✝¹) ⊗
                        (forget₂ (BialgCat R) (AlgCat R)).obj x✝)).symm ≪≫
                  ((Iso.refl
                        ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ⊗ᵢ
                    Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝))) ≪≫
                α_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²) ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)
                    ((forget₂ (BialgCat R) (AlgCat R)).obj x✝) ≪≫
                  (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²) ⊗ᵢ
                      Iso.refl
                        ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝)) ≪≫
                    Iso.refl
                      ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗
                        (forget₂ (BialgCat R) (AlgCat R)).obj (x✝¹ ⊗ x✝))).hom)).comp
      Algebra.TensorProduct.includeRight

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : BialgCat R
⊢ (AlgHom.restrictScalars R (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (λ_ x✝).hom))).comp
      Algebra.TensorProduct.includeRight =
    (AlgHom.restrictScalars R
          (AlgCat.Hom.hom
            (((Iso.refl
                      ((forget₂ (BialgCat R) (AlgCat R)).obj (𝟙_ (BialgCat R)) ⊗
                        (forget₂ (BialgCat R) (AlgCat R)).obj x✝)).symm ≪≫
                  ((Iso.refl (𝟙_ (AlgCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝))) ≪≫
                λ_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝)).hom)).comp
      Algebra.TensorProduct.includeRight

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : BialgCat R
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (ρ_ x✝).hom)).comp Algebra.TensorProduct.includeLeft =
    (AlgCat.Hom.hom
          (((Iso.refl
                    ((forget₂ (BialgCat R) (AlgCat R)).obj x✝ ⊗
                      (forget₂ (BialgCat R) (AlgCat R)).obj (𝟙_ (BialgCat R)))).symm ≪≫
                (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝) ⊗ᵢ (Iso.refl (𝟙_ (AlgCat R))).symm)) ≪≫
              ρ_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝)).hom).comp
      Algebra.TensorProduct.includeLeft

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x =
    (adj1.rightAdjointUniq adj3).hom.app x

Tactic:
← rightAdjointUniq_trans adj1 adj2 adj3

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x =
    ((adj1.rightAdjointUniq adj2).hom ≫ (adj2.rightAdjointUniq adj3).hom).app x
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⊓ b) = f' a ⊓ f' b

Tactic:
simpa only [h] using map_inf f

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⊓ b) = f' a ⊓ f' b

Tactic:
simpa only [h] using map_inf f

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⊓ b) = f' a ⊓ f' b

Tactic:
simpa only [h] using map_inf f

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ α ∘ₗ ρ⁻¹ = LinearMap.id ⊗ₘ ρ⁻¹

Tactic:
by ext; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
N' : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
⊢ β ∘ₗ f ⊗ₘ g = g ⊗ₘ f ∘ₗ β

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯ =
    Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
      Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯

Tactic:
ext : 2; apply MonoidAlgebra.ringHom_ext <;> intro <;> simp

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a b : R
n : ℕ
ha : Irreducible a
hb : b ≠ 0
⊢ ↑n ≤ emultiplicity a b ↔ replicate n (normalize a) ≤ normalizedFactors b

Tactic:
rw [← pow_dvd_iff_le_emultiplicity]

Goal state after:
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a b : R
n : ℕ
ha : Irreducible a
hb : b ≠ 0
⊢ a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ (TensorProduct.mk R
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R N)))).X)).compr₂ₛₗ
      ((TensorProduct.mk R
            ↑(Opposite.unop
                (Opposite.unop
                    ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                      ((comonEquivalence R).symm.inverse.obj (of R M ⊗ of R N)))).X)
            ↑(Opposite.unop
                (Opposite.unop
                    ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                      ((comonEquivalence R).symm.inverse.obj (of R P)))).X)).compr₂ₛₗ
        (α_ (of R M) (of R N) (of R P)).hom.toCoalgHom'.toLinearMap) =
    (TensorProduct.mk R
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R N)))).X)).compr₂ₛₗ
      ((TensorProduct.mk R
            ↑(Opposite.unop
                (Opposite.unop
                    ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                      ((comonEquivalence R).symm.inverse.obj (of R M ⊗ of R N)))).X)
            ↑(Opposite.unop
                (Opposite.unop
                    ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                      ((comonEquivalence R).symm.inverse.obj (of R P)))).X)).compr₂ₛₗ
        ↑(TensorProduct.assoc R M N P))

Tactic:
by ext; rfl

Goal state after: