awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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
rw₃ rw₄ : colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op J

Tactic:
rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    limitsOfShape_op, op_monotone_iff]

Premises used: CategoryTheory.ObjectProperty.limitsOfShape_op, CategoryTheory.ObjectProperty.op_monotone_iff, CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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
rw₃ rw₄ : limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P ↔ limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ≤ P
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ ↔ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P.op J

Tactic:
rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    colimitsOfShape_op, op_monotone_iff]

Premises used: CategoryTheory.ObjectProperty.colimitsOfShape_op, CategoryTheory.ObjectProperty.op_monotone_iff, CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 rwa rwa₁ rwa₂ rwa₃ : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P J
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ

Tactic:
rwa [← isClosedUnderColimitsOfShape_iff_op]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_op
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 rwa rwa₁ rwa₂ rwa₃ : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ

Tactic:
rwa [← isClosedUnderLimitsOfShape_iff_op]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff_op
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 rwa rwa₁ rwa₂ rwa₃ : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op J

Tactic:
rwa [← isClosedUnderColimitsOfShape_op_iff_op]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_op_iff_op
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 rwa rwa₁ rwa₂ rwa₃ : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P.op J

Tactic:
rwa [← isClosedUnderLimitsOfShape_op_iff_op]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_op_iff_op
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
Q : ObjectProperty.{v_1, u_1} Cᵒᵖ
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} Q J ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} Q.unop Jᵒᵖ

Tactic:
(Q.unop.isClosedUnderLimitsOfShape_op_iff_op J).symm

Premises used: CategoryTheory.ObjectProperty.unop, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_op_iff_op, CategoryTheory.ObjectProperty.op, Iff.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
Q : ObjectProperty.{v_1, u_1} Cᵒᵖ
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} Q J ↔ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} Q.unop Jᵒᵖ

Tactic:
(Q.unop.isClosedUnderColimitsOfShape_op_iff_op J).symm

Premises used: CategoryTheory.ObjectProperty.unop, CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_op_iff_op, CategoryTheory.ObjectProperty.op, Iff.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
Q : ObjectProperty.{v_1, u_1} Cᵒᵖ
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} Q Jᵒᵖ ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} Q.unop J

Tactic:
(Q.unop.isClosedUnderLimitsOfShape_iff_op J).symm

Premises used: CategoryTheory.ObjectProperty.unop, CategoryTheory.ObjectProperty.op, Iff.symm, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff_op
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
Q : ObjectProperty.{v_1, u_1} Cᵒᵖ
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} Q Jᵒᵖ ↔ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} Q.unop J

Tactic:
(Q.unop.isClosedUnderColimitsOfShape_iff_op J).symm

Premises used: CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_op, CategoryTheory.ObjectProperty.unop, CategoryTheory.ObjectProperty.op, Iff.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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'
Q : ObjectProperty.{v_1, u_1} Cᵒᵖ
inst_4 rwa rwa₁ rwa₂ rwa₃ : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} Q J
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} Q.unop Jᵒᵖ

Tactic:
rwa [← isClosedUnderColimitsOfShape_iff_unop]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_unop
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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'
Q : ObjectProperty.{v_1, u_1} Cᵒᵖ
inst_4 rwa rwa₁ rwa₂ rwa₃ : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} Q J
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} Q.unop Jᵒᵖ

Tactic:
rwa [← isClosedUnderLimitsOfShape_iff_unop]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff_unop
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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'
Q : ObjectProperty.{v_1, u_1} Cᵒᵖ
inst_4 rwa rwa₁ rwa₂ rwa₃ : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} Q Jᵒᵖ
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} Q.unop J

Tactic:
rwa [← isClosedUnderColimitsOfShape_op_iff_unop]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_op_iff_unop
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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'
Q : ObjectProperty.{v_1, u_1} Cᵒᵖ
inst_4 rwa rwa₁ rwa₂ rwa₃ : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} Q Jᵒᵖ
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} Q.unop J

Tactic:
rwa [← isClosedUnderLimitsOfShape_op_iff_unop]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_op_iff_unop
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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
⊢ (h.r ≫ h.i) ≫ h.r = 𝟙 Y ≫ h.r

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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
let : P X
⊢ P X

Tactic:
let c : Cofork (h.r ≫ h.i) (𝟙 Y) := Cofork.ofπ h.r (by simp)
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 ⋯
s : Cofork (h.r ≫ h.i) (𝟙 Y)
⊢ c.π ≫ (fun (s : Cofork (h.r ≫ h.i) (𝟙 Y)) ↦ h.i ≫ s.π) s = s.π

Tactic:
simpa using s.condition

Premises used: CategoryTheory.Limits.Cofork.condition
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 ⋯
s : Cofork (h.r ≫ h.i) (𝟙 Y)
m : c.pt ⟶ s.pt
hm : h.r ≫ m = s.π
⊢ m = (fun (s : Cofork (h.r ≫ h.i) (𝟙 Y)) ↦ h.i ≫ s.π) s

Tactic:
simp [← hm]
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 ⋯
have : ∀ (hc : IsColimit c), P X
⊢ 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])
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 ⋯
hc : IsColimit c
⊢ P ((parallelPair (h.r ≫ h.i) (𝟙 Y)).obj WalkingParallelPair.zero)

Tactic:
hY
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 ⋯
hc : IsColimit c
⊢ P ((parallelPair (h.r ≫ h.i) (𝟙 Y)).obj WalkingParallelPair.zero)

Tactic:
exact hY
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 ⋯
hc : IsColimit c
⊢ P ((parallelPair (h.r ≫ h.i) (𝟙 Y)).obj WalkingParallelPair.one)

Tactic:
hY
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 ⋯
hc : IsColimit c
⊢ P ((parallelPair (h.r ≫ h.i) (𝟙 Y)).obj WalkingParallelPair.one)

Tactic:
exact hY
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 ⋯
hc : IsColimit c
⊢ P X

Tactic:
exact P.prop_of_isColimit hc (by rintro (_ | _) <;> exact hY)

Premises used: CategoryTheory.ObjectProperty.prop_of_isColimit
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : IsEmpty J
X : C
h_1 : Nonempty (IsTerminal.{v_1, u_1} X)
h : IsTerminal.{v_1, u_1} X
⊢ ∀ (j : J),
    P
      (Functor.obj.{v', v_1, u', u_1}
        (LimitPresentation.diag (X := X)
          { diag := Functor.obj (Functor.const J) X, π := 𝟙 (Functor.obj (Functor.const J) X),
            isLimit :=
              (Equiv.symm (isLimitEquivIsTerminalOfIsEmpty C { pt := X, π := 𝟙 (Functor.obj (Functor.const J) X) }) :
                  (a : IsTerminal { pt := X, π := 𝟙 ((Functor.const J).obj X) }.pt) →
                    IsLimit { pt := X, π := 𝟙 ((Functor.const J).obj X) })
                h })
        j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
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 : IsEmpty J
X : C
h_1 : Nonempty (IsInitial.{v_1, u_1} X)
h : IsInitial.{v_1, u_1} X
⊢ ∀ (j : J),
    P
      (Functor.obj.{v', v_1, u', u_1}
        (ColimitPresentation.diag (X := X)
          { diag := Functor.obj (Functor.const J) X, ι := 𝟙 (Functor.obj (Functor.const J) X),
            isColimit :=
              (Equiv.symm (isColimitEquivIsInitialOfIsEmpty C { pt := X, ι := 𝟙 (Functor.obj (Functor.const J) X) }) :
                  (a : IsInitial { pt := X, ι := 𝟙 ((Functor.const J).obj X) }.pt) →
                    IsColimit { pt := X, ι := 𝟙 ((Functor.const J).obj X) })
                h })
        j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X : C
⊢ (P ⊓ Q) X ↔ P X ∧ Q X

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X : C
⊢ (P ⊔ Q) X ↔ P X ∨ Q X

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X : C
inst_1 : P.Nonempty
⊢ (P ⊔ Q).Nonempty

Tactic:
nonempty_of_prop (Or.inl P.prop_arbitrary)

Premises used: CategoryTheory.ObjectProperty.nonempty_of_prop, Or.inl, CategoryTheory.ObjectProperty.prop_arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X : C
inst_1 : Q.Nonempty
⊢ (P ⊔ Q).Nonempty

Tactic:
nonempty_of_prop (Or.inr Q.prop_arbitrary)

Premises used: CategoryTheory.ObjectProperty.nonempty_of_prop, Or.inr, CategoryTheory.ObjectProperty.prop_arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X : C
inst_1 : Nonempty C
⊢ ⊤ (Classical.arbitrary C)

Tactic:
trivial
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : ∀ (X : C), (P ⊔ Q).isoClosure X ↔ (P.isoClosure ⊔ Q.isoClosure) X
⊢ (P ⊔ Q).isoClosure = P.isoClosure ⊔ Q.isoClosure

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
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
h₁ : P.isoClosure X ∨ Q.isoClosure X → (P ⊔ Q).isoClosure X
⊢ (P ⊔ Q).isoClosure X ↔ P.isoClosure X ∨ Q.isoClosure X

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
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 Y ∨ Q Y

Tactic:
simp only [prop_sup_iff] at hY

Premises used: CategoryTheory.ObjectProperty.prop_sup_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X Y : C
e : X ≅ Y
hY : P Y ∨ Q Y
h : ∀ (hY : P Y), P.isoClosure X ∨ Q.isoClosure X
h₁ : ∀ (hY : Q Y), P.isoClosure X ∨ Q.isoClosure X
⊢ P.isoClosure X ∨ Q.isoClosure X

Tactic:
obtain hY | hY := hY
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X Y : C
e : X ≅ Y
hY : P Y
⊢ P.isoClosure X ∨ Q.isoClosure X

Tactic:
Or.inl ⟨Y, hY, ⟨e⟩⟩

Premises used: Nonempty.intro, Exists.intro, Or.inl
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X Y : C
e : X ≅ Y
hY : P Y
⊢ P.isoClosure X ∨ Q.isoClosure X

Tactic:
exact Or.inl ⟨Y, hY, ⟨e⟩⟩

Premises used: Or.inl
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X Y : C
e : X ≅ Y
hY : Q Y
⊢ P.isoClosure X ∨ Q.isoClosure X

Tactic:
Or.inr ⟨Y, hY, ⟨e⟩⟩

Premises used: Nonempty.intro, Exists.intro, Or.inr
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X Y : C
e : X ≅ Y
hY : Q Y
⊢ P.isoClosure X ∨ Q.isoClosure X

Tactic:
exact Or.inr ⟨Y, hY, ⟨e⟩⟩

Premises used: Or.inr
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X : C
hY : P.isoClosure X
⊢ (P ⊔ Q).isoClosure X

Tactic:
monotone_isoClosure le_sup_left _ hY

Premises used: le_sup_left, CategoryTheory.ObjectProperty.monotone_isoClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X : C
hY : P.isoClosure X
⊢ (P ⊔ Q).isoClosure X

Tactic:
exact monotone_isoClosure le_sup_left _ hY

Premises used: le_sup_left, CategoryTheory.ObjectProperty.monotone_isoClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X : C
hY : Q.isoClosure X
⊢ (P ⊔ Q).isoClosure X

Tactic:
monotone_isoClosure le_sup_right _ hY

Premises used: le_sup_right, CategoryTheory.ObjectProperty.monotone_isoClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X : C
hY : Q.isoClosure X
⊢ (P ⊔ Q).isoClosure X

Tactic:
exact monotone_isoClosure le_sup_right _ hY

Premises used: le_sup_right, CategoryTheory.ObjectProperty.monotone_isoClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X : C
inst_1 : P.IsClosedUnderIsomorphisms
inst_2 : Q.IsClosedUnderIsomorphisms
⊢ (P ⊔ Q).IsClosedUnderIsomorphisms

Tactic:
simp only [isClosedUnderIsomorphisms_iff_isoClosure_eq_self, isoClosure_sup, isoClosure_eq_self]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderIsomorphisms_iff_isoClosure_eq_self, CategoryTheory.ObjectProperty.isoClosure_sup, CategoryTheory.ObjectProperty.isoClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
X : C
⊢ ∀ {X Y : C} (x : X ≅ Y), ⊤ X → ⊤ Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
X : C
⊢ (⨆ (a : α), P a) X ↔ ∃ (a : α), P a X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
a : α
inst_1 : (P a).Nonempty
⊢ ObjectProperty.Nonempty.{v, u} (C := C) (⨆ (a : α), P a)

Tactic:
nonempty_of_prop ((prop_iSup_iff P _).mpr ⟨a, (P a).prop_arbitrary⟩)

Premises used: Iff.mpr, CategoryTheory.ObjectProperty.nonempty_of_prop, Exists.intro, CategoryTheory.ObjectProperty.prop_arbitrary, CategoryTheory.ObjectProperty.prop_iSup_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
⊢ Eq.{u + 1} (α := ObjectProperty.{v, u} C) (isoClosure (⨆ (a : α), P a)) (⨆ (a : α), (P a).isoClosure)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
refine_1 : LE.le.{u} (α := ObjectProperty.{v, u} C) (isoClosure (⨆ (a : α), P a)) (⨆ (a : α), (P a).isoClosure)
refine_2 : LE.le.{u} (α := ObjectProperty.{v, u} C) (⨆ (a : α), (P a).isoClosure) (isoClosure (⨆ (a : α), P a))
⊢ Eq.{u + 1} (α := ObjectProperty.{v, u} C) (isoClosure (⨆ (a : α), P a)) (⨆ (a : α), (P a).isoClosure)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
X Y : C
hY : (⨆ (a : α), P a) Y
e : X ≅ Y
refine_1 : ∀ (hY : ∃ (a : α), P a Y), ∃ (a : α), (P a).isoClosure X
⊢ (⨆ (a : α), (P a).isoClosure) X

Tactic:
simp only [prop_iSup_iff] at hY ⊢

Premises used: CategoryTheory.ObjectProperty.prop_iSup_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
X Y : C
e : X ≅ Y
hY : ∃ (a : α), P a Y
refine_1 : ∀ (a : α) (hY : P a Y), ∃ (a : α), (P a).isoClosure X
⊢ ∃ (a : α), (P a).isoClosure X

Tactic:
obtain ⟨a, hY⟩ := hY
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
X Y : C
e : X ≅ Y
a : α
hY : P a Y
⊢ ∃ (a : α), (P a).isoClosure X

Tactic:
⟨a, _, hY, ⟨e⟩⟩

Premises used: Nonempty.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
X Y : C
e : X ≅ Y
a : α
hY : P a Y
⊢ ∃ (a : α), (P a).isoClosure X

Tactic:
exact ⟨a, _, hY, ⟨e⟩⟩