awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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 (X := pullback k₂ e) (pullback.fst k₂ e)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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₁

Tactic:
have : IsRegularEpi g₁ := by
    apply Regular.regularEpiIsStableUnderBaseChange.of_isPullback h.flip
    dsimp [MorphismProperty.regularEpi]
    infer_instance
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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₁
rw :
  (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 ⋯)
⊢ 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 ⋯))

Tactic:
rw [← cancel_epi (g₁ ≫ pullback.snd e k₁)]

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.CategoryStruct.comp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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 f f ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f))
    (pullback.fst f f ≫ coequalizer.π (pullback.fst f f) (pullback.snd f f))
    (pullback.snd f f ≫ coequalizer.π (pullback.fst f f) (pullback.snd f f))

Tactic:
coequalizer.condition (pullback.fst f f) (pullback.snd f f)

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.coequalizer.condition, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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)
h₂ :
  (g₁ ≫ pullback.snd e k₁) ≫ pullback.snd (coequalizer.desc f ⋯) (coequalizer.desc f ⋯) =
    pullback.snd 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 ⋯)

Tactic:
convert! coequalizer.condition (pullback.fst f f) (pullback.snd f f) using 1

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.coequalizer.condition, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
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))
⊢ IsRegularEpi (strongEpiMonoFactorisation f).e

Tactic:
dsimp [strongEpiMonoFactorisation]

Premises used: CategoryTheory.Regular.strongEpiMonoFactorisation
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
⊢ 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:
infer_instance
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
h : ExtremalEpi f
⊢ (strongEpiMonoFactorisation f).e ≫ (strongEpiMonoFactorisation f).m = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f_1 f : X ⟶ Y
inst_2 : ExtremalEpi f
⊢ IsRegularEpi f

Tactic:
⟨⟨regularEpiOfExtremalEpi f⟩⟩

Premises used: CategoryTheory.Regular.regularEpiOfExtremalEpi, Nonempty.intro, CategoryTheory.IsRegularEpi.mk
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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
⊢ ((A' ⊓ (Subobject.pullback f).obj B').ofLE ((Subobject.pullback f).obj B') ⋯ ≫ pullbackπ f B') ≫ B'.arrow =
    ((A' ⊓ (Subobject.pullback f).obj B').ofLE A' ⋯ ≫ (imageFactorisation f A').F.e) ≫ ((«exists» f).obj A').arrow

Tactic:
simp [← imageFactorisation_F_m, (isPullback _ _).w]

Premises used: CategoryTheory.Subobject.imageFactorisation_F_m, CategoryTheory.Subobject.isPullback, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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
s :
  IsPullback (frobeniusMorphism f A' B' ≫ ((«exists» f).obj A' ⊓ B').ofLE B' ⋯)
    ((A' ⊓ (Subobject.pullback f).obj B').ofLE A' ⋯) B'.arrow
    ((imageFactorisation f A').F.e ≫ ((«exists» f).obj A').arrow)
⊢ frobeniusMorphism f A' B' ≫ ((«exists» f).obj A' ⊓ B').ofLE ((«exists» f).obj A') ⋯ =
    (A' ⊓ (Subobject.pullback f).obj B').ofLE A' ⋯ ≫ (imageFactorisation f A').F.e

Tactic:
simp [frobeniusMorphism]

Premises used: CategoryTheory.Regular.frobeniusMorphism
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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
apply :
  IsPullback (frobeniusMorphism f A' B' ≫ ((«exists» f).obj A' ⊓ B').ofLE B' ⋯)
    ((A' ⊓ (Subobject.pullback f).obj B').ofLE A' ⋯) B'.arrow
    ((imageFactorisation f A').F.e ≫ ((«exists» f).obj A').arrow)
⊢ 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

Tactic:
apply IsPullback.of_right (t := (inf_isPullback ((«exists» f).obj A') B').flip)
    (p := by simp [frobeniusMorphism])

Premises used: CategoryTheory.Subobject.exists, CategoryTheory.Subobject.inf_isPullback, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_right, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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' ≫ ((«exists» f).obj A' ⊓ B').ofLE B' ⋯)
    ((A' ⊓ (Subobject.pullback f).obj B').ofLE A' ⋯) B'.arrow
    ((imageFactorisation f A').F.e ≫ ((«exists» f).obj A').arrow)

Tactic:
simpa [frobeniusMorphism, IsPullback.lift_fst, ← imageFactorisation_F_m,
    (isPullback f B').paste_horiz_iff] using
    (inf_isPullback A' ((Subobject.pullback f).obj B')).flip

Premises used: CategoryTheory.IsPullback.paste_horiz_iff, CategoryTheory.Subobject.imageFactorisation_F_m, CategoryTheory.Subobject.inf_isPullback, CategoryTheory.Subobject.pullback, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.lift_fst, CategoryTheory.Subobject.isPullback, CategoryTheory.Regular.frobeniusMorphism, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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
apply : MorphismProperty.regularEpi C (imageFactorisation f A').F.e
⊢ 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'))

Tactic:
apply regularEpiIsStableUnderBaseChange.of_isPullback (frobeniusMorphism_isPullback f A' B').flip

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.Regular.frobeniusMorphism_isPullback, CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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
⊢ StrongEpi (imageFactorisation f A').F.e

Tactic:
have := strongEpi_of_strongEpiMonoFactorisation (strongEpiMonoFactorisation (A'.arrow ≫ f))
    (imageFactorisation f A').isImage
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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
this : StrongEpi (imageFactorisation f A').F.e
⊢ IsRegularEpi (imageFactorisation f A').F.e

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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
rw :
  ((A' ⊓ (Subobject.pullback f).obj B').ofLE A' ⋯ ≫ (imageFactorisation f A').F.e) ≫ ((«exists» f).obj A').arrow =
    (A' ⊓ (Subobject.pullback f).obj B').arrow ≫ f
⊢ frobeniusMorphism f A' B' ≫ ((«exists» f).obj A' ⊓ B').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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Subobject.inf_comp_left, CategoryTheory.Subobject.exists, CategoryTheory.IsPullback.lift_snd, CategoryTheory.Subobject.inf_isPullback, CategoryTheory.IsPullback.flip, CategoryTheory.Regular.frobeniusMorphism, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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
⊢ ((A' ⊓ (Subobject.pullback f).obj B').ofLE A' ⋯ ≫ (imageFactorisation f A').F.e) ≫ ((«exists» f).obj A').arrow =
    (A' ⊓ (Subobject.pullback f).obj B').arrow ≫ f

Tactic:
simp [← imageFactorisation_F_m]

Premises used: CategoryTheory.Subobject.imageFactorisation_F_m
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
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
⊢ («exists» f).obj (A' ⊓ (Subobject.pullback f).obj B') = («exists» f).obj A' ⊓ B'

Tactic:
eq_of_comm
    (IsImage.isoExt (imageFactorisation _ _).isImage
      (frobeniusStrongEpiMonoFactorisation f A' B').toMonoIsImage)
    (IsImage.isoExt_hom_m (imageFactorisation _ _).isImage
      (frobeniusStrongEpiMonoFactorisation f A' B').toMonoIsImage)

Premises used: CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation, CategoryTheory.Limits.IsImage.isoExt_hom_m, CategoryTheory.Limits.IsImage.isoExt, CategoryTheory.Subobject.eq_of_comm, CategoryTheory.Subobject.imageFactorisation, CategoryTheory.Limits.ImageFactorisation.isImage, CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoIsImage
-- Module: Mathlib.CategoryTheory.RepresentedBy
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)
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))
⊢ 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})

Tactic:
rw [isRepresentedBy_iff, NatTrans.isIso_iff_isIso_app, Opposite.op_surjective.forall]

Premises used: Function.Surjective.forall, CategoryTheory.Functor.isRepresentedBy_iff, CategoryTheory.NatTrans.isIso_iff_isIso_app, Opposite.op_surjective
-- Module: Mathlib.CategoryTheory.RepresentedBy
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))

Tactic:
forall_congr' fun Y ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.CategoryTheory.RepresentedBy
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)
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))
⊢ (∀ {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:
refine forall_congr' fun Y ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.CategoryTheory.RepresentedBy
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
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)))))
⊢ (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:
rw [isIso_iff_bijective, ← Function.Bijective.of_comp_iff _ Equiv.ulift.{w}.symm.bijective,
    ← Function.Bijective.of_comp_iff' Equiv.ulift.{v}.bijective]

Premises used: CategoryTheory.isIso_iff_bijective
-- Module: Mathlib.CategoryTheory.RepresentedBy
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) ↔
    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:
rfl
-- Module: Mathlib.CategoryTheory.RepresentedBy
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
rwa rwa₁ rwa₂ 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})
⊢ 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

Premises used: CategoryTheory.Functor.IsRepresentedBy.iff_isIso_uliftYonedaEquiv