awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ P = (P.inverseImage e.functor).inverseImage e.inverse
have h : ∀ (X : D), P X ↔ (P.inverseImage e.functor).inverseImage e.inverse X
Tactic: ext X
-- 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 J = ObjectProperty.unop (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ)
have h : ∀ (X : C),
  colimitsOfShape.{v', u', v_1, u_1} P J X ↔
    ObjectProperty.unop.{v_1, u_1} (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X
Tactic: ext X
-- 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 ↔
    ObjectProperty.unop.{v_1, u_1} (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X
have h : colimitsOfShape.{v', u', v_1, u_1} P J X →
  (h : ColimitOfShape.{v', u', v_1, u_1} P J X) → LimitOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ (Opposite.op X)
Tactic: refine ⟨fun ⟨h⟩ => ⟨?_⟩, fun ⟨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 :
  colimitsOfShape.{v', u', v_1, u_1} P J X →
    (h : ColimitOfShape.{v', u', v_1, u_1} P J X) → LimitOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ (Opposite.op X)
⊢ colimitsOfShape.{v', u', v_1, u_1} P J X ↔
    ObjectProperty.unop.{v_1, u_1} (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X
have h₁ : ObjectProperty.unop.{v_1, u_1} (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X →
  (h : LimitOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ (Opposite.op X)) → ColimitOfShape.{v', u', v_1, u_1} P J X
Tactic: refine ⟨fun ⟨h⟩ => ⟨?_⟩, fun ⟨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
⊢ limitsOfShape.{v', u', v_1, u_1} P J = ObjectProperty.unop (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ)
have h : ∀ (X : C),
  limitsOfShape.{v', u', v_1, u_1} P J X ↔
    ObjectProperty.unop.{v_1, u_1} (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X
Tactic: ext X
-- 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
⊢ limitsOfShape.{v', u', v_1, u_1} P J X ↔
    ObjectProperty.unop.{v_1, u_1} (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X
have h : limitsOfShape.{v', u', v_1, u_1} P J X →
  (h : LimitOfShape.{v', u', v_1, u_1} P J X) → ColimitOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ (Opposite.op X)
Tactic: refine ⟨fun ⟨h⟩ => ⟨?_⟩, fun ⟨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 :
  limitsOfShape.{v', u', v_1, u_1} P J X →
    (h : LimitOfShape.{v', u', v_1, u_1} P J X) → ColimitOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ (Opposite.op X)
⊢ limitsOfShape.{v', u', v_1, u_1} P J X ↔
    ObjectProperty.unop.{v_1, u_1} (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X
have h₁ : ObjectProperty.unop.{v_1, u_1} (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X →
  (h : ColimitOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ (Opposite.op X)) → LimitOfShape.{v', u', v_1, u_1} P J X
Tactic: refine ⟨fun ⟨h⟩ => ⟨?_⟩, fun ⟨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
⊢ limitsOfShape.{v', u', v_1, u_1} P.op J = (colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ).op
have rw : Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (limitsOfShape.{v', u', v_1, u_1} P.op J)
  (ObjectProperty.op (ObjectProperty.unop (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖᵒᵖ)))
Tactic: rw [colimitsOfShape_eq_unop_limitsOfShape, op_unop,
    P.op.limitsOfShape_congr (opOpEquivalence J)]
-- 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
rw :
  Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (limitsOfShape.{v', u', v_1, u_1} P.op J)
    (ObjectProperty.op (ObjectProperty.unop (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖᵒᵖ)))
⊢ limitsOfShape.{v', u', v_1, u_1} P.op J = (colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ).op
have rw₁ : Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (limitsOfShape.{v', u', v_1, u_1} P.op J)
  (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖᵒᵖ)
Tactic: rw [colimitsOfShape_eq_unop_limitsOfShape, op_unop,
    P.op.limitsOfShape_congr (opOpEquivalence J)]
-- 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
rw :
  Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (limitsOfShape.{v', u', v_1, u_1} P.op J)
    (ObjectProperty.op (ObjectProperty.unop (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖᵒᵖ)))
rw₁ :
  Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (limitsOfShape.{v', u', v_1, u_1} P.op J)
    (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖᵒᵖ)
⊢ limitsOfShape.{v', u', v_1, u_1} P.op J = (colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ).op
have rw₂ : Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (limitsOfShape.{v', u', v_1, u_1} P.op J)
  (limitsOfShape.{v', u', v_1, u_1} P.op J)
Tactic: rw [colimitsOfShape_eq_unop_limitsOfShape, op_unop,
    P.op.limitsOfShape_congr (opOpEquivalence J)]
-- 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.op J = (limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ).op
have rw : Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (colimitsOfShape.{v', u', v_1, u_1} P.op J)
  (ObjectProperty.op (ObjectProperty.unop (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖᵒᵖ)))
Tactic: rw [limitsOfShape_eq_unop_colimitsOfShape, op_unop,
    P.op.colimitsOfShape_congr (opOpEquivalence J)]
-- 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
rw :
  Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (colimitsOfShape.{v', u', v_1, u_1} P.op J)
    (ObjectProperty.op (ObjectProperty.unop (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖᵒᵖ)))
⊢ colimitsOfShape.{v', u', v_1, u_1} P.op J = (limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ).op
have rw₁ : Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (colimitsOfShape.{v', u', v_1, u_1} P.op J)
  (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖᵒᵖ)
Tactic: rw [limitsOfShape_eq_unop_colimitsOfShape, op_unop,
    P.op.colimitsOfShape_congr (opOpEquivalence J)]
-- 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
rw :
  Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (colimitsOfShape.{v', u', v_1, u_1} P.op J)
    (ObjectProperty.op (ObjectProperty.unop (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖᵒᵖ)))
rw₁ :
  Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (colimitsOfShape.{v', u', v_1, u_1} P.op J)
    (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖᵒᵖ)
⊢ colimitsOfShape.{v', u', v_1, u_1} P.op J = (limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ).op
have rw₂ : Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (colimitsOfShape.{v', u', v_1, u_1} P.op J)
  (colimitsOfShape.{v', u', v_1, u_1} P.op J)
Tactic: rw [limitsOfShape_eq_unop_colimitsOfShape, op_unop,
    P.op.colimitsOfShape_congr (opOpEquivalence J)]
-- 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
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P J ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
have rw : colimitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    colimitsOfShape_eq_unop_limitsOfShape, ← op_monotone_iff, op_unop]
-- 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
rw : colimitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P J ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
have rw₁ : colimitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    colimitsOfShape_eq_unop_limitsOfShape, ← op_monotone_iff, op_unop]
-- 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
rw : colimitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
rw₁ : colimitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P J ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
have rw₂ : ObjectProperty.unop (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) ≤ P ↔ limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    colimitsOfShape_eq_unop_limitsOfShape, ← op_monotone_iff, op_unop]
-- 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
rw : colimitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
rw₁ : colimitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₂ :
  ObjectProperty.unop (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) ≤ P ↔ limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P J ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
have rw₃ : ObjectProperty.op (ObjectProperty.unop (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ)) ≤ P.op ↔
  limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    colimitsOfShape_eq_unop_limitsOfShape, ← op_monotone_iff, op_unop]
-- 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
rw : colimitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
rw₁ : colimitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₂ :
  ObjectProperty.unop (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) ≤ P ↔ limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₃ :
  ObjectProperty.op (ObjectProperty.unop (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ)) ≤ P.op ↔
    limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P J ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
have rw₄ : limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op ↔ limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    colimitsOfShape_eq_unop_limitsOfShape, ← op_monotone_iff, op_unop]
-- 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
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J ↔ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
have rw : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J ↔ colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    limitsOfShape_eq_unop_colimitsOfShape, ← op_monotone_iff, op_unop]
-- 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
rw : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J ↔ colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J ↔ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
have rw₁ : limitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    limitsOfShape_eq_unop_colimitsOfShape, ← op_monotone_iff, op_unop]
-- 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
rw : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J ↔ colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₁ : limitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J ↔ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
have rw₂ : ObjectProperty.unop (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) ≤ P ↔
  colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    limitsOfShape_eq_unop_colimitsOfShape, ← op_monotone_iff, op_unop]
-- 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
rw : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J ↔ colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₁ : limitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₂ :
  ObjectProperty.unop (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) ≤ P ↔
    colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J ↔ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
have rw₃ : ObjectProperty.op (ObjectProperty.unop (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ)) ≤ P.op ↔
  colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    limitsOfShape_eq_unop_colimitsOfShape, ← op_monotone_iff, op_unop]
-- 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
rw : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J ↔ colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₁ : limitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₂ :
  ObjectProperty.unop (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) ≤ P ↔
    colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₃ :
  ObjectProperty.op (ObjectProperty.unop (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ)) ≤ P.op ↔
    colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J ↔ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
have rw₄ : colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op ↔ colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    limitsOfShape_eq_unop_colimitsOfShape, ← op_monotone_iff, op_unop]
-- 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
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op J
have rw : colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op J
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    limitsOfShape_op, op_monotone_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
rw : colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op J
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op J
have rw₁ : colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ limitsOfShape.{v', u', v_1, u_1} P.op J ≤ P.op
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    limitsOfShape_op, op_monotone_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
rw : colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op J
rw₁ : colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ limitsOfShape.{v', u', v_1, u_1} P.op J ≤ P.op
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op J
have rw₂ : colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ (colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ).op ≤ P.op
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    limitsOfShape_op, op_monotone_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
rw : colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op J
rw₁ : colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ limitsOfShape.{v', u', v_1, u_1} P.op J ≤ P.op
rw₂ : colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ (colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ).op ≤ P.op
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op J
have rw₃ : colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    limitsOfShape_op, op_monotone_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
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ↔ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P.op J
have rw : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ↔ colimitsOfShape.{v', u', v_1, u_1} P.op J ≤ P.op
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    colimitsOfShape_op, op_monotone_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
rw : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ↔ colimitsOfShape.{v', u', v_1, u_1} P.op J ≤ P.op
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ↔ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P.op J
have rw₁ : limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ colimitsOfShape.{v', u', v_1, u_1} P.op J ≤ P.op
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    colimitsOfShape_op, op_monotone_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
rw : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ↔ colimitsOfShape.{v', u', v_1, u_1} P.op J ≤ P.op
rw₁ : limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ colimitsOfShape.{v', u', v_1, u_1} P.op J ≤ P.op
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ↔ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P.op J
have rw₂ : limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ (limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ).op ≤ P.op
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    colimitsOfShape_op, op_monotone_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
rw : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ↔ colimitsOfShape.{v', u', v_1, u_1} P.op J ≤ P.op
rw₁ : limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ colimitsOfShape.{v', u', v_1, u_1} P.op J ≤ P.op
rw₂ : limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ (limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ).op ≤ P.op
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ↔ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P.op J
have rw₃ : limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P
Tactic: rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    colimitsOfShape_op, op_monotone_iff]
-- 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 : P.IsClosedUnderColimitsOfShape WalkingParallelPair
X Y : C
h : Retract X Y
hY : P Y
c : Cofork (h.r ≫ h.i) (𝟙 Y) := Cofork.ofπ h.r ⋯
⊢ P X
have have : ∀ (hc : IsColimit c), P X
Tactic: have hc : IsColimit c :=
      Cofork.IsColimit.mk _ (fun s ↦ h.i ≫ s.π)
        (fun s ↦ by simpa using s.condition)
        (fun s m hm ↦ by dsimp [c] at hm; simp [← hm])
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
⊢ (P ⊔ Q).isoClosure = P.isoClosure ⊔ Q.isoClosure
have h : ∀ (X : C), (P ⊔ Q).isoClosure X ↔ (P.isoClosure ⊔ Q.isoClosure) X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X : C
⊢ (P ⊔ Q).isoClosure X ↔ P.isoClosure X ∨ Q.isoClosure X
have h : (P ⊔ Q).isoClosure X → P.isoClosure X ∨ Q.isoClosure X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X : C
h : (P ⊔ Q).isoClosure X → P.isoClosure X ∨ Q.isoClosure X
⊢ (P ⊔ Q).isoClosure X ↔ P.isoClosure X ∨ Q.isoClosure X
have h₁ : P.isoClosure X ∨ Q.isoClosure X → (P ⊔ Q).isoClosure X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X Y : C
hY : (P ⊔ Q) Y
e : X ≅ Y
⊢ P.isoClosure X ∨ Q.isoClosure X
have hY₁ : P Y ∨ Q Y
Tactic: simp only [prop_sup_iff] at hY
Cleared hypotheses: hY