mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.lift P.decompId_p P.complement.decompId_p ≫ biprod.desc P.decompId_i P.complement.decompId_i =
    𝟙 ((toKaroubi C).obj P.X)

Tactic:
by
    ext
    simp only [toKaroubi_obj_X, biprod.lift_desc, add_def, comp_f, decompId_p_f, decompId_i_f,
      idem, complement_X, complement_p, comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero,
      add_sub_cancel, id_f, toKaroubi_obj_p]

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    NatTrans.toCatHom₂ (mapWhiskerRight (ρ_ f).hom.toNatTrans (𝟭 D)) =
      (Cat.Hom.isoMk (mapCompLeft D f.toFunctor (𝟙 b).toFunctor)).hom ≫
        (mapPair f.toFunctor (𝟭 D)).toCatHom ◁ (Cat.Hom.isoMk mapPairId).hom ≫
          (ρ_ (mapPair f.toFunctor (𝟭 D)).toCatHom).hom

Tactic:
by intros; exact congr($(mapWhiskerRight_rightUnitor_hom D _).toCatHom₂)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
f : s.pt.I → (U.powerFan α).pt.I
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj (f i)
hm : ∀ (j : α), { f := f, φ := φ } ≫ (U.powerFan α).proj j = s.proj j
i : s.pt.I
⊢ f i = fun a ↦ (s.proj a).f i

Tactic:
ext a

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
f : s.pt.I → (U.powerFan α).pt.I
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj (f i)
hm : ∀ (j : α), { f := f, φ := φ } ≫ (U.powerFan α).proj j = s.proj j
i : s.pt.I
a : α
⊢ f i a = (s.proj a).f i
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj ((fun i a ↦ (s.proj a).f i) i)
hm : ∀ (j : α), { f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj j = s.proj j
i : s.pt.I
⊢ φ i ≫ 𝟙 (∏ᶜ U.obj ∘ fun a ↦ (s.proj a).f i) = Pi.lift fun a ↦ (s.proj a).φ i

Tactic:
ext a

Goal state after:
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj ((fun i a ↦ (s.proj a).f i) i)
hm : ∀ (j : α), { f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj j = s.proj j
i : s.pt.I
a : α
⊢ (φ i ≫ 𝟙 (∏ᶜ U.obj ∘ fun a ↦ (s.proj a).f i)) ≫ Pi.π (U.obj ∘ fun a ↦ (s.proj a).f i) a =
    (Pi.lift fun a ↦ (s.proj a).φ i) ≫ Pi.π (U.obj ∘ fun a ↦ (s.proj a).f i) a
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₂ = x✝ ≫ h.p₁₂
h₂ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
⊢ x✝¹ ≫ h.p₁ = x✝ ≫ h.p₁

Tactic:
simpa using h₁ =≫ h₁₂.p₁

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₂ = x✝ ≫ h.p₁₂
h₂ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
⊢ x✝¹ ≫ h.p₃ = x✝ ≫ h.p₃

Tactic:
simpa using h₂ =≫ h₁₃.p₂

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
x : (F.obj (op j)).obj j
x' : (F.obj (op j')).obj j'
⊢ coendRel F ⟨j, x⟩ ⟨j', x'⟩ ↔ ∃ f y, (hom ((F.map f.op).app j)) y = x ∧ (hom ((F.obj (op j')).map f)) y = x'

Tactic:
by
  constructor
  · rintro ⟨f, x⟩
    exact ⟨f, x, by simp⟩
  · rintro ⟨f, y, rfl, rfl⟩
    exact coendRel.mk f y

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: case refine_1.isMin
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
hj : IsMin j
⊢ hf.incl.app j ≫ g₁ = hf.incl.app j ≫ g₂

Tactic:
obtain rfl := hj.eq_bot
        simpa [← cancel_epi hf.isoBot.inv]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_option
J : Type w
inst✝⁴ : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
⊢ (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
let L₁ := (L none).prod (Functor.pi (fun j => L (some j)))

Goal state after:
case h_option
J : Type w
inst✝⁴ : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) := (L none).prod (Functor.pi fun j ↦ L (some j))
⊢ (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
W X Y Z : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (f : W ⟶ X) (g : Y ⟶ Z),
    Quotient.map₂ Hom.tensor ⋯ f g =
      Quot.map (fun f ↦ f.whiskerRight Y) ⋯ f ≫ Quot.map (fun f ↦ Hom.whiskerLeft X f) ⋯ g

Tactic:
rintro ⟨f⟩ ⟨g⟩
    exact Quotient.sound (tensorHom_def _ _)

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

Goal state before:
pp: case h.tensor
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X✝ Y✝ : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
W X Y Z : F C
f : W ⟶ᵐ Y
g : X ⟶ᵐ Z
hf : motive ⟦f⟧
hg : motive ⟦g⟧
this : homMk f ⊗ₘ homMk g = homMk f ▷ X ≫ Y ◁ homMk g
⊢ motive ⟦f.tensor g⟧

Tactic:
change motive (homMk f ⊗ₘ homMk g)

Goal state after:
case h.tensor
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X✝ Y✝ : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
W X Y Z : F C
f : W ⟶ᵐ Y
g : X ⟶ᵐ Z
hf : motive ⟦f⟧
hg : motive ⟦g⟧
this : homMk f ⊗ₘ homMk g = homMk f ▷ X ≫ Y ◁ homMk g
⊢ motive (homMk f ⊗ₘ homMk g)
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ adj.toMonad.Algebra ⥤ D

Tactic:
refine
    Adjunction.leftAdjointOfEquiv (G := comparison adj)
      (F_obj := fun A => comparisonLeftAdjointObj adj A) (fun A B => ?_) ?_

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
B : D
⊢ (comparisonLeftAdjointObj adj A ⟶ B) ≃ (A ⟶ (comparison adj).obj B)

case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ ∀ (X : adj.toMonad.Algebra) (Y Y' : D) (g : Y ⟶ Y') (h : comparisonLeftAdjointObj adj X ⟶ Y),
    ?refine_1 (h ≫ g) = ?refine_1 h ≫ (comparison adj).map g
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
⊢ (∀ (X : C), (monoidHom φ X).range.Normal) → ∃ ψ, ψ ≫ φ = G ◁ φ ≫ conj G

Tactic:
intro hnormal
    have (X : C) (g : X ⟶ G) (h : X ⟶ H) : ∃ (h' : X ⟶ H), h' ≫ φ = g * h ≫ φ * g⁻¹ :=
      (hnormal X).conj_mem (h ≫ φ) (by simp) g
    choose h' hh' using this
    refine ⟨Yoneda.fullyFaithful.preimage ?_, ?_⟩
    · refine ⟨fun X ↦ ↾fun x ↦ h' _ (x ≫ fst _ _) (x ≫ snd _ _), fun X Y f ↦ ?_⟩
      ext
      simp [← cancel_mono φ, hh', comp_mul, comp_inv]
    · refine yoneda.map_injective ?_
      ext
      simp [hh', conj, comp_mul, comp_inv]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
⊢ homEquiv (f ≫ f₃) =
    homEquiv f ≫
      (ρ_ (functorEnrichedHom C F₁ F₃)).inv ≫
        functorEnrichedHom C F₁ F₃ ◁ (functorHomEquiv C) f₃ ≫ functorEnrichedComp C F₁ F₃ F₃'

Tactic:
dsimp [homEquiv]
  ext j
  dsimp
  ext k
  rw [Category.assoc, Category.assoc, Category.assoc, end_.lift_π, enrichedComp_π,
    tensorHom_def, Category.assoc, whisker_exchange_assoc, whiskerRight_id_assoc,
    Iso.inv_hom_id_assoc, end_.lift_π_assoc, Category.assoc,
    ← MonoidalCategory.whiskerLeft_comp_assoc, Category.assoc, end_.lift_π,
    enrichedOrdinaryCategorySelf_eHomWhiskerRight,
    enrichedOrdinaryCategorySelf_eHomWhiskerLeft]
  dsimp
  rw [pre_id, NatTrans.id_app, Functor.map_id, Category.comp_id,
    Category.comp_id, homEquiv_apply_π, curry_natural_right]
  congr 2
  symm
  apply enrichedOrdinaryCategorySelf_eHomWhiskerLeft

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

Goal state before:
pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| X.X ◁ coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ≫
    X.X ◁
      colimMap
        (parallelPairHom (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) (M₂.actRight ▷ N.X)
          ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯)

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| TensorBimod.actLeft M₂ N

Tactic:
rw [← whiskerLeft_comp, ι_colimMap, parallelPairHom_app_one, whiskerLeft_comp]

Goal state after:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| X.X ◁ f.hom ▷ N.X ≫
    X.X ◁
      colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)) WalkingParallelPair.one

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| TensorBimod.actLeft M₂ N
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case mk.whiskerRight
C : Type u
X Y X₁✝ X₂✝ : F C
f✝ : X₁✝ ⟶ᵐ X₂✝
Y✝ : F C
ih : (fun n ↦ X₁✝.normalizeObj n) = X₂✝.normalizeObj
x✝ : NormalMonoidalObject C
⊢ (X₁✝.tensor Y✝).normalizeObj x✝ = (X₂✝.tensor Y✝).normalizeObj x✝

Tactic:
apply congr_arg₂ _ rfl (congr_fun ih _)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X Y : F C
f g : X ⟶ Y
hfg : (fullNormalize C).map f = (fullNormalize C).map g
hf :
  (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map f ≫ (fullNormalizeIso C).inv.app Y =
    (𝟭 (F C)).map f
⊢ f = g

Tactic:
have hg := NatIso.naturality_2 (fullNormalizeIso.{u} C) g

Goal state after:
C : Type u
X Y : F C
f g : X ⟶ Y
hfg : (fullNormalize C).map f = (fullNormalize C).map g
hf :
  (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map f ≫ (fullNormalizeIso C).inv.app Y =
    (𝟭 (F C)).map f
hg :
  (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map g ≫ (fullNormalizeIso C).inv.app Y =
    (𝟭 (F C)).map g
⊢ f = g
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ 𝒮 ≫ (ρ_ A).inv ≫ A ◁ η ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η

Tactic:
rightUnitor_inv_naturality_assoc

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ (ρ_ A).inv ≫ 𝒮 ▷ 𝟙_ C ≫ A ◁ η ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      A ◁ Δ ≫
        A ◁ A ◁ Δ ≫
          A ◁ A ◁ 𝒮 ▷ A ≫ (((A ◁ (α_ A A A).inv ≫ A ◁ μ ▷ A ≫ A ◁ (β_ A A).hom) ≫ A ◁ 𝒮 ▷ A) ≫ (α_ A A A).inv) ≫ μ ▷ A =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
slice_lhs 2 3 =>
    simp only [← whiskerLeft_comp]
    rw [ComonObj.comul_assoc]
    simp only [whiskerLeft_comp]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      (((((((A ◁ Δ ≫ A ◁ Δ ▷ A ≫ A ◁ (α_ A A A).hom) ≫ A ◁ A ◁ 𝒮 ▷ A) ≫ A ◁ (α_ A A A).inv) ≫ A ◁ μ ▷ A) ≫
              A ◁ (β_ A A).hom) ≫
            A ◁ 𝒮 ▷ A) ≫
          (α_ A A A).inv) ≫
        μ ▷ A =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y z : ↑A
⊢ x * y * z = x * (y * z)

Tactic:
by
      convert! LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (mul_assoc A)) (x ⊗ₜ y ⊗ₜ z)

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y : R
⊢ (Hom.hom η).toFun (x * y) = (Hom.hom η).toFun x * (Hom.hom η).toFun y

Tactic:
have h := LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (one_mul A).symm) (x ⊗ₜ η[A] y)
      rwa [MonoidalCategory.leftUnitor_hom_apply, ← η[A].hom.map_smul] at h

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((α_ R.X R.X P.X).inv ≫ μ ▷ P.X) ≫ P.actLeft =
    R.X ◁ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft

Tactic:
slice_lhs 2 3 => rw [left_assoc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ R.X R.X P.X).inv ≫ (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft =
    R.X ◁ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsFinitelyAccessibleCategory C
X : C
⊢ IsFiltered (CostructuredArrow (ObjectProperty.isFinitelyPresentable C).ι X)

Tactic:
rw [← CategoryTheory.isCardinalFiltered_aleph0_iff.{w},
    ObjectProperty.isFinitelyPresentable_eq_isCardinalPresentable]
  infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
⊢ (localEpi fun x ↦ x ∈ Set.range G.obj) = (MorphismProperty.epimorphisms D).inverseImage F

Tactic:
by
  ext X Y f
  rw [localEpi_mem_range_iff_epi adj]
  simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : T.Additive
F G : T.Algebra
⊢ T.map 0 ≫ G.a = F.a ≫ 0

Tactic:
simp only [Functor.map_zero, zero_comp, comp_zero]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
⊢ F.map 0 ≫ A₂.str = A₁.str ≫ 0

Tactic:
simp only [Functor.map_zero, zero_comp, comp_zero]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
⊢ A₁.str ≫ F.map 0 = 0 ≫ A₂.str

Tactic:
simp only [Functor.map_zero, zero_comp, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u v : Arrow V
f g : u ⟶ v
inst✝ : HasZeroObject V
X✝ Y✝ : V
a : (functor V).obj X✝ ⟶ (functor V).obj Y✝
⊢ ∃ a_1, (functor V).map a_1 = a

Tactic:
by
    obtain ⟨u, rfl⟩ := (quotient V).map_surjective a
    exact ⟨u.right, (quotient V).congr_map (by cat_disch)⟩

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : α
k : β
h : f j = g k
⊢ k ∈ g ⁻¹' {f j}

Tactic:
by simp [h]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : α
k : β
h : f j = g k
⊢ s (f j) = s (g k)

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
M N : DMatrix m n α
h : M = N
⊢ ∀ (i : m) (j : n), M i j = N i j

Tactic:
by simp [h]

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

Goal state before:
pp: C : Type u
D : Type u'
inst✝² : Category.{v, u} C
inst✝¹ : Category.{v', u'} D
e : C ≌ D
inst✝ : IsLocallyPresentable.{w, v, u} C
⊢ IsLocallyPresentable.{w, v', u'} D

Tactic:
obtain ⟨κ, _, _⟩ := IsLocallyPresentable.exists_cardinal.{w} C

Goal state after:
C : Type u
D : Type u'
inst✝² : Category.{v, u} C
inst✝¹ : Category.{v', u'} D
e : C ≌ D
inst✝ : IsLocallyPresentable.{w, v, u} C
κ : Cardinal.{w}
w✝ : Fact κ.IsRegular
h✝ : IsCardinalLocallyPresentable C κ
⊢ IsLocallyPresentable.{w, v', u'} D
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case pos
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nonempty (X ≅ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 1

pp: case neg
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ¬Nonempty (X ≅ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 0

Tactic:
· exact (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y).2 h

Goal state after:
case neg
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ¬Nonempty (X ≅ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 0
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : Fin n
a✝¹ : b ∈ Finset.univ
hb : b ≠ i
x : (f b).ι
a✝ : x ∈ Finset.univ
⊢ ((if h : i = b then if h' : h ▸ j = x then eqToHom ⋯ else 0 else 0) ≫
      if h : i' = b then if h' : h ▸ j' = x then eqToHom ⋯ else 0 else 0) =
    0

Tactic:
dif_neg hb.symm,

Goal state after:
case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : Fin n
a✝¹ : b ∈ Finset.univ
hb : b ≠ i
x : (f b).ι
a✝ : x ∈ Finset.univ
⊢ (0 ≫ if h : i' = b then if h' : h ▸ j' = x then eqToHom ⋯ else 0 else 0) = 0