mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
⊢ ∀ (a b c : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a +
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b) *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c =
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c

Tactic:
intro x y z

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x y z : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel y) *
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel z =
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel z +
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel y *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel z
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case neg.inl
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi hjs : i ∈ s
hji : ¬i < i
⊢ (if i = i then s.piecewise a v i - b i else b i) = if i = i then a i - b i else b i

Tactic:
if_pos rfl,

Goal state after:
case neg.inl
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi hjs : i ∈ s
hji : ¬i < i
⊢ s.piecewise a v i - b i = if i = i then a i - b i else b i
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case neg.inl
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi hjs : i ∈ s
hji : ¬i < i
⊢ s.piecewise a v i - b i = if i = i then a i - b i else b i

Tactic:
if_pos rfl,

Goal state after:
case neg.inl
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi hjs : i ∈ s
hji : ¬i < i
⊢ s.piecewise a v i - b i = a i - b i
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : Category.{t, v} J
F : J ⥤ ModuleCat R
c : Cone F
hc : IsLimit ((forget₂ (ModuleCat R) AddCommGrpCat).mapCone c)
this✝ : HasLimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
this : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
⊢ IsLimit c

Tactic:
have := reflectsLimit_of_reflectsIsomorphisms F (forget₂ (ModuleCat R) AddCommGrpCat)

Goal state after:
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : Category.{t, v} J
F : J ⥤ ModuleCat R
c : Cone F
hc : IsLimit ((forget₂ (ModuleCat R) AddCommGrpCat).mapCone c)
this✝¹ : HasLimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
this✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
this : ReflectsLimit F (forget₂ (ModuleCat R) AddCommGrpCat)
⊢ IsLimit c
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : L.Faithful
X Y : C
f g : Y ⟶ (𝟭 C).obj X
hfg : f ≫ h.unit.app X = g ≫ h.unit.app X
⊢ (h.homEquiv Y (L.obj X)) (L.map f) = (h.homEquiv Y (L.obj X)) (L.map g)

Tactic:
by simpa using hfg

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
⊢ ofHom { toFun := fun g ↦ ⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ } ≫
      kernel.lift f (ofHom (Hom.hom f).ker.subtype) ⋯ =
    𝟙 (kernel f)

Tactic:
refine equalizer.hom_ext ?_

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
⊢ (ofHom { toFun := fun g ↦ ⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ } ≫
        kernel.lift f (ofHom (Hom.hom f).ker.subtype) ⋯) ≫
      equalizer.ι f 0 =
    𝟙 (kernel f) ≫ equalizer.ι f 0
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : R.IsEquivalence
⊢ IsIso h.counit

Tactic:
have := h.isEquivalence_left_of_isEquivalence_right

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : R.IsEquivalence
this : L.IsEquivalence
⊢ IsIso h.counit
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
f : Y ≅ Z
⊢ X ◁ f.inv ≫ X ◁ f.hom = 𝟙 (X ⊗ Z)

Tactic:
rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]

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
X : C
J : Type
inst✝ : Finite J
val✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
⊢ ∑ j, X ◁ b.π j ≫ X ◁ b.ι j = 𝟙 (X ⊗ b.pt)

Tactic:
simp_rw [← id_tensorHom]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Finite J
val✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
⊢ ∑ x, (𝟙 X ⊗ₘ b.π x) ≫ (𝟙 X ⊗ₘ b.ι x) = 𝟙 (X ⊗ b.pt)
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: case intro
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 Y : C
f : J → C
val✝ : Fintype J
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x,
        (𝟙 X ⊗ₘ Y ◁ biproduct.π f x) ≫ (𝟙 X ⊗ₘ biproduct.ι (fun j ↦ Y ⊗ f j) x) ≫ X ◁ biproduct.π (fun j ↦ Y ⊗ f j) j✝
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (X ⊗ Y) ◁ biproduct.π f j✝ ≫ (α_ X Y (f j✝)).hom else 0

Tactic:
simp_rw [← id_tensorHom]

Goal state after:
case intro
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 Y : C
f : J → C
val✝ : Fintype J
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x,
        (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ biproduct.π f x) ≫
          (𝟙 X ⊗ₘ biproduct.ι (fun j ↦ Y ⊗ f j) x) ≫ (𝟙 X ⊗ₘ biproduct.π (fun j ↦ Y ⊗ f j) j✝)
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (𝟙 (X ⊗ Y) ⊗ₘ biproduct.π f j✝) ≫ (α_ X Y (f j✝)).hom else 0
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ : SemimoduleCat R
X₂ : SemimoduleCat R
X₃ : SemimoduleCat R
Y₁ : SemimoduleCat R
Y₂ : SemimoduleCat R
Y₃ : SemimoduleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ∀ (x : ↑X₁) (y : ↑X₂) (z : ↑X₃),
    (Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))) (x ⊗ₜ[R] y ⊗ₜ[R] z)

Tactic:
intro x y z

Goal state after:
R : Type u
inst✝ : CommSemiring R
X₁ : SemimoduleCat R
X₂ : SemimoduleCat R
X₃ : SemimoduleCat R
Y₁ : SemimoduleCat R
Y₂ : SemimoduleCat R
Y₃ : SemimoduleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
x : ↑X₁
y : ↑X₂
z : ↑X₃
⊢ (Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
    (Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))) (x ⊗ₜ[R] y ⊗ₜ[R] 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
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ 𝟙 (F.obj ((X ⊗ Y) ⊗ Z)) = δ F (X ⊗ Y) Z ≫ μ F (X ⊗ Y) Z

Tactic:
δ_μ

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.Monoidal
X Y Z : C
⊢ 𝟙 (F.obj ((X ⊗ Y) ⊗ Z)) = 𝟙 (F.obj ((X ⊗ Y) ⊗ Z))
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y : SemimoduleCat R
f : X ⟶ Y
Z : SemimoduleCat R
⊢ f ▷ Z ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ Z ◁ f

Tactic:
simp_rw [← id_tensorHom]

Goal state after:
R : Type u
inst✝ : CommSemiring R
X Y : SemimoduleCat R
f : X ⟶ Y
Z : SemimoduleCat R
⊢ f ▷ Z ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ (𝟙 Z ⊗ₘ f)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
f : Y ⟶ Z
⊢ X ◁ f ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ f ▷ X

Tactic:
simp_rw [← id_tensorHom]

Goal state after:
R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
f : Y ⟶ Z
⊢ (𝟙 X ⊗ₘ f) ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ f ▷ X
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom ((α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z)

Tactic:
intro x y z

Goal state after:
R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
x : ↑X
y : ↑Y
z : ↑Z
⊢ (Hom.hom ((α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
    (Hom.hom ((X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y)) (x ⊗ₜ[R] y ⊗ₜ[R] z)

Tactic:
intro x y z

Goal state after:
R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
x : ↑X
y : ↑Y
z : ↑Z
⊢ (Hom.hom ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
    (Hom.hom ((α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y)) (x ⊗ₜ[R] y ⊗ₜ[R] 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 ⥤ 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.map (adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
          F.obj (G.obj X) ◁ F.map (G.map (δ F (G.obj Y) (G.obj Z))) ≫
            F.obj (G.obj X) ◁ F.map (G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
              adj.counit.app X ▷ F.obj (G.obj (Y ⊗ Z)) ≫ X ◁ adj.counit.app (Y ⊗ Z)

Tactic:
rw [← whisker_exchange, ← MonoidalCategory.whiskerLeft_comp_assoc,
      ← MonoidalCategory.whiskerLeft_comp_assoc,
      ← MonoidalCategory.whiskerLeft_comp_assoc, assoc, assoc,
      counit_naturality, counit_naturality_assoc, left_triangle_components_assoc,
      MonoidalCategory.whiskerLeft_comp, assoc, tensorHom_def, whisker_exchange]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ identities Cᵒᵖ f ↔ identities C f.unop

Tactic:
obtain ⟨X⟩ := X
  obtain ⟨f⟩ := f
  dsimp
  exact ⟨fun ⟨_⟩ ↦ ⟨_⟩, fun ⟨_⟩ ↦ ⟨_⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
W✝ : MorphismProperty C
F : C ⥤ D
W : MorphismProperty D
inst✝ : W.HasTwoOutOfThreeProperty
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hg : W.inverseImage F g
hfg : W.inverseImage F (f ≫ g)
⊢ W (F.map f ≫ F.map g)

Tactic:
by simpa using hfg

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
W✝ : MorphismProperty C
F : C ⥤ D
W : MorphismProperty D
inst✝ : W.HasTwoOutOfThreeProperty
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : W.inverseImage F f
hfg : W.inverseImage F (f ≫ g)
⊢ W (F.map f ≫ F.map g)

Tactic:
by simpa using hfg

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) ⊗ₘ adj.unit.app Z) ≫
    μ G (F.obj (X ⊗ Y)) (F.obj Z) ≫
      G.map
        ((adj.homEquiv (X ⊗ Y) (F.obj X ⊗ F.obj Y)).symm
              ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷
            F.obj Z ≫
          (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom)

Tactic:
rw [homEquiv_counit, map_comp_assoc, map_comp,
        ← μ_natural_left_assoc, map_comp, map_comp, tensorHom_def'_assoc]
      dsimp
      rw [← comp_whiskerRight_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
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
| (X ⊗ Y) ◁ adj.unit.app Z ≫
    (adj.unit.app (X ⊗ Y) ≫
          G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
            G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫ G.map (adj.counit.app (F.obj X ⊗ F.obj Y))) ▷
        G.obj (F.obj Z) ≫
      μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom
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 : C
⊢ (β_ X (𝟙_ C)).hom ≫ (λ_ X).hom ≫ (ρ_ X).inv = 𝟙 (X ⊗ 𝟙_ C)

Tactic:
rw [braiding_tensorUnit_right]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((ρ_ X).hom ≫ (λ_ X).inv) ≫ (λ_ X).hom ≫ (ρ_ X).inv = 𝟙 (X ⊗ 𝟙_ C)
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)
j : J
r : R
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (((Functor.const J).obj (mkOfSMul (coconePointSMul F))).obj j).smul r =
    (F.obj j).smul r ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j

Tactic:
dsimp
        -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
        erw [mkOfSMul_smul]
        simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
x : ↑H
⊢ ((Hom.hom
            (ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯) ≫
              cokernel.desc f (ofHom (mk' (Hom.hom f).range)) ⋯)).comp
        (mk' (Hom.hom f).range))
      x =
    ((Hom.hom (𝟙 (of (↑H ⧸ (Hom.hom f).range)))).comp (mk' (Hom.hom f).range)) x

Tactic:
dsimp only [hom_comp, hom_ofHom, hom_zero, AddMonoidHom.coe_comp, coe_mk',
      Function.comp_apply, AddMonoidHom.zero_apply, id_eq, lift_mk, hom_id, AddMonoidHom.coe_id]

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
x : ↑H
⊢ (Hom.hom (cokernel.desc f (ofHom (mk' (Hom.hom f).range)) ⋯))
      ((lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯) ↑x) =
    ↑x
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
d : RingCon c.Quotient
⊢ (fun d ↦ mapGen ⇑c.mk') ((fun d ↦ ⟨d.comap c.mk', ⋯⟩) d) = d

Tactic:
ext x y
    simp only
    obtain ⟨x, rfl⟩ := c.mk'_surjective x
    obtain ⟨y, rfl⟩ := c.mk'_surjective y
    rw [mapGen_apply_apply_of_surjective _ (comap_bot c.mk' ▸ comap_mono bot_le) c.mk'_surjective,
      comap_rel]

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
⊢ ∀ x ∈ (ι R).range, x ∈ 1 → x = 0

Tactic:
Submodule.one_eq_range

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ x ∈ (ι R).range, x ∈ (Algebra.linearMap R (TensorAlgebra R M)).range → x = 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
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)) ∘ₗ ↑(TensorProduct.assoc R A A A)) ∘ₗ
          rTensor A comul) ∘ₗ
        comul)
      x

Tactic:
TensorProduct.map_map_comp_assoc_eq,

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.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
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring 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
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' 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
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ f (r₁ * r₂) + g (r₁ •> m₂ + m₁ <• r₂) = f (r₁ * r₂) + g m₁ * f r₂ + f r₁ * g m₂

Tactic:
map_add,

Goal state after:
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring 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
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' 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
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ f (r₁ * r₂) + (g (r₁ •> m₂) + g (m₁ <• r₂)) = f (r₁ * r₂) + g m₁ * f r₂ + f r₁ * g m₂
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)) ∘ₗ ↑(TensorProduct.assoc R B B B)) ∘ₗ
          rTensor B comul) ∘ₗ
        comul)
      x

Tactic:
TensorProduct.map_map_comp_assoc_eq,

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.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
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:
map_add,

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
s : S
g : X ⟶ (restrictScalars f).obj Y
x✝ y✝ : ↑X
⊢ s • ((ConcreteCategory.hom g) x✝ + (ConcreteCategory.hom g) y✝) =
    s • (ConcreteCategory.hom g) x✝ + s • (ConcreteCategory.hom g) y✝