awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ∃ (P₀ : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P₀), P = P₀.isoClosure
have obtain : ∀ (Q : ObjectProperty.{v, u} C),
  ObjectProperty.Small.{w, v, u} Q →
    ∀ (hQ₁ : Q ≤ P) (hQ₂ : P ≤ Q.isoClosure),
      ∃ (P₀ : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P₀), P = P₀.isoClosure
Tactic: obtain ⟨Q, _, hQ₁, hQ₂⟩ := exists_small_le P
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} Q
h : P ≤ Q
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P ≤ Q.isoClosure
have obtain : ∀ (R : ObjectProperty.{v, u} C),
  ObjectProperty.Small.{w, v, u} R →
    ∀ (hR : Q ≤ R.isoClosure), ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P ≤ Q.isoClosure
Tactic: obtain ⟨R, _, hR⟩ := EssentiallySmall.exists_small_le' Q
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} Q
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)
have obtain : ∀ (P' : ObjectProperty.{v, u} C),
  ObjectProperty.Small.{w, v, u} P' → ∀ (hP' : P ≤ P'.isoClosure), ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)
Tactic: obtain ⟨P', _, hP'⟩ := EssentiallySmall.exists_small_le' P
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)
have obtain : ∀ (Q' : ObjectProperty.{v, u} C),
  ObjectProperty.Small.{w, v, u} Q' → ∀ (hQ' : Q ≤ Q'.isoClosure), ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)
Tactic: obtain ⟨Q', _, hQ'⟩ := EssentiallySmall.exists_small_le' Q
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty.{v, u} C
w_1 : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)
have refine : P ⊔ Q ≤ (P' ⊔ Q').isoClosure
Tactic: refine ⟨P' ⊔ Q', inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty.{v, u} C
w_1 : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
⊢ P ⊔ Q ≤ (P' ⊔ Q').isoClosure
have simp : P ≤ (P' ⊔ Q').isoClosure ∧ Q ≤ (P' ⊔ Q').isoClosure
Tactic: simp only [sup_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty.{v, u} C
w_1 : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
⊢ P ≤ (P' ⊔ Q').isoClosure ∧ Q ≤ (P' ⊔ Q').isoClosure
have left : P ≤ (P' ⊔ Q').isoClosure
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty.{v, u} C
w_1 : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
left : P ≤ (P' ⊔ Q').isoClosure
⊢ P ≤ (P' ⊔ Q').isoClosure ∧ Q ≤ (P' ⊔ Q').isoClosure
have right : Q ≤ (P' ⊔ Q').isoClosure
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty.{v, u} C
inst_2 : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst_3 : Small.{w, u_1} α
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), ⨆ (a : α), P a ≤ Q.isoClosure
have h : ∀ (a : α), ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P a ≤ Q.isoClosure
Tactic: have h (a : α) := EssentiallySmall.exists_small_le' (P a)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty.{v, u} C
inst_2 : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst_3 : Small.{w, u_1} α
h : ∀ (a : α), ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P a ≤ Q.isoClosure
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), ⨆ (a : α), P a ≤ Q.isoClosure
have choose : ∀ (Q : (a : α) → ObjectProperty.{v, u} C),
  (∀ (a : α), ObjectProperty.Small.{w, v, u} (Q a)) →
    ∀ (hQ : ∀ (a : α), P a ≤ (Q a).isoClosure),
      ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), ⨆ (a : α), P a ≤ Q.isoClosure
Tactic: choose Q _ hQ using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty.{v, u} C
inst_2 : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst_3 : Small.{w, u_1} α
Q : (a : α) → ObjectProperty.{v, u} C
h : ∀ (a : α), ObjectProperty.Small.{w, v, u} (Q a)
hQ : ∀ (a : α), P a ≤ (Q a).isoClosure
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), ⨆ (a : α), P a ≤ Q.isoClosure
have refine : LE.le.{u} (α := ObjectProperty.{v, u} C) (⨆ (a : α), P a) (isoClosure (⨆ (a : α), Q a))
Tactic: refine ⟨⨆ a, Q a, inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty.{v, u} C
inst_2 : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst_3 : Small.{w, u_1} α
Q : (a : α) → ObjectProperty.{v, u} C
h : ∀ (a : α), ObjectProperty.Small.{w, v, u} (Q a)
hQ : ∀ (a : α), P a ≤ (Q a).isoClosure
⊢ LE.le.{u} (α := ObjectProperty.{v, u} C) (⨆ (a : α), P a) (isoClosure (⨆ (a : α), Q a))
have simp : ∀ (i : α), P i ≤ isoClosure (⨆ (a : α), Q a)
Tactic: simp only [iSup_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op ↔ ObjectProperty.EssentiallySmall.{w, v, u} P
have refine_1 : ObjectProperty.EssentiallySmall.{w, v, u} P.op → ObjectProperty.EssentiallySmall.{w, v, u} P
Tactic: refine ⟨fun _ ↦ ?_, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
refine_1 : ObjectProperty.EssentiallySmall.{w, v, u} P.op → ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op ↔ ObjectProperty.EssentiallySmall.{w, v, u} P
have refine_2 : ObjectProperty.EssentiallySmall.{w, v, u} P → ObjectProperty.EssentiallySmall.{w, v, u} P.op
Tactic: refine ⟨fun _ ↦ ?_, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P.op
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P
have refine_1 : ∀ (Q : ObjectProperty.{v, u} Cᵒᵖ) (h₁ : ObjectProperty.Small.{w, v, u} Q),
  Q ≤ P.op → ∀ (h₂ : P.op ≤ Q.isoClosure), ObjectProperty.EssentiallySmall.{w, v, u} P
Tactic: obtain ⟨Q, h₁, _, h₂⟩ := EssentiallySmall.exists_small_le P.op
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P.op
Q : ObjectProperty.{v, u} Cᵒᵖ
h₁ : ObjectProperty.Small.{w, v, u} Q
left : Q ≤ P.op
h₂ : P.op ≤ Q.isoClosure
⊢ P ≤ Q.unop.isoClosure
have rwa : P ≤ Q.isoClosure.unop
Tactic: rwa [← unop_isoClosure, ← op_monotone_iff, op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P.op
Q : ObjectProperty.{v, u} Cᵒᵖ
h₁ : ObjectProperty.Small.{w, v, u} Q
left : Q ≤ P.op
h₂ : P.op ≤ Q.isoClosure
rwa : P ≤ Q.isoClosure.unop
⊢ P ≤ Q.unop.isoClosure
have rwa₁ : P.op ≤ Q.isoClosure.unop.op
Tactic: rwa [← unop_isoClosure, ← op_monotone_iff, op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op
have refine_2 : ∀ (Q : ObjectProperty.{v, u} C) (h₁ : ObjectProperty.Small.{w, v, u} Q),
  Q ≤ P → ∀ (h₂ : P ≤ Q.isoClosure), ObjectProperty.EssentiallySmall.{w, v, u} P.op
Tactic: obtain ⟨Q, h₁, _, h₂⟩ := EssentiallySmall.exists_small_le P
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
h₁ : ObjectProperty.Small.{w, v, u} Q
left : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ P.op ≤ Q.op.isoClosure
have rwa : P.op ≤ Q.isoClosure.op
Tactic: rwa [← op_isoClosure, op_monotone_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.unop ↔ ObjectProperty.EssentiallySmall.{w, v, u} P
have rw : ObjectProperty.EssentiallySmall.{w, v, u} P.unop.op ↔ ObjectProperty.EssentiallySmall.{w, v, u} P
Tactic: rw [← essentiallySmall_op_iff, op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
rw : ObjectProperty.EssentiallySmall.{w, v, u} P.unop.op ↔ ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.unop ↔ ObjectProperty.EssentiallySmall.{w, v, u} P
have rw₁ : ObjectProperty.EssentiallySmall.{w, v, u} P ↔ ObjectProperty.EssentiallySmall.{w, v, u} P
Tactic: rw [← essentiallySmall_op_iff, op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ EssentiallySmall.{w, v, u} P.FullSubcategory
have obtain : ∀ (Q : ObjectProperty.{v, u} C),
  ObjectProperty.Small.{w, v, u} Q →
    ∀ (h₁ : Q ≤ P) (h₂ : P ≤ Q.isoClosure), EssentiallySmall.{w, v, u} P.FullSubcategory
Tactic: obtain ⟨Q, _, h₁, h₂⟩ := EssentiallySmall.exists_small_le P
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ EssentiallySmall.{w, v, u} P.FullSubcategory
have this : (ιOfLE (P := Q) (P' := P) h₁).IsEquivalence
Tactic: have := (isEquivalence_ιOfLE_iff h₁).2 h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
this : (ιOfLE (P := Q) (P' := P) h₁).IsEquivalence
⊢ EssentiallySmall.{w, v, u} P.FullSubcategory
have rw : EssentiallySmall.{w, v, u} Q.FullSubcategory
Tactic: rw [← essentiallySmall_congr (ιOfLE h₁).asEquivalence]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
F : Functor.{v, v', u, u'} C D
⊢ ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)
have obtain : ∀ (Q : ObjectProperty.{v, u} C),
  ObjectProperty.Small.{w, v, u} Q →
    ∀ (h₁ : Q ≤ P) (h₂ : P ≤ Q.isoClosure), ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)
Tactic: obtain ⟨Q, _, h₁, h₂⟩ := EssentiallySmall.exists_small_le P
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
H₁ : ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v, u} (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y))
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P
have choose : ∀ (P₁ : ObjectProperty.{v', u'} D) (hP₁ : ObjectProperty.Small.{w, v', u'} P₁) (x : (i : D) → P.map F i → D)
  (hP₁x : ∀ (i : D) (a : P.map F i), P₁ (x i a)) (hx : ∀ (i : D) (a : P.map F i), Nonempty.{v' + 1} (i ≅ x i a)),
  ObjectProperty.EssentiallySmall.{w, v, u} P
Tactic: choose P₁ hP₁ x hP₁x hx using H₁.1
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
H₁ : ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v, u} (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y))
P₁ : ObjectProperty.{v', u'} D
hP₁ : ObjectProperty.Small.{w, v', u'} P₁
x : (i : D) → P.map F i → D
hP₁x : ∀ (i : D) (a : P.map F i), P₁ (x i a)
hx : ∀ (i : D) (a : P.map F i), Nonempty.{v' + 1} (i ≅ x i a)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P
have choose : ∀ (P₂ : (Y : D) → ObjectProperty.{v, u} C) (hP₂ : ∀ (Y : D), ObjectProperty.Small.{w, v, u} (P₂ Y))
  (y : (Y : D) → (i : C) → (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y)) i → C)
  (hP₂y : ∀ (Y : D) (i : C) (a : (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y)) i), P₂ Y (y Y i a))
  (hy : ∀ (Y : D) (i : C) (a : (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y)) i), Nonempty.{v + 1} (i ≅ y Y i a)),
  ObjectProperty.EssentiallySmall.{w, v, u} P
Tactic: choose P₂ hP₂ y hP₂y hy using fun Y ↦ (H₂ Y).1
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
⊢ (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)) ↔
    ObjectProperty.EssentiallySmall.{w, v, u} P
have refine_1 : (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)) →
  ∀ (J : Type w) (w : Category.{w', w} J) (e : Equivalence.{v, w', u, w} P.FullSubcategory J),
    ObjectProperty.EssentiallySmall.{w, v, u} P
Tactic: refine ⟨fun ⟨J, _, ⟨e⟩⟩ ↦ ?_, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
refine_1 :
  (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)) →
    ∀ (J : Type w) (w : Category.{w', w} J) (e : Equivalence.{v, w', u, w} P.FullSubcategory J),
      ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)) ↔
    ObjectProperty.EssentiallySmall.{w, v, u} P
have refine_2 : ObjectProperty.EssentiallySmall.{w, v, u} P →
  ∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)
Tactic: refine ⟨fun ⟨J, _, ⟨e⟩⟩ ↦ ?_, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)
have refine_2 : ∀ (Q : ObjectProperty.{v, u} C),
  ObjectProperty.Small.{w, v, u} Q →
    ∀ (h₁ : Q ≤ P) (h₂ : P ≤ Q.isoClosure),
      ∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)
Tactic: obtain ⟨Q, _, h₁, h₂⟩ := EssentiallySmall.exists_small_le.{w} P
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ ∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)
have h₃ : (ιOfLE (P := Q) (P' := P) h₁).IsEquivalence
Tactic: rw [← isEquivalence_ιOfLE_iff h₁] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : LocallySmall.{w', v_1, u_1} C
⊢ (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v_1, w', u_1, w} C J)) ↔
    ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤
have rw : (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v_1, w', u_1, w} C J)) ↔
  ∃ (J : Type w) (x : Category.{w', w} J),
    Nonempty (Equivalence.{v_1, w', u_1, w} (ObjectProperty.FullSubcategory.{v_1, u_1} (C := C) ⊤) J)
Tactic: rw [← ObjectProperty.exists_equivalence_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
⊢ EssentiallySmall.{w, v, u} C ↔ ObjectProperty.EssentiallySmall.{w, v, u} (C := C) ⊤
have rw : EssentiallySmall.{w, v, u} C ↔ ∃ (J : Type w) (x : Category.{w, w} J), Nonempty (Equivalence.{v, w, u, w} C J)
Tactic: rw [← exists_equivalence_iff_of_locallySmall]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔
    LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤
have inr : ∀
  (this :
    ∀ {C : Type u_1} [inst : Category.{v_1, u_1} C] (hC : LocallySmall.{w, v_1, u_1} C),
      EssentiallySmall.{w, v_1, u_1} C ↔
        LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤)
  (hC : ¬LocallySmall.{w, v_1, u_1} C),
  EssentiallySmall.{w, v_1, u_1} C ↔
    LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤
Tactic: wlog hC : LocallySmall.{w} C
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inr :
  ∀
    (this :
      ∀ {C : Type u_1} [inst : Category.{v_1, u_1} C] (hC : LocallySmall.{w, v_1, u_1} C),
        EssentiallySmall.{w, v_1, u_1} C ↔
          LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤)
    (hC : ¬LocallySmall.{w, v_1, u_1} C),
    EssentiallySmall.{w, v_1, u_1} C ↔
      LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤
⊢ EssentiallySmall.{w, v_1, u_1} C ↔
    LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤
have wlog : ∀ {C : Type u_1} [inst : Category.{v_1, u_1} C] (hC : LocallySmall.{w, v_1, u_1} C),
  EssentiallySmall.{w, v_1, u_1} C ↔
    LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤
Tactic: wlog hC : LocallySmall.{w} C
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (goal)
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
hC : LocallySmall.{w, v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔
    LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤
have simp : EssentiallySmall.{w, v_1, u_1} C ↔ ∃ (J : Type w) (x : Category.{w, w} J), Nonempty (Equivalence.{v_1, w, u_1, w} C J)
Tactic: simp only [hC, ← exists_equivalence_iff_of_locallySmall, true_and]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Small (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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : LocallySmall.{w, v_1, u_1} C
H₁ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) fun (x : C) ↦ Nonempty.{v_2 + 1} (F.obj x ≅ Y)
⊢ EssentiallySmall.{w, v_1, u_1} C
have rw : LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤
Tactic: rw [essentiallySmall_iff_objectPropertyEssentiallySmall]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ 𝟙 X ≫ f = f
have rw : Quiver.Hom.op (f.unop ≫ Quiver.Hom.unop (𝟙 X)) = f
Tactic: rw [← op_comp_unop, unop_id, comp_id, Quiver.Hom.op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
rw : Quiver.Hom.op (f.unop ≫ Quiver.Hom.unop (𝟙 X)) = f
⊢ 𝟙 X ≫ f = f
have rw₁ : (f.unop ≫ 𝟙 (unop X)).op = f
Tactic: rw [← op_comp_unop, unop_id, comp_id, Quiver.Hom.op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
rw : Quiver.Hom.op (f.unop ≫ Quiver.Hom.unop (𝟙 X)) = f
rw₁ : (f.unop ≫ 𝟙 (unop X)).op = f
⊢ 𝟙 X ≫ f = f
have rw₂ : f.unop.op = f
Tactic: rw [← op_comp_unop, unop_id, comp_id, Quiver.Hom.op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
rw : Quiver.Hom.op (f.unop ≫ Quiver.Hom.unop (𝟙 X)) = f
rw₁ : (f.unop ≫ 𝟙 (unop X)).op = f
rw₂ : f.unop.op = f
⊢ 𝟙 X ≫ f = f
have rw₃ : f = f
Tactic: rw [← op_comp_unop, unop_id, comp_id, Quiver.Hom.op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f
have rw : Quiver.Hom.op (Quiver.Hom.unop (𝟙 Y) ≫ f.unop) = f
Tactic: rw [← op_comp_unop, unop_id, id_comp, Quiver.Hom.op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
rw : Quiver.Hom.op (Quiver.Hom.unop (𝟙 Y) ≫ f.unop) = f
⊢ f ≫ 𝟙 Y = f
have rw₁ : (𝟙 (unop Y) ≫ f.unop).op = f
Tactic: rw [← op_comp_unop, unop_id, id_comp, Quiver.Hom.op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
rw : Quiver.Hom.op (Quiver.Hom.unop (𝟙 Y) ≫ f.unop) = f
rw₁ : (𝟙 (unop Y) ≫ f.unop).op = f
⊢ f ≫ 𝟙 Y = f
have rw₂ : f.unop.op = f
Tactic: rw [← op_comp_unop, unop_id, id_comp, Quiver.Hom.op_unop]