awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
inst_3 : P.IsClosedUnderIsomorphisms
inst_4 : P.IsStableUnderShift A
X Y : C
a : A
i : X ≅ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y
hY : P Y
⊢ P X

Tactic:
P.prop_of_iso i.symm (P.le_shift a Y hY)

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.Iso.symm, CategoryTheory.ObjectProperty.le_shift
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
inst_3 : P.IsClosedUnderIsomorphisms
inst_4 : P.IsStableUnderShift A
X Y : C
a : A
i : X ≅ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y
hY : P Y
⊢ P X

Tactic:
exact P.prop_of_iso i.symm (P.le_shift a Y hY)

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.Iso.symm, CategoryTheory.ObjectProperty.le_shift
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (shiftClosure ⊥ A) ⊥

Tactic:
shiftClosure_eq_self _

Premises used: CategoryTheory.ObjectProperty.shiftClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (shiftClosure ⊤ A) ⊤

Tactic:
shiftClosure_eq_self _

Premises used: CategoryTheory.ObjectProperty.shiftClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
inst_3 : Q.IsClosedUnderIsomorphisms
inst_4 : Q.IsStableUnderShift A
h : P ≤ Q
rw rw₁ : Q ≤ Q
⊢ Q.shiftClosure A ≤ Q

Tactic:
rw [shiftClosure_eq_self]

Premises used: CategoryTheory.ObjectProperty.shiftClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
E : Type u_3
inst_3 : Category.{v_2, u_3} E
inst_4 : HasShift.{v_2, u_3, u_2} E A
X Y : C
i : X ≅ Y
Z : C
a : A
i' : X ≅ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Z
hZ : P Z
⊢ P.shiftClosure A Y

Tactic:
⟨Z, a, i.symm.trans i', hZ⟩

Premises used: CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.ObjectProperty.shiftClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
E : Type u_3
inst_3 : Category.{v_2, u_3} E
inst_4 : HasShift.{v_2, u_3, u_2} E A
X Y : C
i : X ≅ Y
Z : C
a : A
i' : X ≅ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Z
hZ : P Z
⊢ P.shiftClosure A Y

Tactic:
exact ⟨Z, a, i.symm.trans i', hZ⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
E : Type u_3
inst_3 : Category.{v_2, u_3} E
inst_4 : HasShift.{v_2, u_3, u_2} E A
a : A
X Y : C
b : A
i : X ≅ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Y
hY : P Y
⊢ (P.shiftClosure A).shift a X

Tactic:
⟨Y, b + a, ((shiftFunctor C a).mapIso i).trans <|
      (shiftFunctorAdd C b a).symm.app Y, hY⟩

Premises used: CategoryTheory.ObjectProperty.shift, CategoryTheory.shiftFunctor, CategoryTheory.shiftFunctorAdd, HAdd.hAdd, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.ObjectProperty.shiftClosure, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
E : Type u_3
inst_3 : Category.{v_2, u_3} E
inst_4 : HasShift.{v_2, u_3, u_2} E A
a : A
X Y : C
b : A
i : X ≅ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Y
hY : P Y
⊢ (P.shiftClosure A).shift a X

Tactic:
exact ⟨Y, b + a, ((shiftFunctor C a).mapIso i).trans <|
      (shiftFunctorAdd C b a).symm.app Y, hY⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
inst_3 : P.IsClosedUnderIsomorphisms
h : P.shiftClosure A = P
rw : (P.shiftClosure A).IsStableUnderShift A
⊢ P.IsStableUnderShift A

Tactic:
rw [← h]
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
inst_3 : P.IsClosedUnderIsomorphisms
h : P.shiftClosure A = P
⊢ (P.shiftClosure A).IsStableUnderShift A

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
E : Type u_3
inst_3 : Category.{v_2, u_3} E
inst_4 : HasShift.{v_2, u_3, u_2} E A
inst_5 : P.IsClosedUnderIsomorphisms
G : Type u_4
inst_6 : AddGroup G
inst_7 : HasShift.{v_1, u_1, u_4} C G
a : G
rw : LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) (⨆ (a : G), P.shift a) (⨆ (i : G), (P.shift i).shift a)
⊢ LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) (⨆ (a : G), P.shift a) (shift (⨆ (a : G), P.shift a) a)

Tactic:
rw [shift_iSup]

Premises used: CategoryTheory.ObjectProperty.shift_iSup
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
E : Type u_3
inst_3 : Category.{v_2, u_3} E
inst_4 : HasShift.{v_2, u_3, u_2} E A
inst_5 : P.IsClosedUnderIsomorphisms
G : Type u_4
inst_6 : AddGroup G
inst_7 : HasShift.{v_1, u_1, u_4} C G
a : G
X : C
hX : (⨆ (a : G), P.shift a) X
rw : ∀ (hX : ∃ (a : G), P.shift a X), ∃ (a_1 : G), (P.shift a_1).shift a X
⊢ (⨆ (i : G), (P.shift i).shift a) X

Tactic:
rw [prop_iSup_iff] at hX ⊢

Premises used: CategoryTheory.ObjectProperty.prop_iSup_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
E : Type u_3
inst_3 : Category.{v_2, u_3} E
inst_4 : HasShift.{v_2, u_3, u_2} E A
inst_5 : P.IsClosedUnderIsomorphisms
G : Type u_4
inst_6 : AddGroup G
inst_7 : HasShift.{v_1, u_1, u_4} C G
a : G
X : C
hX : ∃ (a : G), P.shift a X
obtain : ∀ (b : G) (hb : P.shift b X), ∃ (a_1 : G), (P.shift a_1).shift a X
⊢ ∃ (a_1 : G), (P.shift a_1).shift a X

Tactic:
obtain ⟨b, hb⟩ := hX
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
E : Type u_3
inst_3 : Category.{v_2, u_3} E
inst_4 : HasShift.{v_2, u_3, u_2} E A
inst_5 : P.IsClosedUnderIsomorphisms
G : Type u_4
inst_6 : AddGroup G
inst_7 : HasShift.{v_1, u_1, u_4} C G
a : G
X : C
b : G
hb rwa rwa₁ rwa₂ rwa₃ : P.shift b X
⊢ (P.shift (-a + b)).shift a X

Tactic:
rwa [P.shift_shift _ _ _ (add_neg_cancel_left a b)]

Premises used: add_neg_cancel_left, CategoryTheory.ObjectProperty.shift_shift
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
E : Type u_3
inst_3 : Category.{v_2, u_3} E
inst_4 : HasShift.{v_2, u_3, u_2} E A
inst_5 : P.IsClosedUnderIsomorphisms
G : Type u_4
inst_6 : AddGroup G
inst_7 : HasShift.{v_1, u_1, u_4} C G
a : G
X : C
b : G
hb : P.shift b X
⊢ ∃ (a_1 : G), (P.shift a_1).shift a X

Tactic:
exact ⟨-a + b, by rwa [P.shift_shift _ _ _ (add_neg_cancel_left a b)]⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderIsomorphisms
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
a : P.shiftClosure G ≤ ⨆ (x : G), P.shift x
a₁ : ⨆ (x : G), P.shift x ≤ P.shiftClosure G
⊢ P.shiftClosure G = ⨆ (x : G), P.shift x

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderIsomorphisms
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
a : P ≤ ⨆ (x : G), P.shift x
⊢ P.shiftClosure G ≤ ⨆ (x : G), P.shift x

Tactic:
rw [shiftClosure_le_iff]

Premises used: CategoryTheory.ObjectProperty.shiftClosure_le_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderIsomorphisms
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
rw : shift.{v_1, u_1, u_4} P (A := G) 0
| P

Tactic:
rw [← P.shift_zero G]

Premises used: CategoryTheory.ObjectProperty.shift_zero
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderIsomorphisms
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
a : shift.{v_1, u_1, u_4} P (A := G) 0 ≤ ⨆ (x : G), P.shift x
⊢ P ≤ ⨆ (x : G), P.shift x

Tactic:
conv_lhs => rw [← P.shift_zero G]

Premises used: CategoryTheory.ObjectProperty.shift_zero
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderIsomorphisms
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
⊢ shift.{v_1, u_1, u_4} P (A := G) 0 ≤ ⨆ (x : G), P.shift x

Tactic:
le_iSup P.shift (0 : G)

Premises used: CategoryTheory.ObjectProperty.shift, le_iSup, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderIsomorphisms
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
⊢ shift.{v_1, u_1, u_4} P (A := G) 0 ≤ ⨆ (x : G), P.shift x

Tactic:
exact le_iSup P.shift (0 : G)

Premises used: CategoryTheory.ObjectProperty.shift, le_iSup, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderIsomorphisms
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
X : C
hX : (⨆ (x : G), P.shift x) X
a : ∀ (a : G) (ha : P.shift a X), P.shiftClosure G X
⊢ P.shiftClosure G X

Tactic:
obtain ⟨a, ha⟩ := (prop_iSup_iff _ _).mp hX

Premises used: Iff.mp, CategoryTheory.ObjectProperty.prop_iSup_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderIsomorphisms
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
X : C
hX : (⨆ (x : G), P.shift x) X
a : G
ha : P.shift a X
⊢ P.shiftClosure G X

Tactic:
⟨X⟦a⟧, -a, (shiftShiftNeg X a).symm, ha⟩

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.shiftShiftNeg, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.ObjectProperty.shiftClosure, CategoryTheory.Functor.obj, Neg.neg
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderIsomorphisms
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
X : C
hX : (⨆ (x : G), P.shift x) X
a : G
ha : P.shift a X
⊢ P.shiftClosure G X

Tactic:
exact ⟨X⟦a⟧, -a, (shiftShiftNeg X a).symm, ha⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
E : Type u_3
inst_3 : Category.{v_2, u_3} E
inst_4 : HasShift.{v_2, u_3, u_2} E A
inst_5 : P.IsStableUnderShift A
F : Functor.{v_2, v_1, u_3, u_1} E C
hF : ∀ (X : E), P (F.obj X)
inst_6 : F.CommShift A
⊢ NatTrans.CommShift (P.liftCompιIso F hF).hom A

Tactic:
Functor.CommShift.ofComp_compatibility _ _

Premises used: CategoryTheory.Functor.CommShift.ofComp_compatibility
-- Module: Mathlib.CategoryTheory.ObjectProperty.ShiftAdditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
inst_3 : P.IsStableUnderShift A
inst_4 : Preadditive.{v_1, u_1} C
n : A
inst_5 : Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
⊢ (shiftFunctor P.FullSubcategory n ⋙ P.ι).Additive

Tactic:
have := Functor.additive_of_iso (P.ι.commShiftIso n).symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.ShiftAdditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
inst_3 : P.IsStableUnderShift A
inst_4 : Preadditive.{v_1, u_1} C
n : A
inst_5 : Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
this : (shiftFunctor P.FullSubcategory n ⋙ P.ι).Additive
⊢ Functor.Additive.{v_1, u_1, v_1, u_1} (C := P.FullSubcategory) (shiftFunctor P.FullSubcategory n)

Tactic:
apply Functor.additive_of_comp_faithful _ P.ι

Premises used: CategoryTheory.Functor.additive_of_comp_faithful, CategoryTheory.ObjectProperty.ι
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsLocal K
X : C
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
⊢ P X ↔ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y

Tactic:
⟨fun h _ _ hf ↦ IsLocal.component hR _ hf h, fun h ↦ of_presieve hR h⟩

Premises used: CategoryTheory.ObjectProperty.IsLocal.component, CategoryTheory.ObjectProperty.IsLocal.of_presieve, Iff.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
Y : C
f : Y ⟶ X
hf : R f
hX : P X
rw : ∀ (hR : ∃ (𝒰 : K.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f) (Y : C) (f : Y ⟶ X) (hf : R f) (hX : P X), P Y
⊢ P Y

Tactic:
rw [CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover] at hR

Premises used: CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve.{v, u} X
hR : ∃ (𝒰 : K.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
Y : C
f : Y ⟶ X
hf : R f
hX : P X
obtain : ∀ (𝒰 : K.ZeroHypercover X) (hf : Presieve.ofArrows 𝒰.X 𝒰.f f), P Y
⊢ P Y

Tactic:
obtain ⟨𝒰, rfl⟩ := hR

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X Y : C
f : Y ⟶ X
hX : P X
𝒰 : K.ZeroHypercover X
hf : Presieve.ofArrows 𝒰.X 𝒰.f f
⊢ ∀ (i : 𝒰.I₀), P (𝒰.X i)

Tactic:
rw [H 𝒰] at hX
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X Y : C
f : Y ⟶ X
hX : P X
𝒰 : K.ZeroHypercover X
hf : Presieve.ofArrows 𝒰.X 𝒰.f f
hX₁ : ∀ (i : 𝒰.I₀), P (𝒰.X i)
⊢ Presieve.ofArrows 𝒰.X 𝒰.f f

Tactic:
rw [H 𝒰] at hX
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X Y : C
f : Y ⟶ X
𝒰 : K.ZeroHypercover X
hX : ∀ (i : 𝒰.I₀), P (𝒰.X i)
hf : Presieve.ofArrows 𝒰.X 𝒰.f f
obtain : ∀ ⦃Y : C⦄ (i : 𝒰.I₀), P (𝒰.X i)
⊢ P Y

Tactic:
obtain ⟨i⟩ := hf
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
𝒰 : K.ZeroHypercover X
hX : ∀ (i : 𝒰.I₀), P (𝒰.X i)
Y : C
i : 𝒰.I₀
⊢ P (𝒰.X i)

Tactic:
hX i
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
𝒰 : K.ZeroHypercover X
hX : ∀ (i : 𝒰.I₀), P (𝒰.X i)
Y : C
i : 𝒰.I₀
⊢ P (𝒰.X i)

Tactic:
exact hX i
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y
⊢ ∃ (𝒰 : K.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
rw [CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover] at hR

Premises used: CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y
hR₁ : ∃ (𝒰 : K.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y

Tactic:
rw [CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover] at hR

Premises used: CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve.{v, u} X
hR : ∃ (𝒰 : K.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y
obtain : ∀ (𝒰 : K.ZeroHypercover X) (h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, Presieve.ofArrows 𝒰.X 𝒰.f f → P Y), P X
⊢ P X

Tactic:
obtain ⟨𝒰, rfl⟩ := hR

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
𝒰 : K.ZeroHypercover X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, Presieve.ofArrows 𝒰.X 𝒰.f f → P Y
rw : ∀ (i : 𝒰.I₀), P (𝒰.X i)
⊢ P X

Tactic:
rw [H 𝒰]
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
𝒰 : K.ZeroHypercover X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, Presieve.ofArrows 𝒰.X 𝒰.f f → P Y
i : 𝒰.I₀
⊢ P (𝒰.X i)

Tactic:
h ⟨i⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
𝒰 : K.ZeroHypercover X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, Presieve.ofArrows 𝒰.X 𝒰.f f → P Y
i : 𝒰.I₀
⊢ P (𝒰.X i)

Tactic:
exact h ⟨i⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K L : Precoverage.{v, u} C
⊢ ∀ {X : C} {R : Presieve.{v, u} X} (hR : R ∈ K.coverings X) {Y : C} (f : Y ⟶ X) (hf : R f), ⊤ X → ⊤ Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K L : Precoverage.{v, u} C
⊢ ∀ {X : C} {R : Presieve.{v, u} X} (hR : R ∈ K.coverings X) (H : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → ⊤ Y), ⊤ X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsLocal K
X : C
𝒰 : Precoverage.ZeroHypercover.{u_1, v, u} K X
h : ∀ (i : 𝒰.I₀), P (𝒰.X i)
⊢ P X

Tactic:
P.of_presieve 𝒰.mem₀ fun _ f ⟨i⟩ ↦ h i

Premises used: _private.0.CategoryTheory.ObjectProperty.of_zeroHypercover.match_1, CategoryTheory.ObjectProperty.IsLocal.of_presieve, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
K : Precoverage.{v, u} C
inst_1 : P.IsLocal K
X : C
𝒰 : Precoverage.ZeroHypercover.{u_1, v, u} K X
⊢ P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)

Tactic:
⟨fun h i ↦ IsLocal.component 𝒰.mem₀ _ ⟨i⟩ h, fun h ↦ of_zeroHypercover 𝒰 h⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.ObjectProperty.IsLocal.component, CategoryTheory.ObjectProperty.of_zeroHypercover, Iff.intro, CategoryTheory.Precoverage.ZeroHypercover.mem₀, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.Small.{w, v, u} P
⊢ Small.{w, u} P.FullSubcategory

Tactic:
small_of_surjective (f := fun (x : Subtype P) ↦ ⟨x.1, x.2⟩) (fun x ↦ ⟨⟨x.1, x.2⟩, rfl⟩)

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, small_of_surjective, CategoryTheory.ObjectProperty.FullSubcategory.obj, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.Small.{w, v, u} Q
h : P ≤ Q
⊢ ObjectProperty.Small.{w, v, u} P

Tactic:
small_of_injective (Subtype.map_injective h Function.injective_id)

Premises used: small_of_injective, Function.injective_id, Subtype.map_injective
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.Small.{w, v, u} P
⊢ ObjectProperty.Small.{w, v, u} P.op

Tactic:
small_of_injective P.subtypeOpEquiv.injective

Premises used: small_of_injective, CategoryTheory.ObjectProperty.subtypeOpEquiv, Equiv.injective
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} Cᵒᵖ
inst_2 : ObjectProperty.Small.{w, v, u} P
⊢ ObjectProperty.Small.{w, v, u} P.unop

Tactic:
simpa only [← small_congr P.unop.subtypeOpEquiv]

Premises used: small_congr, CategoryTheory.ObjectProperty.unop, CategoryTheory.ObjectProperty.subtypeOpEquiv
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
ι : Type u_1
X : ι → C
inst_2 : Small.{w, u_1} ι
i : ι
⊢ ofObj.{v, u, u_1} X (X i)

Tactic:
simp