awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (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
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J ↔
    IsClosedUnderLimitsOfShape.{v', u', v_2, u_2} P J
have refine : ∀ (H : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J),
  IsClosedUnderLimitsOfShape.{v', u', v_2, u_2} P J
Tactic: refine ⟨fun H ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (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 : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J
⊢ IsClosedUnderLimitsOfShape.{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).IsClosedUnderLimitsOfShape J)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (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 : IsClosedUnderLimitsOfShape.{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.Local (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
Z Z' : C
e : Z ≅ Z'
hZ : W.isLocal Z
X Y : C
f : X ⟶ Y
hf : W f
⊢ Function.Bijective (β := X ⟶ Z') fun (g : Y ⟶ Z') ↦ f ≫ g
have rw : Function.Bijective (α := Y ⟶ Z) (β := X ⟶ Z') ((fun (g : Y ⟶ Z') ↦ f ≫ g) ∘ (⇑e.homToEquiv : (a : Y ⟶ Z) → Y ⟶ Z'))
Tactic: rw [← Function.Bijective.of_comp_iff _ (Iso.homToEquiv e).bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Local (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
Z Z' : C
e : Z ≅ Z'
hZ : W.isLocal Z
X Y : C
f : X ⟶ Y
hf : W f
⊢ Function.Bijective (α := Y ⟶ Z) (β := X ⟶ Z') ((fun (g : Y ⟶ Z') ↦ f ≫ g) ∘ (⇑e.homToEquiv : (a : Y ⟶ Z) → Y ⟶ Z'))
have h : Eq (α := (Y ⟶ Z) → (X ⟶ Z')) ((fun (g : Y ⟶ Z') ↦ f ≫ g) ∘ (⇑e.homToEquiv : (a : Y ⟶ Z) → Y ⟶ Z'))
  (Function.comp (β := X ⟶ Z) (⇑e.homToEquiv : (a : X ⟶ Z) → X ⟶ Z') fun (g : Y ⟶ Z) ↦ f ≫ g)
Tactic: convert! (Iso.homToEquiv e).bijective.comp (hZ f hf) using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Local (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
X X' : C
e : X ≅ X'
hX : W.isColocal X
Y Z : C
g : Y ⟶ Z
hg : W g
⊢ Function.Bijective (β := X' ⟶ Z) fun (f : X' ⟶ Y) ↦ f ≫ g
have rw : Function.Bijective (α := X ⟶ Y) (β := X' ⟶ Z) ((fun (f : X' ⟶ Y) ↦ f ≫ g) ∘ (⇑e.homFromEquiv : (a : X ⟶ Y) → X' ⟶ Y))
Tactic: rw [← Function.Bijective.of_comp_iff _ (Iso.homFromEquiv e).bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Local (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
X X' : C
e : X ≅ X'
hX : W.isColocal X
Y Z : C
g : Y ⟶ Z
hg : W g
⊢ Function.Bijective (α := X ⟶ Y) (β := X' ⟶ Z) ((fun (f : X' ⟶ Y) ↦ f ≫ g) ∘ (⇑e.homFromEquiv : (a : X ⟶ Y) → X' ⟶ Y))
have h : Eq (α := (X ⟶ Y) → (X' ⟶ Z)) ((fun (f : X' ⟶ Y) ↦ f ≫ g) ∘ (⇑e.homFromEquiv : (a : X ⟶ Y) → X' ⟶ Y))
  (Function.comp (β := X ⟶ Z) (⇑e.homFromEquiv : (a : X ⟶ Z) → X' ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g)
Tactic: convert! (Iso.homFromEquiv e).bijective.comp (hX g hg) using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Local (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
Z : C
h : ObjectProperty.limitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.LimitOfShape.{v', u', v, u} W.isLocal J Z
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
have refine : ∀ (g : X ⟶ Z), ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
Tactic: refine ⟨fun g₁ g₂ h ↦ p.isLimit.hom_ext
      (fun j ↦ (p.prop_diag_obj j f hf).1 (by simp [reassoc_of% h])), fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Local (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
Z : C
h : ObjectProperty.limitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.LimitOfShape.{v', u', v, u} W.isLocal J Z
g : X ⟶ Z
⊢ ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
have choose : ∀ (app : (j : J) → Y ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj j)
  (h :
    ∀ (j : J),
      (fun (g : Y ⟶ p.toLimitPresentation (P := W.isLocal).diag.obj j) ↦ f ≫ g) (app j) =
        g ≫ p.toLimitPresentation (P := W.isLocal).π.app j),
  ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
Tactic: choose app h using fun j ↦ (p.prop_diag_obj j f hf).2 (g ≫ p.π.app j)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Local (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isColocal J X
Y Z : C
g : Y ⟶ Z
hg : W g
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isColocal J X
⊢ Function.Bijective (β := X ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g
have refine : ∀ (f : X ⟶ Z), ∃ (a : X ⟶ Y), (fun (f : X ⟶ Y) ↦ f ≫ g) a = f
Tactic: refine ⟨fun f₁ f₂ h ↦ p.isColimit.hom_ext
      (fun j ↦ (p.prop_diag_obj j g hg).1 (by simp [h])), fun f ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Local (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isColocal J X
Y Z : C
g : Y ⟶ Z
hg : W g
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isColocal J X
f : X ⟶ Z
⊢ ∃ (a : X ⟶ Y), (fun (f : X ⟶ Y) ↦ f ≫ g) a = f
have choose : ∀ (app : (j : J) → p.toColimitPresentation (P := W.isColocal).diag.obj j ⟶ Y)
  (h :
    ∀ (j : J),
      (fun (f : p.toColimitPresentation (P := W.isColocal).diag.obj j ⟶ Y) ↦ f ≫ g) (app j) =
        p.toColimitPresentation (P := W.isColocal).ι.app j ≫ f),
  ∃ (a : X ⟶ Y), (fun (f : X ⟶ Y) ↦ f ≫ g) a = f
Tactic: choose app h using fun j ↦ (p.prop_diag_obj j g hg).2 (p.ι.app j ≫ f)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P.op = Q.op
⊢ P = Q
have rw : P.op.unop = Q
Tactic: rw [← P.unop_op, ← Q.unop_op, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P.op = Q.op
rw : P.op.unop = Q
⊢ P = Q
have rw₁ : P.op.unop = Q.op.unop
Tactic: rw [← P.unop_op, ← Q.unop_op, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P.op = Q.op
rw : P.op.unop = Q
rw₁ : P.op.unop = Q.op.unop
⊢ P = Q
have rw₂ : Q.op.unop = Q.op.unop
Tactic: rw [← P.unop_op, ← Q.unop_op, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} Cᵒᵖ
h : P.unop = Q.unop
⊢ P = Q
have rw : P.unop.op = Q
Tactic: rw [← P.op_unop, ← Q.op_unop, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} Cᵒᵖ
h : P.unop = Q.unop
rw : P.unop.op = Q
⊢ P = Q
have rw₁ : P.unop.op = Q.unop.op
Tactic: rw [← P.op_unop, ← Q.op_unop, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} Cᵒᵖ
h : P.unop = Q.unop
rw : P.unop.op = Q
rw₁ : P.unop.op = Q.unop.op
⊢ P = Q
have rw₂ : Q.unop.op = Q.unop.op
Tactic: rw [← P.op_unop, ← Q.op_unop, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
⊢ Eq (α := ObjectProperty.{v, u} Cᵒᵖ) (ObjectProperty.op (ofObj X)) (ofObj fun (i : ι) ↦ op (X i))
have h : ∀ (Z : Cᵒᵖ), ObjectProperty.op.{v, u} (ofObj X) Z ↔ ofObj.{v, u, u_1} (fun (i : ι) ↦ op (X i)) Z
Tactic: ext Z
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ ObjectProperty.op.{v, u} (ofObj X) Z ↔ ofObj.{v, u, u_1} (fun (i : ι) ↦ op (X i)) Z
have h : (∃ (i : ι), X i = unop Z) ↔ ∃ (i : ι), op (X i) = Z
Tactic: simp only [op_iff, ofObj_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (∃ (i : ι), X i = unop Z) ↔ ∃ (i : ι), op (X i) = Z
have h : (∃ (i : ι), X i = unop Z) → ∃ (i : ι), op (X i) = Z
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
h : (∃ (i : ι), X i = unop Z) → ∃ (i : ι), op (X i) = Z
⊢ (∃ (i : ι), X i = unop Z) ↔ ∃ (i : ι), op (X i) = Z
have h₁ : (∃ (i : ι), op (X i) = Z) → ∃ (i : ι), X i = unop Z
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
i : ι
hi : X i = unop Z
⊢ op (X i) = Z
have rw : op (unop Z) = Z
Tactic: rw [hi]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
i : ι
hi : op (X i) = Z
⊢ X i = unop Z
have rw : X i = unop (op (X i))
Tactic: rw [← hi]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ P.isoClosure.op = P.op.isoClosure
have h : ∀ (X : C), P.isoClosure.op (op X) ↔ isoClosure.{v, u} P.op (op X)
Tactic: ext ⟨X⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
⊢ ObjectProperty.unop P.isoClosure = P.unop.isoClosure
have rw : ObjectProperty.op (ObjectProperty.unop P.isoClosure) = P.unop.isoClosure.op
Tactic: rw [← op_injective_iff, P.unop.op_isoClosure, op_unop, op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
rw : ObjectProperty.op (ObjectProperty.unop P.isoClosure) = P.unop.isoClosure.op
⊢ ObjectProperty.unop P.isoClosure = P.unop.isoClosure
have rw₁ : Eq (α := ObjectProperty.{v, u} Cᵒᵖ) (ObjectProperty.op (ObjectProperty.unop P.isoClosure)) P.unop.op.isoClosure
Tactic: rw [← op_injective_iff, P.unop.op_isoClosure, op_unop, op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
rw : ObjectProperty.op (ObjectProperty.unop P.isoClosure) = P.unop.isoClosure.op
rw₁ : Eq (α := ObjectProperty.{v, u} Cᵒᵖ) (ObjectProperty.op (ObjectProperty.unop P.isoClosure)) P.unop.op.isoClosure
⊢ ObjectProperty.unop P.isoClosure = P.unop.isoClosure
have rw₂ : Eq (α := ObjectProperty.{v, u} Cᵒᵖ) (P.isoClosure : ObjectProperty.{v, u} Cᵒᵖ) P.unop.op.isoClosure
Tactic: rw [← op_injective_iff, P.unop.op_isoClosure, op_unop, op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Opposite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
rw : ObjectProperty.op (ObjectProperty.unop P.isoClosure) = P.unop.isoClosure.op
rw₁ : Eq (α := ObjectProperty.{v, u} Cᵒᵖ) (ObjectProperty.op (ObjectProperty.unop P.isoClosure)) P.unop.op.isoClosure
rw₂ : Eq (α := ObjectProperty.{v, u} Cᵒᵖ) (P.isoClosure : ObjectProperty.{v, u} Cᵒᵖ) P.unop.op.isoClosure
⊢ ObjectProperty.unop P.isoClosure = P.unop.isoClosure
have rw₃ : Eq (α := ObjectProperty.{v, u} Cᵒᵖ) (P.isoClosure : ObjectProperty.{v, u} Cᵒᵖ) P.isoClosure
Tactic: rw [← op_injective_iff, P.unop.op_isoClosure, op_unop, op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P : ObjectProperty.{v, u} C
X_1 Y : C
e : X_1 ≅ Y
h : P.rightOrthogonal X_1
X : C
f : X ⟶ Y
hX : P X
⊢ f = 0
have rw : f ≫ e.inv = 0
Tactic: rw [← cancel_mono e.inv, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P : ObjectProperty.{v, u} C
X Y_1 : C
e : X ≅ Y_1
h : P.leftOrthogonal X
Y : C
f : Y_1 ⟶ Y
hY : P Y
⊢ f = 0
have rw : e.hom ≫ f = 0
Tactic: rw [← cancel_epi e.hom, comp_zero]
-- 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 : P.IsStableUnderRetracts
⊢ P.retractClosure = P
have a : P.retractClosure ≤ P
Tactic: apply le_antisymm
-- 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 : P.IsStableUnderRetracts
a : P.retractClosure ≤ P
⊢ P.retractClosure = P
have a₁ : P ≤ P.retractClosure
Tactic: apply le_antisymm
-- 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 : P.IsStableUnderRetracts
X : C
⊢ P.retractClosure X ≤ P X
have a : ∀ (Y : C) (hY : P Y) (e : Retract X Y), P X
Tactic: ⟨Y, hY, ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
inst_1 : Q.IsStableUnderRetracts
h : P ≤ Q
⊢ Q.retractClosure ≤ Q
have rw : Q ≤ Q
Tactic: rw [retractClosure_eq_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ P.isoClosure.retractClosure = P.retractClosure
have refine : P.isoClosure.retractClosure ≤ P.retractClosure
Tactic: refine le_antisymm ?_ (monotone_retractClosure P.le_isoClosure)
-- 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) (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure
have obtain : ∀ (Q : ObjectProperty.{v, u} C),
  ObjectProperty.Small.{w, v, u} Q →
    ∀ (h₁ : Q ≤ P) (h₂ : P ≤ Q.isoClosure),
      ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure
Tactic: obtain ⟨Q, _, h₁, h₂⟩ := ObjectProperty.EssentiallySmall.exists_small_le.{w} P
-- 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₁ : Q ≤ P
h₂ : 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
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure
have choose : ∀ (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 : α)),
  ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure
Tactic: choose X Y h hX using fun (a : Subtype R) ↦ a.2
-- 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₁ : Q ≤ P
h₂ : 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 : α)
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure
have refine : Q.isoClosure.retractClosure ≤ isoClosure (ofObj Y)
Tactic: refine ⟨.ofObj Y, inferInstance, (monotone_retractClosure h₂).trans ?_⟩
-- 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₁ : Q ≤ P
h₂ : 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 : α)
⊢ Q.isoClosure.retractClosure ≤ isoClosure (ofObj Y)
have rw : Q.retractClosure ≤ isoClosure (ofObj Y)
Tactic: rw [retractClosure_isoClosure]
-- 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₁ : Q ≤ P
h₂ : 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)), g (h a) h₁ = g r hx
have w : Q
  (X
    (Subtype.mk (p := R)
      (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)
          (r.r ≫ r.i) sorry))
      sorry))
Tactic: obtain ⟨_, hr⟩ := hX ⟨⟨⟨_, hx⟩, r.r ≫ r.i, by simp⟩, ⟨_, _, r, hx, rfl⟩⟩
-- 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_1 : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : 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
w :
  Q
    (X
      (Subtype.mk (p := R)
        (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)
            (r.r ≫ r.i) ⋯))
        ⋯))
⊢ ∃ (a : Subtype R) (h₁ : Q (X a)), g (h a) h₁ = g r hx
have hr : g
    (h
      (Subtype.mk (p := R)
        (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)
            (r.r ≫ r.i) sorry))
        sorry))
    w =
  (↑(Subtype.mk (p := R)
        (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)
            (r.r ≫ r.i) sorry))
        sorry) :
    α)
Tactic: obtain ⟨_, hr⟩ := hX ⟨⟨⟨_, hx⟩, r.r ≫ r.i, by simp⟩, ⟨_, _, r, hx, rfl⟩⟩
-- 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₁ : Q ≤ P
h₂ : 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
⊢ isoClosure.{v, u} (ofObj Y) y
have obtain : ∀ (a : Subtype R) (h₁ : Q (X a)) (h₂ : g (h a) h₁ = g r hx), isoClosure.{v, u} (ofObj Y) y
Tactic: obtain ⟨a, h₁, h₂⟩ : ∃ (a : Subtype R) (h₁ : Q (X a)), g (h a) h₁ = g r hx := by
      obtain ⟨_, hr⟩ := hX ⟨⟨⟨_, hx⟩, r.r ≫ r.i, by simp⟩, ⟨_, _, r, hx, rfl⟩⟩
      exact ⟨_, _, hr⟩