mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (c.π.app (Opposite.op 0)))

Tactic:
this,

Goal state after:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (i.hom ≫ (limitCone F).π.app (Opposite.op 0)))
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
X : Cᵒᵖ
c : Cone F
hc : IsLimit c
s : (j : J) → (F ⋙ coyoneda.obj X).obj j
hs : s ∈ (F ⋙ coyoneda.obj X).sections
⊢ ∃! x, ∀ (j : J), (hom (((coyoneda.obj X).mapCone c).π.app j)) x = s j

Tactic:
exact ⟨hc.lift (Limits.coneOfSectionCompCoyoneda F X ⟨s, hs⟩), hc.fac _,
      hc.uniq (Limits.coneOfSectionCompCoyoneda F X ⟨s, hs⟩)⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ PreservesLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} yoneda

Tactic:
apply preservesLimits_of_evaluation

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (k : Cᵒᵖ), PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (yoneda ⋙ (evaluation Cᵒᵖ (Type v)).obj k)
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ PreservesLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} coyoneda

Tactic:
apply preservesLimits_of_evaluation

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (k : C), PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (coyoneda ⋙ (evaluation C (Type v)).obj k)
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ PreservesLimitsOfSize.{t, w, v, max (max u v) w', u, max (max u (v + 1)) (w' + 1)} uliftYoneda.{w', v, u}

Tactic:
apply preservesLimits_of_evaluation

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (k : Cᵒᵖ),
    PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
      (uliftYoneda.{w', v, u} ⋙ (evaluation Cᵒᵖ (Type (max w' v))).obj k)
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ PreservesLimitsOfSize.{t, w, v, max (max u v) w', u, max (max u (v + 1)) (w' + 1)} uliftCoyoneda.{w', v, u}

Tactic:
apply preservesLimits_of_evaluation

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (k : C),
    PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
      (uliftCoyoneda.{w', v, u} ⋙ (evaluation C (Type (max w' v))).obj k)
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
P : C ⥤ Type w
t : shrinkCoyoneda.{w, v, u}.obj (op X) ⟶ P
⊢ shrinkCoyonedaEquiv (shrinkCoyonedaEquiv.symm ((ConcreteCategory.hom (P.map f)) (shrinkCoyonedaEquiv t))) =
    shrinkCoyonedaEquiv (shrinkCoyoneda.{w, v, u}.map f.op ≫ shrinkCoyonedaEquiv.symm (shrinkCoyonedaEquiv t))

Tactic:
rw [← shrinkCoyonedaEquiv_naturality]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
P : C ⥤ Type w
t : shrinkCoyoneda.{w, v, u}.obj (op X) ⟶ P
⊢ shrinkCoyonedaEquiv (shrinkCoyonedaEquiv.symm ((ConcreteCategory.hom (P.map f)) (shrinkCoyonedaEquiv t))) =
    (ConcreteCategory.hom (P.map f.op.unop)) (shrinkCoyonedaEquiv (shrinkCoyonedaEquiv.symm (shrinkCoyonedaEquiv t)))
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.Full
inst✝ : R.Faithful
⊢ IsIso (R.whiskerLeft h.unit)

Tactic:
by
  have := h.right_triangle
  rw [← IsIso.eq_comp_inv] at this
  rw [this]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
h : ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)
X Y : C
f : X ⟶ Y
r : R
this : r • f = (r • 𝟙 X) ≫ f
⊢ F.map (r • f) = r • F.map f

Tactic:
this,

Goal state after:
case mpr
R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
h : ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)
X Y : C
f : X ⟶ Y
r : R
this : r • f = (r • 𝟙 X) ≫ f
⊢ F.map ((r • 𝟙 X) ≫ f) = r • F.map f
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
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ f ⊗ₘ ∑ j ∈ s, g j = ∑ j ∈ s, f ⊗ₘ g j

Tactic:
by
  simp only [tensorHom_def, whiskerLeft_sum, Preadditive.comp_sum]

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

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

Tactic:
by
  simp [ih_η, ih_θ]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f₁ g₁ f₂ g₂ : C
η : f₁ ⟶ g₁
η' : f₁ ≅ g₁
ih_η : η'.hom = η
θ : f₂ ⟶ g₂
θ' : f₂ ≅ g₂
ih_θ : θ'.hom = θ
⊢ (η' ⊗ᵢ θ').hom = η ⊗ₘ θ

Tactic:
by
  simp [ih_η, 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
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 (G.obj X ⊗ G.obj Y) (G.obj Z) ≫
      F.map (adj.unit.app (G.obj X ⊗ G.obj Y)) ▷ F.obj (G.obj Z) ≫
        F.map (G.map (δ F (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
          F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y)) ▷ F.obj (G.obj Z) ≫
            (adj.counit.app (X ⊗ Y) ⊗ₘ adj.counit.app Z) ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))

Tactic:
this,

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 (G.obj X ⊗ G.obj Y) (G.obj Z) ≫
      F.map (adj.unit.app (G.obj X ⊗ G.obj Y)) ▷ F.obj (G.obj Z) ≫
        F.map (G.map (δ F (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
          (adj.counit.app (F.obj (G.obj X) ⊗ F.obj (G.obj Y)) ⊗ₘ adj.counit.app Z) ≫
            (adj.counit.app X ⊗ₘ adj.counit.app Y) ▷ Z ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (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 ⥤ 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 (G.obj X ⊗ G.obj Y) (G.obj Z) ≫
      F.map (adj.unit.app (G.obj X ⊗ G.obj Y)) ▷ F.obj (G.obj Z) ≫
        F.map (G.map (δ F (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
          (adj.counit.app (F.obj (G.obj X) ⊗ F.obj (G.obj Y)) ⊗ₘ adj.counit.app Z) ≫
            (adj.counit.app X ⊗ₘ adj.counit.app Y) ▷ Z ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))

Tactic:
this,

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 (G.obj X ⊗ G.obj Y) (G.obj Z) ≫
      F.map (adj.unit.app (G.obj X ⊗ G.obj Y)) ▷ F.obj (G.obj Z) ≫
        (adj.counit.app (F.obj (G.obj X ⊗ G.obj Y)) ⊗ₘ adj.counit.app Z) ≫
          δ F (G.obj X) (G.obj Y) ▷ Z ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y) ▷ Z ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : C ⥤ D
⊢ (Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c) ≅ c.map G

Tactic:
refine PushoutCocone.ext (Iso.refl _) ?_ ?_
      · dsimp only [inl]
        simp
      · dsimp only [inr]
        simp

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✝ W W'✝ : MorphismProperty C
W' : ?m.4
P Q : MorphismProperty C
inst✝¹ : P.HasTwoOutOfThreeProperty
inst✝ : Q.HasTwoOutOfThreeProperty
this✝¹ : P.HasOfPostcompProperty (P ⊓ Q)
this✝ : P.HasOfPrecompProperty (P ⊓ Q)
this : Q.HasOfPostcompProperty (P ⊓ Q)
⊢ (P ⊓ Q).HasTwoOutOfThreeProperty

Tactic:
have : Q.HasOfPrecompProperty (P ⊓ Q) := .of_le _ _ inf_le_right

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
W✝ W W'✝ : MorphismProperty C
W' : ?m.4
P Q : MorphismProperty C
inst✝¹ : P.HasTwoOutOfThreeProperty
inst✝ : Q.HasTwoOutOfThreeProperty
this✝² : P.HasOfPostcompProperty (P ⊓ Q)
this✝¹ : P.HasOfPrecompProperty (P ⊓ Q)
this✝ : Q.HasOfPostcompProperty (P ⊓ Q)
this : Q.HasOfPrecompProperty (P ⊓ Q)
⊢ (P ⊓ Q).HasTwoOutOfThreeProperty
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.injective C f
hg : MorphismProperty.injective C g
⊢ Injective (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f))

Tactic:
exact hg.comp hf

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.surjective C f
hg : MorphismProperty.surjective C g
⊢ Surjective (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f))

Tactic:
exact hg.comp hf

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.bijective C f
hg : MorphismProperty.bijective C g
⊢ Bijective (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f))

Tactic:
exact hg.comp hf

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 : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ e.counitIso.inv.app (𝟙_ D) ≫ e.functor.map (η e.inverse) = ε e.functor

Tactic:
rw [← cancel_epi (η e.functor), Monoidal.η_ε, ← functor_map_ε_inverse_comp_counitIso_hom_app,
    Category.assoc, Iso.hom_inv_id_app_assoc, Monoidal.map_ε_η]

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 : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ e.counitInv.app (𝟙_ D) ≫ e.functor.map (η e.inverse) = ε e.functor

Tactic:
rw [← cancel_epi (η e.functor), Monoidal.η_ε, ← functor_map_ε_inverse_comp_counitIso_hom_app,
    Category.assoc, Iso.hom_inv_id_app_assoc, Monoidal.map_ε_η]

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j : J
x : ↑((F ⋙ uliftFunctor).obj j)
⊢ (quotUliftToQuot F) ((Quot.ι (F ⋙ uliftFunctor) j) x) = (Quot.ι F j) x.down

Tactic:
by
  dsimp [quotUliftToQuot, Quot.ι]
  conv_lhs => erw [AddMonoidHom.comp_apply (QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor)))
    (DFinsupp.singleAddHom _ j), QuotientAddGroup.lift_mk']
  simp only [DFinsupp.singleAddHom_apply,
    DFinsupp.sumAddHom_single, AddMonoidHom.coe_comp, Function.comp_apply]
  rfl

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
d : D
⊢ L₂.map (α.app d) ≫ adj₂.counit.app d = ((conjugateEquiv adj₁ adj₂).symm α).app (R₁.obj d) ≫ adj₁.counit.app d

Tactic:
conv_lhs => rw [← (conjugateEquiv adj₁ adj₂).right_inv α]

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
d : D
⊢ L₂.map (((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app d) ≫ adj₂.counit.app d =
    ((conjugateEquiv adj₁ adj₂).symm α).app (R₁.obj d) ≫ adj₁.counit.app d
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
n : ℕ
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (x ^ (n + 1)).snd = (x ^ n * x).snd

Tactic:
simp_rw [snd_mul, snd_pow_eq_sum, Nat.pred_succ]

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
n : ℕ
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (List.map (fun i ↦ x.fst ^ (n - i) •> x.snd <• x.fst ^ i) (List.range (n + 1))).sum =
    (x ^ n).fst •> x.snd + (List.map (fun i ↦ x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i) (List.range n)).sum <• x.fst
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
c : C
⊢ adj₁.unit.app c ≫ α.app (L₁.obj c) = adj₂.unit.app c ≫ R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app c)

Tactic:
conv_lhs => rw [← (conjugateEquiv adj₁ adj₂).right_inv α]

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
c : C
⊢ adj₁.unit.app c ≫ ((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c) =
    adj₂.unit.app c ≫ R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app c)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹)) +
        (b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))

Tactic:
neg_add

Goal state after:
case h2
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
⊢ ((↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
          TensorProduct.map (TensorProduct.map (lsingle i) (lsingle i)) (lsingle i)) ∘ₗ
        rTensor (A i) comul) ∘ₗ
      comul =
    ((TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ
          ↑(TensorProduct.assoc R (A i) (A i) (A i))) ∘ₗ
        rTensor (A i) comul) ∘ₗ
      comul

Tactic:
TensorProduct.map_map_comp_assoc_eq

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

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
⊢ ((↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ
          TensorProduct.map (TensorProduct.map (lsingle i) (lsingle i)) (lsingle i)) ∘ₗ
        rTensor A comul) ∘ₗ
      comul =
    ((TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ ↑(TensorProduct.assoc R A A A)) ∘ₗ
        rTensor A comul) ∘ₗ
      comul

Tactic:
TensorProduct.map_map_comp_assoc_eq

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

Goal state before:

Tactic:
(μ ∘ₗ (ε ⊗ₘ ε)) ∘ₗ δ
    _ = (μ ∘ₗ ε ▷ R) ∘ₗ (C ◁ ε ∘ₗ δ) := by simp [coassoc_simps]
    _ = ε := by ext; simp

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

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
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ (whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x = adj2.unit.app x

Tactic:
← homEquiv_leftAdjointUniq_hom_app adj1 adj2

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
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ (whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x =
    (adj1.homEquiv x (F'.obj x)) ((adj1.leftAdjointUniq adj2).hom.app x)
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f : M →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃
⊢ (f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α) ∘ₗ f = (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f

Tactic:
TensorProduct.map_map_comp_assoc_eq

Goal state after:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f : M →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃
⊢ (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f = (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₃ : Type u_16
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N₃
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
⊢ α ∘ₗ f₁₂ ⊗ₘ f₃ = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id

Tactic:
rw [← LinearMap.comp_assoc, map_map_comp_assoc_eq]
  simp only [coassoc_simps]

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
A : Mon Cᵒᵖ
⊢ μ.unop ≫ unop A.X ◁ η.unop = (ρ_ (unop A.X)).inv

Tactic:
rw [← unop_whiskerLeft, ← unop_comp, MonObj.mul_one]

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
A : Mon Cᵒᵖ
⊢ (ρ_ A.X).hom.unop = (ρ_ (unop A.X)).inv
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
⊢ mk = Submonoid.LocalizationMap.mk' (monoidOf x)

Tactic:
simp [Localization.mk_eq_monoidOf_mk']

Goal state after: