awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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))
⊢ 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 right : Function.Surjective (α := (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
-- 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.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))
have left : Mono ((toRange p).app i)
Tactic: rw [← mono_iff_injective]
-- 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.Surjective (α := (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 right : Epi ((toRange p).app i)
Tactic: rw [← epi_iff_surjective]
-- 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)
G : Subfunctor F
p : F' ⟶ F
U V : C
f : U ⟶ V
⊢ Subset (α := Set (F'.obj U))
    (Set.preimage (β := F.obj U)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app U)) :
        (a : (fun (X : Type w) ↦ X) (F'.obj U)) → (fun (X : Type w) ↦ X) (F.obj U))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V)) ⁻¹'
        G.obj V))
    (Set.preimage (β := (fun (X : Type w) ↦ X) (F'.obj V))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f)) :
        (a : (fun (X : Type w) ↦ X) (F'.obj U)) → (fun (X : Type w) ↦ X) (F'.obj V))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app V)) :
          (a : (fun (X : Type w) ↦ X) (F'.obj V)) → (fun (X : Type w) ↦ X) (F.obj V)) ⁻¹'
        G.obj V))
have simp : Subset (α := Set (F'.obj U))
  ((fun (x : F'.obj U) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj U) → F.obj V)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app U) : (a : F'.obj U) → F.obj U) x : F.obj U)) ⁻¹'
    G.obj V)
  ((fun (x : F'.obj U) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj U) → F.obj V)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app U) : (a : F'.obj U) → F.obj U) x : F.obj U)) ⁻¹'
    G.obj V)
Tactic: simp only [Set.preimage_preimage, NatTrans.naturality_apply]
-- 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)
G : Subfunctor F
p : F' ⟶ F
⊢ range ((G.preimage p).ι ≫ p) ≤ G
have rw : (range (G.preimage p).ι).image p ≤ G
Tactic: rw [range_comp, range_ι, image_le_iff]
-- 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)
G : Subfunctor F
p : F' ⟶ F
rw : (range (G.preimage p).ι).image p ≤ G
⊢ range ((G.preimage p).ι ≫ p) ≤ G
have rw₁ : (G.preimage p).image p ≤ G
Tactic: rw [range_comp, range_ι, image_le_iff]
-- 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)
G : Subfunctor F
p : F' ⟶ F
rw : (range (G.preimage p).ι).image p ≤ G
rw₁ : (G.preimage p).image p ≤ G
⊢ range ((G.preimage p).ι ≫ p) ≤ G
have rw₂ : G.preimage p ≤ G.preimage p
Tactic: rw [range_comp, range_ι, image_le_iff]
-- 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)
G : Subfunctor F
p : F' ⟶ F
⊢ G.preimage p = ⊤ ↔ range p ≤ G
have rw : G.preimage p = ⊤ ↔ ⊤ ≤ G.preimage p
Tactic: rw [← image_top, image_le_iff]
-- 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)
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
⊢ (G.preimage p).image p = G
have a : (G.preimage p).image p ≤ G
Tactic: apply le_antisymm
-- 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)
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
a : (G.preimage p).image p ≤ G
⊢ (G.preimage p).image p = G
have a₁ : G ≤ (G.preimage p).image p
Tactic: apply le_antisymm
-- 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)
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
⊢ (G.preimage p).image p ≤ G
have a : G.preimage p ≤ G.preimage p
Tactic: rw [image_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Image (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
i : C
x : F.obj i
hx : x ∈ G.obj i
⊢ x ∈ ((G.preimage p).image p).obj i
have hp₁ : ∀ (k : C),
  Function.Surjective (α := F'.obj k) (β := F.obj k)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app k)) : (a : F'.obj k) → F.obj k)
Tactic: simp only [NatTrans.epi_iff_epi_app, epi_iff_surjective] at hp
Cleared hypotheses: hp
-- 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)
G : Subfunctor F
p : F' ⟶ F
i : C
x : F.obj i
hx : x ∈ G.obj i
hp :
  ∀ (k : C),
    Function.Surjective (α := F'.obj k) (β := F.obj k)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app k)) : (a : F'.obj k) → F.obj k)
⊢ x ∈ ((G.preimage p).image p).obj i
have a : ∀ (y : F'.obj i)
  (hx :
    Membership.mem (α := F.obj i) (G.obj i)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) : (a : F'.obj i) → F.obj i) y : F.obj i)),
  Membership.mem (α := F.obj i) (((G.preimage p).image p).obj i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) : (a : F'.obj i) → F.obj i) y : F.obj i)
Tactic: obtain ⟨y, rfl⟩ := hp _ x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
G : Subfunctor F
⊢ ofSection x ≤ G ↔ x ∈ G.obj X
have mp : ofSection x ≤ G → x ∈ G.obj X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
G : Subfunctor F
mp : ofSection x ≤ G → x ∈ G.obj X
⊢ ofSection x ≤ G ↔ x ∈ G.obj X
have mpr : x ∈ G.obj X → ofSection x ≤ G
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
⊢ (ofSection x).image f =
    ofSection (X := 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)
have a : (ofSection x).image f ≤
  ofSection (X := 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)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
a :
  (ofSection x).image f ≤
    ofSection (X := 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)
⊢ (ofSection x).image f =
    ofSection (X := 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)
have a₁ : ofSection (X := 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) ≤
  (ofSection x).image f
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
⊢ (ofSection x).image f ≤
    ofSection (X := 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)
have a : Membership.mem (α := (fun (X : Type w) ↦ X) (F'.obj X)) (γ := Set ((fun (X : Type w) ↦ X) (F'.obj X)))
  (obj
    (ofSection (X := 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))
    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 :
    (fun (X : Type w) ↦ X) (F'.obj X))
Tactic: rw [image_le_iff, ofSection_le_iff, preimage_obj, Set.mem_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : Cᵒᵖ
x : F.obj X
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
⊢ ofSection (X := 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) ≤
    (ofSection x).image f
have a : ∃ x_1 ∈ (ofSection x).obj X,
  Eq (α := F'.obj X) ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) : (a : F.obj X) → F'.obj X) x_1 : F'.obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) : (a : F.obj X) → F'.obj X) x : F'.obj X)
Tactic: simp only [ofSection_le_iff, image_obj, Set.mem_image]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : Cᵒᵖ
x : F.obj X
⊢ ofSection x =
    range (F' := Functor.obj yoneda (Opposite.unop X))
      ((Equiv.symm yonedaEquiv : (a : F.obj (Opposite.op (Opposite.unop X))) → yoneda.obj (Opposite.unop X) ⟶ F) x)
have obj : ∀ (U : Cᵒᵖ) (y : F.obj U),
  y ∈ (ofSection x).obj U ↔
    Membership.mem (γ := Set (F.obj U))
      (obj
        (range (F' := Functor.obj yoneda (Opposite.unop X))
          ((Equiv.symm yonedaEquiv : (a : F.obj (Opposite.op (Opposite.unop X))) → yoneda.obj (Opposite.unop X) ⟶ F) x))
        U)
      y
Tactic: ext U y
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔
    Membership.mem (γ := Set (F.obj U))
      (obj
        (range (F' := Functor.obj yoneda (Opposite.unop X))
          ((Equiv.symm yonedaEquiv : (a : F.obj (Opposite.op (Opposite.unop X))) → yoneda.obj (Opposite.unop X) ⟶ F) x))
        U)
      y
have obj : (∃ (f : X ⟶ U), (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj U) x = y) ↔
  ∃ (y_1 : Opposite.unop U ⟶ Opposite.unop X),
    (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj X) → yoneda.obj (Opposite.unop X) ⟶ F) x) U) :
          (a : Opposite.unop U ⟶ Opposite.unop X) → F.obj U)
        y_1 =
      y
Tactic: simp only [ofSection_obj, Set.mem_setOf_eq, Opposite.op_unop, range_obj, yoneda_obj_obj,
    Set.mem_range]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ (f : X ⟶ U), (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj U) x = y) ↔
    ∃ (y_1 : Opposite.unop U ⟶ Opposite.unop X),
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj X) → yoneda.obj (Opposite.unop X) ⟶ F) x) U) :
            (a : Opposite.unop U ⟶ Opposite.unop X) → F.obj U)
          y_1 =
        y
have obj : (∃ (f : X ⟶ U), (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj U) x = y) →
  ∃ (y_1 : Opposite.unop U ⟶ Opposite.unop X),
    (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj X) → yoneda.obj (Opposite.unop X) ⟶ F) x) U) :
          (a : Opposite.unop U ⟶ Opposite.unop X) → F.obj U)
        y_1 =
      y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
obj :
  (∃ (f : X ⟶ U), (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj U) x = y) →
    ∃ (y_1 : Opposite.unop U ⟶ Opposite.unop X),
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj X) → yoneda.obj (Opposite.unop X) ⟶ F) x) U) :
            (a : Opposite.unop U ⟶ Opposite.unop X) → F.obj U)
          y_1 =
        y
⊢ (∃ (f : X ⟶ U), (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj U) x = y) ↔
    ∃ (y_1 : Opposite.unop U ⟶ Opposite.unop X),
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj X) → yoneda.obj (Opposite.unop X) ⟶ F) x) U) :
            (a : Opposite.unop U ⟶ Opposite.unop X) → F.obj U)
          y_1 =
        y
have obj₁ : (∃ (y_1 : Opposite.unop U ⟶ Opposite.unop X),
    (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : F.obj X) → yoneda.obj (Opposite.unop X) ⟶ F) x) U) :
          (a : Opposite.unop U ⟶ Opposite.unop X) → F.obj U)
        y_1 =
      y) →
  ∃ (f : X ⟶ U), (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj U) x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : C
f : Functor.obj yoneda X ⟶ F
⊢ range f = ofSection (X := Opposite.op X) ((yonedaEquiv : (a : yoneda.obj X ⟶ F) → F.obj (Opposite.op X)) f)
have rw : range f =
  range (F' := Functor.obj yoneda (Opposite.unop (Opposite.op X)))
    ((Equiv.symm yonedaEquiv :
        (a : F.obj (Opposite.op (Opposite.unop (Opposite.op X)))) → yoneda.obj (Opposite.unop (Opposite.op X)) ⟶ F)
      ((yonedaEquiv : (a : yoneda.obj X ⟶ F) → F.obj (Opposite.op X)) f))
Tactic: rw [ofSection_eq_range, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : C
f : Functor.obj yoneda X ⟶ F
rw :
  range f =
    range (F' := Functor.obj yoneda (Opposite.unop (Opposite.op X)))
      ((Equiv.symm yonedaEquiv :
          (a : F.obj (Opposite.op (Opposite.unop (Opposite.op X)))) → yoneda.obj (Opposite.unop (Opposite.op X)) ⟶ F)
        ((yonedaEquiv : (a : yoneda.obj X ⟶ F) → F.obj (Opposite.op X)) f))
⊢ range f = ofSection (X := Opposite.op X) ((yonedaEquiv : (a : yoneda.obj X ⟶ F) → F.obj (Opposite.op X)) f)
have rw₁ : range f = range f
Tactic: rw [ofSection_eq_range, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
⊢ ofSection x =
    range (F' := Functor.obj uliftYoneda.{w, v, u} (Opposite.unop X))
      ((Equiv.symm uliftYonedaEquiv :
          (a : F.obj (Opposite.op (Opposite.unop X))) → uliftYoneda.{w, v, u}.obj (Opposite.unop X) ⟶ F)
        x)
have obj : ∀ (U : Cᵒᵖ) (y : F.obj U),
  y ∈ (ofSection x).obj U ↔
    Membership.mem (γ := Set (F.obj U))
      (obj
        (range (F' := Functor.obj uliftYoneda.{w, v, u} (Opposite.unop X))
          ((Equiv.symm uliftYonedaEquiv :
              (a : F.obj (Opposite.op (Opposite.unop X))) → uliftYoneda.{w, v, u}.obj (Opposite.unop X) ⟶ F)
            x))
        U)
      y
Tactic: ext U y
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔
    Membership.mem (γ := Set (F.obj U))
      (obj
        (range (F' := Functor.obj uliftYoneda.{w, v, u} (Opposite.unop X))
          ((Equiv.symm uliftYonedaEquiv :
              (a : F.obj (Opposite.op (Opposite.unop X))) → uliftYoneda.{w, v, u}.obj (Opposite.unop X) ⟶ F)
            x))
        U)
      y
have obj : y ∈ (ofSection x).obj U ↔
  Membership.mem (γ := Set (F.obj U))
    (Set.range fun (y : ULift.{w, v} (Opposite.unop U ⟶ Opposite.unop X)) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map y.down.op) : (a : F.obj X) → F.obj U) x)
    y
Tactic: dsimp [uliftYonedaEquiv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔
    Membership.mem (γ := Set (F.obj U))
      (Set.range fun (y : ULift.{w, v} (Opposite.unop U ⟶ Opposite.unop X)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map y.down.op) : (a : F.obj X) → F.obj U) x)
      y
have obj : y ∈ (ofSection x).obj U ↔
  ∃ (x_1 : Opposite.unop U ⟶ Opposite.unop X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1.op) : (a : F.obj X) → F.obj U) x = y
Tactic: simp only [Set.mem_range, ULift.exists]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔
    ∃ (x_1 : Opposite.unop U ⟶ Opposite.unop X),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1.op) : (a : F.obj X) → F.obj U) x = y
have obj : y ∈ (ofSection x).obj U →
  ∃ (x_1 : Opposite.unop U ⟶ Opposite.unop X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1.op) : (a : F.obj X) → F.obj U) x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
obj :
  y ∈ (ofSection x).obj U →
    ∃ (x_1 : Opposite.unop U ⟶ Opposite.unop X),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1.op) : (a : F.obj X) → F.obj U) x = y
⊢ y ∈ (ofSection x).obj U ↔
    ∃ (x_1 : Opposite.unop U ⟶ Opposite.unop X),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1.op) : (a : F.obj X) → F.obj U) x = y
have obj₁ : (∃ (x_1 : Opposite.unop U ⟶ Opposite.unop X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1.op) : (a : F.obj X) → F.obj U) x = y) →
  y ∈ (ofSection x).obj U
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : C
f : Functor.obj yoneda X ⋙ uliftFunctor.{w, v} ⟶ F
⊢ range f =
    ofSection (X := Opposite.op X)
      ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X ⟶ F) → F.obj (Opposite.op X)) f)
have rw : range f =
  range (F' := Functor.obj uliftYoneda.{w, v, u} (Opposite.unop (Opposite.op X)))
    ((Equiv.symm uliftYonedaEquiv :
        (a : F.obj (Opposite.op (Opposite.unop (Opposite.op X)))) →
          uliftYoneda.{w, v, u}.obj (Opposite.unop (Opposite.op X)) ⟶ F)
      ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X ⟶ F) → F.obj (Opposite.op X)) f))
Tactic: rw [ofSection_eq_range', Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.OfSection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : C
f : Functor.obj yoneda X ⋙ uliftFunctor.{w, v} ⟶ F
rw :
  range f =
    range (F' := Functor.obj uliftYoneda.{w, v, u} (Opposite.unop (Opposite.op X)))
      ((Equiv.symm uliftYonedaEquiv :
          (a : F.obj (Opposite.op (Opposite.unop (Opposite.op X)))) →
            uliftYoneda.{w, v, u}.obj (Opposite.unop (Opposite.op X)) ⟶ F)
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X ⟶ F) → F.obj (Opposite.op X)) f))
⊢ range f =
    ofSection (X := Opposite.op X)
      ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X ⟶ F) → F.obj (Opposite.op X)) f)
have rw₁ : range f = range f
Tactic: rw [ofSection_eq_range', Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Sieves (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ unop U
f₂ : Y₂ ⟶ unop U
h₁ : (G.sieveOfSection s).arrows f₁
h₂ : (G.sieveOfSection s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Eq (α := (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Y₁))) → (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
        (G.familyOfElementsOfSection s f₁ h₁) :
      (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Y₂))) → (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
        (G.familyOfElementsOfSection s f₂ h₂) :
      (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
have refine : Eq.{w + 1} (α := F.obj (op Z))
  (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Y₁))) → (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
        (G.familyOfElementsOfSection s f₁ h₁)) :
    F.obj (op Z))
  (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Y₂))) → (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
        (G.familyOfElementsOfSection s f₂ h₂)) :
    F.obj (op Z))
Tactic: refine Subtype.ext ?_