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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
F : C ⥤ Type (max w v₁)
t : F.obj X
⊢ uliftCoyonedaEquiv.symm ((ConcreteCategory.hom (F.map f)) t) =
    uliftCoyoneda.{w, v₁, u₁}.map f.op ≫ uliftCoyonedaEquiv.symm t

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (Skeleton C) ∧ LocallySmall.{w, v, u} C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
⊢ LocallySmall.{w, v, u} C

Tactic:
by

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
⊢ uliftCoyonedaEquiv (uliftCoyoneda.{w, v₁, u₁}.map f) = { down := f.unop }

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Quiver.IsThin C
⊢ EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (Skeleton C)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : Cᵒᵖ) (p : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
φ : Arrow C → (s : C) × (t : C) × (s ⟶ t) := fun f ↦ ⟨f.left, ⟨f.right, f.hom⟩⟩
s t : C
f f' : (𝟭 C).obj s ⟶ (𝟭 C).obj t
h :
  Arrow.right { left := s, right := t, hom := f } = Arrow.right { left := s, right := t, hom := f' } ∧
    Arrow.hom { left := s, right := t, hom := f } ≍ Arrow.hom { left := s, right := t, hom := f' }
⊢ f = f'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v} (Arrow C)

Tactic:
by

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✝ F : J ⥤ C
⊢ ((↾fun c ↦ { pt := c.fst, ι := c.snd }) ≫ ↾fun c ↦ ⟨c.pt, c.ι⟩) = 𝟙 ((X : C) × F.cocones.obj X)

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Small.{w, u} C
inst✝³ : LocallySmall.{w, v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Small.{w, u'} D
inst✝ : LocallySmall.{w, v', u'} D
⊢ Small.{w, max (max (max u' u) v') v} (C ⥤ D)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : LocallySmall.{w, v', u'} A
C : Type w
inst✝ : SmallCategory C
P Q : C ⥤ A
f g : P ⟶ Q
h : f.app = g.app
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Balanced

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Balanced C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
fmono : Mono f
fepi : Epi f
⊢ IsIso f

Tactic:
by

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
F : J ⥤ C
c c' : Cone F
f g : c ⟶ c'
w : f.hom = g.hom
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ ∀ {X_1 Y : C ⥤ Type (max w v₁)} (f : X_1 ⟶ Y),
    ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).map f ≫
        (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation C (Type (max v₁ w)) ⋙
                  (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                    uliftFunctor.{u₁, max v₁ w}).obj
              X).map
          f

Tactic:
by

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
F : J ⥤ C
c d : Cone F
f : c ≅ d
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 c.pt

Tactic:
by

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
F : J ⥤ C
c d : Cone F
f : c ≅ d
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 d.pt

Tactic:
by

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
c d : Cone F
f : c ≅ d
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 c.pt ∧ f.inv.hom ≫ f.hom.hom = 𝟙 d.pt

Tactic:
by

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

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

Tactic:
by

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
c d : Cone F
f : c ≅ d
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 d.pt ∧ f.hom.hom ≫ f.inv.hom = 𝟙 c.pt

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).map f ≫
        (NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation C (Type (max v₁ w)) ⋙
              (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                uliftFunctor.{u₁, max v₁ w}).map
          f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝ : IsIso i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ i ≫ inv i ≫ f = f

Tactic:
by

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
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c c' : Cone F
f : c ⟶ c'
G : C ⥤ D
j : J
⊢ G.map f.hom ≫ G.map (c'.π.app j) = G.map (c.π.app j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type u₂
X : Type u₂
inst✝ : Unique X
s : ↑F.sections
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ (((const C).obj X).map x✝ ≫ ↾fun x ↦ ↑s x✝¹) = (↾fun x ↦ ↑s x✝²) ≫ F.map x✝

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝ : IsIso i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ (inv i ≫ f) ≫ p = g

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type u₂
X : Type u₂
inst✝ : Unique X
τ : (const C).obj X ⟶ F
⊢ ↑F.sections

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = i ≫ i' ≫ g
⊢ (i ≫ i') ≫ ⋯.lift = f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = i ≫ i' ≫ g
⊢ ⋯.lift ≫ p = g

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type u₂
X : Type u₂
inst✝ : Unique X
τ : (const C).obj X ⟶ F
⊢ (fun s ↦ { app := fun j ↦ ↾fun x ↦ ↑s j, naturality := ⋯ })
      ((fun τ ↦ ⟨fun j ↦ (ConcreteCategory.hom (τ.app j)) default, ⋯⟩) τ) =
    τ

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
⊢ sq.HasLift

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Type u₂
f : F ⟶ G
X : Type u₂
inst✝ : Unique X
x : ↑F.sections
⊢ (G.sectionsEquivHom X) ((ConcreteCategory.hom ((sectionsFunctor C).map f)) x) = (F.sectionsEquivHom X) x ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Type u₂
f : F ⟶ G
X : Type u₂
inst✝ : Unique X
τ : (const C).obj X ⟶ F
⊢ (G.sectionsEquivHom X).symm (τ ≫ f) =
    (ConcreteCategory.hom ((sectionsFunctor C).map f)) ((F.sectionsEquivHom X).symm τ)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i' p

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
⊢ HasLiftingProperty i p ↔ HasLiftingProperty i' p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X : C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
x✝ : (F.op ⋙ uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)).obj X✝
⊢ F.map
      (Equiv.ulift
        ((ConcreteCategory.hom
              ((F.op ⋙ uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)).map f ≫
                (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom)).toFun
          x✝)) =
    F.map
      (Equiv.ulift
        ((ConcreteCategory.hom
              ((Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫
                (uliftYoneda.{v₂, v₁, u₁}.obj X).map f)).toFun
          x✝))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X : C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (F.op ⋙ uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)).map f ≫
      (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom =
    (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫ (uliftYoneda.{v₂, v₁, u₁}.obj X).map f

Tactic:
by

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
e : K ≌ J
s : Cone (e.functor ⋙ F)
⊢ ∀ (j : K),
    (((whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom) ⋙ whiskering e.functor).obj s).π.app j =
      (Iso.refl (((whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom) ⋙ whiskering e.functor).obj s).pt).hom ≫
        ((𝟭 (Cone (e.functor ⋙ F))).obj s).π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝¹ : Cᵒᵖ
x✝ : ((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op).obj X✝).obj x✝¹
⊢ F.map
      (Equiv.ulift
        ((ConcreteCategory.hom
              (((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op).map f ≫
                    (hF.homNatIso Y✝).hom).app
                x✝¹)).toFun
          x✝)) =
    F.map
      (Equiv.ulift ((ConcreteCategory.hom (((hF.homNatIso X✝).hom ≫ uliftYoneda.{v₂, v₁, u₁}.map f).app x✝¹)).toFun x✝))

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
h : RetractArrow f' f
g : Z ⟶ W
inst✝ : HasLiftingProperty g f
u : Z ⟶ X'
v : W ⟶ Y'
sq : CommSq u g f' v
⊢ (u ≫ Arrow.Hom.left h.i) ≫ f = g ≫ v ≫ Arrow.Hom.right h.i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op).map f ≫ (hF.homNatIso Y✝).hom =
    (hF.homNatIso X✝).hom ≫ uliftYoneda.{v₂, v₁, u₁}.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
h : Retract X Y
⊢ h.r.op ≫ h.i.op = 𝟙 (Opposite.op X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
h : Retract X Y
F : C ⥤ D
⊢ F.map h.i ≫ F.map h.r = 𝟙 (F.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ (Arrow.Hom.right h.r).op ≫ (Arrow.mk g.op).hom = (Arrow.mk f.op).hom ≫ (Arrow.Hom.left h.r).op

Tactic:
by

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
A : Cone F
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((const J).obj (G.obj A.pt)).map f ≫ G.map (A.π.app Y) = G.map (A.π.app X) ≫ (F ⋙ G).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ (Arrow.Hom.right h.i).op ≫ (Arrow.mk f.op).hom = (Arrow.mk g.op).hom ≫ (Arrow.Hom.left h.i).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : (F ⋙ uliftCoyoneda.{v₁, v₂, u₂}.obj (op (F.obj X))).obj X✝
⊢ F.map
      (Equiv.ulift
        ((ConcreteCategory.hom
              ((F ⋙ uliftCoyoneda.{v₁, v₂, u₂}.obj (op (F.obj X))).map f ≫
                (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom)).toFun
          x✝)) =
    F.map
      (Equiv.ulift
        ((ConcreteCategory.hom
              ((Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫
                (uliftCoyoneda.{v₂, v₁, u₁}.obj (op X)).map f)).toFun
          x✝))

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i p ↔ ∀ (φ : mk i ⟶ mk p), Nonempty (LiftStruct φ)

Tactic:
by

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✝
j : J
⊢ G.map (G.preimage t.hom ≫ Y✝.π.app j) = G.map (X✝.π.app j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (F ⋙ uliftCoyoneda.{v₁, v₂, u₂}.obj (op (F.obj X))).map f ≫
      (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom =
    (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫
      (uliftCoyoneda.{v₂, v₁, u₁}.obj (op X)).map f

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op ⋯ ≫
      Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op ⋯ =
    𝟙 (Arrow.mk f.op)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
x✝¹ : C
x✝ : ((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft C D (Type (max v₁ v₂))).obj F).obj X✝).obj x✝¹
⊢ F.map
      (Equiv.ulift
        ((ConcreteCategory.hom
              (((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft C D (Type (max v₁ v₂))).obj F).map f ≫
                    (hF.homNatIso' (unop Y✝)).hom).app
                x✝¹)).toFun
          x✝)) =
    F.map
      (Equiv.ulift
        ((ConcreteCategory.hom (((hF.homNatIso' (unop X✝)).hom ≫ uliftCoyoneda.{v₂, v₁, u₁}.map f).app x✝¹)).toFun x✝))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
h✝ : RetractArrow f✝ g✝
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ (Arrow.Hom.right h.r).unop ≫ (Arrow.mk g.unop).hom = (Arrow.mk f.unop).hom ≫ (Arrow.Hom.left h.r).unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
h✝ : RetractArrow f✝ g✝
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ (Arrow.Hom.right h.i).unop ≫ (Arrow.mk f.unop).hom = (Arrow.mk g.unop).hom ≫ (Arrow.Hom.left h.i).unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft C D (Type (max v₁ v₂))).obj F).map f ≫
      (hF.homNatIso' (unop Y✝)).hom =
    (hF.homNatIso' (unop X✝)).hom ≫ uliftCoyoneda.{v₂, v₁, u₁}.map f

Tactic:
by

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 F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
K : J ⥤ C
⊢ (functoriality K F).ReflectsIsomorphisms

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
h✝ : RetractArrow f✝ g✝
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop ⋯ ≫
      Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop ⋯ =
    𝟙 (Arrow.mk f.unop)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Retract

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
X Y : C
h : Retract X Y
⊢ F.map h.i ≫ (Arrow.mk (τ.app Y)).hom = (Arrow.mk (τ.app X)).hom ≫ G.map h.i

Tactic:
by

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
X Y : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
⊢ f.hom.op ≫ X.op.π.app j = Y.op.π.app j

Tactic:
by

Goal state after: