awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} 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_1 : (s : Cone F) → s.pt ⟶ t.pt
fac_1 : ∀ (s : Cone F) (j : J), lift_1 s ≫ t.π.app j = s.π.app j
uniq_1 : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift_1 s
mk : lift = lift_1
⊢ { lift := lift, fac := fac, uniq := uniq : IsLimit t } = { lift := lift_1, fac := fac_1, uniq := uniq_1 }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F G : Functor.{v₁, v₃, u₁, u₃} J C
c : Cone F
d : Cone G
hd : IsLimit d
α : F ⟶ G
j : J
⊢ map c hd α ≫ d.π.app j = c.π.app j ≫ α.app j

Tactic:
fac _ _ _

Premises used: CategoryTheory.Limits.IsLimit.map, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
c : Cone F
t : IsLimit c
⊢ t.lift c = 𝟙 c.pt

Tactic:
(t.uniq _ _ fun _ => id_comp _).symm

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.IsLimit.uniq, Eq.symm, CategoryTheory.NatTrans.app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
w : g.hom = (h.liftConeMorphism s).hom
⊢ g = h.liftConeMorphism s

Tactic:
apply ConeMorphism.ext

Premises used: CategoryTheory.Limits.ConeMorphism.ext
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g.hom = (h.liftConeMorphism s).hom

Tactic:
h.uniq _ _ g.w

Premises used: CategoryTheory.Limits.ConeMorphism.w, CategoryTheory.Limits.IsLimit.uniq
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g.hom = (h.liftConeMorphism s).hom

Tactic:
exact h.uniq _ _ g.w

Premises used: CategoryTheory.Limits.ConeMorphism.w, CategoryTheory.Limits.IsLimit.uniq
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
h : IsLimit t
s : Cone F
⊢ ∃! l : s.pt ⟶ t.pt, ∀ (j : J), l ≫ t.π.app j = s.π.app j

Tactic:
⟨h.lift s, h.fac s, h.uniq s⟩

Premises used: CategoryTheory.Limits.IsLimit.uniq, ExistsUnique, And.intro, Exists.intro, CategoryTheory.Limits.IsLimit.lift, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
ht : ∀ (s : Cone F), ∃! l : s.pt ⟶ t.pt, ∀ (j : J), l ≫ t.π.app j = s.π.app j
choose :
  (s : (s : Cone F) → s.pt ⟶ t.pt) →
    (hs : ∀ (s_1 : Cone F), (fun (l : s_1.pt ⟶ t.pt) ↦ ∀ (j : J), l ≫ t.π.app j = s_1.π.app j) (s s_1)) →
      (hs' :
          ∀ (s_1 : Cone F) (y : s_1.pt ⟶ t.pt),
            (fun (l : s_1.pt ⟶ t.pt) ↦ ∀ (j : J), l ≫ t.π.app j = s_1.π.app j) y → y = s s_1) →
        IsLimit t
⊢ IsLimit t

Tactic:
choose s hs hs' using ht
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
s : (s : Cone F) → s.pt ⟶ t.pt
hs : ∀ (s_1 : Cone F), (fun (l : s_1.pt ⟶ t.pt) ↦ ∀ (j : J), l ≫ t.π.app j = s_1.π.app j) (s s_1)
hs' :
  ∀ (s_1 : Cone F) (y : s_1.pt ⟶ t.pt), (fun (l : s_1.pt ⟶ t.pt) ↦ ∀ (j : J), l ≫ t.π.app j = s_1.π.app j) y → y = s s_1
⊢ IsLimit t

Tactic:
exact ⟨s, hs, hs'⟩
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
lift : (s : Cone F) → s ⟶ t
uniq : ∀ (s : Cone F) (m : s ⟶ t), m = lift s
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ { hom := m, w := w : ConeMorphism s t } = lift s

Tactic:
apply uniq
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
s t : Cone F
P : IsLimit s
Q : IsLimit t
f : s ⟶ t
⊢ IsIso f

Tactic:
⟨⟨P.liftConeMorphism t, ⟨P.uniq_cone_morphism, Q.uniq_cone_morphism⟩⟩⟩

Premises used: And.intro, Exists.intro, CategoryTheory.Limits.IsLimit.liftConeMorphism, CategoryTheory.Limits.IsLimit.uniq_cone_morphism, CategoryTheory.IsIso.mk
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
s t : Cone F
P : IsLimit s
Q : IsLimit t
j : J
⊢ (P.conePointUniqueUpToIso Q).hom ≫ t.π.app j = s.π.app j

Tactic:
(uniqueUpToIso P Q).hom.w _

Premises used: CategoryTheory.Limits.ConeMorphism.w, CategoryTheory.Limits.IsLimit.uniqueUpToIso, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
s t : Cone F
P : IsLimit s
Q : IsLimit t
j : J
⊢ (P.conePointUniqueUpToIso Q).inv ≫ s.π.app j = t.π.app j

Tactic:
(uniqueUpToIso P Q).inv.w _

Premises used: CategoryTheory.Limits.ConeMorphism.w, CategoryTheory.Limits.IsLimit.uniqueUpToIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
r s t : Cone F
P : IsLimit s
Q : IsLimit t
⊢ ∀ (j : J), (P.lift r ≫ (P.conePointUniqueUpToIso Q).hom) ≫ t.π.app j = r.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
r s t : Cone F
P : IsLimit s
Q : IsLimit t
⊢ ∀ (j : J), (Q.lift r ≫ (P.conePointUniqueUpToIso Q).inv) ≫ s.π.app j = r.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
r t : Cone F
P : IsLimit r
i : r ≅ t
s : Cone F
m : s ⟶ t
rw : m ≫ i.inv = P.liftConeMorphism s
⊢ m = (fun (s : Cone F) ↦ P.liftConeMorphism s ≫ i.hom) s

Tactic:
rw [← i.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
r t : Cone F
P : IsLimit r
i : r ≅ t
s : Cone F
m : s ⟶ t
⊢ m ≫ i.inv = P.liftConeMorphism s

Tactic:
apply P.uniq_cone_morphism

Premises used: CategoryTheory.Limits.IsLimit.uniq_cone_morphism
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
r t : Cone F
P : IsLimit r
i : r ≅ t
s : Cone F
⊢ (P.ofIsoLimit i).lift s = P.lift s ≫ i.hom.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
r t : Cone F
i : r ≅ t
P : IsLimit r
⊢ (equivIsoLimit i : (a : IsLimit r) → IsLimit t) P = P.ofIsoLimit i

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsLimit.mkConeMorphism, CategoryTheory.Limits.IsLimit.ofIsoLimit, rfl
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
r t : Cone F
i : r ≅ t
P : IsLimit t
⊢ ((equivIsoLimit i).symm : (a : IsLimit t) → IsLimit r) P = P.ofIsoLimit i.symm

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsLimit.mkConeMorphism, CategoryTheory.Limits.IsLimit.ofIsoLimit, rfl
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
r t : Cone F
P : IsLimit r
i : IsIso (P.lift t)
⊢ IsIso (P.liftConeMorphism t).hom

Tactic:
haveI : IsIso (P.liftConeMorphism t).hom := i
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
r t : Cone F
P : IsLimit r
i : IsIso (P.lift t)
this : IsIso (P.liftConeMorphism t).hom
⊢ IsIso (P.liftConeMorphism t)

Tactic:
haveI : IsIso (P.liftConeMorphism t) := Cone.cone_iso_of_hom_iso _
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
r t : Cone F
P : IsLimit r
i : IsIso (P.lift t)
this_1 : IsIso (P.liftConeMorphism t).hom
this : IsIso (P.liftConeMorphism t)
symm : t ≅ r
⊢ r ≅ t

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
r t : Cone F
P : IsLimit r
i : IsIso (P.lift t)
this_1 : IsIso (P.liftConeMorphism t).hom
this : IsIso (P.liftConeMorphism t)
⊢ t ≅ r

Tactic:
apply asIso (P.liftConeMorphism t)

Premises used: CategoryTheory.Limits.IsLimit.liftConeMorphism, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
h : IsLimit t
W : C
m : W ⟶ t.pt
⊢ m = h.lift { pt := W, π := { app := fun (b : J) ↦ m ≫ t.π.app b, naturality := ⋯ : NatTrans (obj (const J) W) F } }

Tactic:
h.uniq { pt := W, π := { app := fun b => m ≫ t.π.app b } } m fun _ => rfl

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.NatTrans.mk, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Cone.mk, CategoryTheory.NatTrans.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
rw :
  Eq (α := W ⟶ t.pt)
    (h.lift { pt := W, π := { app := fun (b : J) ↦ f ≫ t.π.app b, naturality := ⋯ : NatTrans (obj (const J) W) F } } :
      { pt := W, π := { app := fun (b : J) ↦ f ≫ t.π.app b, naturality := ⋯ : NatTrans (obj (const J) W) F } :
            Cone F }.pt ⟶
        t.pt)
    (h.lift { pt := W, π := { app := fun (b : J) ↦ f' ≫ t.π.app b, naturality := ⋯ : NatTrans (obj (const J) W) F } })
⊢ f = f'

Tactic:
rw [h.hom_lift f, h.hom_lift f']

Premises used: CategoryTheory.Limits.IsLimit.hom_lift
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
h₁ :
  Eq (α := (X : J) → obj.{v₁, v₃, u₁, u₃} (obj (const J) W) X ⟶ F.obj X) (fun (b : J) ↦ f ≫ t.π.app b) fun (b : J) ↦
    f' ≫ t.π.app b
⊢ Eq (α := W ⟶ t.pt)
    (h.lift { pt := W, π := { app := fun (b : J) ↦ f ≫ t.π.app b, naturality := ⋯ : NatTrans (obj (const J) W) F } } :
      { pt := W, π := { app := fun (b : J) ↦ f ≫ t.π.app b, naturality := ⋯ : NatTrans (obj (const J) W) F } :
            Cone F }.pt ⟶
        t.pt)
    (h.lift { pt := W, π := { app := fun (b : J) ↦ f' ≫ t.π.app b, naturality := ⋯ : NatTrans (obj (const J) W) F } })

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ Eq (α := (X : J) → obj.{v₁, v₃, u₁, u₃} (obj (const J) W) X ⟶ F.obj X) (fun (b : J) ↦ f ≫ t.π.app b) fun (b : J) ↦
    f' ≫ t.π.app b

Tactic:
funext w

Premises used: funext
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ Eq (α := (X : J) → obj.{v₁, v₃, u₁, u₃} (obj (const J) W) X ⟶ F.obj X) (fun (b : J) ↦ f ≫ t.π.app b) fun (b : J) ↦
    f' ≫ t.π.app b

Tactic:
exact funext w

Premises used: funext
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
s t : Cone F
hs : IsLimit s
h : Nonempty (IsLimit t)
ht : IsLimit t
⊢ ∀ (j : J), (hs.lift t ≫ ht.lift s) ≫ t.π.app j = 𝟙 t.pt ≫ t.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
s t : Cone F
hs : IsLimit s
h : Nonempty (IsLimit t)
ht : IsLimit t
⊢ ∀ (j : J), (ht.lift s ≫ hs.lift t) ≫ s.π.app j = 𝟙 s.pt ≫ s.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₂, v₄, u₂, u₄} K D
h : Cone G ≌ Cone F
c : Cone G
P : IsLimit (h.functor.obj c)
s : Cone G
⊢ lift ((ofConeEquiv h : (a : IsLimit (h.functor.obj c)) → IsLimit c) P) s =
    ((h.unitIso.hom.app s).hom ≫ ConeMorphism.hom (h.inverse.map (P.liftConeMorphism (h.functor.obj s)))) ≫
      (h.unitIso.inv.app c).hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₂, v₄, u₂, u₄} K D
h : Cone G ≌ Cone F
c : Cone G
P : IsLimit c
s : Cone F
⊢ lift ((Equiv.symm (ofConeEquiv h) : (a : IsLimit c) → IsLimit (h.functor.obj c)) P) s =
    (h.counitIso.inv.app s).hom ≫ ConeMorphism.hom (h.functor.map (P.liftConeMorphism (h.inverse.obj s)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F G : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
t : Cone G
P : IsLimit s
Q : IsLimit t
w : F ≅ G
⊢ ∀ (j : J), (map s Q w.hom ≫ map t P w.inv) ≫ s.π.app j = 𝟙 s.pt ≫ s.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F G : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
t : Cone G
P : IsLimit s
Q : IsLimit t
w : F ≅ G
⊢ ∀ (j : J), (map t P w.inv ≫ map s Q w.hom) ≫ t.π.app j = 𝟙 t.pt ≫ t.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F G : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
t : Cone G
P : IsLimit s
Q : IsLimit t
w : F ≅ G
j : J
⊢ (P.conePointsIsoOfNatIso Q w).hom ≫ t.π.app j = s.π.app j ≫ w.hom.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F G : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
t : Cone G
P : IsLimit s
Q : IsLimit t
w : F ≅ G
j : J
⊢ (P.conePointsIsoOfNatIso Q w).inv ≫ s.π.app j = t.π.app j ≫ w.inv.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F G : Functor.{v₁, v₃, u₁, u₃} J C
r s : Cone F
t : Cone G
P : IsLimit s
Q : IsLimit t
w : F ≅ G
⊢ ∀ (j : J), (P.lift r ≫ (P.conePointsIsoOfNatIso Q w).hom) ≫ t.π.app j = map r Q w.hom ≫ t.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F G : Functor.{v₁, v₃, u₁, u₃} J C
r s : Cone G
t : Cone F
P : IsLimit t
Q : IsLimit s
w : F ≅ G
⊢ ∀ (j : J), (Q.lift r ≫ (P.conePointsIsoOfNatIso Q w).inv) ≫ t.π.app j = map r P w.inv ≫ t.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
apply :
  ∀ (j : J),
    CategoryStruct.comp (Y := t.pt)
          (Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) :
            ((Cone.equivalenceOfReindexing e.symm w').functor.obj s).pt ⟶ t.pt)
          (P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) :
            ((Cone.equivalenceOfReindexing e w).functor.obj t).pt ⟶ s.pt) ≫
        s.π.app j =
      𝟙 s.pt ≫ s.π.app j
⊢ Eq (α := s.pt ⟶ s.pt)
    (CategoryStruct.comp (Y := t.pt)
        (Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) :
          ((Cone.equivalenceOfReindexing e.symm w').functor.obj s).pt ⟶ t.pt)
        (P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) :
          ((Cone.equivalenceOfReindexing e w).functor.obj t).pt ⟶ s.pt) :
      s.pt ⟶ s.pt)
    (𝟙 s.pt : s.pt ⟶ s.pt)

Tactic:
apply hom_ext P

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
dsimp :
  CategoryStruct.comp (Y := t.pt)
        (Q.lift
            ((Cone.postcompose (e.inverse.whiskerLeft w.inv ≫ (e.invFunIdAssoc G).hom)).obj
              (Cone.whisker e.inverse s)) :
          ((Cone.postcompose (e.inverse.whiskerLeft w.inv ≫ (e.invFunIdAssoc G).hom)).obj
                (Cone.whisker e.inverse s)).pt ⟶
            t.pt)
        (P.lift ((Cone.postcompose w.hom).obj (Cone.whisker e.functor t)) :
          ((Cone.postcompose w.hom).obj (Cone.whisker e.functor t)).pt ⟶ s.pt) ≫
      s.π.app j =
    𝟙 s.pt ≫ s.π.app j
⊢ CategoryStruct.comp (Y := t.pt)
        (Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) :
          ((Cone.equivalenceOfReindexing e.symm w').functor.obj s).pt ⟶ t.pt)
        (P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) :
          ((Cone.equivalenceOfReindexing e w).functor.obj t).pt ⟶ s.pt) ≫
      s.π.app j =
    𝟙 s.pt ≫ s.π.app j

Tactic:
dsimp [w']
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
simp :
  s.π.app (e.inverse.obj (e.functor.obj j)) ≫
      w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ G.map (e.counit.app (e.functor.obj j)) ≫ w.hom.app j =
    s.π.app j
⊢ CategoryStruct.comp (Y := t.pt)
        (Q.lift
            ((Cone.postcompose (e.inverse.whiskerLeft w.inv ≫ (e.invFunIdAssoc G).hom)).obj
              (Cone.whisker e.inverse s)) :
          ((Cone.postcompose (e.inverse.whiskerLeft w.inv ≫ (e.invFunIdAssoc G).hom)).obj
                (Cone.whisker e.inverse s)).pt ⟶
            t.pt)
        (P.lift ((Cone.postcompose w.hom).obj (Cone.whisker e.functor t)) :
          ((Cone.postcompose w.hom).obj (Cone.whisker e.functor t)).pt ⟶ s.pt) ≫
      s.π.app j =
    𝟙 s.pt ≫ s.π.app j

Tactic:
simp only [Limits.Cone.whisker_π, Limits.Cone.postcompose_obj_π, fac, whiskerLeft_app,
        assoc, id_comp, invFunIdAssoc_hom_app, fac_assoc, NatTrans.comp_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cone.whisker_π, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Limits.Cone.postcompose_obj_π, CategoryTheory.Equivalence.invFunIdAssoc_hom_app, CategoryTheory.Limits.IsLimit.fac_assoc, CategoryTheory.NatTrans.comp_app, CategoryTheory.Limits.IsLimit.fac, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
rw :
  s.π.app (e.inverse.obj (e.functor.obj j)) ≫
      w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ (e.functor ⋙ G).map (e.unitInv.app j) ≫ w.hom.app j =
    s.π.app j
⊢ s.π.app (e.inverse.obj (e.functor.obj j)) ≫
      w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ G.map (e.counit.app (e.functor.obj j)) ≫ w.hom.app j =
    s.π.app j

Tactic:
rw [counit_app_functor, ← Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_map, CategoryTheory.Equivalence.counit_app_functor
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ w.hom.app j = w.hom.app (obj.{v₁, v₁, u₁, u₁} (𝟭 J) j)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ w.hom.app j = w.hom.app (obj.{v₁, v₁, u₁, u₁} (𝟭 J) j)

Tactic:
have l :
        NatTrans.app w.hom j = NatTrans.app w.hom ((𝟭 J).obj j) := by dsimp