awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Retract (goal)
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
⊢ isoClosure.{v, u} (ofObj Y) y
have obtain : ∀ (hx : Q (X a)) (r : Retract y (X a)) (h₂ : g (h a) h₁ = g r hx), isoClosure.{v, u} (ofObj Y) y
Tactic: obtain rfl : x = X a := Subtype.ext_iff.1 (congr_arg Sigma.fst h₂.symm)
Cleared hypotheses: x, hx, r, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Retract (hypothesis)
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
have 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 })
Tactic: rw [Sigma.ext_iff, heq_eq_eq] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Retract (hypothesis)
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
⊢ isoClosure.{v, u} (ofObj Y) y
have hri : (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
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
⊢ shift.{v_1, u_1, u_2} P (A := A) 0 = P
have h : ∀ (X : C), shift.{v_1, u_1, u_2} P (A := A) 0 X ↔ P X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
⊢ (P.shift b).shift a = P.shift c
have h₁ : ∀ (X : C), (P.shift b).shift a X ↔ P.shift c X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
⊢ (P ⊔ Q).shift a = P.shift a ⊔ Q.shift a
have h : ∀ (x : C), (P ⊔ Q).shift a x ↔ (P.shift a ⊔ Q.shift a) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (shift (⨆ (i : ι), P i) a) (⨆ (i : ι), (P i).shift a)
have h : ∀ (x : C), shift.{v_1, u_1, u_2} (⨆ (i : ι), P i) a x ↔ (⨆ (i : ι), (P i).shift a) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
have refine : ∀ (hX : 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 _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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 X
have rw : (P.shift (-g)).shift g X
Tactic: rw [← P.shift_zero G, ← P.shift_shift g (-g) 0 (by simp)]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
have refine : P.shiftClosure A ≤ P
Tactic: refine le_antisymm ?_ P.le_shiftClosure
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
⊢ Q.shiftClosure A ≤ Q
have rw : Q ≤ Q
Tactic: rw [shiftClosure_eq_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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.IsStableUnderShift A
have rw : (P.shiftClosure A).IsStableUnderShift A
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
⊢ LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) (⨆ (a : G), P.shift a) (shift (⨆ (a : G), P.shift a) a)
have rw : LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) (⨆ (a : G), P.shift a) (⨆ (i : G), (P.shift i).shift a)
Tactic: rw [shift_iSup]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
⊢ (⨆ (i : G), (P.shift i).shift a) X
have rw : ∀ (hX : ∃ (a : G), P.shift a X), ∃ (a_1 : G), (P.shift a_1).shift a X
Tactic: rw [prop_iSup_iff] at hX ⊢
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
⊢ ∃ (a_1 : G), (P.shift a_1).shift a X
have obtain : ∀ (b : G) (hb : P.shift b X), ∃ (a_1 : G), (P.shift a_1).shift a X
Tactic: obtain ⟨b, hb⟩ := hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
⊢ P.shiftClosure G = ⨆ (x : G), P.shift x
have a : P.shiftClosure G ≤ ⨆ (x : G), P.shift x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
⊢ P.shiftClosure G = ⨆ (x : G), P.shift x
have a₁ : ⨆ (x : G), P.shift x ≤ P.shiftClosure G
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
⊢ P.shiftClosure G ≤ ⨆ (x : G), P.shift x
have a : P ≤ ⨆ (x : G), P.shift x
Tactic: rw [shiftClosure_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
| P
have rw : shift.{v_1, u_1, u_4} P (A := G) 0
Tactic: rw [← P.shift_zero G]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
⊢ P ≤ ⨆ (x : G), P.shift x
have a : shift.{v_1, u_1, u_4} P (A := G) 0 ≤ ⨆ (x : G), P.shift x
Tactic: conv_lhs => rw [← P.shift_zero G]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Shift (goal)
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
⊢ P.shiftClosure G X
have a : ∀ (a : G) (ha : P.shift a X), P.shiftClosure G X
Tactic: obtain ⟨a, ha⟩ := (prop_iSup_iff _ _).mp hX
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ShiftAdditive (hypothesis)
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)
⊢ Functor.Additive.{v_1, u_1, v_1, u_1} (C := P.FullSubcategory) (shiftFunctor P.FullSubcategory n)
have this : (shiftFunctor P.FullSubcategory n ⋙ P.ι).Additive
Tactic: have := Functor.additive_of_iso (P.ι.commShiftIso n).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.SiteLocal (goal)
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
⊢ P Y
have rw : ∀ (hR : ∃ (𝒰 : K.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f) (Y : C) (f : Y ⟶ X) (hf : R f) (hX : P X), P Y
Tactic: rw [CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover] at hR
Cleared hypotheses: hR, Y, f, hf, hX
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.SiteLocal (goal)
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
⊢ P Y
have obtain : ∀ (𝒰 : K.ZeroHypercover X) (hf : Presieve.ofArrows 𝒰.X 𝒰.f f), P Y
Tactic: obtain ⟨𝒰, rfl⟩ := hR
Cleared hypotheses: R, hR, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.SiteLocal (hypothesis)
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
⊢ P Y
have hX₁ : ∀ (i : 𝒰.I₀), P (𝒰.X i)
Tactic: rw [H 𝒰] at hX
Cleared hypotheses: hX, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.SiteLocal (goal)
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
⊢ P Y
have obtain : ∀ ⦃Y : C⦄ (i : 𝒰.I₀), P (𝒰.X i)
Tactic: obtain ⟨i⟩ := hf
Cleared hypotheses: Y, f, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.SiteLocal (hypothesis)
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
⊢ P X
have hR₁ : ∃ (𝒰 : K.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
Tactic: rw [CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover] at hR
Cleared hypotheses: hR, h
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.SiteLocal (goal)
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
⊢ P X
have obtain : ∀ (𝒰 : K.ZeroHypercover X) (h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, Presieve.ofArrows 𝒰.X 𝒰.f f → P Y), P X
Tactic: obtain ⟨𝒰, rfl⟩ := hR
Cleared hypotheses: R, hR, h
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.SiteLocal (goal)
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
⊢ P X
have rw : ∀ (i : 𝒰.I₀), P (𝒰.X i)
Tactic: rw [H 𝒰]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
⊢ ObjectProperty.Small.{w, v, u} P.unop ↔ ObjectProperty.Small.{w, v, u} P
have rw : ObjectProperty.Small.{w, v, u} P.unop.op ↔ ObjectProperty.Small.{w, v, u} P
Tactic: rw [← small_op_iff, op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
rw : ObjectProperty.Small.{w, v, u} P.unop.op ↔ ObjectProperty.Small.{w, v, u} P
⊢ ObjectProperty.Small.{w, v, u} P.unop ↔ ObjectProperty.Small.{w, v, u} P
have rw₁ : ObjectProperty.Small.{w, v, u} P ↔ ObjectProperty.Small.{w, v, u} P
Tactic: rw [← small_op_iff, op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure
have obtain : ∀ (Q : ObjectProperty.{v, u} C),
  ObjectProperty.Small.{w, v, u} Q →
    ∀ (hQ : P ≤ Q.isoClosure),
      ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure
Tactic: obtain ⟨Q, _, hQ⟩ := exists_small_le' P
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure
have h : ∀ (X' : Subtype P'), ∃ (X : Subtype P), Nonempty.{v + 1} ((↑X' : C) ≅ (↑X : C))
Tactic: have h (X' : Subtype P') : ∃ (X : Subtype P), Nonempty (X'.1 ≅ X.1) :=
    ⟨⟨X'.2.2.choose, X'.2.2.choose_spec.choose⟩, X'.2.2.choose_spec.choose_spec⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
h : ∀ (X' : Subtype P'), ∃ (X : Subtype P), Nonempty.{v + 1} ((↑X' : C) ≅ (↑X : C))
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure
have choose : ∀ (φ : (X' : Subtype P') → Subtype P) (hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))),
  ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure
Tactic: choose φ hφ using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure
have refine_1 : ObjectProperty.Small.{w, v, u} (C := C) fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)
Tactic: refine ⟨fun X ↦ X ∈ Set.range (Subtype.val ∘ φ), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
refine_1 : ObjectProperty.Small.{w, v, u} (C := C) fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure
have refine_2 : (fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)) ≤ P
Tactic: refine ⟨fun X ↦ X ∈ Set.range (Subtype.val ∘ φ), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
refine_1 : ObjectProperty.Small.{w, v, u} (C := C) fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)
refine_2 : (fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)) ≤ P
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure
have refine_3 : P ≤ isoClosure fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)
Tactic: refine ⟨fun X ↦ X ∈ Set.range (Subtype.val ∘ φ), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
X : C
hX : X ∈ Set.range (Subtype.val (p := P) ∘ φ)
⊢ P X
have hX₁ : ∃ (a : C) (b : P' a), (↑(φ (Subtype.mk (p := fun (a : C) ↦ P' a) a b)) : C) = X
Tactic: simp only [Set.mem_range, Function.comp_apply, Subtype.exists] at hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
X : C
hX : ∃ (a : C) (b : P' a), (↑(φ (Subtype.mk (p := fun (a : C) ↦ P' a) a b)) : C) = X
⊢ P X
have refine_2 : ∀ (Y : C) (hY : P' Y), P (↑(φ (Subtype.mk (p := fun (a : C) ↦ P' a) Y hY)) : C)
Tactic: obtain ⟨Y, hY, rfl⟩ := hX
Cleared hypotheses: X, hX
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
X : C
hX : P X
⊢ isoClosure.{v, u} (fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)) X
have refine_3 : ∀ (Y : C) (hY : Q Y) (e : X ≅ Y), isoClosure.{v, u} (fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)) X
Tactic: obtain ⟨Y, hY, ⟨e⟩⟩ := hQ _ hX
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
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.EssentiallySmall.{w, v, u} P
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.isoClosure ≤ Q.isoClosure
have obtain : ∀ (Q : ObjectProperty.{v, u} C),
  ObjectProperty.Small.{w, v, u} Q →
    Q ≤ P →
      P ≤ Q.isoClosure →
        ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.isoClosure ≤ Q.isoClosure
Tactic: obtain ⟨Q, _, _, _⟩ := EssentiallySmall.exists_small_le.{w} P