mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y : limit (F ⋙ objects)
X : J
⊢ (↾fun g ↦ eqToHom ⋯ ≫ (F.map (𝟙 X)).toFunctor.map g ≫ eqToHom ⋯) =
    𝟙 ((hom (limit.π (F ⋙ objects) X)) X✝ ⟶ (hom (limit.π (F ⋙ objects) X)) Y)

Tactic:
ext f
    let : Category (objects.obj (F.obj X)) := (inferInstance : Category (F.obj X))
    simp [Functor.congr_hom congr($(F.map_id X).toFunctor) f]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
hB : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
⊢ L.Final

Tactic:
let L' := sA.inverse ⋙ L ⋙ sT.functor

Goal state after:
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
hB : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
⊢ L.Final
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: case inl
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x✝ y✝ : A
f✝ : x✝ ⟶ y✝
⊢ F.map ((Sum.inl_ A B).map f✝) ≫
      (match (Sum.inl_ A B).obj y✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom =
    (match (Sum.inl_ A B).obj x✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom ≫
      G.map ((Sum.inl_ A B).map f✝)

pp: case inr
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x✝ y✝ : B
f✝ : x✝ ⟶ y✝
⊢ F.map ((Sum.inr_ A B).map f✝) ≫
      (match (Sum.inr_ A B).obj y✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom =
    (match (Sum.inr_ A B).obj x✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom ≫
      G.map ((Sum.inr_ A B).map f✝)

Tactic:
· simpa using! e₁.hom.naturality _

Goal state after:
case inr
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x✝ y✝ : B
f✝ : x✝ ⟶ y✝
⊢ F.map ((Sum.inr_ A B).map f✝) ≫
      (match (Sum.inr_ A B).obj y✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom =
    (match (Sum.inr_ A B).obj x✝ with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom ≫
      G.map ((Sum.inr_ A B).map f✝)
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

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
X✝ Y✝ : (D ≌ C)ᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (symmEquivInverse C D ⋙ symmEquivFunctor C D).map x✝ ≫ (Iso.refl (Opposite.unop Y✝)).op.hom =
    (Iso.refl (Opposite.unop X✝)).op.hom ≫ (𝟭 (D ≌ C)ᵒᵖ).map x✝

Tactic:
by simp [symm, symmEquivInverse]

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

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj Y ⟶ L.obj X₁
hφ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk φ) =
    s.π.app (StructuredArrow.mk φ)
eq :
  ((const (StructuredArrow (L.obj Y) L)).obj s.pt).map (StructuredArrow.homMk f ⋯) ≫
      s.π.app (StructuredArrow.mk (φ ≫ L.map f)) =
    s.π.app (StructuredArrow.mk φ) ≫ (StructuredArrow.proj (L.obj Y) L ⋙ F).map (StructuredArrow.homMk f ⋯)
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk (φ ≫ L.map f)) =
    s.π.app (StructuredArrow.mk (φ ≫ L.map f))

Tactic:
dsimp at eq hφ ⊢

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj Y ⟶ L.obj X₁
hφ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫ G.map φ ≫ e.inv.app X₁ = s.π.app (StructuredArrow.mk φ)
eq : 𝟙 s.pt ≫ s.π.app (StructuredArrow.mk (φ ≫ L.map f)) = s.π.app (StructuredArrow.mk φ) ≫ F.map f
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫ G.map (φ ≫ L.map f) ≫ e.inv.app X₂ =
    s.π.app (StructuredArrow.mk (φ ≫ L.map f))
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁴ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝³ : HasZeroMorphisms C
inst✝² : (i : I) → HasZeroMorphisms (D i)
inst✝¹ : ∀ (i : I), (F i).PreservesZeroMorphisms
inst✝ : HasZeroObject C
X : C
hX : ∀ (i : I), IsZero ((F i).obj X)
φ : 0 ⟶ X := 0
⊢ IsZero X

Tactic:
have : IsIso φ := by
    rw [hP.isIso_iff]
    exact fun i ↦ (Functor.map_isZero _ (isZero_zero _)).isIso (hX i) _

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁴ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝³ : HasZeroMorphisms C
inst✝² : (i : I) → HasZeroMorphisms (D i)
inst✝¹ : ∀ (i : I), (F i).PreservesZeroMorphisms
inst✝ : HasZeroObject C
X : C
hX : ∀ (i : I), IsZero ((F i).obj X)
φ : 0 ⟶ X := 0
this : IsIso φ
⊢ IsZero X
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj Y ⟶ L.obj X₂
hφ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk φ) =
    s.π.app (StructuredArrow.mk φ)
this : IsIso (F.map w)
eq :
  ((const (StructuredArrow (L.obj Y) L)).obj s.pt).map (StructuredArrow.homMk w ⋯) ≫ s.π.app (StructuredArrow.mk φ) =
    s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) ≫
      (StructuredArrow.proj (L.obj Y) L ⋙ F).map (StructuredArrow.homMk w ⋯)
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app
        (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) =
    s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))

Tactic:
dsimp at eq hφ ⊢

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj Y ⟶ L.obj X₂
hφ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫ G.map φ ≫ e.inv.app X₂ = s.π.app (StructuredArrow.mk φ)
this : IsIso (F.map w)
eq :
  𝟙 s.pt ≫ s.π.app (StructuredArrow.mk φ) =
    s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) ≫ F.map w
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      G.map (φ ≫ (Localization.isoOfHom L W w hw).inv) ≫ e.inv.app X₁ =
    s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case inl
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val✝ : ι₁
⊢ (IsLimit.lift h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.casesOn i c₁.pt c₂.pt)) i
          (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) ⋯) ≫
      (mk bc.pt (c₁.combPairHoms c₂ bc)).proj (Sum.inl val✝) =
    s.proj (Sum.inl val✝)

Tactic:
simp only [fan_mk_proj, combPairHoms]
        erw [← Category.assoc, h.fac]
        simp only [pair_obj_left, mk_π_app, IsLimit.fac]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
X Y Z : C
inst✝² : IsConnected X
inst✝¹ : IsGalois Y
inst✝ : IsGalois Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ autMap (f ≫ g) = autMap g ∘ autMap f

Tactic:
refine funext fun σ ↦ autMap_unique _ σ _ ?_

Goal state after:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
X Y Z : C
inst✝² : IsConnected X
inst✝¹ : IsGalois Y
inst✝ : IsGalois Z
f : X ⟶ Y
g : Y ⟶ Z
σ : Aut X
⊢ (f ≫ g) ≫ ((autMap g ∘ autMap f) σ).hom = σ.hom ≫ f ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case inr
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val✝ : ι₂
⊢ (IsLimit.lift h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.casesOn i c₁.pt c₂.pt)) i
          (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) ⋯) ≫
      (mk bc.pt (c₁.combPairHoms c₂ bc)).proj (Sum.inr val✝) =
    s.proj (Sum.inr val✝)

Tactic:
simp only [fan_mk_proj, combPairHoms]
        erw [← Category.assoc, h.fac]
        simp only [pair_obj_left, mk_π_app, IsLimit.fac]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : FiberFunctor F
g : Aut F
h : ∀ (X : C) (x : (F.obj X).obj), g • x = x
X : C
x : (F.obj X).obj
⊢ (ConcreteCategory.hom (g.hom.app X)) x = (ConcreteCategory.hom ((Iso.hom 1).app X)) x

Tactic:
exact h X x

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

Goal state before:
pp: case inr
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
⊢ IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J

pp: J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
⊢ IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J

Tactic:
· refine ⟨fun G ⟨⟨c, α, hc⟩, H⟩ U V f ↦ ?_⟩
    have hα (i j) (f : i ⟶ j) : α.app i ≫ c.map f = α.app j := by simp [← NatTrans.naturality]
    have hc' := WithTerminal.isLimitEquiv.symm hc
    have inst : IsConnected (WithTerminal J) := isConnected_of_hasTerminal _
    exact (this (J := WithTerminal J) inst).1 G ⟨⟨WithTerminal.liftToTerminal c Over.mkIdTerminal,
      { app i := i.casesOn α.app (Over.mkIdTerminal.from _) }, isLimitOfReflects (Over.forget _) (by
      refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (WithTerminal.isLimitEquiv.symm hc)
      · exact NatIso.ofComponents (fun i ↦ i.casesOn (fun _ ↦ .refl _) (.refl _)) <| by
          rintro (i | _) (j | _) <;> (try rintro ⟨⟩) <;> simp
      · exact Cone.ext (.refl _) (by rintro ⟨⟩ <;> simp))⟩, fun i ↦
        i.casesOn H (.of_isIso (𝟙 F))⟩ f

Goal state after:
J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
⊢ IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
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 : f ≫ g₁ = f ≫ g₂
j : J
⊢ hf.incl.app j ≫ g₁ = hf.incl.app j ≫ g₂

Tactic:
induction j using SuccOrder.limitRecOn with
      | isMin j hj =>
        obtain rfl := hj.eq_bot
        simpa [← cancel_epi hf.isoBot.inv]
      | succ j hj hj' => exact (hf.map_mem j hj _ hZ).1 (by simpa)
      | isSuccLimit j hj hj' =>
        exact (hf.F.isColimitOfIsWellOrderContinuous j hj).hom_ext
          (fun ⟨k, hk⟩ ↦ by simpa using! hj' _ hk)

Goal state after:
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
x✝¹ x✝ : ↑(Set.Iio j)
g : x✝¹ ⟶ x✝
⊢ (⋯.functor ⋙ hf.F).map g ≫ ↑s (op x✝) = ↑s (op x✝¹) ≫ ((Functor.const ↑(Set.Iio j)).obj Z).map g

Tactic:
dsimp
                simpa only [Category.comp_id] using! s.2 g.op

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

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
⊢ (curriedAssociatorNatIso (LocalizedMonoidal L W ε)).hom ≫
      ofBifunctor.Forward.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Forward.firstMap₃ (LocalizedMonoidal L W ε) =
    ofBifunctor.Forward.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Forward.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Forward.secondMap₃ (braidingNatIso L W ε)

Tactic:
apply natTrans₃_ext (L') (L') (L') W W W

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
⊢ (curriedAssociatorNatIso (LocalizedMonoidal L W ε)).inv ≫
      ofBifunctor.Reverse.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Reverse.firstMap₃ (LocalizedMonoidal L W ε) =
    ofBifunctor.Reverse.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Reverse.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Reverse.secondMap₃ (braidingNatIso L W ε)

Tactic:
apply natTrans₃_ext (L') (L') (L') W W W

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case triangle
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)
⊢ (α_ (projectObj f✝ X✝) (𝟙_ D) (projectObj f✝ Y✝)).hom ≫ projectObj f✝ X✝ ◁ (λ_ (projectObj f✝ Y✝)).hom =
    (ρ_ (projectObj f✝ X✝)).hom ▷ projectObj f✝ Y✝

Tactic:
MonoidalCategory.triangle

Goal state after:
case triangle
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)
⊢ (ρ_ (projectObj f✝ X✝)).hom ▷ projectObj f✝ Y✝ = (ρ_ (projectObj f✝ X✝)).hom ▷ projectObj f✝ Y✝
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

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
inst✝ : MonoidalLeftAction C D
c₁✝ c₂✝ c₃✝ c₄✝ : Cᵒᵖ
d₁✝ d₂✝ : Dᵒᵖ
f : unop c₂✝ ⟶ unop c₁✝
g : unop c₄✝ ⟶ unop c₃✝
h : unop d₂✝ ⟶ unop d₁✝
⊢ ((op f ⊗ₘ op g).unop ⊙ₗₘ Quiver.Hom.unop (op h)).op ≫ (αₗ (unop c₂✝) (unop c₄✝) (unop d₂✝)).symm.op.hom =
    (αₗ (unop c₁✝) (unop c₃✝) (unop d₁✝)).symm.op.hom ≫
      (Quiver.Hom.unop (op f) ⊙ₗₘ (Quiver.Hom.unop (op g) ⊙ₗₘ Quiver.Hom.unop (op h)).op.unop).op

Tactic:
apply Quiver.Hom.unop_inj
        have := (αₗ (unop _) (unop _) (unop _)).inv ≫=
          MonoidalLeftAction.actionAssocIso_hom_naturality f g h
        simp only [Iso.inv_hom_id_assoc] at this
        simp [← this]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
X : C
h₁ h₂ : ModObj M X
H : γ = γ
⊢ h₁ = h₂

Tactic:
cases h₁

Goal state after:
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
X : C
h₂ : ModObj M X
smul✝ : M ⊙ₗ X ⟶ X
one_smul✝ : η ⊵ₗ X ≫ smul✝ = (λₗ X).hom
mul_smul✝ : μ ⊵ₗ X ≫ smul✝ = (αₗ M M X).hom ≫ M ⊴ₗ smul✝ ≫ smul✝
H : γ = γ
⊢ { smul := smul✝, one_smul := one_smul✝, mul_smul := mul_smul✝ } = h₂
Module: Mathlib.CategoryTheory.Monoidal.Mod

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
this : μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X
⊢ μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom =
    (αₗ N N Y).hom ≫ N ⊴ₗ ((e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom) ≫ (e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom

Tactic:
reassoc_of% this

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
this : μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X
⊢ ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X ≫ γ ≫ e₂.hom =
    (αₗ N N Y).hom ≫ N ⊴ₗ ((e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom) ≫ (e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom
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
x y : C × C
f : x ⟶ y
this :
  F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ F.obj x.1 ◁ (ihom (F.obj x.1)).map (G.map (f.1 ▷ x.2)) =
    F.obj x.1 ◁ ℌ.π x.2 y.1 ≫ F.obj x.1 ◁ (MonoidalClosed.pre (F.map f.1)).app (G.obj (y.1 ⊗ x.2))
⊢ F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.map f.1 ▷ (ihom (F.obj y.1)).obj (G.obj (y.1 ⊗ x.2)) ≫
        (ihom.ev (F.obj y.1)).app (G.obj (y.1 ⊗ x.2)) ≫ G.map (y.1 ◁ f.2) =
    F.obj x.1 ◁ ℌ.π x.2 x.1 ≫
      F.obj x.1 ◁ (ihom (F.obj x.1)).map (G.map (f.1 ▷ x.2)) ≫
        (ihom.ev (F.obj x.1)).app (G.obj (y.1 ⊗ x.2)) ≫ G.map (y.1 ◁ f.2)

Tactic:
reassoc_of% this

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
x y : C × C
f : x ⟶ y
this :
  F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ F.obj x.1 ◁ (ihom (F.obj x.1)).map (G.map (f.1 ▷ x.2)) =
    F.obj x.1 ◁ ℌ.π x.2 y.1 ≫ F.obj x.1 ◁ (MonoidalClosed.pre (F.map f.1)).app (G.obj (y.1 ⊗ x.2))
⊢ F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.map f.1 ▷ (ihom (F.obj y.1)).obj (G.obj (y.1 ⊗ x.2)) ≫
        (ihom.ev (F.obj y.1)).app (G.obj (y.1 ⊗ x.2)) ≫ G.map (y.1 ◁ f.2) =
    F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.obj x.1 ◁ (MonoidalClosed.pre (F.map f.1)).app (G.obj (y.1 ⊗ x.2)) ≫
        (ihom.ev (F.obj x.1)).app (G.obj (y.1 ⊗ x.2)) ≫ G.map (y.1 ◁ f.2)
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ isArtinianObject X ↔ ∀ (f : ℕ →o (Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m

Tactic:
isArtinianObject,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ WellFoundedLT (Subobject X) ↔ ∀ (f : ℕ →o (Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject X), ¬StrictAnti f
⊢ isArtinianObject X

Tactic:
isArtinianObject,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject X), ¬StrictAnti f
⊢ WellFoundedLT (Subobject X)
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
r : ℤ
α : F ⟶ G
⊢ T.map (r • α.f) ≫ G.a = F.a ≫ (r • α.f)

Tactic:
rw [Functor.map_zsmul, zsmul_comp, Monad.Algebra.Hom.h, comp_zsmul]

Goal state after: