mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sigma.Basic

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
q : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ q ≅ F i
⊢ ∀ {X Y : (i : I) × C i} (f : X ⟶ Y),
    q.map f ≫
        (match Y with
          | ⟨i, X⟩ => (h i).app X).hom =
      (match X with
          | ⟨i, X⟩ => (h i).app X).hom ≫
        (desc F).map f

Tactic:
rintro ⟨i, X⟩ ⟨_, _⟩ ⟨f⟩
    apply (h i).hom.naturality f

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ (res f s).core t ↔ x ∈ s → f x ∈ t

Tactic:
simp [mem_core, mem_res]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Fiber

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₁} 𝒮
inst✝ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
S : 𝒮
X✝ Y✝ Z✝ : p.Fiber S
φ : { φ // p.IsHomLift (𝟙 S) φ }
ψ : { φ // p.IsHomLift (𝟙 S) φ }
⊢ p.IsHomLift (𝟙 S) (↑φ ≫ ↑ψ)

Tactic:
have := φ.2; have := ψ.2; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
a'✝ : 𝒳
g : p.obj a'✝ ⟶ R
φ' : a'✝ ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a'✝ ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
⊢ (τ ≫ ψ) ≫ φ = φ'

Tactic:
by simp only [assoc, IsCartesian.fac, τ]

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
c : C
f : ↑(F.obj c)
d : C
g : ↑(F.obj d)
u : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
⊢ { base := u, fiber := x } ≫
      { base := coeqHom u v,
        fiber := coeqHom (eqToHom ⋯ ≫ (F.map (coeqHom u v)).toFunctor.map x) ((F.map (coeqHom u v)).toFunctor.map y) } =
    { base := v, fiber := y } ≫
      { base := coeqHom u v,
        fiber := coeqHom (eqToHom ⋯ ≫ (F.map (coeqHom u v)).toFunctor.map x) ((F.map (coeqHom u v)).toFunctor.map y) }

Tactic:
apply Grothendieck.ext _ _ (coeq_condition u v)
      refine Eq.trans ?_ (eqToHom _ ≫= coeq_condition _ _)
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_5, u_2} H
F F' : C ⥤ H
e : F ≅ F'
W : MorphismProperty C
⊢ F.HasLeftDerivedFunctor W ↔ F'.HasLeftDerivedFunctor W

Tactic:
by
  rw [hasLeftDerivedFunctor_iff F W.Q W, hasLeftDerivedFunctor_iff F' W.Q W,
    hasRightExtension_iff_of_iso₂ W.Q e]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: G : Type u
inst✝² : Group G
X : Action FintypeCat G
inst✝¹ : IsConnected X
x : X.V.obj
inst✝ : Fintype (G ⧸ MulAction.stabilizer G x)
this : MulAction.IsPretransitive G X.V.obj
e : X.V.obj ≃ G ⧸ MulAction.stabilizer G x :=
  (Equiv.Set.univ X.V.obj).symm.trans ((Equiv.setCongr ⋯).trans (MulAction.orbitEquivQuotientStabilizer G x))
σ : G
a : G ⧸ MulAction.stabilizer G x
⊢ (ConcreteCategory.hom
        ((Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).ρ σ ≫
          (FintypeCat.equivEquivIso e.symm).hom))
      a =
    (ConcreteCategory.hom ((FintypeCat.equivEquivIso e.symm).hom ≫ X.ρ σ)) a

Tactic:
obtain ⟨τ, rfl⟩ := Quotient.exists_rep a

Goal state after:
G : Type u
inst✝² : Group G
X : Action FintypeCat G
inst✝¹ : IsConnected X
x : X.V.obj
inst✝ : Fintype (G ⧸ MulAction.stabilizer G x)
this : MulAction.IsPretransitive G X.V.obj
e : X.V.obj ≃ G ⧸ MulAction.stabilizer G x :=
  (Equiv.Set.univ X.V.obj).symm.trans ((Equiv.setCongr ⋯).trans (MulAction.orbitEquivQuotientStabilizer G x))
σ τ : G
⊢ (ConcreteCategory.hom
        ((Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).ρ σ ≫
          (FintypeCat.equivEquivIso e.symm).hom))
      ⟦τ⟧ =
    (ConcreteCategory.hom ((FintypeCat.equivEquivIso e.symm).hom ≫ X.ρ σ)) ⟦τ⟧
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
t : (AutGalois F)ᵐᵒᵖ
⊢ (⇑(endMulEquivAutGalois F) ∘ ⇑(Aut.toEnd F)) (asIso ((endMulEquivAutGalois F).symm t)) = t

Tactic:
exact (MulEquiv.eq_symm_apply (endMulEquivAutGalois F)).mp rfl

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: case e'_2
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Symmetrify V
f : X ⟶ Y
this :
  Φ.map (inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
⊢ Groupoid.inv ((Quotient.functor redStep).toPrefunctor.map f.toPath) =
    inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)

Tactic:
simp only [Groupoid.inv_eq_inv]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: case e'_3
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Symmetrify V
f : X ⟶ Y
this :
  Φ.map (inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
⊢ Groupoid.inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))

Tactic:
simp only [Groupoid.inv_eq_inv]

Goal state after:
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 Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| (MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).inv ≫
    (β_ (MonoidalCategoryStruct.tensorObj (X i₁) (Y i₂)) (Z i₃)).hom ≫
      MonoidalCategoryStruct.tensorHom (𝟙 (Z i₃)) (ιTensorObj X Y i₁ i₂ (i₁ + i₂) ⋯) ≫
        ιTensorObj Z (tensorObj X Y) i₃ (i₁ + i₂) k ⋯ ≫ (associator Z X Y).inv k

Tactic:
BraidedCategory.braiding_tensor_left_hom,

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 Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| (MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).inv ≫
    ((MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
        MonoidalCategoryStruct.whiskerLeft (X i₁) (β_ (Y i₂) (Z i₃)).hom ≫
          (MonoidalCategoryStruct.associator (X i₁) (Z i₃) (Y i₂)).inv ≫
            MonoidalCategoryStruct.whiskerRight (β_ (X i₁) (Z i₃)).hom (Y i₂) ≫
              (MonoidalCategoryStruct.associator (Z i₃) (X i₁) (Y i₂)).hom) ≫
      MonoidalCategoryStruct.tensorHom (𝟙 (Z i₃)) (ιTensorObj X Y i₁ i₂ (i₁ + i₂) ⋯) ≫
        ιTensorObj Z (tensorObj X Y) i₃ (i₁ + i₂) k ⋯ ≫ (associator Z X Y).inv k
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: case right
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
X : C
f g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
a : (multispanShapeCoend J).R
⊢ (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ f =
    (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ g

Tactic:
· exact h _

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

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ NatTrans.toCatHom₂ (mapWhiskerRight (α_ f✝ g✝ h✝).hom.toNatTrans (𝟭 D)) =
    (Cat.Hom.isoMk (mapCompLeft D (f✝ ≫ g✝).toFunctor h✝.toFunctor)).hom ≫
      (Cat.Hom.isoMk (mapCompLeft D f✝.toFunctor g✝.toFunctor)).hom ▷ (mapPair h✝.toFunctor (𝟭 D)).toCatHom ≫
        (α_ (mapPair f✝.toFunctor (𝟭 D)).toCatHom (mapPair g✝.toFunctor (𝟭 D)).toCatHom
              (mapPair h✝.toFunctor (𝟭 D)).toCatHom).hom ≫
          (mapPair f✝.toFunctor (𝟭 D)).toCatHom ◁ (Cat.Hom.isoMk (mapCompLeft D g✝.toFunctor h✝.toFunctor)).inv ≫
            (Cat.Hom.isoMk (mapCompLeft D f✝.toFunctor (g✝ ≫ h✝).toFunctor)).inv

Tactic:
exact congr($(mapWhiskerRight_associator_hom D _ _ _).toCatHom₂)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : FormalCoproduct C
i : X.I
⊢ Sigma.ι X.toFun i ≫ X.coproductIsoSelf.hom = Hom.fromIncl i (𝟙 (X.obj i))

Tactic:
simp [coproductIsoSelf]

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₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
⊢ ∃ φ, φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃

Tactic:
obtain ⟨φ₁₂, w₁, w₂⟩ := h₁₂.isPullback.exists_lift g₁ g₂ (by cat_disch)
  obtain ⟨φ₂₃, w₂', w₃⟩ := h₂₃.isPullback.exists_lift g₂ g₃ (by cat_disch)
  obtain ⟨φ, w₁₂, w₂₃⟩ := h.chosenPullback.isPullback.exists_lift φ₁₂ φ₂₃ (by cat_disch)
  refine ⟨φ, ?_, ?_, ?_⟩
  · rw [← w₁, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₁]
  · rw [← w₂, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₂]
  · rw [← w₃, ← w₂₃, Category.assoc, ← p₂₃, p₂₃_p₃]

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

Goal state before:
pp: case refl
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m k : ℕ
hh : ¬k < n
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < n then M i else N i) k ≫ eqToHom ⋯

Tactic:
| refl =>

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

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m k : ℕ
h : n ≤ m
hh : ¬k < m
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯

Tactic:
induction h using Nat.leRec with

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

Goal state before:
pp: case e_a.refl
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n m : ℕ
h : m < m + 1
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
    Pi.π (fun m_1 ↦ if m_1 < m + 1 then M m_1 else N m_1) m

Tactic:
| refl =>

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝² : Category.{v₄, u₄} A'
inst✝¹ : Category.{v₅, u₅} B'
inst✝ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
h : IsIso f.left ∧ IsIso f.base ∧ IsIso f.right
⊢ IsIso f

Tactic:
by
    obtain ⟨_, _, _⟩ := h
    use mkIso (asIso f.left) (asIso f.right) (asIso f.base)
      f.left_coherence f.right_coherence |>.inv
    aesop_cat

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
C : Type u'
inst✝ : Category.{v', u'} C
W : J ⥤ Type w
F✝ : J ⥤ C
pt : C
π : ⦃j : J⦄ → W.obj j → (pt ⟶ F✝.obj j)
hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), π x ≫ F✝.map f = π ((ConcreteCategory.hom (W.map f)) x)
F : J ⥤ C
j : J
x✝¹ x✝ : (coyoneda.obj (op j)).Elements
f : x✝¹ ⟶ x✝
⊢ ((Functor.const (coyoneda.obj (op j)).Elements).obj (F.obj j)).map f ≫ F.map x✝.snd =
    F.map x✝¹.snd ≫ (CategoryOfElements.π (coyoneda.obj (op j)) ⋙ F).map f

Tactic:
simp [← Functor.map_comp, Category.id_comp, f.prop.symm]

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

Goal state before:
pp: case refl
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f✝

Tactic:
| refl =>

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ { of := (f ≫ g) ≫ T.η.app Z } = { of := f ≫ T.η.app Y } ≫ { of := g ≫ T.η.app Z }

Tactic:
by
    unfold_projs
    simp [← T.η.naturality g]

Goal state after:
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✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
⊢ (comparison adj).IsEquivalence

Tactic:
have : ∀ (X : Algebra adj.toMonad), IsIso ((comparisonAdjunction adj).unit.app X) := by
      intro X
      apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget adj.toMonad) ?_ _
      · change IsIso ((comparisonAdjunction adj).unit.app X).f
        rw [comparisonAdjunction_unit_f]
        change
          IsIso
            (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X)
                (unitColimitOfPreservesCoequalizer X)).hom
        exact (IsColimit.coconePointUniqueUpToIso _ _).isIso_hom

Goal state after:
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✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
⊢ (comparison adj).IsEquivalence
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c₁ c₁' c₂ c₂' : C
c₃ c₃' : D
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
e :
  (Functor.OplaxMonoidal.δ F c₁ c₂).unmop.app c₃ ≫
      (F.map f).unmop.app ((F.obj c₂).unmop.obj c₃) ≫ (F.obj c₁').unmop.map ((F.map g).unmop.app c₃) =
    (F.map (f ⊗ₘ g)).unmop.app c₃ ≫ (Functor.OplaxMonoidal.δ F c₁' c₂').unmop.app c₃
⊢ ((fun {c c'} f d ↦ (F.map f).unmop.app d) (f ⊗ₘ g) c₃ ≫
        (fun c x x_1 f ↦ (F.obj c).unmop.map f) (c₁' ⊗ c₂') c₃ c₃' h) ≫
      ((Functor.Monoidal.μIso F c₁' c₂').unmop.app c₃').symm.hom =
    ((Functor.Monoidal.μIso F c₁ c₂).unmop.app c₃).symm.hom ≫
      (fun {c c'} f d ↦ (F.map f).unmop.app d) f ((F.obj c₂).unmop.obj c₃) ≫
        (fun c x x_1 f ↦ (F.obj c).unmop.map f) c₁' ((F.obj c₂).unmop.obj c₃) ((F.obj c₂').unmop.obj c₃')
          ((fun {c c'} f d ↦ (F.map f).unmop.app d) g c₃ ≫ (fun c x x_1 f ↦ (F.obj c).unmop.map f) c₂' c₃ c₃' h)

Tactic:
simp [reassoc_of% e]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D ⥤ D
inst✝ : F.Monoidal
c₁ c₁' : D
c₂ c₂' c₃ c₃' : C
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
e :
  (Functor.OplaxMonoidal.δ F c₂ c₃).app c₁ ≫ (F.map h).app ((F.obj c₂).obj c₁) ≫ (F.obj c₃').map ((F.map g).app c₁) =
    (F.map (g ⊗ₘ h)).app c₁ ≫ (Functor.OplaxMonoidal.δ F c₂' c₃').app c₁
⊢ ((fun {d d'} f c ↦ (F.obj c).map f) f (c₂ ⊗ c₃) ≫
        (fun d x x_1 f ↦ (F.map f).app d) c₁' (c₂ ⊗ c₃) (c₂' ⊗ c₃') (g ⊗ₘ h)) ≫
      ((Functor.Monoidal.μIso F c₂' c₃').app c₁').symm.hom =
    ((Functor.Monoidal.μIso F c₂ c₃).app c₁).symm.hom ≫
      (fun {d d'} f c ↦ (F.obj c).map f)
          ((fun {d d'} f c ↦ (F.obj c).map f) f c₂ ≫ (fun d x x_1 f ↦ (F.map f).app d) c₁' c₂ c₂' g) c₃ ≫
        (fun d x x_1 f ↦ (F.map f).app d) ((F.obj c₂').obj c₁') c₃ c₃' h

Tactic:
simp [reassoc_of% e]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : MonoidalCategory D
inst✝⁴ : SymmetricCategory D
inst✝³ : MonoidalClosed D
R : C ⥤ D
inst✝² : R.Faithful
inst✝¹ : R.Full
L : D ⥤ C
adj : L ⊣ R
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
this : d ◁ adj.unit.app ((ihom d).obj (R.obj c)) ≫ adjRetractionAux adj c d = (ihom.ev d).app (R.obj c)
⊢ adj.unit.app ((ihom d).obj (R.obj c)) ≫ adjRetraction adj c d = 𝟙 ((𝟭 D).obj ((ihom d).obj (R.obj c)))

Tactic:
simp only [id_obj, adjRetraction, ← curry_natural_left, this]

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
inst✝⁵ : MonoidalCategory D
inst✝⁴ : SymmetricCategory D
inst✝³ : MonoidalClosed D
R : C ⥤ D
inst✝² : R.Faithful
inst✝¹ : R.Full
L : D ⥤ C
adj : L ⊣ R
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
this : d ◁ adj.unit.app ((ihom d).obj (R.obj c)) ≫ adjRetractionAux adj c d = (ihom.ev d).app (R.obj c)
⊢ curry ((ihom.ev d).app (R.obj c)) = 𝟙 ((ihom d).obj (R.obj c))
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:
apply DayConvolution.corepresentableBy F H |>.homEquiv.injective

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
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.corepresentableBy F H).homEquiv (DayConvolution.map (𝟙 F) (ℌ.map η ℌ') ≫ ℌ'.ev_app) =
    (DayConvolution.corepresentableBy F H).homEquiv (ℌ.ev_app ≫ η)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

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

Tactic:
funext n
      simp [congr_fun ih₁ n, congr_fun ih₂ (normalizeObj Y n)]

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

Goal state before:
pp: case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ η ≫ A ◁ 𝒮 ▷ A

pp: case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).inv

pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ▷ A

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (λ_ A).inv

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ (𝟙_ C) A).hom

Tactic:
simp only [← whiskerLeft_comp]
    rw [whisker_exchange]
    simp only [whiskerLeft_comp]

Goal state after:
case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ 𝟙_ C ≫ A ◁ A ◁ η

case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).inv

case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ▷ A

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (λ_ A).inv

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ (𝟙_ C) A).hom
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 = (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
slice_lhs 2 3 =>
    rw [← whisker_exchange]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ ε ▷ A ≫ (𝟙_ C ◁ ε ≫ η ▷ 𝟙_ C) ≫ (ρ_ A).hom = (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η