awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
a : P.isoClosure ≤ P
⊢ P.isoClosure = P
have a₁ : P ≤ P.isoClosure
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
X : C
⊢ P.isoClosure X ≤ P X
have a : ∀ (Y : C) (hY : P Y) (e : X ≅ Y), P X
Tactic: ⟨Y, hY, ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
inst_1 : Q.IsClosedUnderIsomorphisms
h : P ≤ Q
⊢ Q.isoClosure ≤ Q
have rw : Q ≤ Q
Tactic: rw [isoClosure_eq_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : P.isoClosure = P
⊢ P.IsClosedUnderIsomorphisms
have rw : P.isoClosure.IsClosedUnderIsomorphisms
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
⊢ (P.strictMap F).isoClosure = P.map F
have refine_1 : (P.strictMap F).isoClosure ≤ P.map F
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
refine_1 : (P.strictMap F).isoClosure ≤ P.map F
⊢ (P.strictMap F).isoClosure = P.map F
have refine_2 : P.map F ≤ (P.strictMap F).isoClosure
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
⊢ (P.strictMap F).isoClosure ≤ P.map F
have refine_1 : P.strictMap F ≤ P.map F
Tactic: rw [isoClosure_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
⊢ P.isoClosure.map F = P.map F
have refine : P.isoClosure.map F ≤ P.map F
Tactic: refine le_antisymm ?_ (map_monotone P.le_isoClosure F)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ClosureShift (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.IsStableUnderShift A
a : A
X : C
⊢ P.retractClosure X ≤ P.retractClosure.shift a X
have this : ∀ (Y : C) (hY : P Y) (i : X ⟶ Y) (r : Y ⟶ X) (w : i ≫ r = 𝟙 X), P.retractClosure.shift a X
Tactic: ⟨Y, hY, i, r, w⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ClosureShift (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 : AddGroup A
inst_2 : HasShift.{v_1, u_1, u_2} C A
α : Type u_3
J : α → Type u_4
inst_3 : (i : α) → Category.{u_5, u_4} (J i)
inst_4 : P.IsStableUnderShift A
a : A
X : C
hX : limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J X
⊢ (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X
have of_mem : ∀ (X : C) (hX : P X), (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X
Tactic: induction hX with
    | of_mem X hX => exact limitsClosure.of_mem _ (IsStableUnderShiftBy.le_shift X hX)
    | of_isoClosure e hX hX' => exact limitsClosure.of_isoClosure ((shiftFunctor C a).mapIso e) hX'
    | of_limitPresentation pres h h' =>
      exact limitsClosure.of_limitPresentation (pres.map (shiftFunctor C a)) h'
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ClosureShift (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 : AddGroup A
inst_2 : HasShift.{v_1, u_1, u_2} C A
α : Type u_3
J : α → Type u_4
inst_3 : (i : α) → Category.{u_5, u_4} (J i)
inst_4 : P.IsStableUnderShift A
a : A
X : C
hX : limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J X
of_mem : ∀ (X : C) (hX : P X), (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X
⊢ (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X
have of_isoClosure : ∀ {X Y : C} (e : X ≅ Y) (hX : limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J X)
  (hX' : (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X),
  (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a Y
Tactic: induction hX with
    | of_mem X hX => exact limitsClosure.of_mem _ (IsStableUnderShiftBy.le_shift X hX)
    | of_isoClosure e hX hX' => exact limitsClosure.of_isoClosure ((shiftFunctor C a).mapIso e) hX'
    | of_limitPresentation pres h h' =>
      exact limitsClosure.of_limitPresentation (pres.map (shiftFunctor C a)) h'
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ClosureShift (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 : AddGroup A
inst_2 : HasShift.{v_1, u_1, u_2} C A
α : Type u_3
J : α → Type u_4
inst_3 : (i : α) → Category.{u_5, u_4} (J i)
inst_4 : P.IsStableUnderShift A
a : A
X : C
hX : limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J X
of_mem : ∀ (X : C) (hX : P X), (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X
of_isoClosure :
  ∀ {X Y : C} (e : X ≅ Y) (hX : limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J X)
    (hX' : (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X),
    (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a Y
⊢ (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X
have of_limitPresentation : ∀ {X : C} {a_1 : α} (pres : Limits.LimitPresentation.{u_5, u_4, v_1, u_1} (J a_1) X)
  (h : ∀ (j : J a_1), limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J (pres.diag.obj j))
  (h' : ∀ (j : J a_1), (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a (pres.diag.obj j)),
  (limitsClosure.{u_3, u_5, u_4, v_1, u_1} P J).shift a X
Tactic: induction hX with
    | of_mem X hX => exact limitsClosure.of_mem _ (IsStableUnderShiftBy.le_shift X hX)
    | of_isoClosure e hX hX' => exact limitsClosure.of_isoClosure ((shiftFunctor C a).mapIso e) hX'
    | of_limitPresentation pres h h' =>
      exact limitsClosure.of_limitPresentation (pres.map (shiftFunctor C a)) h'
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
J : Type u'
inst_1 : Category.{v', u'} J
hJ : HasCardinalLT (Arrow.{v', u'} J) κ
⊢ IsClosedUnderColimitsOfShape.{v', u', v, u} (P.colimitsCardinalClosure κ) J
have obtain : ∀ (S : SmallCategoryCardinalLT κ) (e : Equivalence.{w, v', w, u'} (SmallCategoryCardinalLT.categoryFamily κ S) J),
  IsClosedUnderColimitsOfShape.{v', u', v, u} (P.colimitsCardinalClosure κ) J
Tactic: obtain ⟨S, ⟨e⟩⟩ := SmallCategoryCardinalLT.exists_equivalence κ J hJ
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
J : Type u'
inst_1 : Category.{v', u'} J
hJ : HasCardinalLT (Arrow.{v', u'} J) κ
S : SmallCategoryCardinalLT κ
e : Equivalence.{w, v', w, u'} (SmallCategoryCardinalLT.categoryFamily κ S) J
⊢ IsClosedUnderColimitsOfShape.{v', u', v, u} (P.colimitsCardinalClosure κ) J
have rw : IsClosedUnderColimitsOfShape.{w, w, v, u} (P.colimitsCardinalClosure κ) (SmallCategoryCardinalLT.categoryFamily κ S)
Tactic: rw [isClosedUnderColimitsOfShape_iff_of_equivalence _ e.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
Q : ObjectProperty.{v, u} C
inst_1 : Q.IsClosedUnderIsomorphisms
hQ : ∀ (J : Type w) [inst_2 : SmallCategory J], HasCardinalLT (Arrow J) κ → Q.IsClosedUnderColimitsOfShape J
h : P ≤ Q
⊢ P.colimitsCardinalClosure κ ≤ Q
have this : ∀ (i : SmallCategoryCardinalLT κ),
  IsClosedUnderColimitsOfShape.{w, w, v, u} Q (SmallCategoryCardinalLT.categoryFamily κ i)
Tactic: have (i : SmallCategoryCardinalLT κ) := hQ _ i.hasCardinalLT
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
⊢ HasCardinalLT (Arrow WalkingParallelPair) Cardinal.aleph0
have simp : Finite (Arrow WalkingParallelPair)
Tactic: simp only [hasCardinalLT_aleph0_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
⊢ (P.colimitsCardinalClosure κ).IsStableUnderRetracts
have this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
Tactic: have := P.isClosedUnderColimitsOfShape_colimitsCardinalClosure κ
    WalkingParallelPair (HasCardinalLT.of_le (by
      simp only [hasCardinalLT_aleph0_iff]
      infer_instance)
    (Cardinal.IsRegular.aleph0_le Fact.out))
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
⊢ colimitsClosure.{t, v', u', v, u} P.isoClosure J = colimitsClosure.{t, v', u', v, u} P J
have refine : P.isoClosure ≤ colimitsClosure.{t, v', u', v, u} P J
Tactic: refine le_antisymm (colimitsClosure_le ?_)
    (colimitsClosure_monotone _ P.le_isoClosure)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
⊢ P.isoClosure ≤ colimitsClosure.{t, v', u', v, u} P J
have rw : P ≤ colimitsClosure.{t, v', u', v, u} P J
Tactic: rw [isoClosure_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
⊢ colimitsClosure.{t, v', u', v, u} P J =
    ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ)
have refine_1 : colimitsClosure.{t, v', u', v, u} P J ≤ ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
refine_1 :
  colimitsClosure.{t, v', u', v, u} P J ≤
    ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ)
⊢ colimitsClosure.{t, v', u', v, u} P J =
    ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ)
have refine_2 : ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ) ≤ colimitsClosure.{t, v', u', v, u} P J
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
⊢ colimitsClosure.{t, v', u', v, u} P J ≤
    ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ)
have refine_1 : P ≤ ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ)
Tactic: apply colimitsClosure_le
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
⊢ P ≤ ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ)
have refine_1 : P.op ≤ limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ
Tactic: rw [← op_monotone_iff, op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
⊢ ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ) ≤
    colimitsClosure.{t, v', u', v, u} P J
have refine_2 : (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ) ≤ (colimitsClosure.{t, v', u', v, u} P J).op
Tactic: rw [← op_monotone_iff, op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
⊢ (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ) ≤ (colimitsClosure.{t, v', u', v, u} P J).op
have refine_2 : P.op ≤ (colimitsClosure.{t, v', u', v, u} P J).op
Tactic: apply limitsClosure_le
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
⊢ P.op ≤ (colimitsClosure.{t, v', u', v, u} P J).op
have refine_2 : P ≤ colimitsClosure.{t, v', u', v, u} P J
Tactic: rw [op_monotone_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : LocallySmall.{w, v, u} C
inst_4 : Small.{w, t} α
inst_5 : ∀ (a : α), Small.{w, u'} (J a)
inst_6 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (colimitsClosure.{t, v', u', v, u} P J)
have rw : ObjectProperty.EssentiallySmall.{w, v, u}
  (ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ))
Tactic: rw [colimitsClosure_eq_unop_limitsClosure]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
α : Type t
J : α → Type u'
inst_1 : (a : α) → Category.{v', u'} (J a)
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : LocallySmall.{w, v, u} C
inst_4 : Small.{w, t} α
inst_5 : ∀ (a : α), Small.{w, u'} (J a)
inst_6 : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
⊢ ObjectProperty.EssentiallySmall.{w, v, u}
    (ObjectProperty.unop (limitsClosure.{t, v', u', v, u} P.op fun (a : α) ↦ (J a)ᵒᵖ))
have this : ∀ (a : α), Small.{w, u'} (J a)ᵒᵖ
Tactic: have (a : α) : Small.{w} (J a)ᵒᵖ := Opposite.small
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : Nonempty J
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (strictColimitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥
have rw : LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) (strictColimitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : Nonempty J
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (colimitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥
have rw : LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) (colimitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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
⊢ (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure = colimitsOfShape.{v', u', v_1, u_1} P J
have refine_1 : (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure ≤ colimitsOfShape.{v', u', v_1, u_1} P J
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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
refine_1 : (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure ≤ colimitsOfShape.{v', u', v_1, u_1} P J
⊢ (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure = colimitsOfShape.{v', u', v_1, u_1} P J
have refine_2 : colimitsOfShape.{v', u', v_1, u_1} P J ≤ (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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
⊢ (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure ≤ colimitsOfShape.{v', u', v_1, u_1} P J
have refine_1 : strictColimitsOfShape.{v', u', v_1, u_1} P J ≤ colimitsOfShape.{v', u', v_1, u_1} P J
Tactic: rw [isoClosure_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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
X : C
⊢ colimitsOfShape.{v', u', v_1, u_1} P J X ≤ (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure X
have refine_2 : ∀ (h : ColimitOfShape.{v', u', v_1, u_1} P J X), (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure X
Tactic: ⟨h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (hypothesis)
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
X : C
h : ColimitOfShape.{v', u', v_1, u_1} P J X
⊢ (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure X
have this : HasColimit h.toColimitPresentation (P := P).diag
Tactic: have := h.hasColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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
Q : ObjectProperty.{v_1, u_1} C
hPQ : P ≤ Q
X : C
⊢ colimitsOfShape.{v', u', v_1, u_1} P J X ≤ colimitsOfShape.{v', u', v_1, u_1} Q J X
have this : ∀ (h : ColimitOfShape.{v', u', v_1, u_1} P J X), colimitsOfShape.{v', u', v_1, u_1} Q J X
Tactic: ⟨h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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
⊢ colimitsOfShape.{v', u', v_1, u_1} P.isoClosure J = colimitsOfShape.{v', u', v_1, u_1} P J
have refine : colimitsOfShape.{v', u', v_1, u_1} P.isoClosure J ≤ colimitsOfShape.{v', u', v_1, u_1} P J
Tactic: refine le_antisymm ?_ (colimitsOfShape_monotone _ (P.le_isoClosure))
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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
X : C
⊢ colimitsOfShape.{v', u', v_1, u_1} P.isoClosure J X ≤ colimitsOfShape.{v', u', v_1, u_1} P J X
have this : ∀ (h : ColimitOfShape.{v', u', v_1, u_1} P.isoClosure J X), colimitsOfShape.{v', u', v_1, u_1} P J X
Tactic: ⟨h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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
X : C
h : ColimitOfShape.{v', u', v_1, u_1} P.isoClosure J X
⊢ colimitsOfShape.{v', u', v_1, u_1} P J X
have choose : ∀ (obj : (j : J) → C) (h₁ : ∀ (j : J), P (obj j))
  (h₂ : ∀ (j : J), Nonempty.{v_1 + 1} (h.toColimitPresentation (P := P.isoClosure).diag.obj j ≅ obj j)),
  colimitsOfShape.{v', u', v_1, u_1} P J X
Tactic: choose obj h₁ h₂ using h.prop_diag_obj
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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.Small.{w, v_1, u_1} (strictColimitsOfShape.{v', u', v_1, u_1} P J)
have refine : Function.Surjective (β := Subtype (strictColimitsOfShape.{v', u', v_1, u_1} P J))
  fun (F : { F : Functor.{v', v_1, u', u_1} J P.FullSubcategory // HasColimit (F ⋙ P.ι) }) ↦
  Subtype.mk (p := strictColimitsOfShape.{v', u', v_1, u_1} P J) (colimit ((↑F : J ⥤ P.FullSubcategory) ⋙ P.ι)) sorry
Tactic: refine small_of_surjective
    (f := fun (F : { F : J ⥤ P.FullSubcategory // HasColimit (F ⋙ P.ι) }) ↦
      (⟨_, letI := F.2; ⟨F.1 ⋙ P.ι, fun j ↦ (F.1.obj j).2⟩⟩)) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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 : strictColimitsOfShape.{v', u', v_1, u_1} P J ≤ P
| P
have rw : P.isoClosure
Tactic: rw [← P.isoClosure_eq_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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 : strictColimitsOfShape.{v', u', v_1, u_1} P J ≤ P
⊢ colimitsOfShape.{v', u', v_1, u_1} P J ≤ P
have conv_rhs : colimitsOfShape.{v', u', v_1, u_1} P J ≤ P.isoClosure
Tactic: conv_rhs => rw [← P.isoClosure_eq_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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 : strictColimitsOfShape.{v', u', v_1, u_1} P J ≤ P
⊢ colimitsOfShape.{v', u', v_1, u_1} P J ≤ P.isoClosure
have rw : (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure ≤ P.isoClosure
Tactic: rw [← isoClosure_strictColimitsOfShape]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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
⊢ LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) (colimitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥
have rw : LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) ⊥ ⊥
Tactic: rw [colimitsOfShape_bot]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J ↔
    IsClosedUnderColimitsOfShape.{v', u', v_2, u_2} P J
have refine : ∀ (H : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J),
  IsClosedUnderColimitsOfShape.{v', u', v_2, u_2} P J
Tactic: refine ⟨fun H ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (goal)
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 : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J
⊢ IsClosedUnderColimitsOfShape.{v', u', v_2, u_2} P J
have h : P = (P.inverseImage e.functor).inverseImage e.inverse
Tactic: convert!
    (inferInstance :
      ((P.inverseImage e.functor).inverseImage e.inverse).IsClosedUnderColimitsOfShape J)