awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : HasPushouts.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsStableUnderCobaseChange
inst_4 : P.HasOfPrecompProperty P
⊢ ObjectProperty.IsClosedUnderColimitsOfShape (C := Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))
    (commaObj (Functor.fromPUnit X) (𝟭 T) P) WalkingSpan

Tactic:
apply Under.closedUnderColimitsOfShape_pushout

Premises used: CategoryTheory.Under.closedUnderColimitsOfShape_pushout
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst_1 : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_2 : HasPushouts.{v_1, u_1} T
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.HasOfPrecompProperty P
inst : HasColimitsOfShape WalkingSpan (Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))
inst₁ :
  ObjectProperty.IsClosedUnderColimitsOfShape (C := Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))
    (commaObj (Functor.fromPUnit X) (𝟭 T) P) WalkingSpan
⊢ HasPushouts (P.Under ⊤ X)

Tactic:
apply +allowSynthFailures hasColimitsOfShape_of_closedUnderColimitsOfShape

Premises used: CategoryTheory.MorphismProperty.Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : HasPushouts.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.ContainsIdentities
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.HasOfPrecompProperty P
inst_6 : HasFiniteWidePushouts.{v_1, u_1} T
⊢ HasFiniteColimits (P.Under ⊤ X)

Tactic:
hasFiniteColimits_of_hasColimits_of_createsFiniteColimits (Under.forget P ⊤ X)

Premises used: CategoryTheory.Limits.hasFiniteColimits_of_hasColimits_of_createsFiniteColimits, CategoryTheory.MorphismProperty.Under.forget, Top.top
-- Module: Mathlib.CategoryTheory.Limits.MorphismProperty
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : HasPushouts.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.ContainsIdentities
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.HasOfPrecompProperty P
⊢ PreservesFiniteColimits (C := P.Under ⊤ X) (Under.forget P ⊤ X)

Tactic:
preservesFiniteColimits_of_preservesInitial_and_pushouts (Under.forget P ⊤ X)

Premises used: CategoryTheory.Limits.preservesFiniteColimits_of_preservesInitial_and_pushouts, CategoryTheory.MorphismProperty.Under.forget, Top.top
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.leftOp
j : Jᵒᵖ
⊢ Quiver.Hom.op (Quiver.Hom.unop (hc.desc (coconeOfConeLeftOp s)) ≫ (coneLeftOpOfCocone c).π.app j) = (s.π.app j).op

Tactic:
simp only [coneLeftOpOfCocone_π_app, op_comp, Quiver.Hom.op_unop, IsColimit.fac,
        coconeOfConeLeftOp_ι_app, op_unop]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.op_comp, Opposite.op_unop, Quiver.Hom.op_unop, CategoryTheory.Limits.coneLeftOpOfCocone_π_app, CategoryTheory.Limits.coconeOfConeLeftOp_ι_app
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.leftOp
m : s.pt ⟶ (coneLeftOpOfCocone c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneLeftOpOfCocone c).π.app j = s.π.app j
⊢ m = Quiver.Hom.unop (hc.desc (coconeOfConeLeftOp s))

Tactic:
Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.leftOp
m : s.pt ⟶ (coneLeftOpOfCocone c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneLeftOpOfCocone c).π.app j = s.π.app j
refine :
  ∀ (j : J),
    (c.ι.app j ≫ m.op).unop =
      Quiver.Hom.unop (c.ι.app j ≫ Quiver.Hom.op (Quiver.Hom.unop (hc.desc (coconeOfConeLeftOp s))))
⊢ m = Quiver.Hom.unop (hc.desc (coconeOfConeLeftOp s))

Tactic:
refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.leftOp
m : s.pt ⟶ (coneLeftOpOfCocone c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneLeftOpOfCocone c).π.app j = s.π.app j
j : J
⊢ (c.ι.app j ≫ m.op).unop =
    Quiver.Hom.unop (c.ι.app j ≫ Quiver.Hom.op (Quiver.Hom.unop (hc.desc (coconeOfConeLeftOp s))))

Tactic:
simpa only [Quiver.Hom.op_unop, IsColimit.fac, coconeOfConeLeftOp_ι_app] using w (op j)

Premises used: CategoryTheory.Limits.IsColimit.fac, Quiver.Hom.op_unop, Opposite.op, CategoryTheory.Limits.coconeOfConeLeftOp_ι_app
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.leftOp
j : Jᵒᵖ
⊢ Quiver.Hom.op ((coconeLeftOpOfCone c).ι.app j ≫ Quiver.Hom.unop (hc.lift (coneOfCoconeLeftOp s))) = (s.ι.app j).op

Tactic:
simp only [coconeLeftOpOfCone_ι_app, op_comp, Quiver.Hom.op_unop, IsLimit.fac,
        coneOfCoconeLeftOp_π_app, op_unop]

Premises used: CategoryTheory.op_comp, Opposite.op_unop, Quiver.Hom.op_unop, CategoryTheory.Limits.coneOfCoconeLeftOp_π_app, CategoryTheory.Limits.coconeLeftOpOfCone_ι_app, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.leftOp
m : (coconeLeftOpOfCone c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeLeftOpOfCone c).ι.app j ≫ m = s.ι.app j
⊢ m = Quiver.Hom.unop (hc.lift (coneOfCoconeLeftOp s))

Tactic:
Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)

Premises used: Quiver.Hom.op_inj, CategoryTheory.Limits.IsLimit.hom_ext, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.leftOp
m : (coconeLeftOpOfCone c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeLeftOpOfCone c).ι.app j ≫ m = s.ι.app j
refine :
  ∀ (j : J),
    Eq (α := unop (F.obj j) ⟶ unop (op s.pt)) (Quiver.Hom.unop (m.op ≫ c.π.app j))
      (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (hc.lift (coneOfCoconeLeftOp s))) ≫ c.π.app j))
⊢ m = Quiver.Hom.unop (hc.lift (coneOfCoconeLeftOp s))

Tactic:
refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)

Premises used: Quiver.Hom.op_inj, CategoryTheory.Limits.IsLimit.hom_ext, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.leftOp
m : (coconeLeftOpOfCone c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeLeftOpOfCone c).ι.app j ≫ m = s.ι.app j
j : J
⊢ Eq (α := unop (F.obj j) ⟶ unop (op s.pt)) (Quiver.Hom.unop (m.op ≫ c.π.app j))
    (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (hc.lift (coneOfCoconeLeftOp s))) ≫ c.π.app j))

Tactic:
simpa only [Quiver.Hom.op_unop, IsLimit.fac, coneOfCoconeLeftOp_π_app] using w (op j)

Premises used: Quiver.Hom.op_unop, CategoryTheory.Limits.coneOfCoconeLeftOp_π_app, Opposite.op, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cocone F
hc : IsColimit c
s : Cone F.rightOp
j : J
⊢ Quiver.Hom.unop (Quiver.Hom.op (hc.desc (coconeOfConeRightOp s)) ≫ (coneRightOpOfCocone c).π.app j) = (s.π.app j).unop

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cocone F
hc : IsColimit c
s : Cone F.rightOp
m : s.pt ⟶ (coneRightOpOfCocone c).pt
w : ∀ (j : J), m ≫ (coneRightOpOfCocone c).π.app j = s.π.app j
⊢ m = Quiver.Hom.op (hc.desc (coconeOfConeRightOp s))

Tactic:
Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cocone F
hc : IsColimit c
s : Cone F.rightOp
m : s.pt ⟶ (coneRightOpOfCocone c).pt
w : ∀ (j : J), m ≫ (coneRightOpOfCocone c).π.app j = s.π.app j
refine :
  ∀ (j : Jᵒᵖ),
    (c.ι.app j ≫ m.unop).op =
      Quiver.Hom.op (c.ι.app j ≫ Quiver.Hom.unop (Quiver.Hom.op (hc.desc (coconeOfConeRightOp s))))
⊢ m = Quiver.Hom.op (hc.desc (coconeOfConeRightOp s))

Tactic:
refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cocone F
hc : IsColimit c
s : Cone F.rightOp
m : s.pt ⟶ (coneRightOpOfCocone c).pt
w : ∀ (j : J), m ≫ (coneRightOpOfCocone c).π.app j = s.π.app j
j : Jᵒᵖ
⊢ (c.ι.app j ≫ m.unop).op =
    Quiver.Hom.op (c.ι.app j ≫ Quiver.Hom.unop (Quiver.Hom.op (hc.desc (coconeOfConeRightOp s))))

Tactic:
simpa only [Quiver.Hom.unop_op, IsColimit.fac] using w (unop j)

Premises used: CategoryTheory.Limits.IsColimit.fac, Quiver.Hom.unop_op, Opposite.unop
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cone F
hc : IsLimit c
s : Cocone F.rightOp
j : J
⊢ Quiver.Hom.unop ((coconeRightOpOfCone c).ι.app j ≫ Quiver.Hom.op (hc.lift (coneOfCoconeRightOp s))) = (s.ι.app j).unop

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cone F
hc : IsLimit c
s : Cocone F.rightOp
m : (coconeRightOpOfCone c).pt ⟶ s.pt
w : ∀ (j : J), (coconeRightOpOfCone c).ι.app j ≫ m = s.ι.app j
⊢ m = Quiver.Hom.op (hc.lift (coneOfCoconeRightOp s))

Tactic:
Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)

Premises used: Quiver.Hom.op_inj, CategoryTheory.Limits.IsLimit.hom_ext, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cone F
hc : IsLimit c
s : Cocone F.rightOp
m : (coconeRightOpOfCone c).pt ⟶ s.pt
w : ∀ (j : J), (coconeRightOpOfCone c).ι.app j ≫ m = s.ι.app j
refine :
  ∀ (j : Jᵒᵖ),
    (m.unop ≫ c.π.app j).op =
      Quiver.Hom.op (Quiver.Hom.unop (Quiver.Hom.op (hc.lift (coneOfCoconeRightOp s))) ≫ c.π.app j)
⊢ m = Quiver.Hom.op (hc.lift (coneOfCoconeRightOp s))

Tactic:
refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cone F
hc : IsLimit c
s : Cocone F.rightOp
m : (coconeRightOpOfCone c).pt ⟶ s.pt
w : ∀ (j : J), (coconeRightOpOfCone c).ι.app j ≫ m = s.ι.app j
j : Jᵒᵖ
⊢ (m.unop ≫ c.π.app j).op =
    Quiver.Hom.op (Quiver.Hom.unop (Quiver.Hom.op (hc.lift (coneOfCoconeRightOp s))) ≫ c.π.app j)

Tactic:
simpa only [Quiver.Hom.unop_op, IsLimit.fac] using w (unop j)

Premises used: Quiver.Hom.unop_op, Opposite.unop, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.unop
j : J
⊢ Quiver.Hom.op (Quiver.Hom.unop (hc.desc (coconeOfConeUnop s)) ≫ (coneUnopOfCocone c).π.app j) = (s.π.app j).op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.unop
m : s.pt ⟶ (coneUnopOfCocone c).pt
w : ∀ (j : J), m ≫ (coneUnopOfCocone c).π.app j = s.π.app j
⊢ m = Quiver.Hom.unop (hc.desc (coconeOfConeUnop s))

Tactic:
Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.unop
m : s.pt ⟶ (coneUnopOfCocone c).pt
w : ∀ (j : J), m ≫ (coneUnopOfCocone c).π.app j = s.π.app j
refine :
  ∀ (j : Jᵒᵖ),
    (c.ι.app j ≫ m.op).unop =
      Quiver.Hom.unop (c.ι.app j ≫ Quiver.Hom.op (Quiver.Hom.unop (hc.desc (coconeOfConeUnop s))))
⊢ m = Quiver.Hom.unop (hc.desc (coconeOfConeUnop s))

Tactic:
refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.unop
m : s.pt ⟶ (coneUnopOfCocone c).pt
w : ∀ (j : J), m ≫ (coneUnopOfCocone c).π.app j = s.π.app j
j : Jᵒᵖ
⊢ (c.ι.app j ≫ m.op).unop = Quiver.Hom.unop (c.ι.app j ≫ Quiver.Hom.op (Quiver.Hom.unop (hc.desc (coconeOfConeUnop s))))

Tactic:
simpa only [Quiver.Hom.op_unop, IsColimit.fac] using w (unop j)

Premises used: CategoryTheory.Limits.IsColimit.fac, Quiver.Hom.op_unop, Opposite.unop
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.unop
j : J
⊢ Quiver.Hom.op ((coconeUnopOfCone c).ι.app j ≫ Quiver.Hom.unop (hc.lift (coneOfCoconeUnop s))) = (s.ι.app j).op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.unop
m : (coconeUnopOfCone c).pt ⟶ s.pt
w : ∀ (j : J), (coconeUnopOfCone c).ι.app j ≫ m = s.ι.app j
⊢ m = Quiver.Hom.unop (hc.lift (coneOfCoconeUnop s))

Tactic:
Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)

Premises used: Quiver.Hom.op_inj, CategoryTheory.Limits.IsLimit.hom_ext, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.unop
m : (coconeUnopOfCone c).pt ⟶ s.pt
w : ∀ (j : J), (coconeUnopOfCone c).ι.app j ≫ m = s.ι.app j
refine :
  ∀ (j : Jᵒᵖ),
    Eq (α := unop (F.obj j) ⟶ unop (op s.pt)) (Quiver.Hom.unop (m.op ≫ c.π.app j))
      (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (hc.lift (coneOfCoconeUnop s))) ≫ c.π.app j))
⊢ m = Quiver.Hom.unop (hc.lift (coneOfCoconeUnop s))

Tactic:
refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)

Premises used: Quiver.Hom.op_inj, CategoryTheory.Limits.IsLimit.hom_ext, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.unop
m : (coconeUnopOfCone c).pt ⟶ s.pt
w : ∀ (j : J), (coconeUnopOfCone c).ι.app j ≫ m = s.ι.app j
j : Jᵒᵖ
⊢ Eq (α := unop (F.obj j) ⟶ unop (op s.pt)) (Quiver.Hom.unop (m.op ≫ c.π.app j))
    (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (hc.lift (coneOfCoconeUnop s))) ≫ c.π.app j))

Tactic:
simpa only [Quiver.Hom.op_unop, IsLimit.fac] using w (unop j)

Premises used: Quiver.Hom.op_unop, Opposite.unop, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cocone F.leftOp
hc : IsColimit c
s : Cone F
j : J
⊢ Quiver.Hom.unop (Quiver.Hom.op (hc.desc (coconeLeftOpOfCone s)) ≫ (coneOfCoconeLeftOp c).π.app j) = (s.π.app j).unop

Tactic:
simp only [coneOfCoconeLeftOp_π_app, unop_comp, Quiver.Hom.unop_op, IsColimit.fac,
        coconeLeftOpOfCone_ι_app, unop_op]

Premises used: CategoryTheory.Limits.IsColimit.fac, Quiver.Hom.unop_op, CategoryTheory.Limits.coneOfCoconeLeftOp_π_app, CategoryTheory.unop_comp, CategoryTheory.Limits.coconeLeftOpOfCone_ι_app, Opposite.unop_op
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cocone F.leftOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeLeftOp c).pt
w : ∀ (j : J), m ≫ (coneOfCoconeLeftOp c).π.app j = s.π.app j
⊢ m = Quiver.Hom.op (hc.desc (coconeLeftOpOfCone s))

Tactic:
Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cocone F.leftOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeLeftOp c).pt
w : ∀ (j : J), m ≫ (coneOfCoconeLeftOp c).π.app j = s.π.app j
refine :
  ∀ (j : Jᵒᵖ),
    (c.ι.app j ≫ m.unop).op =
      Quiver.Hom.op (c.ι.app j ≫ Quiver.Hom.unop (Quiver.Hom.op (hc.desc (coconeLeftOpOfCone s))))
⊢ m = Quiver.Hom.op (hc.desc (coconeLeftOpOfCone s))

Tactic:
refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cocone F.leftOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeLeftOp c).pt
w : ∀ (j : J), m ≫ (coneOfCoconeLeftOp c).π.app j = s.π.app j
j : Jᵒᵖ
⊢ (c.ι.app j ≫ m.unop).op = Quiver.Hom.op (c.ι.app j ≫ Quiver.Hom.unop (Quiver.Hom.op (hc.desc (coconeLeftOpOfCone s))))

Tactic:
simpa only [Quiver.Hom.unop_op, IsColimit.fac, coneOfCoconeLeftOp_π_app] using w (unop j)

Premises used: CategoryTheory.Limits.IsColimit.fac, Quiver.Hom.unop_op, CategoryTheory.Limits.coneOfCoconeLeftOp_π_app, Opposite.unop
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cone F.leftOp
hc : IsLimit c
s : Cocone F
j : J
⊢ Quiver.Hom.unop ((coconeOfConeLeftOp c).ι.app j ≫ Quiver.Hom.op (hc.lift (coneLeftOpOfCocone s))) = (s.ι.app j).unop

Tactic:
simp only [coconeOfConeLeftOp_ι_app, unop_comp, Quiver.Hom.unop_op, IsLimit.fac,
        coneLeftOpOfCocone_π_app, unop_op]

Premises used: Quiver.Hom.unop_op, CategoryTheory.unop_comp, CategoryTheory.Limits.coneLeftOpOfCocone_π_app, Opposite.unop_op, CategoryTheory.Limits.coconeOfConeLeftOp_ι_app, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cone F.leftOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeLeftOp c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfConeLeftOp c).ι.app j ≫ m = s.ι.app j
⊢ m = Quiver.Hom.op (hc.lift (coneLeftOpOfCocone s))

Tactic:
Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)

Premises used: Quiver.Hom.op_inj, CategoryTheory.Limits.IsLimit.hom_ext, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cone F.leftOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeLeftOp c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfConeLeftOp c).ι.app j ≫ m = s.ι.app j
refine :
  ∀ (j : Jᵒᵖ),
    (m.unop ≫ c.π.app j).op =
      Quiver.Hom.op (Quiver.Hom.unop (Quiver.Hom.op (hc.lift (coneLeftOpOfCocone s))) ≫ c.π.app j)
⊢ m = Quiver.Hom.op (hc.lift (coneLeftOpOfCocone s))

Tactic:
refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cone F.leftOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeLeftOp c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfConeLeftOp c).ι.app j ≫ m = s.ι.app j
j : Jᵒᵖ
⊢ (m.unop ≫ c.π.app j).op = Quiver.Hom.op (Quiver.Hom.unop (Quiver.Hom.op (hc.lift (coneLeftOpOfCocone s))) ≫ c.π.app j)

Tactic:
simpa only [Quiver.Hom.unop_op, IsLimit.fac, coconeOfConeLeftOp_ι_app] using w (unop j)

Premises used: Quiver.Hom.unop_op, CategoryTheory.Limits.coconeOfConeLeftOp_ι_app, Opposite.unop, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cocone F.rightOp
hc : IsColimit c
s : Cone F
j : Jᵒᵖ
⊢ Quiver.Hom.op (Quiver.Hom.unop (hc.desc (coconeRightOpOfCone s)) ≫ (coneOfCoconeRightOp c).π.app j) = (s.π.app j).op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cocone F.rightOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeRightOp c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneOfCoconeRightOp c).π.app j = s.π.app j
⊢ m = Quiver.Hom.unop (hc.desc (coconeRightOpOfCone s))

Tactic:
Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cocone F.rightOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeRightOp c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneOfCoconeRightOp c).π.app j = s.π.app j
refine :
  ∀ (j : J),
    (c.ι.app j ≫ m.op).unop =
      Quiver.Hom.unop (c.ι.app j ≫ Quiver.Hom.op (Quiver.Hom.unop (hc.desc (coconeRightOpOfCone s))))
⊢ m = Quiver.Hom.unop (hc.desc (coconeRightOpOfCone s))

Tactic:
refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cocone F.rightOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeRightOp c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneOfCoconeRightOp c).π.app j = s.π.app j
j : J
⊢ (c.ι.app j ≫ m.op).unop =
    Quiver.Hom.unop (c.ι.app j ≫ Quiver.Hom.op (Quiver.Hom.unop (hc.desc (coconeRightOpOfCone s))))

Tactic:
simpa only [Quiver.Hom.op_unop, IsColimit.fac] using w (op j)

Premises used: CategoryTheory.Limits.IsColimit.fac, Quiver.Hom.op_unop, Opposite.op
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cone F.rightOp
hc : IsLimit c
s : Cocone F
j : Jᵒᵖ
⊢ Quiver.Hom.op ((coconeOfConeRightOp c).ι.app j ≫ Quiver.Hom.unop (hc.lift (coneRightOpOfCocone s))) = (s.ι.app j).op

Tactic:
simp