-- Mathlib/CategoryTheory/Yoneda.lean
@[ext]
lemma CorepresentableBy.ext {F : C ⥤ Type v} {X : C} {e e' : F.CorepresentableBy X}
    (h : e.homEquiv (𝟙 X) = e'.homEquiv (𝟙 X)) : e = e'

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = F.map g (e f)
e' : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he' : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e' (f ≫ g) = F.map g (e' f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
⊢ e = e'

Tactic:
ext

Result:
case h.H
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = F.map g (e f)
e' : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he' : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e' (f ≫ g) = F.map g (e' f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
x✝¹ : C
x✝ : X ⟶ x✝¹
⊢ e x✝ = e' x✝

Proof state:
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e' : F.CorepresentableBy X
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = F.map g (e f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = e'.homEquiv (𝟙 X)
this : ∀ {Y : C} (f : X ⟶ Y), { homEquiv := e, homEquiv_comp := he }.homEquiv f = e'.homEquiv f
⊢ { homEquiv := e, homEquiv_comp := he } = e'

Tactic:
obtain ⟨e', he'⟩ := e'

Result:
case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = F.map g (e f)
e' : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he' : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e' (f ≫ g) = F.map g (e' f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
⊢ { homEquiv := e, homEquiv_comp := he } = { homEquiv := e', homEquiv_comp := he' }

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X✝ : C
e e' : F.CorepresentableBy X✝
h : e.homEquiv (𝟙 X✝) = e'.homEquiv (𝟙 X✝)
X : C
f : X✝ ⟶ X
⊢ e.homEquiv f = e'.homEquiv f

Tactic:
rw [e.homEquiv_eq, e'.homEquiv_eq, h]

Result:
no goals

Proof state:
case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he he' : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = F.map g (e f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = { homEquiv := e, homEquiv_comp := he' }.homEquiv (𝟙 X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e, homEquiv_comp := he' }.homEquiv f
⊢ { homEquiv := e, homEquiv_comp := he } = { homEquiv := e, homEquiv_comp := he' }

Tactic:
rfl

Result:
no goals

Proof state:
case h.H
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = F.map g (e f)
e' : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he' : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e' (f ≫ g) = F.map g (e' f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
x✝¹ : C
x✝ : X ⟶ x✝¹
⊢ e x✝ = e' x✝

Tactic:
apply this

Result:
no goals

Proof state:
case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = F.map g (e f)
e' : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he' : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e' (f ≫ g) = F.map g (e' f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
⊢ { homEquiv := e, homEquiv_comp := he } = { homEquiv := e', homEquiv_comp := he' }

Tactic:
obtain rfl : @e = @e' := by ext; apply this

Result:
case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he he' : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = F.map g (e f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = { homEquiv := e, homEquiv_comp := he' }.homEquiv (𝟙 X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e, homEquiv_comp := he' }.homEquiv f
⊢ { homEquiv := e, homEquiv_comp := he } = { homEquiv := e, homEquiv_comp := he' }

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e e' : F.CorepresentableBy X
h : e.homEquiv (𝟙 X) = e'.homEquiv (𝟙 X)
this : ∀ {Y : C} (f : X ⟶ Y), e.homEquiv f = e'.homEquiv f
⊢ e = e'

Tactic:
obtain ⟨e, he⟩ := e

Result:
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e' : F.CorepresentableBy X
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = F.map g (e f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = e'.homEquiv (𝟙 X)
this : ∀ {Y : C} (f : X ⟶ Y), { homEquiv := e, homEquiv_comp := he }.homEquiv f = e'.homEquiv f
⊢ { homEquiv := e, homEquiv_comp := he } = e'

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e e' : F.CorepresentableBy X
h : e.homEquiv (𝟙 X) = e'.homEquiv (𝟙 X)
⊢ e = e'

Tactic:
have : ∀ {Y : C} (f : X ⟶ Y), e.homEquiv f = e'.homEquiv f := fun {X} f ↦ by
  rw [e.homEquiv_eq, e'.homEquiv_eq, h]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e e' : F.CorepresentableBy X
h : e.homEquiv (𝟙 X) = e'.homEquiv (𝟙 X)
this : ∀ {Y : C} (f : X ⟶ Y), e.homEquiv f = e'.homEquiv f
⊢ e = e'