awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x) ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y)
eq :
  (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).fst (β :=
    fun (t : Type (max v w)) ↦ t → C)
⊢ ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (IsCofiltered.eq g g') ⋯).obj (P :=
        cofilteredClosure f)
have eq₁ : CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
    (Sigma.mk (β := fun (n : ℕ) ↦
      (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
        t → C))
      (max n m).succ (Eq.mpr sorry (CofilteredClosureSmall.InductiveStep.eq sorry sorry x y g g'))) =
  (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (IsCofiltered.eq g g') sorry).obj (P := cofilteredClosure f)
Tactic: refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x) ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y)
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).fst (β :=
    fun (t : Type (max v w)) ↦ t → C)
have eq : CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
  CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1
Tactic: simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x) ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y)
⊢ CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
    CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1
have eq : n < max n m + 1
Tactic: refine CofilteredClosureSmall.InductiveStep.eq ?_ ?_ x y g g'
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x) ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y)
eq : n < max n m + 1
⊢ CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
    CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1
have eq₁ : m < max n m + 1
Tactic: refine CofilteredClosureSmall.InductiveStep.eq ?_ ?_ x y g g'
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x) ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y)
⊢ n < max n m + 1
have eq : n ≤ max n m
Tactic: apply Nat.lt_succ_of_le
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x) ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y)
⊢ m < max n m + 1
have eq : m ≤ max n m
Tactic: apply Nat.lt_succ_of_le
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x) ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y)
⊢ CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        (max n m).succ (Eq.mpr ⋯ (CofilteredClosureSmall.InductiveStep.eq ⋯ ⋯ x y g g'))) =
    (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (eq g g') ⋯).obj (P := cofilteredClosure f)
have eq : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).snd (β :=
    fun (t : Type (max v w)) ↦ t → C) (Eq.mpr sorry (CofilteredClosureSmall.InductiveStep.eq sorry sorry x y g g')) =
  eq g g'
Tactic: simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x) ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y)
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).snd (β :=
      fun (t : Type (max v w)) ↦ t → C) (Eq.mpr ⋯ (CofilteredClosureSmall.InductiveStep.eq ⋯ ⋯ x y g g')) =
    eq g g'
have eq : Sigma.snd (β := fun (t : Type (max v w)) ↦ t → C)
    (Sigma.mk (β := fun (t : Type (max v w)) ↦ t → C)
      (CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
        CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1)
      (CofilteredClosureSmall.inductiveStepRealization (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
        CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1))
    (Eq.mpr (β :=
      CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
        CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1)
      sorry (CofilteredClosureSmall.InductiveStep.eq sorry sorry x y g g')) =
  eq g g'
Tactic: rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
h : cofilteredClosure.{w, v, u} f j
⊢ ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) j h).obj (P := cofilteredClosure f)
have base : ∀ (x : α),
  ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      ObjectProperty.FullSubcategory.obj (P := cofilteredClosure f)
        (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (f x) sorry)
Tactic: induction h with
  | base x =>
    refine ⟨⟨0, ?_⟩,?_⟩
    · simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      exact ULift.up x
    · simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization,
        CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl
  | min hj₁ hj₂ ih ih' =>
    rcases ih with ⟨⟨n, x⟩, rfl⟩
    rcases ih' with ⟨⟨m, y⟩, rfl⟩
    refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
    · simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      refine CofilteredClosureSmall.InductiveStep.min ?_ ?_ x y
      all_goals apply Nat.lt_succ_of_le
      exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]
    · simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
      rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl
  | eq hj₁ hj₂ g g' ih ih' =>
    rcases ih with ⟨⟨n, x⟩, rfl⟩
    rcases ih' with ⟨⟨m, y⟩, rfl⟩
    refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
    · simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      refine CofilteredClosureSmall.InductiveStep.eq ?_ ?_ x y g g'
      all_goals apply Nat.lt_succ_of_le
      exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]
    · simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
      rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
h : cofilteredClosure.{w, v, u} f j
base :
  ∀ (x : α),
    ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
      CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
        ObjectProperty.FullSubcategory.obj (P := cofilteredClosure f)
          (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (f x) ⋯)
⊢ ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) j h).obj (P := cofilteredClosure f)
have min : ∀ {j j' : C} (hj₁ : cofilteredClosure.{w, v, u} f j) (hj₂ : cofilteredClosure.{w, v, u} f j')
  (ih :
    ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
      CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
        (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) j hj₁).obj (P := cofilteredClosure f))
  (ih' :
    ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
      CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
        (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) j' hj₂).obj (P := cofilteredClosure f)),
  ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (min.{v, u} j j') sorry).obj (P := cofilteredClosure f)
Tactic: induction h with
  | base x =>
    refine ⟨⟨0, ?_⟩,?_⟩
    · simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      exact ULift.up x
    · simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization,
        CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl
  | min hj₁ hj₂ ih ih' =>
    rcases ih with ⟨⟨n, x⟩, rfl⟩
    rcases ih' with ⟨⟨m, y⟩, rfl⟩
    refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
    · simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      refine CofilteredClosureSmall.InductiveStep.min ?_ ?_ x y
      all_goals apply Nat.lt_succ_of_le
      exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]
    · simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
      rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl
  | eq hj₁ hj₂ g g' ih ih' =>
    rcases ih with ⟨⟨n, x⟩, rfl⟩
    rcases ih' with ⟨⟨m, y⟩, rfl⟩
    refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
    · simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      refine CofilteredClosureSmall.InductiveStep.eq ?_ ?_ x y g g'
      all_goals apply Nat.lt_succ_of_le
      exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]
    · simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
      rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.FintypeCat (goal)
Goal:
X : FintypeCat
f : X.obj → X.obj
⊢ homMk f = 𝟙 X ↔ f = id
have mp : homMk f = 𝟙 X → f = id
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.FintypeCat (goal)
Goal:
X : FintypeCat
f : X.obj → X.obj
mp : homMk f = 𝟙 X → f = id
⊢ homMk f = 𝟙 X ↔ f = id
have mpr : f = id → homMk f = 𝟙 X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.FintypeCat (goal)
Goal:
X : FintypeCat
f : X.obj → X.obj
h : homMk f = 𝟙 X
⊢ f = id
have mp : ∀ (x : X.obj), f x = id x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.FintypeCat (goal)
Goal:
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h : X.obj → Z.obj
⊢ homMk h = homMk f ≫ homMk g ↔ h = g ∘ f
have mp : homMk h = homMk f ≫ homMk g → h = g ∘ f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.FintypeCat (goal)
Goal:
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h : X.obj → Z.obj
mp : homMk h = homMk f ≫ homMk g → h = g ∘ f
⊢ homMk h = homMk f ≫ homMk g ↔ h = g ∘ f
have mpr : h = g ∘ f → homMk h = homMk f ≫ homMk g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.FintypeCat (goal)
Goal:
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h_1 : X.obj → Z.obj
h : homMk h_1 = homMk f ≫ homMk g
⊢ h_1 = g ∘ f
have mp : ∀ (x : X.obj), h_1 x = (g ∘ f) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.FintypeCat (goal)
Goal:
X Y : Skeleton
h_1 : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ ULift.down.{u, 0} (h.inv (h.hom { down := a : ULift.{u, 0} (Fin X.len) })) = a
have change : ULift.down.{u, 0} ((h.hom ≫ h.inv) { down := a : ULift.{u, 0} (Fin X.len) }) = a
Tactic: change ((h.hom ≫ h.inv) _).down = _
-- Lean 4 proof step from Mathlib.CategoryTheory.FintypeCat (goal)
Goal:
X Y : Skeleton
h_1 : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ ULift.down.{u, 0} ((h.hom ≫ h.inv) { down := a : ULift.{u, 0} (Fin X.len) }) = a
have simp : ULift.down.{u, 0} (𝟙 X { down := a }) = a
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.FintypeCat (goal)
Goal:
X Y : Skeleton
h_1 : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ ULift.down.{u, 0} (h.hom (h.inv { down := a : ULift.{u, 0} (Fin Y.len) })) = a
have change : ULift.down.{u, 0} ((h.inv ≫ h.hom) { down := a : ULift.{u, 0} (Fin Y.len) }) = a
Tactic: change ((h.inv ≫ h.hom) _).down = _
-- Lean 4 proof step from Mathlib.CategoryTheory.FintypeCat (goal)
Goal:
X Y : Skeleton
h_1 : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ ULift.down.{u, 0} ((h.inv ≫ h.hom) { down := a : ULift.{u, 0} (Fin Y.len) }) = a
have simp : ULift.down.{u, 0} (𝟙 Y { down := a }) = a
Tactic: simp