mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝ : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : ι → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h✝¹ : ∀ (i : ι), IsConnected (gZ i)
h✝ : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
⊢ is2.inv ≫ (functorToAction F).map (Sigma.desc gf) = u'.inv ≫ t.hom ≫ i

Tactic:
refine Sigma.hom_ext _ _ (fun j ↦ ?_)

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝ : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : ι → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h✝¹ : ∀ (i : ι), IsConnected (gZ i)
h✝ : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
j : ι
⊢ Sigma.ι (fun i ↦ (functorToAction F).obj (gZ i)) j ≫ is2.inv ≫ (functorToAction F).map (Sigma.desc gf) =
    Sigma.ι (fun i ↦ (functorToAction F).obj (gZ i)) j ≫ u'.inv ≫ t.hom ≫ i
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).obj ≃ { p // (ConcreteCategory.hom (F.map i)) p.1 = (ConcreteCategory.hom (F.map j)) p.2 } :=
  fiberPullbackEquiv F i j
y : (F.obj Y).obj := e.symm ⟨(a, b), h⟩
hn : ∀ (a : IsInitial Y), False
this✝ : IsIso u
this : IsIso v
hu : (ConcreteCategory.hom (G.map u)) y = a
hv : (ConcreteCategory.hom (G.map v)) y = b
⊢ (ConcreteCategory.hom (F.map ((asIso u).symm ≪≫ asIso v).hom)) a = b

Tactic:
← hu,

Goal state after:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).obj ≃ { p // (ConcreteCategory.hom (F.map i)) p.1 = (ConcreteCategory.hom (F.map j)) p.2 } :=
  fiberPullbackEquiv F i j
y : (F.obj Y).obj := e.symm ⟨(a, b), h⟩
hn : ∀ (a : IsInitial Y), False
this✝ : IsIso u
this : IsIso v
hu : (ConcreteCategory.hom (G.map u)) y = a
hv : (ConcreteCategory.hom (G.map v)) y = b
⊢ (ConcreteCategory.hom (F.map ((asIso u).symm ≪≫ asIso v).hom)) ((ConcreteCategory.hom (G.map u)) y) = b
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case h.left
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x y : (F.obj A).obj
fi1 : A ≅ A
hfi1 : (ConcreteCategory.hom (F.map fi1.hom)) x = a
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨fi2, hfi2⟩ := subobj_selfProd_trans h1 y

Goal state after:
case h.left
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x y : (F.obj A).obj
fi1 : A ≅ A
hfi1 : (ConcreteCategory.hom (F.map fi1.hom)) x = a
fi2 : A ≅ A
hfi2 : (ConcreteCategory.hom (F.map fi2.hom)) y = a
⊢ ∃ g, g • x = y
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
f g : AutGalois F
h : ∀ (A : PointedGaloisObject F), (π F A) f = (π F A) g
⊢ f = g

Tactic:
ext A

Goal state after:
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
f g : AutGalois F
h : ∀ (A : PointedGaloisObject F), (π F A) f = (π F A) g
A : PointedGaloisObject F
⊢ ↑f A = ↑g A
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| (MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
    (MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).inv ≫
      MonoidalCategoryStruct.whiskerRight (β_ (X i₁) (Y i₂)).hom (Z i₃) ≫
        (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)).hom ≫
          MonoidalCategoryStruct.whiskerLeft (Y i₂) (β_ (X i₁) (Z i₃)).hom ≫
            (MonoidalCategoryStruct.associator (Y i₂) (Z i₃) (X i₁)).inv ≫
              MonoidalCategoryStruct.tensorHom (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯) (𝟙 (X i₁)) ≫
                ιTensorObj (tensorObj Y Z) X (i₂ + i₃) i₁ k ⋯ ≫ (associator Y Z X).hom k

Tactic:
Iso.hom_inv_id_assoc,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.whiskerRight (β_ (X i₁) (Y i₂)).hom (Z i₃) ≫
    (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)).hom ≫
      MonoidalCategoryStruct.whiskerLeft (Y i₂) (β_ (X i₁) (Z i₃)).hom ≫
        (MonoidalCategoryStruct.associator (Y i₂) (Z i₃) (X i₁)).inv ≫
          MonoidalCategoryStruct.tensorHom (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯) (𝟙 (X i₁)) ≫
            ιTensorObj (tensorObj Y Z) X (i₂ + i₃) i₁ k ⋯ ≫ (associator Y Z X).hom k
Module: Mathlib.CategoryTheory.IsoCat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
f : IsoCat D E
⊢ 𝟭 C = e.functor ⋙ e.inverse

Tactic:
exact e.unit_eq

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

Goal state before:
pp: case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
a✝ : D
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) (𝟙 (right a✝)) =
    𝟙
      (match right a✝ with
      | left x => F.obj x
      | right x => G.obj x)

Tactic:
dsimp only [id_right, homInduction_right]
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback b.inr 0 b.fst 0

Tactic:
apply flip

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback 0 b.inr 0 b.fst
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout b.inl 0 b.snd 0

Tactic:
apply flip

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout 0 b.inl 0 b.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case inst.isTrue
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : val✝ < n + 1
h✝ : ↑⟨val✝, property✝⟩ < n
⊢ Epi (eqToHom ⋯)

pp: case inst.isFalse
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : val✝ < n + 1
h✝ : ¬↑⟨val✝, property✝⟩ < n
⊢ Epi (eqToHom ⋯ ≫ f ↑⟨val✝, property✝⟩ ≫ eqToHom ⋯)

Tactic:
all_goals infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case inst.isTrue
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : ¬val✝ < n + 1
h✝ : ↑⟨val✝, property✝⟩ < n
⊢ IsIso (eqToHom ⋯)

pp: case inst.isFalse
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : ¬val✝ < n + 1
h✝ : ¬↑⟨val✝, property✝⟩ < n
⊢ IsIso (eqToHom ⋯)

Tactic:
all_goals infer_instance

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

Goal state before:
pp: case refine_1
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 : (fun g ↦ f ≫ g) g₁ = (fun g ↦ f ≫ g) g₂
j : J
⊢ { pt := Y, ι := hf.incl }.ι.app j ≫ g₁ = { pt := Y, ι := hf.incl }.ι.app j ≫ g₂

Tactic:
dsimp at h ⊢

Goal state after:
case refine_1
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
⊢ hf.incl.app j ≫ g₁ = hf.incl.app j ≫ g₂
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: 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 : X ⟶ Z
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ hf.F.op ⋙ yoneda.obj Z).sections
c : Cocone (⋯.functor ⋙ hf.F) := { pt := Z, ι := { app := fun k ↦ ↑s (op k), naturality := ⋯ } }
⊢ ∃ y, ∀ (i : J) (hi : i < j), (ConcreteCategory.hom ((hf.F.op ⋙ yoneda.obj Z).map (homOfLE ⋯).op)) y = ↑s (op ⟨i, hi⟩)

Tactic:
exact ⟨(hf.F.isColimitOfIsWellOrderContinuous j hj).desc c, fun k hk ↦
            by simpa using! (hf.F.isColimitOfIsWellOrderContinuous j hj).fac c ⟨k, hk⟩⟩

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

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

Tactic:
intro J

Goal state after:
case h_option
J : Type w
⊢ ∀ [Fintype J],
    (∀ {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_1 : (j : Option J) → Category.{v₂, u₂} (D j)] (L : (j : Option J) → C j ⥤ D j)
        (W : (j : Option J) → MorphismProperty (C j)) [∀ (j : Option J), (W j).ContainsIdentities]
        [∀ (j : Option J), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ (tensorLeft R.X).map (P.actRight ▷ Q.X) ≫ (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X =
    ((α_ R.X (P.X ⊗ S.X) Q.X).inv ≫ (α_ R.X P.X S.X).inv ▷ Q.X ≫ P.actLeft ▷ S.X ▷ Q.X) ≫ P.actRight ▷ Q.X

Tactic:
dsimp
          simp only [Category.assoc]
          slice_lhs 1 2 => rw [associator_inv_naturality_middle]
          slice_rhs 3 4 => rw [← comp_whiskerRight, middle_assoc, comp_whiskerRight]
          simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁵ : Category.{v₂, u₂} V
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory V
inst✝² : MonoidalClosed V
F G H : C ⥤ V
inst✝¹ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
ℌ' : DayConvolutionInternalHom F G' H'
inst✝ : DayConvolution F H'
η : G ⟶ G'
⊢ DayConvolution.map (𝟙 F) (ℌ.map η ℌ') ≫ ℌ'.ev_app = ℌ.ev_app ≫ η

Tactic:
by
  apply DayConvolution.corepresentableBy F H |>.homEquiv.injective
  dsimp
  ext ⟨x, y⟩
  simp [MonoidalClosed.uncurry_eq, ← whiskerLeft_comp_assoc]

Goal state after:
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)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫
                (α_ (A ⊗ A) A A).hom ≫ (A ⊗ A) ◁ (β_ A A).hom ≫ (((A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ μ ▷ (A ⊗ A)) ≫ A ◁ μ) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
slice_lhs 11 12 =>
    rw [MonObj.mul_assoc_flip]

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)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫
                (α_ (A ⊗ A) A A).hom ≫
                  (A ⊗ A) ◁ (β_ A A).hom ≫ (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ μ ▷ (A ⊗ A) ≫ (α_ A A A).inv ≫ μ ▷ A ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝¹ : IsFiltered J
inst✝ : ∀ (j : J), IsFiltered (I j)
⊢ Nonempty (Total P)

Tactic:
obtain ⟨j⟩ : Nonempty J := IsFiltered.nonempty

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝¹ : IsFiltered J
inst✝ : ∀ (j : J), IsFiltered (I j)
j : J
⊢ Nonempty (Total P)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁵ : Category.{v₂, u₂} V
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory V
D : Type u₃
inst✝² : Category.{v₃, u₃} D
inst✝¹ : MonoidalCategoryStruct D
inst✝ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d₁ d₂ d₁' d₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
x y : C
⊢ ((DayConvolution.corepresentableBy ((ι C V D).obj d₁) ((ι C V D).obj d₁')).homEquiv ((ι C V D).map (f ⊗ₘ f'))).app
      (x, y) =
    ((DayConvolution.corepresentableBy ((ι C V D).obj d₁) ((ι C V D).obj d₁')).homEquiv
          (DayConvolution.map ((ι C V D).map f) ((ι C V D).map f'))).app
      (x, y)

Tactic:
simp only [externalProductBifunctor_obj_obj, Functor.comp_obj, tensor_obj,
    DayConvolution.corepresentableBy_homEquiv_apply_app,
    DayConvolution.unit_app_map_app]

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁵ : Category.{v₂, u₂} V
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory V
D : Type u₃
inst✝² : Category.{v₃, u₃} D
inst✝¹ : MonoidalCategoryStruct D
inst✝ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d₁ d₂ d₁' d₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
x y : C
⊢ (DayConvolution.unit ((ι C V D).obj d₁) ((ι C V D).obj d₁')).app (x, y) ≫ ((ι C V D).map (f ⊗ₘ f')).app (x ⊗ y) =
    (((ι C V D).map f).app x ⊗ₘ ((ι C V D).map f').app y) ≫
      (DayConvolution.unit ((ι C V D).obj d₂) ((ι C V D).obj d₂')).app (x, y)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
W X Y Z : Mon C
M M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
⊢ M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
      f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
        colimit.ι
          (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))
            ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫
              M'.X ◁ TensorBimod.actLeft N P))
          WalkingParallelPair.one =
    (α_ M.X N.X P.X).inv ≫
      (f.hom ▷ N.X ≫
            colimit.ι (parallelPair (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft))
              WalkingParallelPair.one) ▷
          P.X ≫
        (PreservesCoequalizer.iso (tensorRight P.X) (M'.actRight ▷ N.X)
              ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)).inv ≫
          coequalizer.desc
            ((α_ M'.X N.X P.X).hom ≫
              M'.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
                coequalizer.π (M'.actRight ▷ TensorBimod.X N P)
                  ((α_ M'.X X.X (TensorBimod.X N P)).hom ≫ M'.X ◁ TensorBimod.actLeft N P))
            ⋯

Tactic:
slice_rhs 2 2 => rw [comp_whiskerRight]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
W X Y Z : Mon C
M M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
⊢ M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
      f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
        colimit.ι
          (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))
            ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫
              M'.X ◁ TensorBimod.actLeft N P))
          WalkingParallelPair.one =
    (α_ M.X N.X P.X).inv ≫
      ((f.hom ▷ N.X ▷ P.X ≫
            colimit.ι (parallelPair (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft))
                WalkingParallelPair.one ▷
              P.X) ≫
          (PreservesCoequalizer.iso (tensorRight P.X) (M'.actRight ▷ N.X)
              ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)).inv) ≫
        coequalizer.desc
          ((α_ M'.X N.X P.X).hom ≫
            M'.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
              coequalizer.π (M'.actRight ▷ TensorBimod.X N P)
                ((α_ M'.X X.X (TensorBimod.X N P)).hom ≫ M'.X ◁ TensorBimod.actLeft N P))
          ⋯
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✝¹ x✝ : V
f g : x✝¹ ⟶ x✝
eq : (quotient V).map (homMk 0 f ⋯) = (quotient V).map (homMk 0 g ⋯)
⊢ f = g

Tactic:
quotient_map_eq_iff

Goal state after:
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✝¹ x✝ : V
f g : x✝¹ ⟶ x✝
eq : Nonempty (RightHomotopy (homMk 0 f ⋯) (homMk 0 g ⋯))
⊢ f = g
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case neg
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 : α
w : j ∈ g ⁻¹' {f k}
h : ¬f k = g j
⊢ False

Tactic:
exact h w.symm

Goal state after: