mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
f : X ⟶ Y
X' : C
⊢ (G.map (δ F X X') ≫ δ G (F.obj X) (F.obj X')) ≫ (F ⋙ G).map f ▷ (F ⋙ G).obj X' =
    (F ⋙ G).map (f ▷ X') ≫ G.map (δ F Y X') ≫ δ G (F.obj Y) (F.obj X')

Tactic:
dsimp
    rw [assoc, δ_natural_left, ← G.map_comp_assoc, δ_natural_left, map_comp, assoc]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ x✝ : ModuleCat R
⊢ equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.associator x✝² x✝¹ x✝).hom =
    (((Iso.refl
              (MonoidalCategoryStruct.tensorObj
                (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorObj x✝² x✝¹))
                (equivalenceSemimoduleCat.functor.obj x✝))).symm ≪≫
          MonoidalCategory.tensorIso
            (Iso.refl
                (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝²)
                  (equivalenceSemimoduleCat.functor.obj x✝¹))).symm
            (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
        MonoidalCategoryStruct.associator (equivalenceSemimoduleCat.functor.obj x✝²)
            (equivalenceSemimoduleCat.functor.obj x✝¹) (equivalenceSemimoduleCat.functor.obj x✝) ≪≫
          MonoidalCategory.tensorIso (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝²))
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝¹)
                  (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
            Iso.refl
              (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝²)
                (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorObj x✝¹ x✝)))).hom

Tactic:
ext1; exact TensorProduct.ext (TensorProduct.ext rfl)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case e_a
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (((((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫ LaxMonoidal.μ F X Y ▷ G.obj Z) ≫ i.hom.app (X ⊗ Y) ▷ G.obj Z) ≫
          (i.inv.app (X ⊗ Y) ⊗ₘ i.inv.app Z)) ≫
        LaxMonoidal.μ F (X ⊗ Y) Z) ≫
      F.map (α_ X Y Z).hom =
    (((((α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫ G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z)) ≫
            G.obj X ◁ LaxMonoidal.μ F Y Z) ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z)) ≫
        (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z))) ≫
      LaxMonoidal.μ F X (Y ⊗ Z)

Tactic:
slice_lhs 3 4 =>
      rw [← tensorHom_id, tensorHom_comp_tensorHom]
      simp only [Iso.hom_inv_id_app, Category.id_comp, id_tensorHom]

Goal state after:
case e_a
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫ (F.obj (X ⊗ Y) ◁ i.inv.app Z ≫ LaxMonoidal.μ F (X ⊗ Y) Z) ≫ F.map (α_ X Y Z).hom =
    (((((α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫ G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z)) ≫
            G.obj X ◁ LaxMonoidal.μ F Y Z) ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z)) ≫
        (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z))) ≫
      LaxMonoidal.μ F X (Y ⊗ Z)
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
i j : J
f : i ⟶ j
⊢ (forget₂ (ModuleCat R) AddCommGrpCat).map
      (F.map f ≫ homMk (colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j) ⋯) =
    (forget₂ (ModuleCat R) AddCommGrpCat).map
      (homMk (colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) i) ⋯ ≫
        ((Functor.const J).obj (mkOfSMul (coconePointSMul F))).map f)

Tactic:
simp only [Functor.map_comp, forget₂_map_homMk]

Goal state after:
R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
i j : J
f : i ⟶ j
⊢ (forget₂ (ModuleCat R) AddCommGrpCat).map (F.map f) ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) i ≫
      (forget₂ (ModuleCat R) AddCommGrpCat).map (((Functor.const J).obj (mkOfSMul (coconePointSMul F))).map f)
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
⊢ C a

Tactic:
let s : Subalgebra R (TensorAlgebra R M) :=
    { carrier := {a | C a}
      mul_mem' := @mul
      add_mem' := @add
      algebraMap_mem' := algebraMap }

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
⊢ C a
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
⊢ (comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B =
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B

Tactic:
comp_assoc,

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
⊢ comul ∘ₗ LinearMap.fst R A B ∘ₗ inl R A B =
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B
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
⊢ 0⁻¹ = 0

Tactic:
← inl_zero,

Goal state after:
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
⊢ (inl 0)⁻¹ = inl 0
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
⊢ comul = (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B

Tactic:
comp_assoc,

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
⊢ comul = TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul ∘ₗ inl R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: 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
⊢ (comul ∘ₗ LinearMap.fst R A B) ∘ₗ inr R A B =
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B

Tactic:
comp_assoc,

Goal state after:
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
⊢ comul ∘ₗ LinearMap.fst R A B ∘ₗ inr R A B =
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: 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
⊢ 0 = (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B

Tactic:
comp_assoc,

Goal state after:
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
⊢ 0 = TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul ∘ₗ inr R A B
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
⊢ (comul ∘ₗ LinearMap.snd R A B) ∘ₗ inl R A B =
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inl R A B

Tactic:
comp_assoc,

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
⊢ comul ∘ₗ LinearMap.snd R A B ∘ₗ inl R A B =
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inl R A B
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
⊢ 0 = (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inl R A B

Tactic:
comp_assoc,

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
⊢ 0 = TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul ∘ₗ inl R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: 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
⊢ (comul ∘ₗ LinearMap.snd R A B) ∘ₗ inr R A B =
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inr R A B

Tactic:
comp_assoc,

Goal state after:
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
⊢ comul ∘ₗ LinearMap.snd R A B ∘ₗ inr R A B =
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: 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
⊢ comul = (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inr R A B

Tactic:
comp_assoc,

Goal state after:
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
⊢ comul = TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul ∘ₗ inr R A B
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))
      (((TensorProduct.map (TensorProduct.map (inl R A B) (inl R A B)) (inl R A B) ∘ₗ rTensor A comul) ∘ₗ comul) x) =
    ((TensorProduct.map (inl R A B) (TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ lTensor A comul) ∘ₗ comul) x

Tactic:
comp_assoc,

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
x : A
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((TensorProduct.map (TensorProduct.map (inl R A B) (inl R A B)) (inl R A B) ∘ₗ rTensor A comul ∘ₗ comul) x) =
    (TensorProduct.map (inl R A B) (TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ lTensor A comul ∘ₗ comul) x
Module: Mathlib.RingTheory.Coalgebra.Basic

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

Tactic:
comp_assoc,

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

Tactic:
comp_assoc,

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
⊢ rTensor (A × B) counit ∘ₗ comul ∘ₗ inl R A B = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inl R A B
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
⊢ (lTensor R (inl R A B) ∘ₗ rTensor A counit) ∘ₗ comul = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inl R A B

Tactic:
comp_assoc,

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
⊢ lTensor R (inl R A B) ∘ₗ rTensor A counit ∘ₗ comul = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inl R A B
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
⊢ (rTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inl R A B

pp: 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
⊢ (rTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B

Tactic:
· rw [comp_assoc, comul_comp_inl, ← comp_assoc, rTensor_comp_map, counit_comp_inl,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]

Goal state after:
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
⊢ (rTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: 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
⊢ (rTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B

Tactic:
comp_assoc,

Goal state after:
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
⊢ rTensor (A × B) counit ∘ₗ comul ∘ₗ inr R A B = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: 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
⊢ (lTensor R (inr R A B) ∘ₗ rTensor B counit) ∘ₗ comul = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B

Tactic:
comp_assoc,

Goal state after:
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
⊢ lTensor R (inr R A B) ∘ₗ rTensor B counit ∘ₗ comul = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B
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
⊢ (lTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inl R A B

Tactic:
comp_assoc,

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
⊢ lTensor (A × B) counit ∘ₗ comul ∘ₗ inl R A B = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inl R A B
Module: Mathlib.Algebra.Category.CoalgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : CoalgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (CoalgCat R)).map f)
⊢ IsIso f

Tactic:
by
    let i := asIso ((forget (CoalgCat.{v} R)).map f)
    let e : X ≃ₗc[R] Y := { f.toCoalgHom, i.toEquiv with }
    exact ⟨e.toCoalgIso.isIso_hom.1⟩

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
⊢ (rTensor R (inl R A B) ∘ₗ lTensor A counit) ∘ₗ comul = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inl R A B

Tactic:
comp_assoc,

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
⊢ rTensor R (inl R A B) ∘ₗ lTensor A counit ∘ₗ comul = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inl R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: 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
⊢ (lTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B

Tactic:
comp_assoc,

Goal state after:
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
⊢ lTensor (A × B) counit ∘ₗ comul ∘ₗ inr R A B = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: 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
⊢ (rTensor R (inr R A B) ∘ₗ lTensor B counit) ∘ₗ comul = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B

Tactic:
comp_assoc,

Goal state after:
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
⊢ rTensor R (inr R A B) ∘ₗ lTensor B counit ∘ₗ comul = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B
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)
i : ι
⊢ (↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
        rTensor (Π₀ (i : ι), A i) comul ∘ₗ comul) ∘ₗ
      lsingle i =
    (lTensor (Π₀ (i : ι), A i) comul ∘ₗ comul) ∘ₗ lsingle i

Tactic:
comp_assoc,

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)
i : ι
⊢ ↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
      rTensor (Π₀ (i : ι), A i) comul ∘ₗ comul ∘ₗ lsingle i =
    lTensor (Π₀ (i : ι), A i) comul ∘ₗ comul ∘ₗ lsingle i
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)
i : ι
⊢ ((↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
          rTensor (Π₀ (i : ι), A i) comul) ∘ₗ
        TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ
      comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) ∘ₗ comul

Tactic:
comp_assoc,

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