mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
e : E ≅ E'
h : E'.IsPointwiseRightKanExtension
⊢ (fun h Y ↦ (isPointwiseRightKanExtensionAtEquivOfIso e Y) (h Y))
      ((fun h Y ↦ (isPointwiseRightKanExtensionAtEquivOfIso e Y).symm (h Y)) h) =
    h

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} C'
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : Category.{v_4, u_4} D
inst✝² : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝¹ : F'.IsRightKanExtension α
G : C ⥤ H
i : F ≅ G
G' : D ⥤ H
β : L ⋙ G' ⟶ G
inst✝ : G'.IsRightKanExtension β
⊢ L.whiskerLeft (G'.liftOfIsRightKanExtension β F' (α ≫ i.hom) ≫ F'.liftOfIsRightKanExtension α G' (β ≫ i.inv)) ≫ α =
    L.whiskerLeft (𝟙 F') ≫ α

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} C'
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : Category.{v_4, u_4} D
inst✝² : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝¹ : F'.IsRightKanExtension α
G : C ⥤ H
i : F ≅ G
G' : D ⥤ H
β : L ⋙ G' ⟶ G
inst✝ : G'.IsRightKanExtension β
⊢ L.whiskerLeft (F'.liftOfIsRightKanExtension α G' (β ≫ i.inv) ≫ G'.liftOfIsRightKanExtension β F' (α ≫ i.hom)) ≫ β =
    L.whiskerLeft (𝟙 G') ≫ β

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
⊢ F''.IsRightKanExtension α' → IsIso φ

Tactic:
intro
    rw [F'.hom_ext_of_isRightKanExtension α φ (rightKanExtensionUnique _ α' _ α).hom
      (by simp [comm])]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

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
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
G : D ⥤ H
⊢ L.whiskerLeft ((L.ranAdjunction H).unit.app G) ≫ L.ranCounit.app (L ⋙ G) = 𝟙 (L ⋙ G)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
G : D ⥤ H
β : F' ⟶ G
⊢ α ≫ L.whiskerLeft ((fun β ↦ F'.descOfIsLeftKanExtension α G β) ((fun β ↦ α ≫ L.whiskerLeft β) β)) =
    α ≫ L.whiskerLeft β

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} C'
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : Category.{v_4, u_4} D
inst✝² : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝¹ : F'.IsLeftKanExtension α
G : C ⥤ H
i : F ≅ G
G' : D ⥤ H
β : G ⟶ L ⋙ G'
inst✝ : G'.IsLeftKanExtension β
⊢ α ≫ L.whiskerLeft (F'.descOfIsLeftKanExtension α G' (i.hom ≫ β) ≫ G'.descOfIsLeftKanExtension β F' (i.inv ≫ α)) =
    α ≫ L.whiskerLeft (𝟙 F')

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} C'
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : Category.{v_4, u_4} D
inst✝² : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝¹ : F'.IsLeftKanExtension α
G : C ⥤ H
i : F ≅ G
G' : D ⥤ H
β : G ⟶ L ⋙ G'
inst✝ : G'.IsLeftKanExtension β
⊢ β ≫ L.whiskerLeft (G'.descOfIsLeftKanExtension β F' (i.inv ≫ α) ≫ F'.descOfIsLeftKanExtension α G' (i.hom ≫ β)) =
    β ≫ L.whiskerLeft (𝟙 G')

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
x : F.obj (op X)
⊢ (ConcreteCategory.hom
        (η.app
          (op (unop (op (CostructuredArrow.mk (yonedaEquiv.symm ((ConcreteCategory.hom (η.app (op X))) x))))).left)))
      x =
    yonedaEquiv (unop (op (CostructuredArrow.mk (yonedaEquiv.symm ((ConcreteCategory.hom (η.app (op X))) x))))).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
s : (CostructuredArrow yoneda A)ᵒᵖ
x : F.obj s
⊢ YonedaCollection.fst (counitForward G (unop s) ((ConcreteCategory.hom (η.app s)) x)).val =
    YonedaCollection.fst ((counitForward F (unop s) x).map₁ (yonedaCollectionPresheafMap₁ η) ⋯).val

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
s : (CostructuredArrow yoneda A)ᵒᵖ
x : F.obj s
⊢ (ConcreteCategory.hom (G.map (eqToHom ⋯)))
      (YonedaCollection.snd ((counitForward F (unop s) x).map₁ (yonedaCollectionPresheafMap₁ η) ⋯).val) =
    YonedaCollection.snd (counitForward G (unop s) ((ConcreteCategory.hom (η.app s)) x)).val

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ yoneda.map f.unop.left ≫ (unop t).hom = (unop s).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ YonedaCollection.fst (counitForward F (unop s) ((ConcreteCategory.hom (F.map f)) x)).val =
    YonedaCollection.fst ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ YonedaCollection.fst (counitForward F (unop t) x).val = t.1.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
p : OverArrows (yonedaCollectionPresheafToA F) s.hom
⊢ YonedaCollection.fst ((counitForward F s ∘ counitBackward F s) p).val = YonedaCollection.fst (id p).val

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
F₁ F₂ : C ⥤ H
α₁ : L.RightExtension F₁
α₂ : L.RightExtension F₂
e : F₁ ≅ F₂
e' : CostructuredArrow.left α₁ ≅ CostructuredArrow.left α₂
h : L.whiskerLeft e'.hom ≫ CostructuredArrow.hom α₂ = CostructuredArrow.hom α₁ ≫ e.hom
⊢ ((whiskeringLeft C D H).obj L).map e'.hom ≫ CostructuredArrow.hom α₂ =
    CostructuredArrow.hom ((L.rightExtensionEquivalenceOfIso₂ e).functor.obj α₁)

Tactic:
by simp [rightExtensionEquivalenceOfIso₂, h]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case refine_1
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension β
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)

Tactic:
apply IsInitial.isInitialIffObj Ψ.inverse _ |>.invFun
    haveI := LeftExtension.isUniversalPrecomp₂ α hα h
    let i :
        (LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β) ≅
        Ψ.inverse.obj (LeftExtension.mk F₂ γ) :=
      StructuredArrow.isoMk (NatIso.ofComponents fun _ ↦ .refl _) <| by
        ext x
        simp [Ψ, ← congr_app hγ x, ← Functor.map_comp]
    exact IsInitial.ofIso this i

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{v_1, u_2} J
inst✝⁹ : Category.{v_2, u_1} D
inst✝⁸ : HasColimitsOfShape J C
inst✝⁷ : HasColimitsOfShape J D
inst✝⁶ : HasExactColimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteLimits F
inst✝⁴ : ReflectsFiniteLimits F
inst✝³ : HasFiniteLimits C
inst✝² : PreservesColimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cone G
hc : IsLimit c
⊢ (Cone.postcompose (G.isoWhiskerLeft (preservesColimitNatIso F).symm).hom).obj
      (((whiskeringRight J C D).obj F ⋙ colim).mapCone c) ≅
    F.mapCone (colim.mapCone c)

Tactic:
exact Cone.ext ((preservesColimitNatIso F).symm.app _)
        fun i ↦ (preservesColimitNatIso F).inv.naturality _

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
⊢ HasExactLimitsOfShape J D

Tactic:
have : HasLimitsOfShape J D := Adjunction.hasLimitsOfShape_of_equivalence e.inverse
  refine ⟨⟨fun _ _ _ => ⟨@fun K => ?_⟩⟩⟩
  refine preservesColimit_of_natIso K (?_ : e.congrRight.inverse ⋙ lim ⋙ e.functor ≅ lim)
  apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso
  exact isoWhiskerLeft (_ ⋙ lim) e.unitIso.symm ≪≫ (preservesLimitNatIso e.inverse).symm

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
this✝ : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
this : PreservesColimitsOfSize.{0, 0, v, v'', u, u''} F
⊢ PreservesColimit H lim

Tactic:
let e : (whiskeringRight J _ _).obj F ⋙ lim ⋙ G ≅ lim :=
      isoWhiskerLeft _ (preservesLimitNatIso G) ≪≫
        (Functor.associator _ _ _).symm ≪≫
        isoWhiskerRight (whiskeringRightObjCompIso F G) _ ≪≫
        isoWhiskerRight ((whiskeringRight J C C).mapIso (asIso adj.unit).symm) _ ≪≫
        isoWhiskerRight whiskeringRightObjIdIso _ ≪≫ lim.leftUnitor

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
this✝ : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
this : PreservesColimitsOfSize.{0, 0, v, v'', u, u''} F
e : (whiskeringRight J C D).obj F ⋙ lim ⋙ G ≅ lim :=
  ((whiskeringRight J C D).obj F).isoWhiskerLeft (preservesLimitNatIso G) ≪≫
    (((whiskeringRight J C D).obj F).associator ((whiskeringRight J D C).obj G) lim).symm ≪≫
      isoWhiskerRight (F.whiskeringRightObjCompIso G) lim ≪≫
        isoWhiskerRight ((whiskeringRight J C C).mapIso (asIso adj.unit).symm) lim ≪≫
          isoWhiskerRight whiskeringRightObjIdIso lim ≪≫ lim.leftUnitor
⊢ PreservesColimit H lim
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ Hom.right ((isoMk (Subobject.underlyingIso (Hom.right (MonoOver.mk f).arrow)) ⋯).hom ≫ f) =
    Hom.right (homMk (projectSubobject (Subobject.mk f)).arrow hq)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : ⊥.IsSeparating
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ ∀ (G : C), ⊥ G → ∀ (h : G ⟶ x✝³), h ≫ x✝¹ = h ≫ x✝

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : ⊥.IsCoseparating
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ ∀ (G : C), ⊥ G → ∀ (h : x✝² ⟶ G), x✝¹ ≫ h = x✝ ≫ h

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : ⊥.IsDetecting
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ∀ (G : C), ⊥ G → ∀ (h : G ⟶ Y✝), ∃! h', h' ≫ f = h

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : ⊥.IsCodetecting
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ∀ (G : C), ⊥ G → ∀ (h : X✝ ⟶ G), ∃! h', f ≫ h' = h

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
t : Trident f
ht : IsLimit t
Z : C
k : Z ⟶ t.pt
⊢ ∀ (j₁ j₂ : J), (k ≫ t.ι) ≫ f j₁ = (k ≫ t.ι) ≫ f j₂

Tactic:
by simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
t : Cotrident f
ht : IsColimit t
Z : C
k : t.pt ⟶ Z
⊢ ∀ (j₁ j₂ : J), f j₁ ≫ t.π ≫ k = f j₂ ≫ t.π ≫ k

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Subobject.underlying.obj (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
⊢ ((isoMk (Subobject.underlyingIso f.unop.left.op).unop ⋯).op.hom ≫ f).unop =
    (homMk (projectQuotient (Subobject.mk f)).arrow.unop hq).op.unop

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
this : IsIso (P.ofLE Q h₁)
⊢ inv (P.ofLE Q h₁) ≫ P.arrow = Q.arrow

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g
x✝⁴ x✝³ : C
x✝² x✝¹ : x✝⁴ ⟶ x✝³
hfg : ∀ (G_1 : C), ObjectProperty.singleton G G_1 → ∀ (h : G_1 ⟶ x✝⁴), h ≫ x✝² = h ≫ x✝¹
x✝ : G ⟶ x✝⁴
⊢ ObjectProperty.singleton G G

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g
x✝⁴ x✝³ : C
x✝² x✝¹ : x✝⁴ ⟶ x✝³
hfg : ∀ (G_1 : C), ObjectProperty.singleton G G_1 → ∀ (h : x✝³ ⟶ G_1), x✝² ≫ h = x✝¹ ≫ h
x✝ : x✝³ ⟶ G
⊢ ObjectProperty.singleton G G

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h) → IsIso f
x✝³ x✝² : C
x✝¹ : x✝³ ⟶ x✝²
hf : ∀ (G_1 : C), ObjectProperty.singleton G G_1 → ∀ (h : G_1 ⟶ x✝²), ∃! h', h' ≫ x✝¹ = h
x✝ : G ⟶ x✝²
⊢ ObjectProperty.singleton G G

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : X ⟶ G), ∃! h', f ≫ h' = h) → IsIso f
x✝³ x✝² : C
x✝¹ : x✝³ ⟶ x✝²
hf : ∀ (G_1 : C), ObjectProperty.singleton G G_1 → ∀ (h : x✝³ ⟶ G_1), ∃! h', x✝¹ ≫ h' = h
x✝ : x✝³ ⟶ G
⊢ ObjectProperty.singleton G G

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
c : Cofan f
hc : IsColimit c
h : IsSeparator c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj f G → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
g : c.pt ⟶ X
b : Discrete β
⊢ ObjectProperty.ofObj f (f b.as)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
hG : IsSeparator G
⊢ ObjectProperty.singleton G ≤ ObjectProperty.pair G H

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
hH : IsSeparator H
⊢ ObjectProperty.singleton H ≤ ObjectProperty.pair G H

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
b : β
hb : IsSeparator (f b)
⊢ ObjectProperty.singleton (f b) ≤ ObjectProperty.ofObj f

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
c : Fan f
hc : IsLimit c
h : IsCoseparator c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj f G → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
g : Y ⟶ c.pt
b : Discrete β
⊢ ObjectProperty.ofObj f (f b.as)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
hG : IsCoseparator G
⊢ ObjectProperty.singleton G ≤ ObjectProperty.pair G H

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
hH : IsCoseparator H
⊢ ObjectProperty.singleton H ≤ ObjectProperty.pair G H

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
b : β
hb : IsCoseparator (f b)
⊢ ObjectProperty.singleton (f b) ≤ ObjectProperty.ofObj f

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
isc : IsColimit
  ((Over.forget c.pt).mapCocone
    (colimit.cocone
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))) :=
  isColimitOfPreserves (Over.forget c.pt)
    (colimit.isColimit
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
i : I
⊢ c.ι.app i ≫
      (hc.coconePointUniqueUpToIso isc).hom ≫
        (colimit
            ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙
              CostructuredArrow.toOver yoneda c.pt)).hom =
    c.ι.app i ≫ (Over.mk (𝟙 c.pt)).hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i : C
x : F i
⊢ (equivOfIsColimit hc) ((equivOfIsColimit hc).symm (c.inj i x)) = (equivOfIsColimit hc) ⟨i, x⟩

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
x :
  (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
      (coconeπOpCompShrinkYonedaObj F X)).pt
⊢ ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).ιColimitType (op (F.elementsMk X x))
        (shrinkYonedaObjObjEquiv.symm (𝟙 X))) =
    x

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: 𝕜 : Type ?u.3
inst✝¹ : DivisionRing 𝕜
inst✝ : CharZero 𝕜
q : 𝕜
⊢ q / ↑0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
hn : Even n
⊢ n.negOnePow = 1

Tactic:
obtain ⟨k, rfl⟩ := hn

Goal state after:
k : ℤ
⊢ (k + k).negOnePow = 1
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
hn : Odd n
⊢ n.negOnePow = -1

Tactic:
obtain ⟨k, rfl⟩ := hn

Goal state after:
k : ℤ
⊢ (2 * k + 1).negOnePow = -1
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f ((2 * n) • c)

Tactic:
rw [mul_comm, mul_zsmul, two_zsmul, ← two_nsmul]
  exact h.periodic.zsmul n

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (-↑(n + 1) * c) = 0

Tactic:
neg_mul,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (-(↑(n + 1) * c)) = 0
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ {x ∈ range n | p x} ↔ x < n ∧ p x

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case succ.succ
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime : ∀ (p : ℕ), Prime p → motive p
composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)
n p a : ℕ
hp : Prime p
ha : motive (a + 1 + 1)
⊢ motive (p * (a + 1 + 1))

Tactic:
exact composite _ hp.two_le (prime _ hp) _ a.one_lt_succ_succ ha

Goal state after: