awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Yoneda.Injective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
refine_1 :
  ∀
    (h :
      (preadditiveYonedaObj J ⋙
          forget (ModuleCat (End J)) (FC := fun (x1 x2 : ModuleCat (End J)) ↦
            LinearMap (R := End J) (RingHom.id (End J)) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
            ModuleCat.carrier)).PreservesEpimorphisms),
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J)
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj yoneda J) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J)
have refine_2 : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J) →
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj yoneda J)
Tactic: refine ⟨fun h : (preadditiveYonedaObj J ⋙ (forget <| ModuleCat (End J))).PreservesEpimorphisms =>
    ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Yoneda.Projective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
⊢ Projective.{v, u} P ↔ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))
have rw : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P)) ↔
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))
Tactic: rw [projective_iff_preservesEpimorphisms_coyoneda_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Yoneda.Projective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P)) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))
have refine_1 : ∀
  (h :
    Functor.PreservesEpimorphisms
      (Functor.obj preadditiveCoyoneda (op P) ⋙
        forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier))),
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))
Tactic: refine ⟨fun h : (preadditiveCoyoneda.obj (op P) ⋙
      forget AddCommGrpCat).PreservesEpimorphisms => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Yoneda.Projective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
refine_1 :
  ∀
    (h :
      Functor.PreservesEpimorphisms
        (Functor.obj preadditiveCoyoneda (op P) ⋙
          forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier))),
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P)) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))
have refine_2 : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P)) →
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P))
Tactic: refine ⟨fun h : (preadditiveCoyoneda.obj (op P) ⋙
      forget AddCommGrpCat).PreservesEpimorphisms => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Yoneda.Projective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
⊢ Projective.{v, u} P ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
have rw : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P)) ↔
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
Tactic: rw [projective_iff_preservesEpimorphisms_coyoneda_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Yoneda.Projective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P)) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
have refine_1 : ∀
  (h :
    (preadditiveCoyonedaObj P ⋙
        forget (ModuleCat (End P)ᵐᵒᵖ) (FC := fun (x1 x2 : ModuleCat (End P)ᵐᵒᵖ) ↦
          LinearMap (R := (End P)ᵐᵒᵖ) (RingHom.id (End P)ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
          ModuleCat.carrier)).PreservesEpimorphisms),
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
Tactic: refine ⟨fun h : (preadditiveCoyonedaObj P ⋙ forget _).PreservesEpimorphisms => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Yoneda.Projective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
refine_1 :
  ∀
    (h :
      (preadditiveCoyonedaObj P ⋙
          forget (ModuleCat (End P)ᵐᵒᵖ) (FC := fun (x1 x2 : ModuleCat (End P)ᵐᵒᵖ) ↦
            LinearMap (R := (End P)ᵐᵒᵖ) (RingHom.id (End P)ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
            ModuleCat.carrier)).PreservesEpimorphisms),
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P)) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
have refine_2 : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P) →
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P))
Tactic: refine ⟨fun h : (preadditiveCoyonedaObj P ⋙ forget _).PreservesEpimorphisms => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Adjunction (goal)
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
X : C
inst_3 : IsCardinalPresentable.{w, v, u} X κ
inst_4 : G.IsCardinalAccessible κ
⊢ IsCardinalPresentable.{w, v', u'} (F.obj X) κ
have rw : Functor.IsCardinalAccessible (Functor.obj uliftCoyoneda.{v, v', u'} (op (F.obj X))) κ
Tactic: rw [isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj.{v}]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Adjunction (hypothesis)
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
P : ObjectProperty.{v, u} C
hP : P.IsCardinalFilteredGenerator κ
inst_3 : G.IsCardinalAccessible κ
inst_4 : G.Full
inst_5 : G.Faithful
Y : D
X : C
hX : P X
e : F.obj X ≅ Y
⊢ isCardinalPresentable.{w, v', u'} D κ Y
have hX' : isCardinalPresentable.{w, v, u} C κ X
Tactic: have hX' := hP.le_isCardinalPresentable X hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Adjunction (hypothesis)
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
P : ObjectProperty.{v, u} C
hP : P.IsCardinalFilteredGenerator κ
inst_3 : G.IsCardinalAccessible κ
inst_4 : G.Full
inst_5 : G.Faithful
Y : D
X : C
hX : P X
e : F.obj X ≅ Y
hX' : isCardinalPresentable.{w, v, u} C κ X
⊢ isCardinalPresentable.{w, v', u'} D κ Y
have hX'₁ : IsCardinalPresentable.{w, v, u} X κ
Tactic: rw [isCardinalPresentable_iff] at hX' ⊢
Cleared hypotheses: hX'
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Adjunction (hypothesis)
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
P : ObjectProperty.{v, u} C
hP : P.IsCardinalFilteredGenerator κ
inst_3 : G.IsCardinalAccessible κ
inst_4 : G.Full
inst_5 : G.Faithful
Y : D
X : C
hX : P X
e : F.obj X ≅ Y
hX' : IsCardinalPresentable.{w, v, u} X κ
⊢ IsCardinalPresentable.{w, v', u'} Y κ
have this : IsCardinalPresentable.{w, v', u'} (F.obj X) κ
Tactic: have := adj.isCardinalPresentable_leftAdjoint_obj κ X
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Adjunction (hypothesis)
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
P : ObjectProperty.{v, u} C
hP : P.IsCardinalFilteredGenerator κ
inst_3 : G.IsCardinalAccessible κ
inst_4 : G.Full
inst_5 : G.Faithful
Y : D
⊢ ∃ (J : Type w) (x : SmallCategory J) (_ : IsCardinalFiltered J κ), (P.map F).colimitsOfShape J Y
have this : F.IsLeftAdjoint
Tactic: have := adj.isLeftAdjoint
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Adjunction (goal)
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
P : ObjectProperty.{v, u} C
hP : P.IsCardinalFilteredGenerator κ
inst_3 : G.IsCardinalAccessible κ
inst_4 : G.Full
inst_5 : G.Faithful
Y : D
this : F.IsLeftAdjoint
⊢ ∃ (J : Type w) (x : SmallCategory J) (_ : IsCardinalFiltered J κ), (P.map F).colimitsOfShape J Y
have obtain : ∀ (J : Type w) (w : SmallCategory J),
  IsCardinalFiltered J κ →
    ∀ (hY : P.ColimitOfShape J (G.obj Y)),
      ∃ (J : Type w) (x : SmallCategory J) (_ : IsCardinalFiltered J κ), (P.map F).colimitsOfShape J Y
Tactic: obtain ⟨J, _, _, ⟨hY⟩⟩ := hP.exists_colimitsOfShape (G.obj Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Adjunction (goal)
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasCardinalFilteredGenerator.{w, v, u} C κ
inst_4 : G.IsCardinalAccessible κ
inst_5 : G.Full
inst_6 : G.Faithful
⊢ ∃ (P : ObjectProperty.{v', u'} D) (_ : ObjectProperty.EssentiallySmall.{w, v', u'} P), P.IsCardinalFilteredGenerator κ
have obtain : ∀ (P : ObjectProperty.{v, u} C),
  ObjectProperty.EssentiallySmall.{w, v, u} P →
    ∀ (hP : P.IsCardinalFilteredGenerator κ),
      ∃ (P : ObjectProperty.{v', u'} D) (_ : ObjectProperty.EssentiallySmall.{w, v', u'} P),
        P.IsCardinalFilteredGenerator κ
Tactic: obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_generator C κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Adjunction (goal)
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
inst_2 : IsLocallyPresentable.{w, v, u} C
⊢ IsLocallyPresentable.{w, v', u'} D
have obtain : ∀ (κ : Cardinal.{w}) (w : Fact κ.IsRegular),
  IsCardinalLocallyPresentable.{w, v, u} C κ → IsLocallyPresentable.{w, v', u'} D
Tactic: obtain ⟨κ, _, _⟩ := IsLocallyPresentable.exists_cardinal.{w} C
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Adjunction (goal)
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
inst_2 : IsAccessibleCategory.{w, v, u} C
⊢ IsAccessibleCategory.{w, v', u'} D
have obtain : ∀ (κ : Cardinal.{w}) (w : Fact κ.IsRegular),
  IsCardinalAccessibleCategory.{w, v, u} C κ → IsAccessibleCategory.{w, v', u'} D
Tactic: obtain ⟨κ, _, _⟩ := IsAccessibleCategory.exists_cardinal.{w} C
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
J : Type u₃
inst_4 : Category.{v₃, u₃} J
inst_5 : EssentiallySmall.{w, v₃, u₃} J
inst_6 : IsCardinalFiltered.{w, v₃, u₃} J κ
⊢ PreservesColimitsOfShape.{v₃, u₃, v₁, v₂, u₁, u₂} J F
have this : IsCardinalFiltered (SmallModel.{w, v₃, u₃} J) κ
Tactic: have := IsCardinalFiltered.of_equivalence κ (equivSmallModel.{w} J)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
J : Type u₃
inst_4 : Category.{v₃, u₃} J
inst_5 : EssentiallySmall.{w, v₃, u₃} J
inst_6 : IsCardinalFiltered.{w, v₃, u₃} J κ
this : IsCardinalFiltered (SmallModel.{w, v₃, u₃} J) κ
⊢ PreservesColimitsOfShape.{v₃, u₃, v₁, v₂, u₁, u₂} J F
have this₁ : PreservesColimitsOfShape.{w, w, v₁, v₂, u₁, u₂} (SmallModel.{w, v₃, u₃} J) F
Tactic: have := F.preservesColimitsOfShape_of_isCardinalAccessible κ (SmallModel.{w} J)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
κ' : Cardinal.{w}
inst_4 : Fact κ'.IsRegular
h : κ ≤ κ'
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ'
⊢ PreservesColimitsOfShape J F
have this : IsCardinalFiltered J κ
Tactic: have := IsCardinalFiltered.of_le J h
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
J : Type w
x : SmallCategory J
hκ : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J G
have this : PreservesColimitsOfShape J F
Tactic: have := F.preservesColimitsOfShape_of_isCardinalAccessible κ J
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G_1 : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G_1
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
E : Type u₃
inst_3 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : F.IsCardinalAccessible κ
inst_5 : G.IsCardinalAccessible κ
⊢ (F ⋙ G).IsCardinalAccessible κ
have this : ∀ (J : Type w) [inst_6 : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J F
Tactic: have := F.preservesColimitsOfShape_of_isCardinalAccessible κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G_1 : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G_1
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
E : Type u₃
inst_3 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : F.IsCardinalAccessible κ
inst_5 : G.IsCardinalAccessible κ
this : ∀ (J : Type w) [inst_6 : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J F
⊢ (F ⋙ G).IsCardinalAccessible κ
have this₁ : ∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J G
Tactic: have := G.preservesColimitsOfShape_of_isCardinalAccessible κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
A : C
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
F : Functor.{w, v₁, w, u₁} J C
c : Cocone F
hc : IsColimit c
⊢ IsColimit (F := F ⋙ obj (const C) A) (mapCocone (obj (const C) A) c)
have h : IsFiltered J
Tactic: have h := isFiltered_of_isCardinalFiltered J κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
A : C
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v₁, w, u₁} J C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
j : J
⊢ IsIso (X := obj (F ⋙ obj (const C) A) j) (Y :=
    obj.{w, v₁, w, u₁} (obj (const J) (Cocone.pt (F := F ⋙ obj (const C) A) (mapCocone (obj (const C) A) c))) j)
    (NatTrans.app (Cocone.ι (mapCocone (obj (const C) A) c)) j)
have dsimp : IsIso.{v₁, u₁} (𝟙 A)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
A : C
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v₁, w, u₁} J C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
⊢ IsColimit (F := F ⋙ obj (const C) A) (mapCocone (obj (const C) A) c)
have this : ∀ (j : J),
  IsIso (X := obj (F ⋙ obj (const C) A) j) (Y :=
    obj.{w, v₁, w, u₁} (obj (const J) (Cocone.pt (F := F ⋙ obj (const C) A) (mapCocone (obj (const C) A) c))) j)
    (NatTrans.app (Cocone.ι (mapCocone (obj (const C) A) c)) j)
Tactic: have (j : J) : IsIso ((((const C).obj A).mapCocone c).ι.app j) := by
              dsimp
              infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
A : C
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v₁, w, u₁} J C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
this :
  ∀ (j : J),
    IsIso (X := obj (F ⋙ obj (const C) A) j) (Y :=
      obj.{w, v₁, w, u₁} (obj (const J) (Cocone.pt (F := F ⋙ obj (const C) A) (mapCocone (obj (const C) A) c))) j)
      (NatTrans.app (Cocone.ι (mapCocone (obj (const C) A) c)) j)
x_1 : J
x_2 : Nonempty.some ⋯ ⟶ x_1
⊢ IsIso (X := obj (F ⋙ obj (const C) A) (Nonempty.some ⋯)) (map (F ⋙ obj (const C) A) x_2)
have dsimp : IsIso.{v₁, u₁} (𝟙 A)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst_4 : IsAccessible.{w, v₂, v₃, u₂, u₃} G
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)
have obtain : ∀ (κF : Cardinal.{w}) (w : Fact κF.IsRegular), F.IsCardinalAccessible κF → IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)
Tactic: obtain ⟨κF, _, _⟩ := IsAccessible.exists_cardinal (F := F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst_4 : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w : Fact κF.IsRegular
h : F.IsCardinalAccessible κF
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)
have obtain : ∀ (κG : Cardinal.{w}) (w : Fact κG.IsRegular), G.IsCardinalAccessible κG → IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)
Tactic: obtain ⟨κG, _, _⟩ := IsAccessible.exists_cardinal (F := G)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst_4 : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w : Fact κF.IsRegular
h : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w_1 : Fact κG.IsRegular
h_1 : G.IsCardinalAccessible κG
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)
have this : Fact (Cardinal.IsRegular.{w} (max κF κG))
Tactic: have : Fact (κF ⊔ κG).IsRegular := ⟨iteInduction (fun _ ↦ Fact.out) (fun _ ↦ Fact.out)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst_4 : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w : Fact κF.IsRegular
h : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w_1 : Fact κG.IsRegular
h_1 : G.IsCardinalAccessible κG
this : Fact (Cardinal.IsRegular.{w} (max κF κG))
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)
have this₁ : IsCardinalAccessible.{w, v₁, v₂, u₁, u₂} F (max κF κG)
Tactic: have := isCardinalAccessible_of_le F (by simp : κF ≤ κF ⊔ κG)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst_4 : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w : Fact κF.IsRegular
h : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w_1 : Fact κG.IsRegular
h_1 : G.IsCardinalAccessible κG
this_1 : Fact (Cardinal.IsRegular.{w} (max κF κG))
this : IsCardinalAccessible.{w, v₁, v₂, u₁, u₂} F (max κF κG)
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)
have this₁ : IsCardinalAccessible.{w, v₂, v₃, u₂, u₃} G (max κF κG)
Tactic: have := isCardinalAccessible_of_le G (by simp : κG ≤ κF ⊔ κG)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
A : C
⊢ IsAccessible.{w, v₁, v₁, u₁, u₁} (obj (const C) A)
have this : Fact Cardinal.aleph0.IsRegular
Tactic: have : Fact Cardinal.aleph0.IsRegular := Cardinal.fact_isRegular_aleph0
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 Y : C
e : X_1 ≅ Y
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
X : ObjectProperty.FullSubcategory.{v₁, u₁} (isCardinalPresentable C κ)
⊢ IsCardinalPresentable.{w, v₁, u₁} (Functor.obj (ObjectProperty.ι (isCardinalPresentable C κ)) X) κ
have dsimp : IsCardinalPresentable.{w, v₁, u₁} (X.obj (P := isCardinalPresentable C κ)) κ
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
κ' : Cardinal.{w}
inst_2 : Fact κ'.IsRegular
h : κ ≤ κ'
X : C
hX : isCardinalPresentable.{w, v₁, u₁} C κ X
⊢ isCardinalPresentable.{w, v₁, u₁} C κ' X
have hX₁ : IsCardinalPresentable.{w, v₁, u₁} X κ
Tactic: rw [isCardinalPresentable_iff] at hX ⊢
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
e_1 : X ≅ Y
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
X_1 Y_1 : C
e : X_1 ≅ Y_1
hX : isCardinalPresentable.{w, v₁, u₁} C κ X_1
⊢ isCardinalPresentable.{w, v₁, u₁} C κ Y_1
have hX₁ : IsCardinalPresentable.{w, v₁, u₁} X_1 κ
Tactic: rw [isCardinalPresentable_iff] at hX ⊢
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
⊢ IsCardinalPresentable.{w, v₃, u₃} (e.functor.obj X) κ
have refine : ∀ (J : Type w) (x : SmallCategory J),
  IsCardinalFiltered J κ →
    ∀ {Y : Functor.{w, v₃, w, u₃} J C'}, PreservesColimit Y (Functor.obj coyoneda (op (e.functor.obj X)))
Tactic: refine ⟨fun J _ _ ↦ ⟨fun {Y} ↦ ?_⟩⟩