awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
h :
  Function.Surjective (β := { x : κ.ord.ToType // x ∈ Set.range f }) fun (i : ι) ↦
    Subtype.mk (p := fun (x : κ.ord.ToType) ↦ x ∈ Set.range f) (f i) ⋯
hs : ∀ (j : κ.ord.ToType), ∃ (k : ι), j < f k
⊢ Order.cof κ.ord.ToType ≤ Cardinal.mk ι
have refine : ∀ (j : κ.ord.ToType), ∃ y ∈ Set.range f, j ≤ y
Tactic: refine (Order.cof_le fun j ↦ ?_).trans (Cardinal.mk_le_of_surjective h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
h :
  Function.Surjective (β := { x : κ.ord.ToType // x ∈ Set.range f }) fun (i : ι) ↦
    Subtype.mk (p := fun (x : κ.ord.ToType) ↦ x ∈ Set.range f) (f i) ⋯
hs : ∀ (j : κ.ord.ToType), ∃ (k : ι), j < f k
j : κ.ord.ToType
⊢ ∃ y ∈ Set.range f, j ≤ y
have obtain : ∀ (k : ι) (hk : j < f k), ∃ y ∈ Set.range f, j ≤ y
Tactic: obtain ⟨k, hk⟩ := hs j
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
j₀ : J
A : Type w
x : SmallCategory A
F : A ⥤ Under.{v, u} j₀
hA : HasCardinalLT (Arrow A) κ
⊢ Cocone F
have this : IsFiltered.{v, u} J
Tactic: have := isFiltered_of_isCardinalFiltered J κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
j₀ : J
A : Type w
x_1 : SmallCategory A
F : A ⥤ Under.{v, u} j₀
hA : HasCardinalLT (Arrow A) κ
this : IsFiltered.{v, u} J
c : Cocone (F ⋙ Under.forget j₀) := cocone (F ⋙ Under.forget j₀) hA
x : (a : A) → j₀ ⟶ IsFiltered.max.{v, u} j₀ c.pt :=
  fun (a : A) ↦ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt
⊢ Cocone F
have hκ' : HasCardinalLT A κ
Tactic: have hκ' : HasCardinalLT A κ := hasCardinalLT_of_hasCardinalLT_arrow hA
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
j₀ : J
A : Type w
x_1 : SmallCategory A
F : A ⥤ Under.{v, u} j₀
hA : HasCardinalLT (Arrow A) κ
this : IsFiltered.{v, u} J
c : Cocone (F ⋙ Under.forget j₀) := cocone (F ⋙ Under.forget j₀) hA
x : (a : A) → j₀ ⟶ IsFiltered.max.{v, u} j₀ c.pt :=
  fun (a : A) ↦ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt
hκ' : HasCardinalLT A κ
a b : A
f : a ⟶ b
⊢ Eq (α := F.obj a ⟶ Functor.obj (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) b)
    (F.map f ≫ Under.homMk (c.ι.app b ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ⋯)
    (Under.homMk (c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ⋯ ≫
      Functor.map (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) f)
have h : Eq (α :=
  (F.obj a).right ⟶ (Functor.obj (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) b).right)
  (Under.Hom.right (F.map f ≫ Under.homMk (c.ι.app b ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') sorry))
  (Under.Hom.right
    (Under.homMk (c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') sorry ≫
      Functor.map (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) f))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
j₀ : J
A : Type w
x_1 : SmallCategory A
F : A ⥤ Under.{v, u} j₀
hA : HasCardinalLT (Arrow A) κ
this : IsFiltered.{v, u} J
c : Cocone (F ⋙ Under.forget j₀) := cocone (F ⋙ Under.forget j₀) hA
x : (a : A) → j₀ ⟶ IsFiltered.max.{v, u} j₀ c.pt :=
  fun (a : A) ↦ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt
hκ' : HasCardinalLT A κ
a b : A
f : a ⟶ b
⊢ Eq (α :=
    (F.obj a).right ⟶ (Functor.obj (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) b).right)
    (Under.Hom.right (F.map f ≫ Under.homMk (c.ι.app b ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ⋯))
    (Under.Hom.right
      (Under.homMk (c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ⋯ ≫
        Functor.map (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) f))
have this₁ : (F ⋙ Under.forget j₀).map f ≫ c.ι.app b = c.ι.app a
Tactic: have := c.w f
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
j₀ : J
A : Type w
x_1 : SmallCategory A
F : A ⥤ Under.{v, u} j₀
hA : HasCardinalLT (Arrow A) κ
this_1 : IsFiltered.{v, u} J
c : Cocone (F ⋙ Under.forget j₀) := cocone (F ⋙ Under.forget j₀) hA
x : (a : A) → j₀ ⟶ IsFiltered.max.{v, u} j₀ c.pt :=
  fun (a : A) ↦ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt
hκ' : HasCardinalLT A κ
a b : A
f : a ⟶ b
this : (F ⋙ Under.forget j₀).map f ≫ c.ι.app b = c.ι.app a
⊢ Eq (α :=
    (F.obj a).right ⟶ (Functor.obj (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) b).right)
    (Under.Hom.right (F.map f ≫ Under.homMk (c.ι.app b ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ⋯))
    (Under.Hom.right
      (Under.homMk (c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ⋯ ≫
        Functor.map (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) f))
have h : Under.Hom.right (F.map f) ≫ c.ι.app b ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ' =
  (c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ≫ 𝟙 (coeq x hκ')
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J₁ : Type u
J₂ : Type u'
inst : Category.{v, u} J₁
inst_1 : Category.{v', u'} J₂
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : IsCardinalFiltered.{w, v, u} J₁ κ
inst_4 : IsCardinalFiltered.{w, v', u'} J₂ κ
A : Type w
inst_5 : SmallCategory A
F : A ⥤ J₁ × J₂
hC : HasCardinalLT (Arrow A) κ
c₁ : Cocone (F ⋙ Prod.fst J₁ J₂) := cocone (F ⋙ Prod.fst J₁ J₂) hC
c₂ : Cocone (F ⋙ Prod.snd J₁ J₂) := cocone (F ⋙ Prod.snd J₁ J₂) hC
i j : A
f : i ⟶ j
⊢ F.map f ≫ (c₁.ι.app j, c₂.ι.app j) =
    (c₁.ι.app i, c₂.ι.app i) ≫ Functor.map (Functor.obj (Functor.const A) (c₁.pt, c₂.pt)) f
have h₁ : (F.map f ≫ (c₁.ι.app j, c₂.ι.app j)).1 =
  ((c₁.ι.app i, c₂.ι.app i) ≫ Functor.map (Functor.obj (Functor.const A) (c₁.pt, c₂.pt)) f).1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J₁ : Type u
J₂ : Type u'
inst : Category.{v, u} J₁
inst_1 : Category.{v', u'} J₂
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : IsCardinalFiltered.{w, v, u} J₁ κ
inst_4 : IsCardinalFiltered.{w, v', u'} J₂ κ
A : Type w
inst_5 : SmallCategory A
F : A ⥤ J₁ × J₂
hC : HasCardinalLT (Arrow A) κ
c₁ : Cocone (F ⋙ Prod.fst J₁ J₂) := cocone (F ⋙ Prod.fst J₁ J₂) hC
c₂ : Cocone (F ⋙ Prod.snd J₁ J₂) := cocone (F ⋙ Prod.snd J₁ J₂) hC
i j : A
f : i ⟶ j
h₁ :
  (F.map f ≫ (c₁.ι.app j, c₂.ι.app j)).1 =
    ((c₁.ι.app i, c₂.ι.app i) ≫ Functor.map (Functor.obj (Functor.const A) (c₁.pt, c₂.pt)) f).1
⊢ F.map f ≫ (c₁.ι.app j, c₂.ι.app j) =
    (c₁.ι.app i, c₂.ι.app i) ≫ Functor.map (Functor.obj (Functor.const A) (c₁.pt, c₂.pt)) f
have h₂ : (F.map f ≫ (c₁.ι.app j, c₂.ι.app j)).2 =
  ((c₁.ι.app i, c₂.ι.app i) ≫ Functor.map (Functor.obj (Functor.const A) (c₁.pt, c₂.pt)) f).2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
ι : Type u'
J : ι → Type u
inst : (i : ι) → Category.{v, u} (J i)
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : ∀ (i : ι), IsCardinalFiltered.{w, v, u} (J i) κ
A : Type w
inst_3 : SmallCategory A
F : A ⥤ ((i : ι) → J i)
hC : HasCardinalLT (Arrow A) κ
c : (i : ι) → Cocone (F ⋙ Pi.eval J i) := fun (i : ι) ↦ cocone (F ⋙ Pi.eval J i) hC
X Y : A
f : X ⟶ Y
⊢ Eq (α := F.obj X ⟶ Functor.obj (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) Y)
    (F.map f ≫ fun (i : ι) ↦ (c i).ι.app Y)
    ((fun (i : ι) ↦ (c i).ι.app X) ≫ Functor.map (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) f)
have w : ∀ (i : ι),
  Eq.{v + 1} (α := F.obj X i ⟶ Functor.obj (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) Y i)
    ((F.map f ≫ fun (i : ι) ↦ (c i).ι.app Y) i :
      F.obj X i ⟶ Functor.obj (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) Y i)
    (((fun (i : ι) ↦ (c i).ι.app X) ≫ Functor.map (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) f) i :
      F.obj X i ⟶ Functor.obj (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) Y i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : J
k : ι → J
f : (i : ι) → j ⟶ k i
hι : HasCardinalLT ι κ
⊢ ∃ (m : J) (a : (i : ι) → k i ⟶ m) (b : j ⟶ m), ∀ (i : ι), f i ≫ a i = b
have obtain : ∀ (l : J) (hl : ∀ (i : ι), Nonempty.{v + 1} (k i ⟶ l)),
  ∃ (m : J) (a : (i : ι) → k i ⟶ m) (b : j ⟶ m), ∀ (i : ι), f i ≫ a i = b
Tactic: obtain ⟨l, hl⟩ := h₁ k hι
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : J
k : ι → J
f : (i : ι) → j ⟶ k i
hι : HasCardinalLT ι κ
l : J
hl : ∀ (i : ι), Nonempty.{v + 1} (k i ⟶ l)
a : (i : ι) → k i ⟶ l := fun (i : ι) ↦ ⋯.some
⊢ ∃ (m : J) (a : (i : ι) → k i ⟶ m) (b : j ⟶ m), ∀ (i : ι), f i ≫ a i = b
have obtain : ∀ (m : J) (b : l ⟶ m) (c : j ⟶ m) (hm : ∀ (i : ι), (f i ≫ a i) ≫ b = c),
  ∃ (m : J) (a : (i : ι) → k i ⟶ m) (b : j ⟶ m), ∀ (i : ι), f i ≫ a i = b
Tactic: obtain ⟨m, b, c, hm⟩ := h₂ (fun i ↦ f i ≫ a i) hι
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
i : ι
⊢ ∃ (l : J) (p : k ⟶ l), f₁ i ≫ p = f₂ i ≫ p
have obtain : ∀ (l : J) (a : k ⟶ l) (b : j i ⟶ l)
  (hl :
    ∀ (i_1 : PUnit.{w + 1} ⊕ PUnit.{w + 1}),
      Sum.elim (fun (x : PUnit.{w + 1}) ↦ f₁ i) (fun (x : PUnit.{w + 1}) ↦ f₂ i) i_1 ≫ a = b),
  ∃ (l : J) (p : k ⟶ l), f₁ i ≫ p = f₂ i ≫ p
Tactic: obtain ⟨l, a, b, hl⟩ := h₂ (Sum.elim (fun (_ : PUnit.{w + 1}) ↦ f₁ i)
      (fun (_ : PUnit.{w + 1}) ↦ f₂ i))
        (hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out))
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
⊢ ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a
have this : ∀ (i : ι), ∃ (l : J) (p : k ⟶ l), f₁ i ≫ p = f₂ i ≫ p
Tactic: have (i : ι) : ∃ (l : J) (p : k ⟶ l), f₁ i ≫ p = f₂ i ≫ p := by
    obtain ⟨l, a, b, hl⟩ := h₂ (Sum.elim (fun (_ : PUnit.{w + 1}) ↦ f₁ i)
      (fun (_ : PUnit.{w + 1}) ↦ f₂ i))
        (hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out))
    exact ⟨l, a, (hl (Sum.inl .unit)).trans (hl (Sum.inr .unit)).symm⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
this : ∀ (i : ι), ∃ (l : J) (p : k ⟶ l), f₁ i ≫ p = f₂ i ≫ p
⊢ ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a
have choose : ∀ (l : (i : ι) → J) (p : (i : ι) → k ⟶ l i) (hp : ∀ (i : ι), f₁ i ≫ p i = f₂ i ≫ p i),
  ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a
Tactic: choose l p hp using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
l : (i : ι) → J
p : (i : ι) → k ⟶ l i
hp : ∀ (i : ι), f₁ i ≫ p i = f₂ i ≫ p i
⊢ ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a
have obtain : ∀ (l_1 : J) (a : (i : ι) → l i ⟶ l_1) (b : k ⟶ l_1) (h : ∀ (i : ι), p i ≫ a i = b),
  ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a
Tactic: obtain ⟨l, a, b, h⟩ := isCardinalFiltered_iff_aux₁ h₁ h₂ p hι
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
⊢ IsCardinalFiltered.{w, v, u} J κ ↔
    (∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)) ∧
      ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
        HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
have refine : ((∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
      HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b) →
  ∀ (h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k))
    (h₂ :
      ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
        HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b)
    {A : Type w} {x : SmallCategory A} (F : Functor.{w, v, w, u} A J) (hA : HasCardinalLT (Arrow A) κ),
    Nonempty (Cocone F)
Tactic: refine ⟨fun _ ↦ ⟨fun ι j hι ↦ ⟨_, fun i ↦ ⟨toMax j hι i⟩⟩,
    fun ι j k f hι ↦ ⟨_, _, _, coeq_condition f hι⟩⟩,
    fun ⟨h₁, h₂⟩ ↦ ⟨fun {A _} F hA ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h :
  (∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
      HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
A : Type w
x : SmallCategory A
F : Functor.{w, v, w, u} A J
hA : HasCardinalLT (Arrow A) κ
⊢ Nonempty (Cocone F)
have obtain : ∀ (j : J) (hj : ∀ (i : A), Nonempty.{v + 1} (F.obj i ⟶ j)), Nonempty (Cocone F)
Tactic: obtain ⟨j, hj⟩ := h₁ F.obj (hasCardinalLT_of_hasCardinalLT_arrow hA)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h :
  (∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
      HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
A : Type w
x : SmallCategory A
F : Functor.{w, v, w, u} A J
hA : HasCardinalLT (Arrow A) κ
j : J
hj : ∀ (i : A), Nonempty.{v + 1} (F.obj i ⟶ j)
a : (i : A) → F.obj i ⟶ j := fun (i : A) ↦ ⋯.some
⊢ Nonempty (Cocone F)
have obtain : ∀ (l : J) (b : j ⟶ l) (hb : ∀ (i : Arrow A), (F.map i.hom ≫ a i.right) ≫ b = a i.left ≫ b), Nonempty (Cocone F)
Tactic: obtain ⟨l, b, hb⟩ := isCardinalFiltered_iff_aux₂ h₁ h₂
    (fun (f : Arrow A) ↦ F.map f.hom ≫ a f.right)
    (fun (f : Arrow A) ↦ a f.left) hA
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
⊢ ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a
have this : IsFiltered.{v, u} J
Tactic: have := isFiltered_of_isCardinalFiltered J κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
this : IsFiltered.{v, u} J
⊢ ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a
have obtain : ∀ (l : J) (a : (i : ι) → IsFiltered.coeq (f₁ i) (f₂ i) ⟶ l) (b : k ⟶ l)
  (h : ∀ (i : ι), IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = b), ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a
Tactic: obtain ⟨l, a, b, h⟩ := IsCardinalFiltered.wideSpan
    (fun i ↦ IsFiltered.coeqHom (f₁ i) (f₂ i)) hι
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
this : IsFiltered.{v, u} J
l : J
a : (i : ι) → IsFiltered.coeq (f₁ i) (f₂ i) ⟶ l
b : k ⟶ l
h : ∀ (i : ι), IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = b
i : ι
⊢ f₁ i ≫ b = f₂ i ≫ b
have rw : f₁ i ≫ IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = f₂ i ≫ IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i
Tactic: rw [← h i, IsFiltered.coeq_condition_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
this : IsFiltered.{v, u} J
l : J
a : (i : ι) → IsFiltered.coeq (f₁ i) (f₂ i) ⟶ l
b : k ⟶ l
h : ∀ (i : ι), IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = b
i : ι
rw : f₁ i ≫ IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = f₂ i ≫ IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i
⊢ f₁ i ≫ b = f₂ i ≫ b
have rw₁ : f₂ i ≫ IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = f₂ i ≫ IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i
Tactic: rw [← h i, IsFiltered.coeq_condition_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
⊢ IsCardinalFiltered.{w, v', u'} J₂ κ
have this : IsFiltered.{v, u} J₁
Tactic: have := isFiltered_of_isCardinalFiltered J₁ κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
⊢ IsCardinalFiltered.{w, v', u'} J₂ κ
have h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
Tactic: obtain ⟨h₁, h₂⟩ := (Functor.final_iff_of_isFiltered F).1 inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
⊢ IsCardinalFiltered.{w, v', u'} J₂ κ
have h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
Tactic: obtain ⟨h₁, h₂⟩ := (Functor.final_iff_of_isFiltered F).1 inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
⊢ IsCardinalFiltered.{w, v', u'} J₂ κ
have rw : (∀ ⦃ι : Type w⦄ (j : ι → J₂), HasCardinalLT ι κ → ∃ (k : J₂), ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ k)) ∧
  ∀ ⦃ι : Type w⦄ ⦃j k : J₂⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
Tactic: rw [isCardinalFiltered_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
⊢ (∀ ⦃ι : Type w⦄ (j : ι → J₂), HasCardinalLT ι κ → ∃ (k : J₂), ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ k)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J₂⦄ (f : ι → (j ⟶ k)),
      HasCardinalLT ι κ → ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
have refine_1 : ∀ (ι : Type w) (j : ι → J₂) (hι : HasCardinalLT ι κ), ∃ (k : J₂), ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ k)
Tactic: refine ⟨fun ι j hι ↦ ?_, fun ι j k f hι ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
refine_1 : ∀ (ι : Type w) (j : ι → J₂) (hι : HasCardinalLT ι κ), ∃ (k : J₂), ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ k)
⊢ (∀ ⦃ι : Type w⦄ (j : ι → J₂), HasCardinalLT ι κ → ∃ (k : J₂), ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ k)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J₂⦄ (f : ι → (j ⟶ k)),
      HasCardinalLT ι κ → ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
have refine_2 : ∀ (ι : Type w) (j k : J₂) (f : ι → (j ⟶ k)) (hι : HasCardinalLT ι κ),
  ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
Tactic: refine ⟨fun ι j hι ↦ ?_, fun ι j k f hι ↦ ?_⟩