awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁_1 : Q ≤ P
h₂_1 : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y x : C
hx : Q x
r : Retract y x
a : Subtype R
h₁ : Q (X a)
h₂ : g (h a) h₁ = g r hx
obtain : ∀ (hx : Q (X a)) (r : Retract y (X a)) (h₂ : g (h a) h₁ = g r hx), isoClosure.{v, u} (ofObj Y) y
⊢ isoClosure.{v, u} (ofObj Y) y

Tactic:
obtain rfl : x = X a := Subtype.ext_iff.1 (congr_arg Sigma.fst h₂.symm)

Premises used: Sigma.fst, Subtype.ext_iff, congr_arg, Iff.mp, Eq.symm, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁_1 : Q ≤ P
h₂_1 : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ : g (h a) h₁ = g r hx
⊢ (g (h a) h₁).fst (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) =
      (g r hx).fst (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) ∧
    (g (h a) h₁).snd (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) =
      (g r hx).snd (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p })

Tactic:
rw [Sigma.ext_iff, heq_eq_eq] at h₂

Premises used: heq_eq_eq, Sigma.ext_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁_1 : Q ≤ P
h₂_1 : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ :
  (g (h a) h₁).fst (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) =
      (g r hx).fst (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) ∧
    (g (h a) h₁).snd (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) =
      (g r hx).snd (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p })
⊢ (h a).r ≫ (h a).i = r.r ≫ r.i

Tactic:
Subtype.ext_iff.1 h₂.2

Premises used: Subtype.ext_iff, And.right, Iff.mp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁_1 : Q ≤ P
h₂_1 : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ :
  (g (h a) h₁).fst (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) =
      (g r hx).fst (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) ∧
    (g (h a) h₁).snd (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) =
      (g r hx).snd (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p })
⊢ (h a).r ≫ (h a).i = r.r ≫ r.i

Tactic:
exact Subtype.ext_iff.1 h₂.2

Premises used: Subtype.ext_iff, And.right, Iff.mp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁_1 : Q ≤ P
h₂_1 : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ : g (h a) h₁ = g r hx
⊢ (h a).r ≫ (h a).i = r.r ≫ r.i

Tactic:
have hri : (h a).r ≫ (h a).i = r.r ≫ r.i := by
      rw [Sigma.ext_iff, heq_eq_eq] at h₂
      exact Subtype.ext_iff.1 h₂.2
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁_1 : Q ≤ P
h₂_1 : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ : g (h a) h₁ = g r hx
hri : (h a).r ≫ (h a).i = r.r ≫ r.i
⊢ (r.i ≫ (h a).r) ≫ (h a).i ≫ r.r = 𝟙 y

Tactic:
simp [reassoc_of% hri]
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁_1 : Q ≤ P
h₂_1 : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ : g (h a) h₁ = g r hx
hri : (h a).r ≫ (h a).i = r.r ≫ r.i
⊢ ((h a).i ≫ r.r) ≫ r.i ≫ (h a).r = 𝟙 (Y (Subtype.mk (p := R) (↑a : α) ⋯))

Tactic:
simp [← reassoc_of% hri]
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁_1 : Q ≤ P
h₂_1 : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ : g (h a) h₁ = g r hx
hri : (h a).r ≫ (h a).i = r.r ≫ r.i
⊢ isoClosure.{v, u} (ofObj Y) y

Tactic:
exact ⟨_, ⟨a.1, a.2⟩, ⟨{
      hom := r.i ≫ (h a).r
      inv := (h a).i ≫ r.r
      hom_inv_id := by simp [reassoc_of% hri]
      inv_hom_id := by simp [← reassoc_of% hri]
    }⟩⟩
-- 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
a : A
X : C
⊢ P.shift a X ↔ P (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)

Tactic:
Iff.rfl

Premises used: CategoryTheory.ObjectProperty.shift, Iff.rfl
-- 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 : ∀ (X : C), shift.{v_1, u_1, u_2} P (A := A) 0 X ↔ P X
⊢ shift.{v_1, u_1, u_2} P (A := A) 0 = P

Tactic:
ext X
-- 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
X : C
⊢ shift.{v_1, u_1, u_2} P (A := A) 0 X ↔ P X

Tactic:
P.prop_iff_of_iso ((shiftFunctorZero C A).app X)

Premises used: CategoryTheory.ObjectProperty.shift, CategoryTheory.shiftFunctorZero, CategoryTheory.ObjectProperty.prop_iff_of_iso, CategoryTheory.Iso.app
-- 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
X : C
⊢ shift.{v_1, u_1, u_2} P (A := A) 0 X ↔ P X

Tactic:
exact P.prop_iff_of_iso ((shiftFunctorZero C A).app X)

Premises used: CategoryTheory.shiftFunctorZero, CategoryTheory.ObjectProperty.prop_iff_of_iso, CategoryTheory.Iso.app
-- 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
a b c : A
h : a + b = c
inst_3 : P.IsClosedUnderIsomorphisms
h₁ : ∀ (X : C), (P.shift b).shift a X ↔ P.shift c X
⊢ (P.shift b).shift a = P.shift c

Tactic:
ext X
-- 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
a b c : A
h : a + b = c
inst_3 : P.IsClosedUnderIsomorphisms
X : C
⊢ (P.shift b).shift a X ↔ P.shift c X

Tactic:
P.prop_iff_of_iso ((shiftFunctorAdd' C a b c h).symm.app X)

Premises used: CategoryTheory.ObjectProperty.shift, CategoryTheory.shiftFunctorAdd', CategoryTheory.ObjectProperty.prop_iff_of_iso, CategoryTheory.Iso.symm, CategoryTheory.Iso.app
-- 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
a b c : A
h : a + b = c
inst_3 : P.IsClosedUnderIsomorphisms
X : C
⊢ (P.shift b).shift a X ↔ P.shift c X

Tactic:
exact P.prop_iff_of_iso ((shiftFunctorAdd' C a b c h).symm.app X)

Premises used: CategoryTheory.shiftFunctorAdd', CategoryTheory.ObjectProperty.prop_iff_of_iso, CategoryTheory.Iso.symm, CategoryTheory.Iso.app
-- 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
a : A
h : ∀ (x : C), (P ⊔ Q).shift a x ↔ (P.shift a ⊔ Q.shift a) x
⊢ (P ⊔ Q).shift a = P.shift a ⊔ Q.shift a

Tactic:
ext
-- 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
a : A
x : C
⊢ (P ⊔ Q).shift a x ↔ (P.shift a ⊔ Q.shift a) x

Tactic:
simp [prop_shift_iff]

Premises used: CategoryTheory.ObjectProperty.prop_shift_iff
-- 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
ι : Sort u_4
P : ι → ObjectProperty.{v_1, u_1} C
a : A
h : ∀ (x : C), shift.{v_1, u_1, u_2} (⨆ (i : ι), P i) a x ↔ (⨆ (i : ι), (P i).shift a) x
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (shift (⨆ (i : ι), P i) a) (⨆ (i : ι), (P i).shift a)

Tactic:
ext
-- 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
ι : Sort u_4
P : ι → ObjectProperty.{v_1, u_1} C
a : A
x : C
⊢ shift.{v_1, u_1, u_2} (⨆ (i : ι), P i) a x ↔ (⨆ (i : ι), (P i).shift a) x

Tactic:
simp [prop_shift_iff]

Premises used: CategoryTheory.ObjectProperty.prop_shift_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
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
a : A
inst_3 : P.IsStableUnderShiftBy a
⊢ P ≤ P.shift a

Tactic:
IsStableUnderShiftBy.le_shift

Premises used: CategoryTheory.ObjectProperty.IsStableUnderShiftBy.le_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
a : A
inst_5 : P.IsStableUnderShiftBy a
inst_6 : P.Nonempty
⊢ (P.shift a).Nonempty

Tactic:
.mono (P.le_shift a)

Premises used: CategoryTheory.ObjectProperty.Nonempty.mono, CategoryTheory.ObjectProperty.le_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
a : A
x : C
h : ⊤ x
⊢ shift.{v_1, u_1, u_2} ⊤ a x

Tactic:
trivial
-- 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
inst_5 : P.IsStableUnderShiftBy a
X Y : C
hY : P Y
e : X ≅ Y
⊢ P.isoClosure.shift a X

Tactic:
⟨Y⟦a⟧, P.le_shift a _ hY, ⟨(shiftFunctor C a).mapIso e⟩⟩

Premises used: CategoryTheory.ObjectProperty.shift, CategoryTheory.shiftFunctor, Nonempty.intro, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj, CategoryTheory.ObjectProperty.le_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
a : A
inst_5 : P.IsStableUnderShiftBy a
X Y : C
hY : P Y
e : X ≅ Y
⊢ P.isoClosure.shift a X

Tactic:
exact ⟨Y⟦a⟧, P.le_shift a _ hY, ⟨(shiftFunctor C a).mapIso e⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
G : Type u_4
inst_1 : AddGroup G
inst_2 : HasShift.{v_1, u_1, u_4} C G
inst_3 : P.IsStableUnderShift G
inst_4 : P.IsClosedUnderIsomorphisms
X : C
g : G
⊢ P (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C g) X) ↔ P X

Tactic:
⟨fun hX ↦ ?_, P.le_shift g _⟩

Premises used: Iff.intro, 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
G : Type u_4
inst_1 : AddGroup G
inst_2 : HasShift.{v_1, u_1, u_4} C G
inst_3 : P.IsStableUnderShift G
inst_4 : P.IsClosedUnderIsomorphisms
X : C
g : G
refine : ∀ (hX : P (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C g) X)), P X
⊢ P (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C g) X) ↔ P X

Tactic:
refine ⟨fun hX ↦ ?_, P.le_shift g _⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
G : Type u_4
inst_1 : AddGroup G
inst_2 : HasShift.{v_1, u_1, u_4} C G
inst_3 : P.IsStableUnderShift G
inst_4 : P.IsClosedUnderIsomorphisms
X : C
g : G
hX : P (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C g) X)
⊢ g + -g = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Shift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
G : Type u_4
inst_1 : AddGroup G
inst_2 : HasShift.{v_1, u_1, u_4} C G
inst_3 : P.IsStableUnderShift G
inst_4 : P.IsClosedUnderIsomorphisms
X : C
g : G
hX : P (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C g) X)
rw : (P.shift (-g)).shift g X
⊢ P X

Tactic:
rw [← P.shift_zero G, ← P.shift_shift g (-g) 0 (by simp)]

Premises used: CategoryTheory.ObjectProperty.shift_zero, CategoryTheory.ObjectProperty.shift_shift, OfNat.ofNat, 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
G : Type u_4
inst_1 : AddGroup G
inst_2 : HasShift.{v_1, u_1, u_4} C G
inst_3 : P.IsStableUnderShift G
inst_4 : P.IsClosedUnderIsomorphisms
X : C
g : G
hX : P (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C g) X)
⊢ (P.shift (-g)).shift g X

Tactic:
P.le_shift (-g) _ hX

Premises used: CategoryTheory.ObjectProperty.shift, Neg.neg, 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
G : Type u_4
inst_1 : AddGroup G
inst_2 : HasShift.{v_1, u_1, u_4} C G
inst_3 : P.IsStableUnderShift G
inst_4 : P.IsClosedUnderIsomorphisms
X : C
g : G
hX : P (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C g) X)
⊢ (P.shift (-g)).shift g X

Tactic:
exact P.le_shift (-g) _ hX

Premises used: Neg.neg, 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
X : C
⊢ P.shiftClosure A X ↔ ∃ (Y : C) (a : A) (x : X ≅ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y), P Y

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.ObjectProperty.shiftClosure
-- 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
X : C
hX : P X
⊢ P.shiftClosure A X

Tactic:
⟨X, 0, (shiftFunctorZero C A).symm.app X, hX⟩

Premises used: CategoryTheory.shiftFunctorZero, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.ObjectProperty.shiftClosure, CategoryTheory.Iso.app, 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
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : C
hX : P X
⊢ P.shiftClosure A X

Tactic:
exact ⟨X, 0, (shiftFunctorZero C A).symm.app X, 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.Nonempty
⊢ (P.shiftClosure A).Nonempty

Tactic:
.mono P.le_shiftClosure

Premises used: CategoryTheory.ObjectProperty.le_shiftClosure, CategoryTheory.ObjectProperty.Nonempty.mono
-- 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
h : P ≤ Q
X Y : C
a : A
i : X ≅ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y
hY : P Y
⊢ Q.shiftClosure A X

Tactic:
⟨Y, a, i, h Y hY⟩

Premises used: Exists.intro, 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
h : P ≤ Q
X Y : C
a : A
i : X ≅ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y
hY : P Y
⊢ Q.shiftClosure A X

Tactic:
refine ⟨Y, a, i, h 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
inst_4 : P.IsStableUnderShift A
⊢ P.shiftClosure A = P

Tactic:
le_antisymm ?_ P.le_shiftClosure

Premises used: CategoryTheory.ObjectProperty.le_shiftClosure, 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
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
refine : P.shiftClosure A ≤ P
⊢ P.shiftClosure A = P

Tactic:
refine le_antisymm ?_ P.le_shiftClosure

Premises used: CategoryTheory.ObjectProperty.le_shiftClosure, le_antisymm