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
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
f✝ g✝ : Y✝ ⟶ Z✝
⊢ (f✝ + g✝) ▷ X✝ = f✝ ▷ X✝ + g✝ ▷ X✝

Tactic:
apply F.map_injective

Goal state after:
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
f✝ g✝ : Y✝ ⟶ Z✝
⊢ F.map ((f✝ + g✝) ▷ X✝) = F.map (f✝ ▷ X✝ + g✝ ▷ X✝)
Module: Mathlib.CategoryTheory.Monoidal.Linear

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ X ◁ (r • f) = r • X ◁ f

Tactic:
apply F.map_injective

Goal state after:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ F.map (X ◁ (r • f)) = F.map (r • X ◁ f)
Module: Mathlib.CategoryTheory.Monoidal.Linear

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ (r • f) ▷ Z = r • f ▷ Z

Tactic:
apply F.map_injective

Goal state after:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ F.map ((r • f) ▷ Z) = F.map (r • f ▷ Z)
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
f g h i : C
inst✝ : MonoidalCoherence g h
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
θ : h ⟶ i
θ' : h ≅ i
ih_θ : θ'.hom = θ
⊢ (η' ≪⊗≫ θ').hom = η ⊗≫ θ

Tactic:
by
  simp [ih_η, ih_θ, monoidalIsoComp, monoidalComp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : p ⊗ f₁ ≅ pf₁
η_g₁ : p ⊗ g₁ ≅ pf₁
η_f₂ : pf₁ ⊗ f₂ ≅ pf₁f₂
η_g₂ : pf₁ ⊗ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
⊢ p ◁ (η ⊗ᵢ θ) ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_f₁ η_f₂

Tactic:
rw [tensorIso_def]
  apply naturality_comp
  · apply naturality_whiskerRight _ _ _ ih_η
  · apply naturality_whiskerLeft _ _ _ ih_θ

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.Monoidal
⊢ CategoryTheory.inv (ε F) = η F

Tactic:
simp [← inv_η]

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.toLaxMonoidal = b.toLaxMonoidal
⊢ ε F ≫ η F = 𝟙 (𝟙_ D)

Tactic:
← @ε_η _ _ _ _ _ _ _ a,

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.toLaxMonoidal = b.toLaxMonoidal
⊢ ε F ≫ η F = ε F ≫ η F
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.toLaxMonoidal = b.toLaxMonoidal
⊢ ε F ≫ η F = ε F ≫ η F

Tactic:
← εIso_hom

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.toLaxMonoidal = b.toLaxMonoidal
⊢ (εIso F).hom ≫ η F = ε F ≫ η F
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 = 𝟙 (𝟙_ D)

Tactic:
← @ε_η _ _ _ _ _ _ _ a,

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 ≫ η F = ε F ≫ η F
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cone F.rightOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeRightOp c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeOfConeRightOp c).ι.app j ≫ m = s.ι.app j
⊢ m = (hc.lift (coneRightOpOfCocone s)).unop

Tactic:
by
    refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)
    simpa only [Quiver.Hom.op_unop, IsLimit.fac] using! w (op j)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ Z✝
⊢ X✝ ◁ f✝ ≫ (β X✝ Z✝).hom = (β X✝ Y✝).hom ≫ f✝ ▷ X✝

Tactic:
apply F.map_injective

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ Z✝
⊢ F.map (X✝ ◁ f✝ ≫ (β X✝ Z✝).hom) = F.map ((β X✝ Y✝).hom ≫ f✝ ▷ X✝)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
Z✝ : C
⊢ f✝ ▷ Z✝ ≫ (β Y✝ Z✝).hom = (β X✝ Z✝).hom ≫ Z✝ ◁ f✝

Tactic:
apply F.map_injective

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
Z✝ : C
⊢ F.map (f✝ ▷ Z✝ ≫ (β Y✝ Z✝).hom) = F.map ((β X✝ Z✝).hom ≫ Z✝ ◁ f✝)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ (α_ X✝ Y✝ Z✝).hom ≫ (β X✝ (Y✝ ⊗ Z✝)).hom ≫ (α_ Y✝ Z✝ X✝).hom =
    (β X✝ Y✝).hom ▷ Z✝ ≫ (α_ Y✝ X✝ Z✝).hom ≫ Y✝ ◁ (β X✝ Z✝).hom

Tactic:
apply F.map_injective

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ F.map ((α_ X✝ Y✝ Z✝).hom ≫ (β X✝ (Y✝ ⊗ Z✝)).hom ≫ (α_ Y✝ Z✝ X✝).hom) =
    F.map ((β X✝ Y✝).hom ▷ Z✝ ≫ (α_ Y✝ X✝ Z✝).hom ≫ Y✝ ◁ (β X✝ Z✝).hom)
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
this : Epi f
⊢ Function.Surjective ⇑(hom ((forget C).map f))

Tactic:
← epi_iff_surjective

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
this : Epi f
⊢ Epi ((forget C).map f)
Module: Mathlib.Algebra.Category.ModuleCat.EpiMono

Goal state before:
pp: R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
← epi_iff_surjective

Goal state after:
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi f
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ (α_ X✝ Y✝ Z✝).inv ≫ (β (X✝ ⊗ Y✝) Z✝).hom ≫ (α_ Z✝ X✝ Y✝).inv =
    X✝ ◁ (β Y✝ Z✝).hom ≫ (α_ X✝ Z✝ Y✝).inv ≫ (β X✝ Z✝).hom ▷ Y✝

Tactic:
apply F.map_injective

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ F.map ((α_ X✝ Y✝ Z✝).inv ≫ (β (X✝ ⊗ Y✝) Z✝).hom ≫ (α_ Z✝ X✝ Y✝).inv) =
    F.map (X✝ ◁ (β Y✝ Z✝).hom ≫ (α_ X✝ Z✝ Y✝).inv ≫ (β X✝ Z✝).hom ▷ Y✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (pushout.inr f.op g.op ≫ (pullbackIsoUnopPushout f g).hom.op).unop = (pullback.snd f g).op.unop

Tactic:
by simp [← pullbackIsoUnopPushout_inv_snd]

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

Goal state before:
pp: case refine_2
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 ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
this : F.OplaxMonoidal := adj.leftAdjointOplaxMonoidal
X Y : D
⊢ μ G X Y = adj.unit.app (G.obj X ⊗ G.obj Y) ≫ G.map (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y))

Tactic:
simp [homEquiv_counit, ← μ_natural, leftAdjointOplaxMonoidal_δ]

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
f : M →+* N
g : N →+* P
x y : M
⊢ (ker (g.comp f)) x y ↔ ((ker g).comap f) x y

Tactic:
by simp [ker_apply, comap_rel]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
⊢ ⇑(mapGen ⇑f) = Relation.Map ⇑c ⇑f ⇑f

Tactic:
refine le_antisymm ?_ <| (RingCon.gi N).gc.le_u_l _

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
⊢ ⇑(mapGen ⇑f) ≤ Relation.Map ⇑c ⇑f ⇑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
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι R = f ↔ g = (lift R) f

Tactic:
← (lift R).symm_apply_eq

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι R = f ↔ (lift R).symm g = f
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R✝ : Type u
inst✝² : CommRing R✝
R : Type v
inst✝¹ : CommRing R
inst✝ : Small.{u, v} R
e : AlgCat R ≌ AlgCat (Shrink.{u, v} R) := restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)
⊢ (forget₂ (AlgCat R) (ModuleCat R)).IsRightAdjoint

Tactic:
have : e.inverse ⋙ forget₂ (AlgCat R) (ModuleCat R) = forget₂ _ _ ⋙
      (ModuleCat.restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)).inverse :=
    rfl

Goal state after:
R✝ : Type u
inst✝² : CommRing R✝
R : Type v
inst✝¹ : CommRing R
inst✝ : Small.{u, v} R
e : AlgCat R ≌ AlgCat (Shrink.{u, v} R) := restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)
this :
  e.inverse ⋙ forget₂ (AlgCat R) (ModuleCat R) =
    forget₂ (AlgCat (Shrink.{u, v} R)) (ModuleCat (Shrink.{u, v} R)) ⋙
      (ModuleCat.restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)).inverse
⊢ (forget₂ (AlgCat R) (ModuleCat R)).IsRightAdjoint
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:
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:
ext; rfl

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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
L₀₁ : A ⥤ B
R₁₀ : B ⥤ A
L₁₂ : B ⥤ C
R₂₁ : C ⥤ B
L₂₃ : C ⥤ D
R₃₂ : D ⥤ C
adj₀₁ : L₀₁ ⊣ R₁₀
adj₁₂ : L₁₂ ⊣ R₂₁
adj₂₃ : L₂₃ ⊣ R₃₂
⊢ (conjugateEquiv (adj₀₁.comp (adj₁₂.comp adj₂₃)) ((adj₀₁.comp adj₁₂).comp adj₂₃)) (L₀₁.associator L₁₂ L₂₃).hom =
    (R₃₂.associator R₂₁ R₁₀).hom

Tactic:
by
  ext X
  simp only [comp_obj, conjugateEquiv_apply_app, Adjunction.comp_unit_app,
    Functor.comp_map, Category.assoc, ← map_comp, associator_hom_app, map_id,
    Adjunction.comp_counit_app, Category.id_comp]
  simp

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:
ext; rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Semiring B
inst✝⁹ : Semiring C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ f : A →ₐc[R] B
f' : A → B
h : f' = ⇑f
⊢ ∀ (x y : A), ((↑f).copy f' h).toFun (x * y) = ((↑f).copy f' h).toFun x * ((↑f).copy f' h).toFun y

Tactic:
intros; simp_all

Goal state after:
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; 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:
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:
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:
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:
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:
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:
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:
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✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
s : S
g : X ⟶ (restrictScalars f).obj Y
x✝ y✝ : ↑X
⊢ s • (ConcreteCategory.hom g) (x✝ + y✝) = s • (ConcreteCategory.hom g) x✝ + s • (ConcreteCategory.hom g) y✝

Tactic:
rw [map_add, smul_add]

Goal state after: