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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
⊢ (leftDistributor X f).inv = ∑ j, biproduct.π (fun j ↦ X ⊗ f j) j ≫ X ◁ biproduct.ι f j

Tactic:
ext
  dsimp [leftDistributor, Functor.mapBiproduct, Functor.mapBicone]
  simp only [Preadditive.comp_sum, biproduct.ι_π_assoc, dite_comp, zero_comp,
    Finset.sum_dite_eq, Finset.mem_univ, ite_true, eqToHom_refl, Category.id_comp,
    biproduct.ι_desc]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
⊢ biproduct.ι (fun j ↦ X ⊗ f j) j ≫ (leftDistributor X f).inv = X ◁ biproduct.ι f j

Tactic:
by
  classical
  cases nonempty_fintype J
  simp [leftDistributor_inv, Preadditive.comp_sum, biproduct.ι_π_assoc, dite_comp]

Goal state after:
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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z = F.map (α_ X Y Z).inv ≫ F.map (α_ X Y Z).hom ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z

Tactic:
← F.map_comp_assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z = F.map ((α_ X Y Z).inv ≫ (α_ X Y Z).hom) ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z
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:
by
    dsimp
    rw [assoc, δ_natural_left, ← G.map_comp_assoc, δ_natural_left, map_comp, assoc]

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

Goal state before:
pp: case ε
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
⊢ ε F ≫ η F = ε F ≫ η F

Tactic:
← εIso_inv

Goal state after:
case ε
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
⊢ ε F ≫ (εIso F).inv = ε F ≫ η F
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j k : C
α : g ≅ f ⊗ h
η : h ⟶ i
ηs : f ⊗ i ⟶ j
η₁ : h ⊗ k ⟶ i ⊗ k
η₂ : f ⊗ h ⊗ k ⟶ f ⊗ i ⊗ k
ηs₁ : (f ⊗ i) ⊗ k ⟶ j ⊗ k
ηs₂ : f ⊗ i ⊗ k ⟶ j ⊗ k
η₃ : f ⊗ h ⊗ k ⟶ j ⊗ k
η₄ : (f ⊗ h) ⊗ k ⟶ j ⊗ k
η₅ : g ⊗ k ⟶ j ⊗ k
e_η₁ : ((Iso.refl h).hom ≫ η ≫ (Iso.refl i).hom) ▷ k = η₁
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : (α_ f i k).inv ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : (α_ f h k).hom ≫ η₃ = η₄
e_η₅ : (α ▷ᵢ k).hom ≫ η₄ = η₅
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅

Tactic:
by
  simp at e_η₁ e_η₅
  simp [e_η₁, e_η₂, e_ηs₁, e_ηs₂, e_η₃, e_η₄, e_η₅]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
η₁ : g ⊗ f ⟶ h ⊗ f
ηθ : (g ⊗ f) ⊗ f' ⟶ (h ⊗ f) ⊗ g'
ηθ₁ : (g ⊗ f) ⊗ f' ⟶ h ⊗ f ⊗ g'
ηθ₂ : g ⊗ f ⊗ f' ⟶ h ⊗ f ⊗ g'
e_η₁ : η ▷ f = η₁
e_ηθ : η₁ ⊗ₘ (Iso.refl f').hom ≫ θ ≫ (Iso.refl g').hom = ηθ
e_ηθ₁ : ηθ ≫ (α_ h f g').hom = ηθ₁
e_ηθ₂ : (α_ g f f').inv ≫ ηθ₁ = ηθ₂
⊢ η ⊗ₘ f ◁ θ = ηθ₂

Tactic:
by
  simp only [← e_η₁, ← e_ηθ, ← e_ηθ₁, ← e_ηθ₂]
  simp [MonoidalCategory.tensorHom_def]

Goal state after:
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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod' G)).1 = η F

Tactic:
change F.map (𝟙 _) ≫ _ = _

Goal state after:
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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ F.map (𝟙 ((diag C).obj (𝟙_ C)).1) ≫ (η (F.prod G)).1 = η F
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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod' G) X Y).1 = δ F X Y

Tactic:
change F.map (𝟙 _) ≫ _ = _

Goal state after:
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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ F.map (𝟙 ((diag C).obj (X ⊗ Y)).1) ≫ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 = δ F X Y
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ?m.108).flip

Tactic:
apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _)

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit ((Cone.postcompose (diagramIsoCospan (cospan g f)).hom).obj c)
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare R₁ H G R₂
c : C
⊢ G.map (adj₁.unit.app c) ≫ ((mateEquiv adj₁ adj₂).toFun ((mateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c) =
    adj₂.unit.app (G.obj ((𝟭 C).obj c)) ≫ R₂.map (((mateEquiv adj₁ adj₂).symm α).app ((𝟭 C).obj c))

Tactic:
exact (unit_mateEquiv adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) c)

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d c : RingCon M
s t : ↑(Set.Ici c)
⊢ { toFun := fun d ↦ mapGen ⇑c.mk', invFun := fun d ↦ ⟨d.comap c.mk', ⋯⟩, left_inv := ⋯, right_inv := ⋯ } s ≤
      { toFun := fun d ↦ mapGen ⇑c.mk', invFun := fun d ↦ ⟨d.comap c.mk', ⋯⟩, left_inv := ⋯, right_inv := ⋯ } t ↔
    s ≤ t

Tactic:
by
    simp only [Equiv.coe_fn_mk, le_def, c.mk'_surjective.forall, ← Subtype.coe_le_coe]
    simp_rw [mapGen_apply_apply_of_surjective c.mk' (c.ker_mk'_eq.trans_le s.2) c.mk'_surjective,
      mapGen_apply_apply_of_surjective c.mk' (c.ker_mk'_eq.trans_le t.2) c.mk'_surjective]

Goal state after:
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
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
of_apply : ∀ {x : M}, ↑(of x) = (TensorAlgebra.ι R) x
x✝ : M
⊢ ((AlgHom.id R (TensorAlgebra R M)).toLinearMap ∘ₗ TensorAlgebra.ι R) x✝ =
    ((s.val.comp ((lift R) of)).toLinearMap ∘ₗ TensorAlgebra.ι R) x✝

Tactic:
simp [of_apply]

Goal state after:
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
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
of_apply : ∀ {x : M}, ↑(of x) = (TensorAlgebra.ι R) x
of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp ((lift R) of)
⊢ C ((AlgHom.id R (TensorAlgebra R M)) a)

Tactic:
of_id

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 }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
of_apply : ∀ {x : M}, ↑(of x) = (TensorAlgebra.ι R) x
of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp ((lift R) of)
⊢ C ((s.val.comp ((lift R) of)) a)
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
repr : Repr R a ι
⊢ ∑ i ∈ repr.index, repr.left i ⊗ₜ[R] counit (repr.right i) = a ⊗ₜ[R] 1

Tactic:
by
  simpa [← repr.eq, map_sum] using congr($(lTensor_counit_comp_comul (R := R) (A := A)) a)

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
⊢ 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:
fst_comp_inl,

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.id = (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 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 ∘ₗ inl R A B) (LinearMap.fst R A B ∘ₗ inl R A B) ∘ₗ comul

Tactic:
fst_comp_inl,

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.id LinearMap.id ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : AddCommMonoid C
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Module R C
inst✝² : CoalgebraStruct R A
inst✝¹ : CoalgebraStruct R B
inst✝ : CoalgebraStruct R C
e✝ e' e : A ≃ₗc[R] B
⊢ TensorProduct.map ↑e.toLinearEquiv.symm ↑e.toLinearEquiv.symm ∘ₗ comul = comul ∘ₗ ↑e.toLinearEquiv.symm

Tactic:
by
      change (TensorProduct.congr (e : A ≃ₗ[R] B) (e : A ≃ₗ[R] B)).symm.toLinearMap ∘ₗ comul
        = comul ∘ₗ (e : A ≃ₗ[R] B).symm
      rw [LinearEquiv.toLinearMap_symm_comp_eq]
      simp only [TensorProduct.congr, toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe,
        LinearEquiv.toLinearMap_ofLinearMap, ← LinearMap.comp_assoc, CoalgHomClass.map_comp_comul]
      rw [← toLinearEquiv_toLinearMap, LinearEquiv.comp_symm_cancel_right]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ ((LinearMap.rTensor B (counit ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ comul) ∘ₗ
      ↑f.toLinearEquiv.symm =
    (TensorProduct.mk R R B) 1

Tactic:
f.toLinearEquiv.comp_toLinearMap_symm_eq

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ (LinearMap.rTensor B (counit ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ comul =
    (TensorProduct.mk R R B) 1 ∘ₗ f.toLinearMap
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ ((LinearMap.lTensor B (counit ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ comul) ∘ₗ
      ↑f.toLinearEquiv.symm =
    (TensorProduct.mk R B R).flip 1

Tactic:
f.toLinearEquiv.comp_toLinearMap_symm_eq

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ (LinearMap.lTensor B (counit ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ comul =
    (TensorProduct.mk R B R).flip 1 ∘ₗ f.toLinearMap
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
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
⊢ ((lift f g hg hfg hgf).comp (inlAlgHom S R M)).range ⊔ Algebra.adjoin S (⇑(lift f g hg hfg hgf) '' Set.range inr) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range ⇑g)

Tactic:
lift_comp_inlHom,

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
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
⊢ f.range ⊔ Algebra.adjoin S (⇑(lift f g hg hfg hgf) '' Set.range inr) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range ⇑g)
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)
⊢ lTensor ((i : n) → A i) counit ∘ₗ comul = (TensorProduct.mk R ((i : n) → A i) R).flip 1

Tactic:
by
    ext : 1
    rw [comp_assoc, comul_comp_single, ← comp_assoc, lTensor_comp_map, counit_comp_single,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]

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_1
S : Type u_2
inst✝³ : Ring R
inst✝² : Ring S
f : R →+* S
J : Type u_3
inst✝¹ : Category.{v_1, u_3} J
F : J ⥤ ModuleCat S
inst✝ : Small.{v, max u_3 v} ↑(F ⋙ forget (ModuleCat S)).sections
c : Cone F
hc : IsLimit c
hc' : IsLimit ((forget₂ (ModuleCat S) AddCommGrpCat).mapCone c)
⊢ IsLimit ((restrictScalars f).mapCone c)

Tactic:
exact isLimitOfReflects (forget₂ _ AddCommGrpCat) hc'

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
g : P →ₗ[R] M ⊗[R] N
⊢ α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹ ∘ₗ g = (f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹ ∘ₗ g

Tactic:
simp_rw [← LinearMap.comp_assoc, ← assoc_symm_comp_map_rid_symm]

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ F.map Δ ≫ F.map (ε ▷ A) ≫ δ F (𝟙_ C) A ≫ η F ▷ F.obj A = F.map (λ_ A).inv ≫ δ F (𝟙_ C) A ≫ η F ▷ F.obj A

Tactic:
← F.map_comp_assoc,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ F.map (Δ ≫ ε ▷ A) ≫ δ F (𝟙_ C) A ≫ η F ▷ F.obj A = F.map (λ_ A).inv ≫ δ F (𝟙_ C) A ≫ η F ▷ F.obj A
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ F.map Δ ≫ F.map (A ◁ ε) ≫ δ F A (𝟙_ C) ≫ F.obj A ◁ η F = F.map (ρ_ A).inv ≫ δ F A (𝟙_ C) ≫ F.obj A ◁ η F

Tactic:
← F.map_comp_assoc,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ F.map (Δ ≫ A ◁ ε) ≫ δ F A (𝟙_ C) ≫ F.obj A ◁ η F = F.map (ρ_ A).inv ≫ δ F A (𝟙_ C) ≫ F.obj A ◁ η F
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ F.map Δ ≫ F.map (A ◁ Δ) ≫ δ F A (A ⊗ A) ≫ F.obj A ◁ δ F A A =
    F.map Δ ≫ F.map (Δ ▷ A) ≫ δ F (A ⊗ A) A ≫ δ F A A ▷ F.obj A ≫ (α_ (F.obj A) (F.obj A) (F.obj A)).hom

Tactic:
← F.map_comp_assoc,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ F.map (Δ ≫ A ◁ Δ) ≫ δ F A (A ⊗ A) ≫ F.obj A ◁ δ F A A =
    F.map (Δ ≫ Δ ▷ A) ≫ δ F (A ⊗ A) A ≫ δ F A A ▷ F.obj A ≫ (α_ (F.obj A) (F.obj A) (F.obj A)).hom
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O : C
inst✝⁸ : ComonObj M
inst✝⁷ : ComonObj N
inst✝⁶ : ComonObj O
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.OplaxMonoidal
X Y : C
inst✝² : ComonObj X
inst✝¹ : ComonObj Y
f : X ⟶ Y
inst✝ : IsComonHom f
⊢ F.map f ≫ F.map ε ≫ η F = F.map ε ≫ η F

Tactic:
← F.map_comp_assoc,

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O : C
inst✝⁸ : ComonObj M
inst✝⁷ : ComonObj N
inst✝⁶ : ComonObj O
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.OplaxMonoidal
X Y : C
inst✝² : ComonObj X
inst✝¹ : ComonObj Y
f : X ⟶ Y
inst✝ : IsComonHom f
⊢ F.map (f ≫ ε) ≫ η F = F.map ε ≫ η F
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O : C
inst✝⁸ : ComonObj M
inst✝⁷ : ComonObj N
inst✝⁶ : ComonObj O
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.OplaxMonoidal
X Y : C
inst✝² : ComonObj X
inst✝¹ : ComonObj Y
f : X ⟶ Y
inst✝ : IsComonHom f
⊢ F.map f ≫ F.map Δ ≫ δ F Y Y = F.map Δ ≫ F.map (f ⊗ₘ f) ≫ δ F Y Y

Tactic:
← F.map_comp_assoc,

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O : C
inst✝⁸ : ComonObj M
inst✝⁷ : ComonObj N
inst✝⁶ : ComonObj O
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.OplaxMonoidal
X Y : C
inst✝² : ComonObj X
inst✝¹ : ComonObj Y
f : X ⟶ Y
inst✝ : IsComonHom f
⊢ F.map (f ≫ Δ) ≫ δ F Y Y = F.map Δ ≫ F.map (f ⊗ₘ f) ≫ δ F Y Y
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O : C
inst✝⁸ : ComonObj M
inst✝⁷ : ComonObj N
inst✝⁶ : ComonObj O
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.OplaxMonoidal
X Y : C
inst✝² : ComonObj X
inst✝¹ : ComonObj Y
f : X ⟶ Y
inst✝ : IsComonHom f
⊢ F.map (f ≫ Δ) ≫ δ F Y Y = F.map Δ ≫ F.map (f ⊗ₘ f) ≫ δ F Y Y

Tactic:
← F.map_comp_assoc,

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O : C
inst✝⁸ : ComonObj M
inst✝⁷ : ComonObj N
inst✝⁶ : ComonObj O
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.OplaxMonoidal
X Y : C
inst✝² : ComonObj X
inst✝¹ : ComonObj Y
f : X ⟶ Y
inst✝ : IsComonHom f
⊢ F.map (f ≫ Δ) ≫ δ F Y Y = F.map (Δ ≫ (f ⊗ₘ f)) ≫ δ F Y Y