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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
⊢ e.changeFunctor (Iso.refl e.functor) = e

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
G G' : C ⥤ D
iso₁ : e.functor ≅ G
iso₂ : G ≅ G'
⊢ (e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ (unop G).rightOpLeftOpIso.hom ≫ η.unop =
    NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (unop F).rightOpLeftOpIso.hom

Tactic:
cat_disch

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

Goal state before:
pp: T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso (Hom.left ff)
inst✝ : IsIso (Hom.right ff)
⊢ ff ≫ homMk (inv (Hom.left ff)) (inv (Hom.right ff)) ⋯ = 𝟙 f ∧
    homMk (inv (Hom.left ff)) (inv (Hom.right ff)) ⋯ ≫ ff = 𝟙 g

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.LeftInverse unop op

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.RightInverse unop op

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.LeftInverse op unop

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.RightInverse op unop

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y Z : C
p : X = Y
q : Y = Z
x : F.obj X
⊢ (ConcreteCategory.hom (F.map (eqToHom q))) ((ConcreteCategory.hom (F.map (eqToHom p))) x) =
    (ConcreteCategory.hom (F.map (eqToHom ⋯))) x

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
x✝ : Aut X
⊢ (fun y ↦ { hom := h.hom ≫ y.hom ≫ h.inv, inv := h.hom ≫ y.inv ≫ h.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ })
      ((fun x ↦ { hom := h.inv ≫ x.hom ≫ h.hom, inv := h.inv ≫ x.inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }) x✝) =
    x✝

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
x✝ : Aut Y
⊢ (fun x ↦ { hom := h.inv ≫ x.hom ≫ h.hom, inv := h.inv ≫ x.inv ≫ h.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ })
      ((fun y ↦ { hom := h.hom ≫ y.hom ≫ h.inv, inv := h.hom ≫ y.inv ≫ h.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }) x✝) =
    x✝

Tactic:
cat_disch

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

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
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ (map α β).map { left := F₁.preimage φ.left, right := F₂.preimage φ.right, w := ⋯ } = φ

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ Y₁ X₂ Y₂ : C
f : X₁ ≅ X₂
g : Y₁ ≅ Y₂
⊢ Function.LeftInverse (fun h ↦ f ≪≫ h ≪≫ g.symm) fun h ↦ f.symm ≪≫ h ≪≫ g

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ Y₁ X₂ Y₂ : C
f : X₁ ≅ X₂
g : Y₁ ≅ Y₂
⊢ Function.RightInverse (fun h ↦ f ≪≫ h ≪≫ g.symm) fun h ↦ f.symm ≪≫ h ≪≫ g

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Conj

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Aut X
⊢ α.conjAut f = α.symm ≪≫ f ≪≫ α

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
⊢ asHom g₁ ≫ f = asHom g₂ ≫ f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget CommRingCat).map f)
    let ff : X →+* Y := f.hom
    let e : X ≃+* Y := { ff, i.toEquiv with }
    exact e.toCommRingCatIso.isIso_hom

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

Goal state before:
pp: case mk.mk
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
lift✝¹ : (s : Cone F) → s.pt ⟶ t.pt
fac✝¹ : ∀ (s : Cone F) (j : J), lift✝¹ s ≫ t.π.app j = s.π.app j
uniq✝¹ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝¹ s
lift✝ : (s : Cone F) → s.pt ⟶ t.pt
fac✝ : ∀ (s : Cone F) (j : J), lift✝ s ≫ t.π.app j = s.π.app j
uniq✝ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝ s
⊢ lift✝¹ = lift✝

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
r t : Cone F
i : r ≅ t
⊢ Function.LeftInverse (fun h ↦ h.ofIsoLimit i.symm) fun h ↦ h.ofIsoLimit i

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
r t : Cone F
i : r ≅ t
⊢ Function.RightInverse (fun h ↦ h.ofIsoLimit i.symm) fun h ↦ h.ofIsoLimit i

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
D : Type u₄
inst✝ : Category.{v₄, u₄} D
G : K ⥤ D
h : Cone G ≌ Cone F
c : Cone G
⊢ Function.LeftInverse (ofRightAdjoint h.symm.toAdjunction) fun P ↦
    (ofRightAdjoint h.toAdjunction P).ofIsoLimit (h.unitIso.symm.app c)

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
D : Type u₄
inst✝ : Category.{v₄, u₄} D
G : K ⥤ D
h : Cone G ≌ Cone F
c : Cone G
⊢ Function.RightInverse (ofRightAdjoint h.symm.toAdjunction) fun P ↦
    (ofRightAdjoint h.toAdjunction P).ofIsoLimit (h.unitIso.symm.app c)

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
D : Type u₄
inst✝ : Category.{v₄, u₄} D
G : K ⥤ D
h : Cocone G ≌ Cocone F
c : Cocone G
⊢ Function.LeftInverse (IsColimit.ofLeftAdjoint h.toAdjunction) fun P ↦
    (IsColimit.ofLeftAdjoint h.symm.toAdjunction P).ofIsoColimit (h.unitIso.symm.app c)

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
D : Type u₄
inst✝ : Category.{v₄, u₄} D
G : K ⥤ D
h : Cocone G ≌ Cocone F
c : Cocone G
⊢ Function.RightInverse (IsColimit.ofLeftAdjoint h.toAdjunction) fun P ↦
    (IsColimit.ofLeftAdjoint h.symm.toAdjunction P).ofIsoColimit (h.unitIso.symm.app c)

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t s : Cone F
e : K ≌ J
⊢ Function.LeftInverse (ofWhiskerEquivalence e) fun h ↦ h.whiskerEquivalence e

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t s : Cone F
e : K ≌ J
⊢ Function.RightInverse (ofWhiskerEquivalence e) fun h ↦ h.whiskerEquivalence e

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F✝ : J ⥤ C
t✝ : Cone F✝
F : J ⥤ C
s : Cone F
G : K ⥤ C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : J ≌ K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := ⋯
⊢ ∀ (j : K),
    (P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) ≫
          Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s)) ≫
        t.π.app j =
      𝟙 t.pt ≫ t.π.app j

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
π : (const J).obj W ⟶ F
⊢ (fun f ↦ (t.extend f).π) ((fun π ↦ h.lift { pt := W, π := π }) π) = π

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝² : Category.{v₂, u₂} K✝
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
F✝ : J ⥤ C
t✝ : Cone F✝
D : Type u₄
inst✝ : Category.{v₄, u₄} D
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (G.mapCone c)

Tactic:
apply postcomposeInvEquiv (isoWhiskerLeft K h :) (mapCone G c) _
  apply t.ofIsoLimit (postcomposeWhiskerLeftMapCone h.symm c).symm

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z W : C
f : yoneda.obj Z ⟶ yoneda.obj W
X : Cᵒᵖ
x : (yoneda.obj Z).obj X
this :
  (ConcreteCategory.hom (f.app (op (unop X)))) ((ConcreteCategory.hom ((yoneda.obj Z).map (Quiver.Hom.op x))) (𝟙 Z)) =
    (ConcreteCategory.hom ((yoneda.obj W).map (Quiver.Hom.op x))) ((ConcreteCategory.hom (f.app (op Z))) (𝟙 Z))
⊢ (ConcreteCategory.hom ((yoneda.map ((ConcreteCategory.hom (f.app (op Z))) (𝟙 (unop (op Z))))).app X)).toFun x =
    (ConcreteCategory.hom (f.app X)).toFun x

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z W : Cᵒᵖ
f : coyoneda.obj Z ⟶ coyoneda.obj W
X : C
x : (coyoneda.obj Z).obj X
this :
  (ConcreteCategory.hom (f.app X)) ((ConcreteCategory.hom ((coyoneda.obj Z).map x)) (𝟙 (unop Z))) =
    (ConcreteCategory.hom ((coyoneda.obj W).map x)) ((ConcreteCategory.hom (f.app (unop Z))) (𝟙 (unop Z)))
⊢ (ConcreteCategory.hom
          ((coyoneda.map (Quiver.Hom.op ((ConcreteCategory.hom (f.app (unop Z))) (𝟙 (unop Z))))).app X)).toFun
      x =
    (ConcreteCategory.hom (f.app X)).toFun x

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.IsomorphismClasses

Goal state before:
pp: case h
C : Cat
x : Quotient (isIsomorphicSetoid ↑C)
⊢ ∀ (a b : ↑C) (p : (isIsomorphicSetoid ↑C) a b), ⋯ = ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.IsomorphismClasses

Goal state before:
pp: case h
C D E : Cat
f : C ⟶ D
g : D ⟶ E
x : Quotient (isIsomorphicSetoid ↑C)
⊢ ∀ (a b : ↑C) (p : (isIsomorphicSetoid ↑C) a b), ⋯ = ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x ↦ x ≫ f
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
⊢ (fun x ↦ x ≫ f) (f ≫ g) = (fun x ↦ x ≫ f) (𝟙 X)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: case h_map.up
X✝ : Type u
X Y : Discrete X✝
down✝ : PLift (X.as = Y.as)
⊢ ((Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X✝)))).map { down := down✝ }).down =
    (eqToHom ⋯ ≫ (𝟭 (Discrete X✝)).map { down := down✝ } ≫ eqToHom ⋯).down

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: case h_map
X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ autoParam
    (∀ (X Y : Discrete X✝) (f_1 : X ⟶ Y),
      (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (f ≫ g)))).map f_1 =
        eqToHom ⋯ ≫
          (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom f)) ⋙
                  Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom g))).map
              f_1 ≫
            eqToHom ⋯)
    ext._auto_1

pp: case h_obj
X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ∀ (X : Discrete X✝),
    (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (f ≫ g)))).obj X =
      (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom f)) ⋙
            Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom g))).obj
        X

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: X✝ Y✝ : Type u
F : typeToCat.obj X✝ ⟶ typeToCat.obj Y✝
⊢ ∀ (X : ↑(typeToCat.obj X✝)),
    (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.obj X = F.toFunctor.obj X

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
s : Set C
inst✝¹ : Small.{w, u} ↑s
inst✝ : LocallySmall.{w, v, u} C
⊢ Function.Injective fun x ↦ ⟨x.obj, ⋯⟩

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: X✝ Y✝ : Type u
F : typeToCat.obj X✝ ⟶ typeToCat.obj Y✝
x y : ↑(typeToCat.obj X✝)
f : x ⟶ y
⊢ ((typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.map f).down =
    (eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯).down

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
K : J ⥤ C
c d : Cone K
f : c ⟶ d
i : IsIso f.hom
⊢ f ≫ { hom := inv f.hom, w := ⋯ } = 𝟙 c ∧ { hom := inv f.hom, w := ⋯ } ≫ f = 𝟙 d

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
E : Type u₅
inst✝¹ : Category.{v₅, u₅} E
F : J ⥤ C
s : Cone F
X : C
f : X ⟶ s.pt
inst✝ : IsIso f
⊢ s.extendHom f ≫ (s.extendIso (asIso' f)).hom = 𝟙 (s.extend f) ∧ (s.extendIso (asIso' f)).hom ≫ s.extendHom f = 𝟙 s

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u₃
inst✝⁴ : Category.{v₃, u₃} C
D : Type u₄
inst✝³ : Category.{v₄, u₄} D
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : J ⥤ C
G : C ⥤ D
inst✝¹ : G.Full
inst✝ : G.Faithful
X✝ Y✝ : Cone F
t : (functoriality F G).obj X✝ ⟶ (functoriality F G).obj Y✝
⊢ (functoriality F G).map { hom := G.preimage t.hom, w := ⋯ } = t

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.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
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Function.LeftInverse (fun l ↦ { l := (adj.homEquiv B X).symm l.l, fac_left := ⋯, fac_right := ⋯ }) fun l ↦
    { l := (adj.homEquiv B X) l.l, fac_left := ⋯, fac_right := ⋯ }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.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
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Function.RightInverse (fun l ↦ { l := (adj.homEquiv B X).symm l.l, fac_left := ⋯, fac_right := ⋯ }) fun l ↦
    { l := (adj.homEquiv B X) l.l, fac_left := ⋯, fac_right := ⋯ }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ Function.LeftInverse (fun s ↦ { section_ := F.preimage s.section_, id := ⋯ }) fun f_1 ↦ f_1.map F

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
x : SplitEpi (F.map f)
⊢ (fun f_1 ↦ f_1.map F) ((fun s ↦ { section_ := F.preimage s.section_, id := ⋯ }) x) = x

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ (X_1 : Discrete PEmpty.{1}) → ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1 ⟶ (Functor.empty C).obj X_1

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ (X_1 : Discrete PEmpty.{1}) → (Functor.empty C).obj X_1 ⟶ ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
⊢ (X : Discrete PEmpty.{1}) → ((Functor.const (Discrete PEmpty.{1})).obj Y).obj X ⟶ F.obj X

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
t : IsLimit { pt := Y, π := { app := fun X ↦ id (Discrete.casesOn X fun as ↦ ⋯.elim), naturality := ⋯ } }
X : C
⊢ (X_1 : Discrete PEmpty.{1}) → ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1 ⟶ F.obj X_1

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
t : IsLimit { pt := Y, π := { app := fun X ↦ id (Discrete.casesOn X fun as ↦ ⋯.elim), naturality := ⋯ } }
X : C
f : X ⟶ Y
⊢ (X_1 : Discrete PEmpty.{1}) → ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1 ⟶ F.obj X_1

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X : C
⊢ (X_1 : Discrete PEmpty.{1}) → F.obj X_1 ⟶ ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X✝ : C
t : IsColimit { pt := X✝, ι := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } }
X : C
⊢ (X_1 : Discrete PEmpty.{1}) → F.obj X_1 ⟶ ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X✝ : C
t : IsColimit { pt := X✝, ι := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } }
X : C
f : X✝ ⟶ X
⊢ (X_1 : Discrete PEmpty.{1}) → F.obj X_1 ⟶ ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
⊢ (X : Discrete PEmpty.{w + 1}) → ((Functor.const (Discrete PEmpty.{w + 1})).obj c.pt).obj X ⟶ F₁.obj X

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
⊢ (X : Discrete PEmpty.{w + 1}) → F₁.obj X ⟶ ((Functor.const (Discrete PEmpty.{w + 1})).obj c.pt).obj X

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit G
α : F ⟶ G
inst✝ : IsIso α
⊢ limMap α ≫ limMap (inv α) = 𝟙 (limit F)

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit G
α : F ⟶ G
inst✝ : IsIso α
⊢ limMap (inv α) ≫ limMap α = 𝟙 (limit G)

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
c : Cone F
X : C
f : X ⟶ c.pt
⊢ lift F (c.extend f) = f ≫ lift F c

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
s : LimitCone (E ⋙ F)
t : LimitCone F
⊢ pre F E = (isoLimitCone t).hom ≫ s.isLimit.lift (Cone.whisker E t.cone) ≫ (isoLimitCone s).inv

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasLimitsOfShape J C
F : J ⥤ C
⊢ pre F (𝟭 J) = lim.map F.leftUnitor.inv

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : C
g : J ⥤ C
⊢ Function.LeftInverse (fun f ↦ { app := fun x ↦ f ≫ limit.π g x, naturality := ⋯ }) fun f ↦
    limit.lift g { pt := c, π := f }

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : C
g : J ⥤ C
⊢ Function.RightInverse (fun f ↦ { app := fun x ↦ f ≫ limit.π g x, naturality := ⋯ }) fun f ↦
    limit.lift g { pt := c, π := f }

Tactic:
cat_disch

Goal state after: