awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → Function.Embedding.{v + 1, w + 1} (X ⟶ Y) Ω := fun (X Y : C) ↦ ⋯.some
e : Equiv.{u + 1, w + 1} C (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w) :=
  Equiv.ofInjective (⇑f₁ : (a : C) → Ω) ⋯
h : CoreSmallCategoryOfSet.{w, v, u} Ω C :=
  { obj := Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω),
    hom := fun (X Y : (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w)) ↦
      Set.range.{w, v + 1} (ι :=
        Quiver.Hom.{v, u} (V := C) ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X : C)
          ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y : C))
        (⇑(f₂ ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X)
              ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y)) :
          (a :
              (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X ⟶
                (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y) →
            Ω),
    objEquiv := e.symm,
    homEquiv := fun {x x_1 : (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w)} ↦
      Equiv.symm
        (Equiv.ofInjective
          (⇑(f₂ ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x)
                ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1)) :
            (a :
                (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x ⟶
                  (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1) →
              Ω)
          ⋯) }
⊢ ∃ (S : SmallCategoryCardinalLT κ), Nonempty (Equivalence.{w, v, w, u} (categoryFamily κ S) C)
have refine : HasCardinalLT (Arrow (↑h.smallCategoryOfSet.obj : Type w)) κ
Tactic: refine ⟨⟨h.smallCategoryOfSet, ?_⟩, ⟨h.equivalence⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
S : Set (Subfunctor F)
U V : C
f : U ⟶ V
x : F.obj U
hx : Membership.mem (γ := Set (F.obj U)) (sSup ((fun (T : Subfunctor F) ↦ T.obj U) '' S)) x
⊢ Membership.mem (γ := Set (F.obj U))
    (Set.preimage (β := (fun (X : Type w) ↦ X) (F.obj V))
      (⇑(hom (FC := TypeCat.Fun) (F.map f)) : (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
      (sSup ((fun (T : Subfunctor F) ↦ T.obj V) '' S)))
    x
have obtain : ∀ (F_1 : Subfunctor F) (h : F_1 ∈ S)
  (h' : Membership.mem (γ := Set (F.obj U)) ((fun (T : Subfunctor F) ↦ T.obj U) F_1) x),
  Membership.mem (γ := Set (F.obj U))
    (Set.preimage (β := (fun (X : Type w) ↦ X) (F.obj V))
      (⇑(hom (FC := TypeCat.Fun) (F.map f)) : (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
      (sSup ((fun (T : Subfunctor F) ↦ T.obj V) '' S)))
    x
Tactic: obtain ⟨_, ⟨F, h, rfl⟩, h'⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F_1 F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F_1
S : Set (Subfunctor F_1)
U V : C
f : U ⟶ V
x : F_1.obj U
F : Subfunctor F_1
h : F ∈ S
h' : Membership.mem (γ := Set (F_1.obj U)) ((fun (T : Subfunctor F_1) ↦ T.obj U) F) x
⊢ Membership.mem (γ := Set (F_1.obj U))
    (Set.preimage (β := (fun (X : Type w) ↦ X) (F_1.obj V))
      (⇑(hom (FC := TypeCat.Fun) (F_1.map f)) :
        (a : (fun (X : Type w) ↦ X) (F_1.obj U)) → (fun (X : Type w) ↦ X) (F_1.obj V))
      (sSup ((fun (T : Subfunctor F_1) ↦ T.obj V) '' S)))
    x
have simp : ∃ i ∈ S,
  Membership.mem (α := F_1.obj V) (i.obj V)
    ((hom (FC := TypeCat.Fun) (F_1.map f) : (a : F_1.obj U) → F_1.obj V) x : F_1.obj V)
Tactic: simp only [Set.sSup_eq_sUnion, Set.sUnion_image, Set.preimage_iUnion,
          Set.mem_iUnion, Set.mem_preimage, exists_prop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
h : G ≤ G'
⊢ homOfLe h ≫ G'.ι = G.ι
have w : ∀ (x : C) (x_1 : G.toFunctor.obj x),
  (hom (FC := TypeCat.Fun) ((homOfLe h ≫ G'.ι).app x)).toFun x_1 = (hom (FC := TypeCat.Fun) (G.ι.app x)).toFun x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
⊢ IsIso (C := Functor.{v, w, u, w + 1} C (Type w)) (X := toFunctor (F := F) ⊤) (ι ⊤)
have refine : ∀ (X : C), IsIso.{w, w + 1} (X := Functor.obj.{v, w, u, w + 1} (toFunctor (F := F) ⊤) X) (NatTrans.app (ι ⊤) X)
Tactic: refine @NatIso.isIso_of_isIso_app _ _ _ _ _ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
X : C
⊢ IsIso.{w, w + 1} (X := Functor.obj.{v, w, u, w + 1} (toFunctor (F := F) ⊤) X) (NatTrans.app (ι ⊤) X)
have rw : Function.Bijective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (toFunctor (F := F) ⊤) X)) (β :=
  (fun (X : Type w) ↦ X) (F.obj X))
  (⇑(hom (FC := TypeCat.Fun) (NatTrans.app (ι ⊤) X)) :
    (a : (fun (X : Type w) ↦ X) (⊤.toFunctor.obj X)) → (fun (X : Type w) ↦ X) (F.obj X))
Tactic: rw [isIso_iff_bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
⊢ G = ⊤ ↔ IsIso G.ι
have mp : G = ⊤ → IsIso G.ι
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
mp : G = ⊤ → IsIso G.ι
⊢ G = ⊤ ↔ IsIso G.ι
have mpr : IsIso G.ι → G = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
H : IsIso G.ι
⊢ G = ⊤
have mpr : ∀ (U : C) (x : F.obj U), x ∈ G.obj U ↔ Membership.mem (γ := Set (F.obj U)) (obj ⊤ U) x
Tactic: ext U x
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
H : IsIso G.ι
U : C
x : F.obj U
⊢ x ∈ G.obj U ↔ Membership.mem (γ := Set (F.obj U)) (obj ⊤ U) x
have mpr : x ∈ G.obj U
Tactic: apply (iff_of_eq (iff_true _)).mpr
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
H : IsIso G.ι
U : C
x : F.obj U
⊢ x ∈ G.obj U
have mpr : Membership.mem (α := F.obj U) (G.obj U)
  ((hom (FC := TypeCat.Fun) (G.ι.app U) : (a : G.toFunctor.obj U) → F.obj U)
      ((hom (FC := TypeCat.Fun) (inv (G.ι.app U)) : (a : F.obj U) → G.toFunctor.obj U) x : G.toFunctor.obj U) :
    F.obj U)
Tactic: rw [← IsIso.inv_hom_id_apply (G.ι.app U) x]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
U V : C
φ : U ⟶ V
x : F₁.obj U
hx : x ∈ A.obj U
h :
  Eq (α := (fun (X : Type w) ↦ X) (F₂.obj U))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app U) :
          (a : (fun (X : Type w) ↦ X) (A.toFunctor.obj U)) → (fun (X : Type w) ↦ X) (F₂.obj U))
        (Subtype.mk (p := fun (x : F₁.obj U) ↦ x ∈ A.obj U) x hx) :
      (fun (X : Type w) ↦ X) (F₂.obj U))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (g.app U) :
          (a : (fun (X : Type w) ↦ X) (A.toFunctor.obj U)) → (fun (X : Type w) ↦ X) (F₂.obj U))
        (Subtype.mk (p := fun (x : F₁.obj U) ↦ x ∈ A.obj U) x hx) :
      (fun (X : Type w) ↦ X) (F₂.obj U))
⊢ Eq (α := F₂.obj V)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.map φ) : (a : F₂.obj U) → F₂.obj V)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app U) : (a : A.toFunctor.obj U) → F₂.obj U)
            (Subtype.mk (p := fun (x : F₁.obj U) ↦ x ∈ A.obj U) x hx) :
          F₂.obj U) :
      F₂.obj V)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.map φ) : (a : F₂.obj U) → F₂.obj V)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (g.app U) : (a : A.toFunctor.obj U) → F₂.obj U)
            (Subtype.mk (p := fun (x : F₁.obj U) ↦ x ∈ A.obj U) x hx) :
          F₂.obj U) :
      F₂.obj V)
have rw : Eq (α := F₂.obj V)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.map φ) : (a : F₂.obj U) → F₂.obj V)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (g.app U) :
            (a : (fun (X : Type w) ↦ X) (A.toFunctor.obj U)) → (fun (X : Type w) ↦ X) (F₂.obj U))
          (Subtype.mk (p := fun (x : F₁.obj U) ↦ x ∈ A.obj U) x hx) :
        (fun (X : Type w) ↦ X) (F₂.obj U)) :
    F₂.obj V)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.map φ) : (a : F₂.obj U) → F₂.obj V)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (g.app U) : (a : A.toFunctor.obj U) → F₂.obj U)
          (Subtype.mk (p := fun (x : F₁.obj U) ↦ x ∈ A.obj U) x hx) :
        F₂.obj U) :
    F₂.obj V)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
G : Functor.{v, w, u, w + 1} C (Type w)
φ : G ⟶ A.toFunctor
⊢ range (φ ≫ A.ι) ≤ Subfunctor.equalizer f g ↔ φ ≫ f = φ ≫ g
have rw : range (φ ≫ A.ι) ≤ Subfunctor.equalizer f g ↔ (φ ≫ f).app = (φ ≫ g).app
Tactic: rw [NatTrans.ext_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Equalizer (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
⊢ Subfunctor.equalizer f g = A ↔ f = g
have this : range (𝟙 A.toFunctor ≫ A.ι) ≤ Subfunctor.equalizer f g ↔ 𝟙 A.toFunctor ≫ f = 𝟙 A.toFunctor ≫ g
Tactic: have := range_le_equalizer_iff f g (𝟙 _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Equalizer (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : range (𝟙 A.toFunctor ≫ A.ι) ≤ Subfunctor.equalizer f g ↔ 𝟙 A.toFunctor ≫ f = 𝟙 A.toFunctor ≫ g
⊢ Subfunctor.equalizer f g = A ↔ f = g
have this₁ : A ≤ Subfunctor.equalizer f g ↔ f = g
Tactic: simp only [Category.id_comp, range_ι] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
⊢ Subfunctor.equalizer f g = A ↔ f = g
have rw : Subfunctor.equalizer f g = A ↔ A ≤ Subfunctor.equalizer f g
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
⊢ Subfunctor.equalizer f g = A ↔ A ≤ Subfunctor.equalizer f g
have mp : Subfunctor.equalizer f g = A → A ≤ Subfunctor.equalizer f g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
mp : Subfunctor.equalizer f g = A → A ≤ Subfunctor.equalizer f g
⊢ Subfunctor.equalizer f g = A ↔ A ≤ Subfunctor.equalizer f g
have mpr : A ≤ Subfunctor.equalizer f g → Subfunctor.equalizer f g = A
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
h : Subfunctor.equalizer f g = A
⊢ A ≤ Subfunctor.equalizer f g
have mp : A ≤ A
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
i : ι
⊢ ofSection (x i) ≤ G
have rw : ofSection (x i) ≤ ⨆ (i : ι), ofSection (x i)
Tactic: rw [← h.iSup_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
i : ι
⊢ Membership.mem (γ := Set (F.obj (X i))) (G.obj (X i)) (x i)
have rw : ofSection (x i) ≤ G
Tactic: rw [← ofSection_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
ι' : Type w''
e : ι' ≃ ι
⊢ G.IsGeneratedBy (X := fun (i' : ι') ↦ X ((e : (a : ι') → ι) i')) fun (i' : ι') ↦ x ((e : (a : ι') → ι) i')
have rw : Eq (α := Subfunctor F) (⨆ (i : ι'), ofSection (X := X ((e : (a : ι') → ι) i)) (x ((e : (a : ι') → ι) i)))
  (⨆ (i : ι), ofSection (x i))
Tactic: rw [isGeneratedBy_iff, ← h.iSup_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
inst_1 : Finite ι
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
⊢ G.IsFinite
have obtain : ∀ (n : ℕ) (e : ι ≃ Fin n), G.IsFinite
Tactic: obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ Eq (α := Subfunctor.{v, v, u} (Functor.obj yoneda X)) (⨆ (i : Unit), Subfunctor.ofSection (𝟙 X)) ⊤
have obj : ∀ (U : Cᵒᵖ) (u : Functor.obj (Functor.obj yoneda X) U),
  Membership.mem (γ := Set (Functor.obj (Functor.obj yoneda X) U))
      (Subfunctor.obj (⨆ (i : Unit), Subfunctor.ofSection (𝟙 X)) U) u ↔
    Membership.mem (γ := Set (Functor.obj (Functor.obj yoneda X) U)) (Subfunctor.obj ⊤ U) u
Tactic: ext U u
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
U : Cᵒᵖ
u : Functor.obj (Functor.obj yoneda X) U
⊢ Membership.mem (γ := Set (Functor.obj (Functor.obj yoneda X) U))
      (Subfunctor.obj (⨆ (i : Unit), Subfunctor.ofSection (𝟙 X)) U) u ↔
    Membership.mem (γ := Set (Functor.obj (Functor.obj yoneda X) U)) (Subfunctor.obj ⊤ U) u
have obj : Membership.mem (γ := Set (unop U ⟶ X))
  (Subfunctor.obj (Subfunctor.ofSection (𝟙 X)) U : Set (Functor.obj (Functor.obj yoneda X) U)) u
Tactic: simp only [yoneda_obj_obj, Subfunctor.iSup_obj, Set.mem_iUnion,
    exists_const, Subfunctor.top_obj, Set.top_eq_univ, Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Image (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
f : F' ⟶ F
G : Subfunctor F
hf : range f ≤ G
x x_1 : C
g : x ⟶ x_1
⊢ (F'.map g ≫
      ↾fun (x : F'.obj x_1) ↦
        Subtype.mk (p := fun (x : F.obj x_1) ↦ x ∈ G.obj x_1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x_1) :
              (a : (fun (X : Type w) ↦ X) (F'.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
            x)
          ⋯) =
    (↾fun (x_2 : F'.obj x) ↦
        Subtype.mk (p := fun (x_3 : F.obj x) ↦ x_3 ∈ G.obj x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x) :
              (a : (fun (X : Type w) ↦ X) (F'.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
            x_2)
          ⋯) ≫
      G.toFunctor.map g
have h : ∀ (x_2 : F'.obj x),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (F'.map g ≫
          ↾fun (x : F'.obj x_1) ↦
            Subtype.mk (p := fun (x : F.obj x_1) ↦ x ∈ G.obj x_1)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x_1) :
                  (a : (fun (X : Type w) ↦ X) (F'.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
                x)
              sorry))
      x_2 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x_3 : F'.obj x) ↦
            Subtype.mk (p := fun (x_4 : F.obj x) ↦ x_4 ∈ G.obj x)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x) :
                  (a : (fun (X : Type w) ↦ X) (F'.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
                x_3)
              sorry) ≫
          G.toFunctor.map g))
      x_2
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Image (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
⊢ range (toRange p) = ⊤
have obj : ∀ (i : C) (x : F.obj i) (hx : x ∈ (range p).obj i),
  Subtype.mk (p := fun (x : F.obj i) ↦ x ∈ (range p).obj i) x hx ∈ (range (toRange p)).obj i ↔
    Membership.mem (γ := Set ((range p).toFunctor.obj i)) (obj ⊤ i)
      (Subtype.mk (p := fun (x : F.obj i) ↦ x ∈ (range p).obj i) x hx)
Tactic: ext i ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Image (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
i : C
x : F.obj i
hx :
  Membership.mem (γ := Set (F.obj i))
    (Set.range (ι := F'.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i)) x
⊢ Membership.mem (γ :=
      Set
        (↑(Set.range (ι := F'.obj i)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i)) :
          Type w))
      (Set.range (ι := F'.obj i)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i)) :
          (a : F'.obj i) → (↑(Set.range (⇑(ConcreteCategory.hom (p.app i)) : (a : F'.obj i) → F.obj i)) : Type w)))
      (Subtype.mk (p := fun (x : F.obj i) ↦
        Membership.mem (γ := Set (F.obj i))
          (Set.range (ι := F'.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
          x)
        x hx) ↔
    Membership.mem (γ :=
      Set
        (↑(Set.range (ι := F'.obj i)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i)) :
          Type w))
      Set.univ
      (Subtype.mk (p := fun (x : F.obj i) ↦
        Membership.mem (γ := Set (F.obj i))
          (Set.range (ι := F'.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
          x)
        x hx)
have obj : ∃ (y : F'.obj i),
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i) :
        (a : F'.obj i) → (↑(Set.range (⇑(ConcreteCategory.hom (p.app i)) : (a : F'.obj i) → F.obj i)) : Type w))
      y =
    Subtype.mk (p := fun (x : F.obj i) ↦
      Membership.mem (γ := Set (F.obj i))
        (Set.range (ι := F'.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
        x)
      x hx
Tactic: simp only [Set.mem_range, Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Image (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
i : C
x : F.obj i
hx :
  Membership.mem (γ := Set (F.obj i))
    {x : F.obj i |
      ∃ (y : F'.obj i), (ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) : (a : F'.obj i) → F.obj i) y = x}
    x
⊢ ∃ (y : F'.obj i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i) :
          (a : F'.obj i) → (↑(Set.range (⇑(ConcreteCategory.hom (p.app i)) : (a : F'.obj i) → F.obj i)) : Type w))
        y =
      Subtype.mk (p := fun (x : F.obj i) ↦
        Membership.mem (γ := Set (F.obj i))
          (Set.range (ι := F'.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
          x)
        x hx
have obj : ∀ (y : F'.obj i),
  ∃ (y_1 : F'.obj i),
    Eq (α :=
      (↑(Set.range (ι := F'.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i)) :
        Type w))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i) :
            (a : F'.obj i) → (↑(Set.range (⇑(ConcreteCategory.hom (p.app i)) : (a : F'.obj i) → F.obj i)) : Type w))
          y_1 :
        (↑(Set.range (ι := F'.obj i)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i)) :
          Type w))
      (Subtype.mk (p := fun (x : F.obj i) ↦
          Membership.mem (γ := Set (F.obj i))
            (Set.range (ι := F'.obj i)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
            x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) : (a : F'.obj i) → F.obj i) y) sorry :
        { x : F.obj i //
          Membership.mem (γ := Set (F.obj i))
            (Set.range (ι := F'.obj i)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
            x })
Tactic: obtain ⟨y, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Image (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
inst_1 : Mono p
⊢ IsIso (toRange p)
have this : Mono (toRange p)
Tactic: have := mono_of_mono_fac (toRange_ι p)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Image (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
inst_1 : Mono p
this : Mono (toRange p)
⊢ IsIso (toRange p)
have rw : ∀ (X : C), IsIso ((toRange p).app X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Image (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
inst_1 : Mono p
this : Mono (toRange p)
i : C
⊢ IsIso ((toRange p).app i)
have rw : Function.Bijective (α := (fun (X : Type w) ↦ X) (F'.obj i)) (β := (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i)) :
    (a : (fun (X : Type w) ↦ X) (F'.obj i)) → (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
Tactic: rw [isIso_iff_bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Image (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
inst_1 : Mono p
this : Mono (toRange p)
i : C
⊢ Function.Bijective (α := (fun (X : Type w) ↦ X) (F'.obj i)) (β := (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i)) :
      (a : (fun (X : Type w) ↦ X) (F'.obj i)) → (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
have left : Function.Injective (α := (fun (X : Type w) ↦ X) (F'.obj i)) (β := (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i)) :
    (a : (fun (X : Type w) ↦ X) (F'.obj i)) → (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
Tactic: constructor