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✝ : Finite J
f : J → C
X Y Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), biproduct.ι f j ▷ X ▷ Y ≫ g = biproduct.ι f j ▷ X ▷ Y ≫ h
⊢ g = h

Tactic:
by
  apply (cancel_epi (α_ _ _ _).inv).mp
  ext
  simp [w]

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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X : C
⊢ (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom

Tactic:
right_unitality

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
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ μ G (F.obj x✝²) (F.obj x✝¹) ▷ G.obj (F.obj x✝) ≫
      μ G (F.obj x✝² ⊗ F.obj x✝¹) (F.obj x✝) ≫
        G.map (μ F x✝² x✝¹ ▷ F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝) ≫ G.map (F.map (α_ x✝² x✝¹ x✝).hom) =
    (α_ (G.obj (F.obj x✝²)) (G.obj (F.obj x✝¹)) (G.obj (F.obj x✝))).hom ≫
      G.obj (F.obj x✝²) ◁ (μ G (F.obj x✝¹) (F.obj x✝) ≫ G.map (μ F x✝¹ x✝)) ≫
        μ G (F.obj x✝²) (F.obj (x✝¹ ⊗ x✝)) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))

Tactic:
MonoidalCategory.whiskerLeft_comp,

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
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ μ G (F.obj x✝²) (F.obj x✝¹) ▷ G.obj (F.obj x✝) ≫
      μ G (F.obj x✝² ⊗ F.obj x✝¹) (F.obj x✝) ≫
        G.map (μ F x✝² x✝¹ ▷ F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝) ≫ G.map (F.map (α_ x✝² x✝¹ x✝).hom) =
    (α_ (G.obj (F.obj x✝²)) (G.obj (F.obj x✝¹)) (G.obj (F.obj x✝))).hom ≫
      (G.obj (F.obj x✝²) ◁ μ G (F.obj x✝¹) (F.obj x✝) ≫ G.obj (F.obj x✝²) ◁ G.map (μ F x✝¹ x✝)) ≫
        μ G (F.obj x✝²) (F.obj (x✝¹ ⊗ x✝)) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))
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 Z : C
⊢ G.map (F.map (α_ X Y Z).hom) ≫
      G.map (δ F X (Y ⊗ Z)) ≫
        G.map (F.obj X ◁ δ F Y Z) ≫ δ G (F.obj X) (F.obj Y ⊗ F.obj Z) ≫ G.obj (F.obj X) ◁ δ G (F.obj Y) (F.obj Z) =
    G.map (F.map (α_ X Y Z).hom) ≫
      G.map (δ F X (Y ⊗ Z)) ≫
        δ G (F.obj X) (F.obj (Y ⊗ Z)) ≫ G.obj (F.obj X) ◁ (G.map (δ F Y Z) ≫ δ G (F.obj Y) (F.obj Z))

Tactic:
MonoidalCategory.whiskerLeft_comp,

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
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ G.map (F.map (α_ X Y Z).hom) ≫
      G.map (δ F X (Y ⊗ Z)) ≫
        G.map (F.obj X ◁ δ F Y Z) ≫ δ G (F.obj X) (F.obj Y ⊗ F.obj Z) ≫ G.obj (F.obj X) ◁ δ G (F.obj Y) (F.obj Z) =
    G.map (F.map (α_ X Y Z).hom) ≫
      G.map (δ F X (Y ⊗ Z)) ≫
        δ G (F.obj X) (F.obj (Y ⊗ Z)) ≫ G.obj (F.obj X) ◁ G.map (δ F Y Z) ≫ G.obj (F.obj X) ◁ δ G (F.obj Y) (F.obj Z)
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
hc : IsLimit c
s : Cocone F.unop
m : (coconeUnopOfCone c).pt ⟶ s.pt
w : ∀ (j : J), (coconeUnopOfCone c).ι.app j ≫ m = s.ι.app j
⊢ m = (hc.lift (coneOfCoconeUnop 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 (unop j)

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
⊢ G.map f ▷ G.obj X' ≫
      (adj.homEquiv (G.obj Y ⊗ G.obj X') (Y ⊗ X'))
        (δ F (G.obj Y) (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')) =
    (adj.homEquiv (G.obj X ⊗ G.obj X') (X ⊗ X')) (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X')) ≫
      G.map (f ▷ X')

Tactic:
simp only [Adjunction.homEquiv_apply, ← adj.unit_naturality_assoc, ← G.map_comp, assoc,
      ← δ_natural_left_assoc F]

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
⊢ adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')) =
    adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X')
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 ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z) =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ (δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
          adj.counit.app X ▷ (Y ⊗ Z)

Tactic:
MonoidalCategory.whiskerLeft_comp,

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z) =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        (F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ F.obj (G.obj X) ◁ (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
          adj.counit.app X ▷ (Y ⊗ Z)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ⊗≫ Y ◁ (β_ X Z).hom ⊗≫ (β_ Y Z).hom ▷ X =
    (α_ X Y Z).inv ≫ 𝟙 ((X ⊗ Y) ⊗ Z) ⊗≫ (X ◁ (β_ Y Z).hom ⊗≫ (β_ X Z).hom ▷ Y ⊗≫ Z ◁ (β_ X Y).hom) ⊗≫ 𝟙 ((Z ⊗ Y) ⊗ X)

Tactic:
← cancel_mono (α_ Z Y X).hom

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ⊗≫ Y ◁ (β_ X Z).hom ⊗≫ (β_ Y Z).hom ▷ X) ≫ (α_ Z Y X).hom =
    ((α_ X Y Z).inv ≫
        𝟙 ((X ⊗ Y) ⊗ Z) ⊗≫ (X ◁ (β_ Y Z).hom ⊗≫ (β_ X Z).hom ▷ Y ⊗≫ Z ◁ (β_ X Y).hom) ⊗≫ 𝟙 ((Z ⊗ Y) ⊗ X)) ≫
      (α_ Z Y X).hom
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 ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    (adj.homEquiv (G.obj X ⊗ 𝟙_ C) X).symm
      (G.obj X ◁ (adj.unit.app (𝟙_ C) ≫ G.map (η F)) ≫
        (adj.homEquiv (G.obj X ⊗ G.obj (𝟙_ D)) (X ⊗ 𝟙_ D))
            (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D))) ≫
          G.map (ρ_ X).hom)

Tactic:
MonoidalCategory.whiskerLeft_comp,

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    (adj.homEquiv (G.obj X ⊗ 𝟙_ C) X).symm
      ((G.obj X ◁ adj.unit.app (𝟙_ C) ≫ G.obj X ◁ G.map (η F)) ≫
        (adj.homEquiv (G.obj X ⊗ G.obj (𝟙_ D)) (X ⊗ 𝟙_ D))
            (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D))) ≫
          G.map (ρ_ X).hom)
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 X✝ Y✝ ▷ F.obj Z✝ ≫ μ F (X✝ ⊗ Y✝) Z✝ ≫ F.map ((α_ X✝ Y✝ Z✝).hom ≫ (β X✝ (Y✝ ⊗ Z✝)).hom ≫ (α_ Y✝ Z✝ X✝).hom) =
    μ F X✝ Y✝ ▷ F.obj Z✝ ≫ μ F (X✝ ⊗ Y✝) Z✝ ≫ F.map ((β X✝ Y✝).hom ▷ Z✝ ≫ (α_ Y✝ X✝ Z✝).hom ≫ Y✝ ◁ (β X✝ Z✝).hom)

Tactic:
rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp, ←
      μ_natural_left_assoc, ← comp_whiskerRight_assoc, w,
      comp_whiskerRight_assoc, Functor.LaxMonoidal.associativity_assoc,
      Functor.LaxMonoidal.associativity_assoc, ← μ_natural_right, ←
      whiskerLeft_comp_assoc, w, whiskerLeft_comp_assoc,
      reassoc_of% w, braiding_naturality_right_assoc,
      Functor.LaxMonoidal.associativity, hexagon_forward_assoc]

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      G.obj (F.obj X) ◁
          ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫
            adj.unit.app (G.obj (F.obj Y) ⊗ G.obj (F.obj Z)) ≫
              G.map (F.map (μ G (F.obj Y) (F.obj Z))) ≫ G.map (adj.counit.app (F.obj Y ⊗ F.obj Z))) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)

Tactic:
MonoidalCategory.whiskerLeft_comp,

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      (G.obj (F.obj X) ◁ (adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫
          G.obj (F.obj X) ◁
            (adj.unit.app (G.obj (F.obj Y) ⊗ G.obj (F.obj Z)) ≫
              G.map (F.map (μ G (F.obj Y) (F.obj Z))) ≫ G.map (adj.counit.app (F.obj Y ⊗ F.obj Z)))) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)
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 G L₁ L₂ H
X✝ : C
⊢ L₂.map (G.map (adj₁.unit.app X✝)) ≫ α.natTrans.app (R₁.obj (L₁.obj X✝)) ≫ H.map (adj₁.counit.app (L₁.obj X✝)) =
    α.natTrans.app X✝

Tactic:
← assoc,

Goal state after:
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 G L₁ L₂ H
X✝ : C
⊢ (L₂.map (G.map (adj₁.unit.app X✝)) ≫ α.natTrans.app (R₁.obj (L₁.obj X✝))) ≫ H.map (adj₁.counit.app (L₁.obj X✝)) =
    α.natTrans.app X✝
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₂
X✝ : D
⊢ G.map (adj₁.unit.app (R₁.obj X✝)) ≫ β.natTrans.app (L₁.obj (R₁.obj X✝)) ≫ R₂.map (H.map (adj₁.counit.app X✝)) =
    β.natTrans.app X✝

Tactic:
← assoc,

Goal state after:
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₂
X✝ : D
⊢ (G.map (adj₁.unit.app (R₁.obj X✝)) ≫ β.natTrans.app (L₁.obj (R₁.obj X✝))) ≫ R₂.map (H.map (adj₁.counit.app X✝)) =
    β.natTrans.app X✝
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₂
X✝ : D
⊢ G.map (adj₁.unit.app (R₁.obj X✝)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X✝) ≫ β.natTrans.app X✝ = β.natTrans.app X✝

Tactic:
← assoc,

Goal state after:
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₂
X✝ : D
⊢ (G.map (adj₁.unit.app (R₁.obj X✝)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X✝)) ≫ β.natTrans.app X✝ = β.natTrans.app X✝
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: case add
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
x y : FreeAlgebra R M
a✝ b✝ : M
⊢ (RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom) (FreeAlgebra.ι R (a✝ + b✝))
    (FreeAlgebra.ι R a✝ + FreeAlgebra.ι R b✝)

Tactic:
simp [Algebra.smul_def, FreeAlgebra.lift_ι_apply,
            map_mul, AlgHom.commutes, map_add, RingCon.ker]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: case smul
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
x y : FreeAlgebra R M
r✝ : R
a✝ : M
⊢ (RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom) (FreeAlgebra.ι R (r✝ • a✝))
    ((algebraMap R (FreeAlgebra R M)) r✝ * FreeAlgebra.ι R a✝)

Tactic:
simp [Algebra.smul_def, FreeAlgebra.lift_ι_apply,
            map_mul, AlgHom.commutes, map_add, RingCon.ker]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 0 •> x.2 + 0 <• x.1 = 0

Tactic:
rw [zero_smul, zero_add, smul_zero]

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

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
κ : ι → Type u_2
Λ : ι → Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_4
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_5
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f g h : F
a : A
repr : Repr R a ι
a₁ : (i : ι) → Repr R (repr.left i) (κ i)
a₂ : (i : ι) → Repr R (repr.right i) (Λ i)
⊢ ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, f (repr.left i) ⊗ₜ[R] (g ((a₂ i).left j) ⊗ₜ[R] h ((a₂ i).right j)) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, f ((a₁ i).left j) ⊗ₜ[R] (g ((a₁ i).right j) ⊗ₜ[R] h (repr.right i))

Tactic:
have := sum_tmul_tmul_eq repr a₁ a₂
  apply_fun TensorProduct.map (f : A →ₗ[R] B)
    (TensorProduct.map (g : A →ₗ[R] B) (h : A →ₗ[R] B)) at this
  simp_all only [map_sum, TensorProduct.map_tmul, LinearMap.coe_coe]

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
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
s : S
m : ↑M
⊢ s ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m

Tactic:
ExtendScalars.smul_tmul,

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
s : S
m : ↑M
⊢ s ⊗ₜ[R] m = (s * 1) ⊗ₜ[R] m
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case tmul
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : ↑X
x : S
⊢ (ConcreteCategory.hom g) (x • 1 ⊗ₜ[R] s) = (Hom.hom g) (x ⊗ₜ[R] s)

Tactic:
ExtendScalars.smul_tmul,

Goal state after:
case tmul
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : ↑X
x : S
⊢ (ConcreteCategory.hom g) ((x * 1) ⊗ₜ[R] s) = (Hom.hom g) (x ⊗ₜ[R] s)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case add
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
ih1 : (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) x✝ = (Hom.hom g) x✝
ih2 : (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) y✝ = (Hom.hom g) y✝
⊢ (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) (x✝ + y✝) = (Hom.hom g) (x✝ + y✝)

Tactic:
rw [map_add, map_add, ih1, ih2]

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
g : (extendScalars f).obj X ⟶ Y
⊢ HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g) = g

Tactic:
let m1 : Module R S := Module.compHom S f; let m2 : Module R Y := Module.compHom Y f
    apply hom_ext
    apply LinearMap.ext; intro z
    induction z using TensorProduct.induction_on with
    | zero => rw [map_zero, map_zero]
    | tmul x s =>
      erw [TensorProduct.lift.tmul]
      simp only [LinearMap.coe_mk]
      change S at x
      dsimp
      erw [← map_smul, ExtendScalars.smul_tmul, mul_one x]
      rfl
    | add _ _ ih1 ih2 => rw [map_add, map_add, ih1, ih2]

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
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x : ↑X
⊢ (Hom.hom (HomEquiv.toRestrictScalars f (HomEquiv.fromExtendScalars f g))) x = (Hom.hom g) x

Tactic:
rw [HomEquiv.toRestrictScalars_hom_apply]

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x : ↑X
⊢ (ConcreteCategory.hom (HomEquiv.fromExtendScalars f g)) (1 ⊗ₜ[R] x) = (Hom.hom g) x
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case tmul
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
x✝ : ↑((restrictScalars f).obj (of S S))
y✝ : ↑X
⊢ (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) (x✝ ⊗ₜ[R] y✝) =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) (x✝ ⊗ₜ[R] y✝)

Tactic:
rw [ExtendRestrictScalarsAdj.homEquiv_symm_apply]
          dsimp
          -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
          erw [ExtendRestrictScalarsAdj.Counit.map_hom_apply,
              ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply]

Goal state after: