awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
⊢ Eq (α :=
    pullback (X := coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Y :=
        coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (coequalizer.desc f ⋯)
        (coequalizer.desc f ⋯) ⟶
      coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f))
    (pullback.fst (coequalizer.desc f ⋯) (coequalizer.desc f ⋯))
    (pullback.snd (coequalizer.desc f ⋯) (coequalizer.desc f ⋯))
have h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)
Tactic: have h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e) := by
    refine .of_right ?_ (by simp [g₁, g₂]) (.of_hasPullback e k₁)
    refine .of_bot ?_ ?_ (.paste_horiz (.of_hasPullback k₂ e) (.of_hasPullback m m))
    · simpa [g₁, g₂, e, m, pullback.lift_fst, pullback.lift_snd] using .of_hasPullback f f
    · simp [g₁, g₂, k₁, d]
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)
⊢ IsRegularEpi g₁
have apply : MorphismProperty.regularEpi C (X := pullback k₂ e) (pullback.fst k₂ e)
Tactic: apply Regular.regularEpiIsStableUnderBaseChange.of_isPullback h.flip
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)
⊢ Eq (α :=
    pullback (X := coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Y :=
        coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (coequalizer.desc f ⋯)
        (coequalizer.desc f ⋯) ⟶
      coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f))
    (pullback.fst (coequalizer.desc f ⋯) (coequalizer.desc f ⋯))
    (pullback.snd (coequalizer.desc f ⋯) (coequalizer.desc f ⋯))
have this : IsRegularEpi g₁
Tactic: have : IsRegularEpi g₁ := by
    apply Regular.regularEpiIsStableUnderBaseChange.of_isPullback h.flip
    dsimp [MorphismProperty.regularEpi]
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)
this : IsRegularEpi g₁
⊢ Eq (α :=
    pullback (X := coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Y :=
        coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (coequalizer.desc f ⋯)
        (coequalizer.desc f ⋯) ⟶
      coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f))
    (pullback.fst (coequalizer.desc f ⋯) (coequalizer.desc f ⋯))
    (pullback.snd (coequalizer.desc f ⋯) (coequalizer.desc f ⋯))
have rw : (g₁ ≫ pullback.snd e k₁) ≫ pullback.fst (coequalizer.desc f sorry) (coequalizer.desc f sorry) =
  (g₁ ≫ pullback.snd e k₁) ≫ pullback.snd (coequalizer.desc f sorry) (coequalizer.desc f sorry)
Tactic: rw [← cancel_epi (g₁ ≫ pullback.snd e k₁)]
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)
this : IsRegularEpi g₁
⊢ (g₁ ≫ pullback.snd e k₁) ≫ pullback.fst (coequalizer.desc f ⋯) (coequalizer.desc f ⋯) =
    (g₁ ≫ pullback.snd e k₁) ≫ pullback.snd (coequalizer.desc f ⋯) (coequalizer.desc f ⋯)
have h₁ : (g₁ ≫ pullback.snd e k₁) ≫ pullback.fst (coequalizer.desc f sorry) (coequalizer.desc f sorry) =
  pullback.fst f f ≫ coequalizer.π (pullback.fst f f) (pullback.snd f f)
Tactic: convert! coequalizer.condition (pullback.fst f f) (pullback.snd f f) using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)
this : IsRegularEpi g₁
h₁ :
  (g₁ ≫ pullback.snd e k₁) ≫ pullback.fst (coequalizer.desc f ⋯) (coequalizer.desc f ⋯) =
    pullback.fst f f ≫ coequalizer.π (pullback.fst f f) (pullback.snd f f)
⊢ (g₁ ≫ pullback.snd e k₁) ≫ pullback.fst (coequalizer.desc f ⋯) (coequalizer.desc f ⋯) =
    (g₁ ≫ pullback.snd e k₁) ≫ pullback.snd (coequalizer.desc f ⋯) (coequalizer.desc f ⋯)
have h₂ : (g₁ ≫ pullback.snd e k₁) ≫ pullback.snd (coequalizer.desc f sorry) (coequalizer.desc f sorry) =
  pullback.snd f f ≫ coequalizer.π (pullback.fst f f) (pullback.snd f f)
Tactic: convert! coequalizer.condition (pullback.fst f f) (pullback.snd f f) using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
⊢ IsRegularEpi (strongEpiMonoFactorisation f).e
have dsimp : IsRegularEpi (Y := coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f))
  (coequalizer.π (pullback.fst f f) (pullback.snd f f))
Tactic: dsimp [strongEpiMonoFactorisation]
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
A B : C
f : A ⟶ B
A' : Subobject.{v, u} A
B' : Subobject.{v, u} B
⊢ IsPullback (frobeniusMorphism f A' B') ((A' ⊓ (Subobject.pullback f).obj B').ofLE A' ⋯)
    (((«exists» f).obj A' ⊓ B').ofLE ((«exists» f).obj A') ⋯) (imageFactorisation f A').F.e
have apply : IsPullback (frobeniusMorphism f A' B' ≫ ((«exists» f).obj A' ⊓ B').ofLE B' sorry)
  ((A' ⊓ (Subobject.pullback f).obj B').ofLE A' sorry) B'.arrow
  ((imageFactorisation f A').F.e ≫ ((«exists» f).obj A').arrow)
Tactic: apply IsPullback.of_right (t := (inf_isPullback ((«exists» f).obj A') B').flip)
    (p := by simp [frobeniusMorphism])
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f_1 : X ⟶ Y
A B : C
f : A ⟶ B
A' : Subobject.{v, u} A
B' : Subobject.{v, u} B
⊢ IsRegularEpi (X := Functor.obj underlying (A' ⊓ (Subobject.pullback f).obj B')) (Y :=
    Functor.obj underlying ((«exists» f).obj A' ⊓ B'))
    (frobeniusMorphism f A' B' :
      Functor.obj underlying (A' ⊓ (Subobject.pullback f).obj B') ⟶ Functor.obj underlying ((«exists» f).obj A' ⊓ B'))
have apply : MorphismProperty.regularEpi C (imageFactorisation f A').F.e
Tactic: apply regularEpiIsStableUnderBaseChange.of_isPullback (frobeniusMorphism_isPullback f A' B').flip
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f_1 : X ⟶ Y
A B : C
f : A ⟶ B
A' : Subobject.{v, u} A
B' : Subobject.{v, u} B
⊢ MorphismProperty.regularEpi C (imageFactorisation f A').F.e
have this : StrongEpi (imageFactorisation f A').F.e
Tactic: have := strongEpi_of_strongEpiMonoFactorisation (strongEpiMonoFactorisation (A'.arrow ≫ f))
    (imageFactorisation f A').isImage
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f_1 : X ⟶ Y
A B : C
f : A ⟶ B
A' : Subobject.{v, u} A
B' : Subobject.{v, u} B
⊢ frobeniusMorphism f A' B' ≫ ((«exists» f).obj A' ⊓ B').arrow = (A' ⊓ (Subobject.pullback f).obj B').arrow ≫ f
have rw : ((A' ⊓ (Subobject.pullback f).obj B').ofLE A' sorry ≫ (imageFactorisation f A').F.e) ≫ ((«exists» f).obj A').arrow =
  (A' ⊓ (Subobject.pullback f).obj B').arrow ≫ f
Tactic: rw [frobeniusMorphism, ← inf_comp_left, ← Category.assoc,
      (inf_isPullback ((«exists» f).obj A') B').flip.lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.RepresentedBy (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 (op X)
⊢ F.IsRepresentedBy x ↔
    IsIso (X := obj uliftYoneda.{w, v, u} X)
      ((Equiv.symm uliftYonedaEquiv :
            (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
          { down := x } :
        obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
have rw : (∀ {Y : C},
    Function.Bijective.{v + 1, w + 1} (β := (fun (X : Type w) ↦ X) (F.obj (op Y))) fun (f : Y ⟶ X) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
        x) ↔
  ∀ (x_1 : C),
    IsIso (C := Type (max w v)) (X := obj (obj uliftYoneda.{w, v, u} X) (op x_1)) (Y :=
      (F ⋙ uliftFunctor.{v, w}).obj (op x_1))
      (NatTrans.app
        ((Equiv.symm uliftYonedaEquiv :
            (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
          { down := x })
        (op x_1))
Tactic: rw [isRepresentedBy_iff, NatTrans.isIso_iff_isIso_app, Opposite.op_surjective.forall]
-- Lean 4 proof step from Mathlib.CategoryTheory.RepresentedBy (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 (op X)
⊢ (∀ {Y : C},
      Function.Bijective.{v + 1, w + 1} (β := (fun (X : Type w) ↦ X) (F.obj (op Y))) fun (f : Y ⟶ X) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
          x) ↔
    ∀ (x_1 : C),
      IsIso (C := Type (max w v)) (X := obj (obj uliftYoneda.{w, v, u} X) (op x_1)) (Y :=
        (F ⋙ uliftFunctor.{v, w}).obj (op x_1))
        (NatTrans.app
          ((Equiv.symm uliftYonedaEquiv :
              (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
            { down := x })
          (op x_1))
have refine : ∀ (Y : C),
  (Function.Bijective.{v + 1, w + 1} (β := (fun (X : Type w) ↦ X) (F.obj (op Y))) fun (f : Y ⟶ X) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
        x) ↔
    IsIso (C := Type (max w v)) (X := obj (obj uliftYoneda.{w, v, u} X) (op Y)) (Y :=
      (F ⋙ uliftFunctor.{v, w}).obj (op Y))
      (NatTrans.app
        ((Equiv.symm uliftYonedaEquiv :
            (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
          { down := x })
        (op Y))
Tactic: refine forall_congr' fun Y ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.RepresentedBy (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 (op X)
Y : C
⊢ (Function.Bijective.{v + 1, w + 1} (β := (fun (X : Type w) ↦ X) (F.obj (op Y))) fun (f : Y ⟶ X) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
        x) ↔
    IsIso (C := Type (max w v)) (X := obj (obj uliftYoneda.{w, v, u} X) (op Y)) (Y :=
      (F ⋙ uliftFunctor.{v, w}).obj (op Y))
      (NatTrans.app
        ((Equiv.symm uliftYonedaEquiv :
            (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
          { down := x })
        (op Y))
have rw : (Function.Bijective.{v + 1, w + 1} (β := (fun (X : Type w) ↦ X) (F.obj (op Y))) fun (f : Y ⟶ X) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
      x) ↔
  Function.Bijective.{v + 1, w + 1} (α := obj (obj yoneda X) (op Y)) (β := F.obj (op Y))
    (Function.comp (β := ULift.{v, w} (F.obj (op Y))) (⇑Equiv.ulift : (a : ULift.{v, w} (F.obj (op Y))) → F.obj (op Y))
      (Function.comp (β := ULift.{w, v} (obj (obj yoneda X) (op Y)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                ((Equiv.symm uliftYonedaEquiv :
                    (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
                  { down := x : ULift.{v, w} (F.obj (op X)) })
                (op Y))) :
          (a : (fun (X : Type (max v w)) ↦ X) ((uliftYoneda.{w, v, u}.obj X).obj (op Y))) →
            (fun (X : Type (max v w)) ↦ X) ((F ⋙ uliftFunctor.{v, w}).obj (op Y)))
        (⇑(Equiv.symm Equiv.ulift) : (a : (yoneda.obj X).obj (op Y)) → ULift.{w, v} ((yoneda.obj X).obj (op Y)))))
Tactic: rw [isIso_iff_bijective, ← Function.Bijective.of_comp_iff _ Equiv.ulift.{w}.symm.bijective,
    ← Function.Bijective.of_comp_iff' Equiv.ulift.{v}.bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.RepresentedBy (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 (op X)
h : F.IsRepresentedBy x
⊢ IsIso (X := obj uliftYoneda.{w, v, u} X)
    ((Equiv.symm uliftYonedaEquiv :
          (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
        { down := x } :
      obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
have rwa : ∀
  (h :
    IsIso (X := obj uliftYoneda.{w, v, u} X)
      ((Equiv.symm uliftYonedaEquiv :
            (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
          { down := x } :
        obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})),
  IsIso (X := obj uliftYoneda.{w, v, u} X)
    ((Equiv.symm uliftYonedaEquiv :
          (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
        { down := x } :
      obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
Tactic: rwa [IsRepresentedBy.iff_isIso_uliftYonedaEquiv] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.RepresentedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
R : F.RepresentableBy X
⊢ F.IsRepresentedBy (X := X)
    (((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X))
have rw : IsIso (C := Cᵒᵖ ⥤ Type (max w v)) (X := (obj uliftYoneda.{w, v, u} X : Cᵒᵖ ⥤ Type (max w v))) (Y :=
  F ⋙ uliftFunctor.{v, w})
  ((Equiv.symm uliftYonedaEquiv :
        (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
      { down := ((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X) } :
    obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
Tactic: rw [IsRepresentedBy.iff_isIso_uliftYonedaEquiv]
-- Lean 4 proof step from Mathlib.CategoryTheory.RepresentedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
R : F.RepresentableBy X
⊢ IsIso (C := Cᵒᵖ ⥤ Type (max w v)) (X := (obj uliftYoneda.{w, v, u} X : Cᵒᵖ ⥤ Type (max w v))) (Y :=
    F ⋙ uliftFunctor.{v, w})
    ((Equiv.symm uliftYonedaEquiv :
          (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
        { down := ((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X) } :
      obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
have h : Eq (α := obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
  ((Equiv.symm uliftYonedaEquiv :
        (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
      { down := ((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X) } :
    obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
  (Iso.hom
      ((equivUliftYonedaIso (F ⋙ uliftFunctor.{v, w}) X :
          (a : (F ⋙ uliftFunctor.{v, w}).RepresentableBy X) → uliftYoneda.{w, v, u}.obj X ≅ F ⋙ uliftFunctor.{v, w})
        ((Equiv.symm representableByUliftFunctorEquiv :
            (a : F.RepresentableBy X) → (F ⋙ uliftFunctor.{v, w}).RepresentableBy X)
          R)) :
    obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
Tactic: convert!
    (RepresentableBy.equivUliftYonedaIso _ _ <|
        representableByUliftFunctorEquiv.{v}.symm R).isIso_hom
-- Lean 4 proof step from Mathlib.CategoryTheory.RepresentedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
R : F.RepresentableBy X
⊢ Eq (α := obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
    ((Equiv.symm uliftYonedaEquiv :
          (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
        { down := ((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X) } :
      obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
    (Iso.hom
        ((equivUliftYonedaIso (F ⋙ uliftFunctor.{v, w}) X :
            (a : (F ⋙ uliftFunctor.{v, w}).RepresentableBy X) → uliftYoneda.{w, v, u}.obj X ≅ F ⋙ uliftFunctor.{v, w})
          ((Equiv.symm representableByUliftFunctorEquiv :
              (a : F.RepresentableBy X) → (F ⋙ uliftFunctor.{v, w}).RepresentableBy X)
            R)) :
      obj uliftYoneda.{w, v, u} X ⟶ F ⋙ uliftFunctor.{v, w})
have h : ∀ (x : Cᵒᵖ) (x_1 : obj (obj uliftYoneda.{w, v, u} X) x),
  Eq (α := (F ⋙ uliftFunctor.{v, w}).obj x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((Equiv.symm uliftYonedaEquiv :
              (a : (F ⋙ uliftFunctor.{v, w}).obj (op X)) → uliftYoneda.{w, v, u}.obj X ⟶ F ⋙ uliftFunctor.{v, w})
            { down := ((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F.obj (op X))) : (a : X ⟶ X) → F.obj (op X)) (𝟙 X) :
              ULift.{v, w} (F.obj (op X)) })
          x))
      x_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
            ((equivUliftYonedaIso (F ⋙ uliftFunctor.{v, w}) X :
                (a : (F ⋙ uliftFunctor.{v, w}).RepresentableBy X) →
                  uliftYoneda.{w, v, u}.obj X ≅ F ⋙ uliftFunctor.{v, w})
              ((Equiv.symm representableByUliftFunctorEquiv :
                  (a : F.RepresentableBy X) → (F ⋙ uliftFunctor.{v, w}).RepresentableBy X)
                R)))
          x))
      x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.RepresentedBy (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 (op X)
h : F.IsRepresentedBy x
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
e : F ≅ F'
⊢ F'.IsRepresentedBy (X := X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (op X)) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F'.obj (op X)))
      x)
have rw : ∃ (R : F'.RepresentableBy X),
  Eq.{w + 1} (α := F'.obj (op X))
    (((R.homEquiv : Equiv.{v + 1, w + 1} (X ⟶ X) (F'.obj (op X))) : (a : X ⟶ X) → F'.obj (op X)) (𝟙 X) : F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (op X)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (F'.obj (op X)))
        x :
      (fun (X : Type w) ↦ X) (F'.obj (op X)))
Tactic: rw [iff_exists_representableBy]