awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_2 : Category.{v', u'} J
J' : Type u''
inst_3 : Category.{v'', u''} J'
inst_4 : ObjectProperty.Small.{w, v_1, u_1} P
inst_5 : LocallySmall.{w, v_1, u_1} C
inst_6 : Small.{w, u'} J
inst_7 : LocallySmall.{w, v', u'} J
⊢ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : P.IsClosedUnderIsomorphisms
h : strictLimitsOfShape.{v', u', v_1, u_1} P J ≤ P
rw : P.isoClosure
| P

Tactic:
rw [← P.isoClosure_eq_self]

Premises used: CategoryTheory.ObjectProperty.isoClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : P.IsClosedUnderIsomorphisms
h : strictLimitsOfShape.{v', u', v_1, u_1} P J ≤ P
conv_rhs : limitsOfShape.{v', u', v_1, u_1} P J ≤ P.isoClosure
⊢ limitsOfShape.{v', u', v_1, u_1} P J ≤ P

Tactic:
conv_rhs => rw [← P.isoClosure_eq_self]

Premises used: CategoryTheory.ObjectProperty.isoClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : P.IsClosedUnderIsomorphisms
h : strictLimitsOfShape.{v', u', v_1, u_1} P J ≤ P
rw : (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure ≤ P.isoClosure
⊢ limitsOfShape.{v', u', v_1, u_1} P J ≤ P.isoClosure

Tactic:
rw [← isoClosure_strictLimitsOfShape]

Premises used: CategoryTheory.ObjectProperty.isoClosure_strictLimitsOfShape
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : P.IsClosedUnderIsomorphisms
h : strictLimitsOfShape.{v', u', v_1, u_1} P J ≤ P
⊢ (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure ≤ P.isoClosure

Tactic:
monotone_isoClosure h

Premises used: CategoryTheory.ObjectProperty.monotone_isoClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : P.IsClosedUnderIsomorphisms
h : strictLimitsOfShape.{v', u', v_1, u_1} P J ≤ P
⊢ (strictLimitsOfShape.{v', u', v_1, u_1} P J).isoClosure ≤ P.isoClosure

Tactic:
exact monotone_isoClosure h

Premises used: CategoryTheory.ObjectProperty.monotone_isoClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_2 : Category.{v', u'} J
J' : Type u''
inst_3 : Category.{v'', u''} J'
inst_4 : Nonempty J
rw rw₁ : LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) ⊥ ⊥
⊢ LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) (limitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥

Tactic:
rw [limitsOfShape_bot]

Premises used: CategoryTheory.ObjectProperty.limitsOfShape_bot
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_2 : Category.{v', u'} J
J' : Type u''
inst_3 : Category.{v'', u''} J'
x : C
h : limitsOfShape.{v', u', v_1, u_1} ⊤ J x
⊢ ⊤ x

Tactic:
trivial
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J
X : C
h : LimitOfShape.{v', u', v_1, u_1} P J X
⊢ P X

Tactic:
P.limitsOfShape_le J _ ⟨h⟩

Premises used: Nonempty.intro, CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.limitsOfShape_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J
F : Functor.{v', v_1, u', u_1} J C
c : Cone F
hc : IsLimit c
hF : ∀ (j : J), P (F.obj j)
⊢ P c.pt

Tactic:
P.limitsOfShape_le J _ ⟨{ diag := _, π := _, isLimit := hc, prop_diag_obj := hF }⟩

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.LimitPresentation.mk, Nonempty.intro, CategoryTheory.ObjectProperty.LimitOfShape.mk, CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.limitsOfShape_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J
F : Functor.{v', v_1, u', u_1} J C
inst_3 : HasLimit F
hF : ∀ (j : J), P (F.obj j)
⊢ P (limit F)

Tactic:
P.prop_of_isLimit (limit.isLimit F) hF

Premises used: CategoryTheory.ObjectProperty.prop_of_isLimit, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u_3
inst_1 : IsClosedUnderLimitsOfShape.{u_3, u_3, v_1, u_1} P (Discrete J)
X : J → C
inst_2 : HasProduct.{u_3, v_1, u_1} X
hF : ∀ (j : J), P (X j)
⊢ P (piObj.{u_3, v_1, u_1} X)

Tactic:
P.prop_of_isLimit (productIsProduct X) (fun _ ↦ hF _)

Premises used: CategoryTheory.ObjectProperty.prop_of_isLimit, CategoryTheory.Limits.productIsProduct, CategoryTheory.Limits.limit, CategoryTheory.Discrete.as
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
J' : Type u''
inst_2 : Category.{v'', u''} J'
G : Functor.{v', v'', u', u''} J J'
inst_3 : G.Initial
⊢ limitsOfShape.{v'', u'', v_1, u_1} P J' ≤ limitsOfShape.{v', u', v_1, u_1} P J

Tactic:
fun _h ⟨h⟩ ↦ ⟨h.reindex G⟩

Premises used: CategoryTheory.ObjectProperty.LimitOfShape.reindex, Nonempty.intro, _private.0.CategoryTheory.ObjectProperty.isoClosure_strictLimitsOfShape.match_1, CategoryTheory.ObjectProperty.limitsOfShape
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
J' : Type u''
inst_2 : Category.{v'', u''} J'
e : Equivalence.{v', v'', u', u''} J J'
⊢ limitsOfShape.{v', u', v_1, u_1} P J = limitsOfShape.{v'', u'', v_1, u_1} P J'

Tactic:
le_antisymm (P.limitsOfShape_le_of_initial e.inverse)
    (P.limitsOfShape_le_of_initial e.functor)

Premises used: CategoryTheory.Equivalence.functor, le_antisymm, CategoryTheory.ObjectProperty.limitsOfShape_le_of_initial, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
J' : Type u''
inst_2 : Category.{v'', u''} J'
e : Equivalence.{v', v'', u', u''} J J'
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J ↔ IsClosedUnderLimitsOfShape.{v'', u'', v_1, u_1} P J'

Tactic:
simp only [isClosedUnderLimitsOfShape_iff, P.limitsOfShape_congr e]

Premises used: CategoryTheory.ObjectProperty.limitsOfShape_congr, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
J' : Type u''
inst_2 : Category.{v'', u''} J'
e : Equivalence.{v', v'', u', u''} J J'
inst_3 rwa rwa₁ rwa₂ rwa₃ : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J
⊢ IsClosedUnderLimitsOfShape.{v'', u'', v_1, u_1} P J'

Tactic:
rwa [← P.isClosedUnderLimitsOfShape_iff_of_equivalence e]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff_of_equivalence
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P_1 : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_2 : Category.{v', u'} J
J' : Type u''
inst_3 : Category.{v'', u''} J'
P : ObjectProperty.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : IsClosedUnderLimitsOfShape.{v', u', v_2, u_2} P J
inst_5 : PreservesLimitsOfShape.{v', u', v_1, v_2, u_1, u_2} J F
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} (P.inverseImage F) J

Tactic:
⟨fun _ ⟨c, H⟩ ↦ ObjectProperty.LimitOfShape.prop (P := P) ⟨c.map F, H⟩⟩

Premises used: CategoryTheory.Limits.LimitPresentation.map, _private.0.CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.inverseImage.match_1, CategoryTheory.ObjectProperty.LimitOfShape.mk, CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.mk, CategoryTheory.ObjectProperty.LimitOfShape.prop, CategoryTheory.ObjectProperty.inverseImage
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : Type u'
inst_2 : Category.{v', u'} J
P : ObjectProperty.{v_2, u_2} D
inst_3 : P.IsClosedUnderIsomorphisms
e : Equivalence.{v_1, v_2, u_1, u_2} C D
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J ↔
    IsClosedUnderLimitsOfShape.{v', u', v_2, u_2} P J

Tactic:
⟨fun H ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : Type u'
inst_2 : Category.{v', u'} J
P : ObjectProperty.{v_2, u_2} D
inst_3 : P.IsClosedUnderIsomorphisms
e : Equivalence.{v_1, v_2, u_1, u_2} C D
refine :
  ∀ (H : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J),
    IsClosedUnderLimitsOfShape.{v', u', v_2, u_2} P J
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J ↔
    IsClosedUnderLimitsOfShape.{v', u', v_2, u_2} P J

Tactic:
refine ⟨fun H ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : Type u'
inst_2 : Category.{v', u'} J
P : ObjectProperty.{v_2, u_2} D
inst_3 : P.IsClosedUnderIsomorphisms
e : Equivalence.{v_1, v_2, u_1, u_2} C D
H : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J
⊢ IsClosedUnderLimitsOfShape.{v', u', v_2, u_2} ((P.inverseImage e.functor).inverseImage e.inverse) J

Tactic:
(inferInstance :
      ((P.inverseImage e.functor).inverseImage e.inverse).IsClosedUnderLimitsOfShape J)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : Type u'
inst_2 : Category.{v', u'} J
P : ObjectProperty.{v_2, u_2} D
inst_3 : P.IsClosedUnderIsomorphisms
e : Equivalence.{v_1, v_2, u_1, u_2} C D
H : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J
h : P = (P.inverseImage e.functor).inverseImage e.inverse
⊢ IsClosedUnderLimitsOfShape.{v', u', v_2, u_2} P J

Tactic:
convert!
    (inferInstance :
      ((P.inverseImage e.functor).inverseImage e.inverse).IsClosedUnderLimitsOfShape J)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : Type u'
inst_2 : Category.{v', u'} J
P : ObjectProperty.{v_2, u_2} D
inst_3 : P.IsClosedUnderIsomorphisms
e : Equivalence.{v_1, v_2, u_1, u_2} C D
H : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J
h : ∀ (X : D), P X ↔ (P.inverseImage e.functor).inverseImage e.inverse X
⊢ P = (P.inverseImage e.functor).inverseImage e.inverse

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : Type u'
inst_2 : Category.{v', u'} J
P : ObjectProperty.{v_2, u_2} D
inst_3 : P.IsClosedUnderIsomorphisms
e : Equivalence.{v_1, v_2, u_1, u_2} C D
H : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J
X : D
⊢ P X ↔ (P.inverseImage e.functor).inverseImage e.inverse X

Tactic:
simpa using P.prop_iff_of_iso (e.counitIso.app X).symm

Premises used: CategoryTheory.ObjectProperty.prop_iff_of_iso, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
⊢ W.isLocal Z ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.MorphismProperty.isLocal
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X : C
⊢ W.isColocal X ↔ ∀ ⦃Y Z : C⦄ (g : Y ⟶ Z), W g → Function.Bijective (β := X ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g

Tactic:
Iff.rfl

Premises used: CategoryTheory.MorphismProperty.isColocal, Iff.rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
Z Z' : C
e : Z ≅ Z'
hZ : W.isLocal Z
X Y : C
f : X ⟶ Y
hf : W f
rw : Function.Bijective (α := Y ⟶ Z) (β := X ⟶ Z') ((fun (g : Y ⟶ Z') ↦ f ≫ g) ∘ (⇑e.homToEquiv : (a : Y ⟶ Z) → Y ⟶ Z'))
⊢ Function.Bijective (β := X ⟶ Z') fun (g : Y ⟶ Z') ↦ f ≫ g

Tactic:
rw [← Function.Bijective.of_comp_iff _ (Iso.homToEquiv e).bijective]

Premises used: CategoryTheory.Iso.homToEquiv, Equiv.bijective, Function.Bijective.of_comp_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
Z Z' : C
e : Z ≅ Z'
hZ : W.isLocal Z
X Y : C
f : X ⟶ Y
hf : W f
⊢ Function.Bijective (α := Y ⟶ Z) (β := X ⟶ Z')
    (Function.comp (β := X ⟶ Z) (⇑e.homToEquiv : (a : X ⟶ Z) → X ⟶ Z') fun (g : Y ⟶ Z) ↦ f ≫ g)

Tactic:
(Iso.homToEquiv e).bijective.comp (hZ f hf)

Premises used: CategoryTheory.Iso.homToEquiv, Equiv.bijective, Function.Bijective.comp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
Z Z' : C
e : Z ≅ Z'
hZ : W.isLocal Z
X Y : C
f : X ⟶ Y
hf : W f
h :
  Eq (α := (Y ⟶ Z) → (X ⟶ Z')) ((fun (g : Y ⟶ Z') ↦ f ≫ g) ∘ (⇑e.homToEquiv : (a : Y ⟶ Z) → Y ⟶ Z'))
    (Function.comp (β := X ⟶ Z) (⇑e.homToEquiv : (a : X ⟶ Z) → X ⟶ Z') fun (g : Y ⟶ Z) ↦ f ≫ g)
⊢ Function.Bijective (α := Y ⟶ Z) (β := X ⟶ Z') ((fun (g : Y ⟶ Z') ↦ f ≫ g) ∘ (⇑e.homToEquiv : (a : Y ⟶ Z) → Y ⟶ Z'))

Tactic:
convert! (Iso.homToEquiv e).bijective.comp (hZ f hf) using 1

Premises used: CategoryTheory.Iso.homToEquiv, Equiv.bijective, Function.Bijective.comp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
Z Z' : C
e : Z ≅ Z'
hZ : W.isLocal Z
X Y : C
f : X ⟶ Y
hf : W f
⊢ Eq (α := (Y ⟶ Z) → (X ⟶ Z')) ((fun (g : Y ⟶ Z') ↦ f ≫ g) ∘ (⇑e.homToEquiv : (a : Y ⟶ Z) → Y ⟶ Z'))
    (Function.comp (β := X ⟶ Z) (⇑e.homToEquiv : (a : X ⟶ Z) → X ⟶ Z') fun (g : Y ⟶ Z) ↦ f ≫ g)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
X X' : C
e : X ≅ X'
hX : W.isColocal X
Y Z : C
g : Y ⟶ Z
hg : W g
rw :
  Function.Bijective (α := X ⟶ Y) (β := X' ⟶ Z) ((fun (f : X' ⟶ Y) ↦ f ≫ g) ∘ (⇑e.homFromEquiv : (a : X ⟶ Y) → X' ⟶ Y))
⊢ Function.Bijective (β := X' ⟶ Z) fun (f : X' ⟶ Y) ↦ f ≫ g

Tactic:
rw [← Function.Bijective.of_comp_iff _ (Iso.homFromEquiv e).bijective]

Premises used: Equiv.bijective, Function.Bijective.of_comp_iff, CategoryTheory.Iso.homFromEquiv
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
X X' : C
e : X ≅ X'
hX : W.isColocal X
Y Z : C
g : Y ⟶ Z
hg : W g
⊢ Function.Bijective (α := X ⟶ Y) (β := X' ⟶ Z)
    (Function.comp (β := X ⟶ Z) (⇑e.homFromEquiv : (a : X ⟶ Z) → X' ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g)

Tactic:
(Iso.homFromEquiv e).bijective.comp (hX g hg)

Premises used: Equiv.bijective, Function.Bijective.comp, CategoryTheory.Iso.homFromEquiv
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
X X' : C
e : X ≅ X'
hX : W.isColocal X
Y Z : C
g : Y ⟶ Z
hg : W g
h :
  Eq (α := (X ⟶ Y) → (X' ⟶ Z)) ((fun (f : X' ⟶ Y) ↦ f ≫ g) ∘ (⇑e.homFromEquiv : (a : X ⟶ Y) → X' ⟶ Y))
    (Function.comp (β := X ⟶ Z) (⇑e.homFromEquiv : (a : X ⟶ Z) → X' ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g)
⊢ Function.Bijective (α := X ⟶ Y) (β := X' ⟶ Z) ((fun (f : X' ⟶ Y) ↦ f ≫ g) ∘ (⇑e.homFromEquiv : (a : X ⟶ Y) → X' ⟶ Y))

Tactic:
convert! (Iso.homFromEquiv e).bijective.comp (hX g hg) using 1

Premises used: Equiv.bijective, Function.Bijective.comp, CategoryTheory.Iso.homFromEquiv
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
X X' : C
e : X ≅ X'
hX : W.isColocal X
Y Z : C
g : Y ⟶ Z
hg : W g
⊢ Eq (α := (X ⟶ Y) → (X' ⟶ Z)) ((fun (f : X' ⟶ Y) ↦ f ≫ g) ∘ (⇑e.homFromEquiv : (a : X ⟶ Y) → X' ⟶ Y))
    (Function.comp (β := X ⟶ Z) (⇑e.homFromEquiv : (a : X ⟶ Z) → X' ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
Z : C
h_1 : ObjectProperty.limitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.LimitOfShape.{v', u', v, u} W.isLocal J Z
g₁ g₂ : Y ⟶ Z
h : Eq.{v + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)
j : J
⊢ Eq.{v + 1} (α := X ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj j)
    ((fun (g : Y ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj j) ↦ f ≫ g)
      (g₁ ≫ { pt := Z, π := p.toLimitPresentation (P := W.isLocal).π }.π.app j))
    ((fun (g : Y ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj j) ↦ f ≫ g)
      (g₂ ≫ { pt := Z, π := p.toLimitPresentation (P := W.isLocal).π }.π.app j))

Tactic:
simp [reassoc_of% h]
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
Z : C
h : ObjectProperty.limitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.LimitOfShape.{v', u', v, u} W.isLocal J Z
refine : ∀ (g : X ⟶ Z), ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g

Tactic:
refine ⟨fun g₁ g₂ h ↦ p.isLimit.hom_ext
      (fun j ↦ (p.prop_diag_obj j f hf).1 (by simp [reassoc_of% h])), fun g ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
Z : C
h : ObjectProperty.limitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.LimitOfShape.{v', u', v, u} W.isLocal J Z
g : X ⟶ Z
choose :
  ∀ (app : (j : J) → Y ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj j)
    (h :
      ∀ (j : J),
        (fun (g : Y ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj j) ↦ f ≫ g) (app j) =
          g ≫ p.toLimitPresentation (P := W.isLocal).π.app j),
    ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
⊢ ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g

Tactic:
choose app h using fun j ↦ (p.prop_diag_obj j f hf).2 (g ≫ p.π.app j)

Premises used: CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj, CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, And.right, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.LimitPresentation.π, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
Z : C
h_1 : ObjectProperty.limitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.LimitOfShape.{v', u', v, u} W.isLocal J Z
g : X ⟶ Z
app : (j : J) → Y ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj j
h :
  ∀ (j : J),
    (fun (g : Y ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj j) ↦ f ≫ g) (app j) =
      g ≫ p.toLimitPresentation (P := W.isLocal).π.app j
x x_1 : J
a : x ⟶ x_1
⊢ Eq.{v + 1} (α := X ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj x_1)
    ((fun (g : Y ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj x_1) ↦ f ≫ g)
      (Functor.map (Functor.obj (Functor.const J) Y) a ≫ app x_1))
    ((fun (g : Y ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj x_1) ↦ f ≫ g)
      (app x ≫ p.toLimitPresentation (P := W.isLocal).diag.map a))

Tactic:
simp [reassoc_of% h, h, p.w a]

Premises used: CategoryTheory.Limits.LimitPresentation.w, CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
Z : C
h_1 : ObjectProperty.limitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.LimitOfShape.{v', u', v, u} W.isLocal J Z
g : X ⟶ Z
app : (j : J) → Y ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj j
h :
  ∀ (j : J),
    (fun (g : Y ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj j) ↦ f ≫ g) (app j) =
      g ≫ p.toLimitPresentation (P := W.isLocal).π.app j
j : J
⊢ (fun (g : Y ⟶ Z) ↦ f ≫ g)
        (p.toLimitPresentation (P := W.isLocal).isLimit.lift { pt := Y, π := { app := app, naturality := ⋯ } }) ≫
      { pt := Z, π := p.toLimitPresentation (P := W.isLocal).π :
              Cone p.toLimitPresentation (P := W.isLocal).diag }.π.app
        j =
    g ≫
      { pt := Z, π := p.toLimitPresentation (P := W.isLocal).π :
              Cone p.toLimitPresentation (P := W.isLocal).diag }.π.app
        j

Tactic:
simp [p.isLimit.fac, h]

Premises used: CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, CategoryTheory.Limits.LimitPresentation.isLimit, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
Z : C
h_1 : ObjectProperty.limitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.LimitOfShape.{v', u', v, u} W.isLocal J Z
g : X ⟶ Z
app : (j : J) → Y ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj j
h :
  ∀ (j : J),
    (fun (g : Y ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj j) ↦ f ≫ g) (app j) =
      g ≫ p.toLimitPresentation (P := W.isLocal).π.app j
⊢ ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g

Tactic:
exact ⟨p.isLimit.lift (Cone.mk _
      { app := app
        naturality _ _ a := (p.prop_diag_obj _ f hf).1
          (by simp [reassoc_of% h, h, p.w a]) }),
      p.isLimit.hom_ext (fun j ↦ by simp [p.isLimit.fac, h])⟩