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_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
l : w.hom.app j = w.hom.app (obj.{v₁, v₁, u₁, u₁} (𝟭 J) j)
rw :
  s.π.app (e.inverse.obj (e.functor.obj j)) ≫
      w.inv.app (e.inverse.obj (e.functor.obj j)) ≫
        w.hom.app ((e.functor ⋙ e.inverse).obj j) ≫ F.map (e.unitInv.app j) =
    s.π.app j
⊢ 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

Tactic:
rw [l, w.hom.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- 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
l : w.hom.app j = w.hom.app (obj.{v₁, v₁, u₁, u₁} (𝟭 J) j)
⊢ s.π.app (e.inverse.obj (e.functor.obj j)) ≫
      w.inv.app (e.inverse.obj (e.functor.obj j)) ≫
        w.hom.app ((e.functor ⋙ e.inverse).obj j) ≫ F.map (e.unitInv.app j) =
    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 : 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 : K),
    CategoryStruct.comp (Y := s.pt)
          (P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) :
            ((Cone.equivalenceOfReindexing e w).functor.obj t).pt ⟶ s.pt)
          (Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) :
            ((Cone.equivalenceOfReindexing e.symm w').functor.obj s).pt ⟶ t.pt) ≫
        t.π.app j =
      𝟙 t.pt ≫ t.π.app j
⊢ Eq (α := t.pt ⟶ t.pt)
    (CategoryStruct.comp (Y := s.pt)
        (P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) :
          ((Cone.equivalenceOfReindexing e w).functor.obj t).pt ⟶ s.pt)
        (Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) :
          ((Cone.equivalenceOfReindexing e.symm w').functor.obj s).pt ⟶ t.pt) :
      t.pt ⟶ t.pt)
    (𝟙 t.pt : t.pt ⟶ t.pt)

Tactic:
apply hom_ext Q

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 : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
h : IsLimit t
W : C
f : W ⟶ t.pt
⊢ ∀ (j : J),
    (fun (π : obj (const J) W ⟶ F) ↦ (h.lift { pt := W, π := π } : { pt := W, π := π : Cone F }.pt ⟶ t.pt))
          ((fun (f : W ⟶ t.pt) ↦ (t.extend f).π) f) ≫
        t.π.app j =
      f ≫ 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
t : Cone F
h : IsLimit t
W : C
f : obj (const J) W ⟶ F
j : J
⊢ (Equiv.symm h.homEquiv : (a : (const J).obj W ⟶ F) → W ⟶ t.pt) f ≫ t.π.app j = f.app j

Tactic:
simp [homEquiv]

Premises used: CategoryTheory.Limits.IsLimit.homEquiv
-- 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 W' : C
f : obj (const J) W ⟶ F
g : W' ⟶ W
⊢ Eq (α := obj (const J) W' ⟶ F)
    ((h.homEquiv : (a : W' ⟶ t.pt) → (const J).obj W' ⟶ F)
        ((Equiv.symm h.homEquiv : (a : (const J).obj W' ⟶ F) → W' ⟶ t.pt) (Functor.map (const J) g ≫ f)) :
      obj (const J) W' ⟶ F)
    ((h.homEquiv : (a : W' ⟶ t.pt) → (const J).obj W' ⟶ F)
        (g ≫ (Equiv.symm h.homEquiv : (a : (const J).obj W ⟶ F) → W ⟶ t.pt) f) :
      obj (const J) W' ⟶ F)

Tactic:
aesop
-- 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
⊢ (h.homIso W).hom = ↾fun (f : ULift.{u₁, v₃} (W ⟶ t.pt)) ↦ (t.extend f.down).π

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, 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
t : Cone F
h : IsLimit t
⊢ obj yoneda t.pt ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones

Tactic:
refine NatIso.ofComponents (fun W => IsLimit.homIso h (unop W))

Premises used: CategoryTheory.NatIso.ofComponents
-- 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
h : IsLimit t
W : C
π : obj (const J) W ⟶ F
j j' : J
f : j ⟶ j'
⊢ π.app j ≫ F.map f = Functor.map (obj (const J) W) f ≫ π.app j'

Tactic:
(π.naturality f).symm

Premises used: CategoryTheory.NatTrans.naturality, Eq.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
t : Cone F
h : IsLimit t
W : C
π : obj (const J) W ⟶ F
j j' : J
f : j ⟶ j'
h₁ :
  (obj.{v₁, v₃, u₁, u₃} (obj (const J) W) j ⟶ F.obj j') = (W ⟶ F.obj j') →
    Functor.map (obj (const J) W) f ≫ π.app j' = (fun (j : J) ↦ π.app j) j'
⊢ Eq (α := W ⟶ F.obj j') ((fun (j : J) ↦ π.app j) j ≫ F.map f) ((fun (j : J) ↦ π.app j) j')

Tactic:
convert! ← (π.naturality f).symm

Premises used: CategoryTheory.NatTrans.naturality, Eq.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
t : Cone F
h : IsLimit t
W : C
π : obj (const J) W ⟶ F
j j' : J
f : j ⟶ j'
e_1 : (obj.{v₁, v₃, u₁, u₃} (obj (const J) W) j ⟶ F.obj j') = (W ⟶ F.obj j')
⊢ Functor.map (obj (const J) W) f ≫ π.app j' = (fun (j : J) ↦ π.app j) j'

Tactic:
apply id_comp

Premises used: 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 : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
h : IsLimit t
W : C
p : { p : (j : J) → W ⟶ F.obj j // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' }
j j' : J
f : j ⟶ j'
dsimp : 𝟙 W ≫ (↑p : (j : J) → W ⟶ F.obj j) j' = (↑p : (j : J) → W ⟶ F.obj j) j ≫ F.map f
⊢ Functor.map (obj (const J) W) f ≫ (↑p : (j : J) → W ⟶ F.obj j) j' = (↑p : (j : J) → W ⟶ F.obj j) j ≫ F.map f

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 : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
h : IsLimit t
W : C
p : { p : (j : J) → W ⟶ F.obj j // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' }
j j' : J
f : j ⟶ j'
rw : (↑p : (j : J) → W ⟶ F.obj j) j' = (↑p : (j : J) → W ⟶ F.obj j) j ≫ F.map f
⊢ 𝟙 W ≫ (↑p : (j : J) → W ⟶ F.obj j) j' = (↑p : (j : J) → W ⟶ F.obj j) j ≫ F.map f

Tactic:
rw [id_comp]

Premises used: 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 : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
h : IsLimit t
W : C
p : { p : (j : J) → W ⟶ F.obj j // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' }
j j' : J
f : j ⟶ j'
⊢ (↑p : (j : J) → W ⟶ F.obj j) j' = (↑p : (j : J) → W ⟶ F.obj j) j ≫ F.map f

Tactic:
(p.2 f).symm

Premises used: Eq.symm, Subtype.property
-- 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
h : IsLimit t
W : C
p : { p : (j : J) → W ⟶ F.obj j // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' }
j j' : J
f : j ⟶ j'
⊢ (↑p : (j : J) → W ⟶ F.obj j) j' = (↑p : (j : J) → W ⟶ F.obj j) j ≫ F.map f

Tactic:
exact (p.2 f).symm

Premises used: Eq.symm, Subtype.property
-- 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_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
j : J
a : G.map (lift s ≫ t.π.app j) = G.map (s.π.app j)
⊢ lift s ≫ t.π.app j = s.π.app j

Tactic:
apply G.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- 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_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
j : J
a : ht.lift (G.mapCone s) ≫ G.map (t.π.app j) = G.map (s.π.app j)
⊢ G.map (lift s ≫ t.π.app j) = G.map (s.π.app j)

Tactic:
rw [G.map_comp, h]

Premises used: CategoryTheory.Functor.map_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 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
j : J
⊢ ht.lift (G.mapCone s) ≫ G.map (t.π.app j) = G.map (s.π.app j)

Tactic:
apply ht.fac

Premises used: 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_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
a : G.map m = G.map (lift s)
⊢ m = lift s

Tactic:
apply G.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- 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_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
a : G.map m = ht.lift (G.mapCone s)
⊢ G.map m = G.map (lift s)

Tactic:
rw [h]
-- 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_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ G.map m = ht.lift (G.mapCone s)

Tactic:
ht.uniq (mapCone G s) _ fun j => ?_

Premises used: CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Functor.mapCone
-- 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_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
a : ∀ (j : J), G.map m ≫ (G.mapCone t).π.app j = (G.mapCone s).π.app j
⊢ G.map m = ht.lift (G.mapCone s)

Tactic:
refine ht.uniq (mapCone G s) _ fun j => ?_

Premises used: CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Functor.mapCone
-- 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_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
j : J
⊢ Eq.{v₄ + 1} (α := G.obj s.pt ⟶ G.obj (F.obj j)) ((fun (f : s.pt ⟶ F.obj j) ↦ G.map f) (m ≫ t.π.app j))
    ((fun (f : s.pt ⟶ F.obj j) ↦ G.map f) (s.π.app j))

Tactic:
congrArg (fun f => G.map f) (w j)

Premises used: congrArg, CategoryTheory.Functor.map
-- 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_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
j : J
h₁ :
  (G.obj s.pt ⟶ G.obj (F.obj j)) = ((G.mapCone s).pt ⟶ (F ⋙ G).obj j) →
    G.map (m ≫ t.π.app j) = G.map m ≫ (G.mapCone t).π.app j
⊢ G.map m ≫ (G.mapCone t).π.app j = (G.mapCone s).π.app j

Tactic:
convert! ← congrArg (fun f => G.map f) (w j)

Premises used: congrArg, CategoryTheory.Functor.map
-- 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_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
j : J
e_1 : (G.obj s.pt ⟶ G.obj (F.obj j)) = ((G.mapCone s).pt ⟶ (F ⋙ G).obj j)
⊢ G.map (m ≫ t.π.app j) = G.map m ≫ (G.mapCone t).π.app j

Tactic:
apply G.map_comp

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K_1 : Type u₂
inst_1 : Category.{v₂, u₂} K_1
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
D : Type u₄
inst_3 : Category.{v₄, u₄} D
K : Functor.{v₁, v₃, u₁, u₃} J C
F G : Functor.{v₃, v₄, u₃, u₄} C D
h : F ≅ G
c : Cone K
t : IsLimit (F.mapCone c)
apply : IsLimit ((Cone.postcompose (K.isoWhiskerLeft h).inv).obj (G.mapCone c))
⊢ IsLimit (G.mapCone c)

Tactic:
apply postcomposeInvEquiv (isoWhiskerLeft K h :) (mapCone G c) _

Premises used: CategoryTheory.Limits.IsLimit.postcomposeInvEquiv, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Functor.mapCone, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K_1 : Type u₂
inst_1 : Category.{v₂, u₂} K_1
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
D : Type u₄
inst_3 : Category.{v₄, u₄} D
K : Functor.{v₁, v₃, u₁, u₃} J C
F G : Functor.{v₃, v₄, u₃, u₄} C D
h : F ≅ G
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit ((Cone.postcompose (K.isoWhiskerLeft h).inv).obj (G.mapCone c))

Tactic:
apply t.ofIsoLimit (postcomposeWhiskerLeftMapCone h.symm c).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.Functor.postcomposeWhiskerLeftMapCone
-- 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
X : C
h : F.cones.RepresentableBy X
s : Cone F
dsimp :
  { pt := s.pt,
      π :=
        (h.homEquiv : (a : s.pt ⟶ X) → (const J).obj s.pt ⟶ F)
          ((Equiv.symm h.homEquiv : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ X) s.π) } =
    s
⊢ coneOfHom h (homOfCone h s) = s

Tactic:
dsimp [coneOfHom, homOfCone]

Premises used: CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom, CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone
-- 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
X : C
h : F.cones.RepresentableBy X
s : Cone F
s_pt : C
s_π : obj (const J) s_pt ⟶ F
e_π :
  (h.homEquiv : (a : { pt := s_pt, π := s_π }.pt ⟶ X) → (const J).obj { pt := s_pt, π := s_π }.pt ⟶ F)
      ((Equiv.symm h.homEquiv : (a : (const J).obj { pt := s_pt, π := s_π }.pt ⟶ F) → { pt := s_pt, π := s_π }.pt ⟶ X)
        { pt := s_pt, π := s_π }.π) =
    s_π
⊢ { pt := { pt := s_pt, π := s_π : Cone F }.pt,
      π :=
        (h.homEquiv : (a : { pt := s_pt, π := s_π }.pt ⟶ X) → (const J).obj { pt := s_pt, π := s_π }.pt ⟶ F)
          ((Equiv.symm h.homEquiv :
              (a : (const J).obj { pt := s_pt, π := s_π }.pt ⟶ F) → { pt := s_pt, π := s_π }.pt ⟶ X)
            { pt := s_pt, π := s_π }.π) } =
    { pt := s_pt, π := s_π : Cone 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
X : C
h : F.cones.RepresentableBy X
s : Cone F
s_pt : C
s_π : obj (const J) s_pt ⟶ F
⊢ (h.homEquiv : (a : { pt := s_pt, π := s_π }.pt ⟶ X) → (const J).obj { pt := s_pt, π := s_π }.pt ⟶ F)
      ((Equiv.symm h.homEquiv : (a : (const J).obj { pt := s_pt, π := s_π }.pt ⟶ F) → { pt := s_pt, π := s_π }.pt ⟶ X)
        { pt := s_pt, π := s_π }.π) =
    s_π

Tactic:
h.homEquiv.apply_symm_apply s_π

Premises used: Equiv.apply_symm_apply, CategoryTheory.Functor.RepresentableBy.homEquiv
-- 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
X : C
h : F.cones.RepresentableBy X
s : Cone F
s_pt : C
s_π : obj (const J) s_pt ⟶ F
⊢ (h.homEquiv : (a : { pt := s_pt, π := s_π }.pt ⟶ X) → (const J).obj { pt := s_pt, π := s_π }.pt ⟶ F)
      ((Equiv.symm h.homEquiv : (a : (const J).obj { pt := s_pt, π := s_π }.pt ⟶ F) → { pt := s_pt, π := s_π }.pt ⟶ X)
        { pt := s_pt, π := s_π }.π) =
    s_π

Tactic:
exact h.homEquiv.apply_symm_apply s_π

Premises used: Equiv.apply_symm_apply, CategoryTheory.Functor.RepresentableBy.homEquiv
-- 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
X : C
h : F.cones.RepresentableBy X
s : Cone F
⊢ { pt := s.pt,
      π :=
        (h.homEquiv : (a : s.pt ⟶ X) → (const J).obj s.pt ⟶ F)
          ((Equiv.symm h.homEquiv : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ X) s.π) } =
    s

Tactic:
match s with
  | .mk s_pt s_π =>
    congr
    exact h.homEquiv.apply_symm_apply s_π
-- 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
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
⊢ homOfCone h (coneOfHom h f) = f

Tactic:
simp [coneOfHom, homOfCone]

Premises used: CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom, CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone
-- 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
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
dsimp :
  Eq (α := Cone F) { pt := Y, π := (h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) f }
    { pt := Y, π := Functor.map (const J) f ≫ (h.homEquiv : (a : X ⟶ X) → (const J).obj X ⟶ F) (𝟙 X) }
⊢ coneOfHom h f = (limitCone h).extend (X := Y) f

Tactic:
dsimp [coneOfHom, limitCone, Cone.extend]

Premises used: CategoryTheory.Limits.Cone.extend, CategoryTheory.Limits.IsLimit.OfNatIso.limitCone, CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom
-- 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
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
e_π :
  Eq (α := obj (const J) Y ⟶ F) ((h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) f : obj (const J) Y ⟶ F)
    (Functor.map (const J) f ≫ (h.homEquiv : (a : X ⟶ X) → (const J).obj X ⟶ F) (𝟙 X) : obj (const J) Y ⟶ F)
⊢ Eq (α := Cone F) { pt := Y, π := (h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) f }
    { pt := Y, π := Functor.map (const J) f ≫ (h.homEquiv : (a : X ⟶ X) → (const J).obj X ⟶ F) (𝟙 X) }

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
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
rw : ((h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) (f ≫ 𝟙 X) : obj (const J) Y ⟶ F)
| ((h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) f : obj (const J) Y ⟶ F)

Tactic:
rw [← Category.comp_id f]

Premises used: CategoryTheory.Category.comp_id
-- 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
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
e_π :
  Eq (α := obj (const J) Y ⟶ F) ((h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) (f ≫ 𝟙 X) : obj (const J) Y ⟶ F)
    (Functor.map (const J) f ≫ (h.homEquiv : (a : X ⟶ X) → (const J).obj X ⟶ F) (𝟙 X) : obj (const J) Y ⟶ F)
⊢ Eq (α := obj (const J) Y ⟶ F) ((h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) f : obj (const J) Y ⟶ F)
    (Functor.map (const J) f ≫ (h.homEquiv : (a : X ⟶ X) → (const J).obj X ⟶ F) (𝟙 X) : obj (const J) Y ⟶ F)

Tactic:
conv_lhs => rw [← Category.comp_id f]

Premises used: CategoryTheory.Category.comp_id
-- 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
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
⊢ Eq (α := obj (const J) Y ⟶ F) ((h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) (f ≫ 𝟙 X) : obj (const J) Y ⟶ F)
    (Functor.map (const J) f ≫ (h.homEquiv : (a : X ⟶ X) → (const J).obj X ⟶ F) (𝟙 X) : obj (const J) Y ⟶ F)

Tactic:
h.homEquiv_comp f (𝟙 X)

Premises used: CategoryTheory.NatTrans.vcomp, Quiver.Hom.unop, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.RepresentableBy.homEquiv_comp