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

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

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

Result:
no goals

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

Tactic:
have : ∀ {X : 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
Y : C
e e' : F.RepresentableBy Y
h : e.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)
this : ∀ {X : C} (f : X ⟶ Y), e.homEquiv f = e'.homEquiv f
⊢ e = e'

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e e' : F.RepresentableBy Y
h : e.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)
this : ∀ {X : 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
Y : C
e' : F.RepresentableBy Y
e : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e (f ≫ g) = F.map f.op (e g)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)
this : ∀ {X : C} (f : X ⟶ Y), { homEquiv := e, homEquiv_comp := he }.homEquiv f = e'.homEquiv f
⊢ { homEquiv := e, homEquiv_comp := he } = e'

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

Proof state:
case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he he' : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e (f ≫ g) = F.map f.op (e g)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 Y) = { homEquiv := e, homEquiv_comp := he' }.homEquiv (𝟙 Y)
this :
  ∀ {X : 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 mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e' : F.RepresentableBy Y
e : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e (f ≫ g) = F.map f.op (e g)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)
this : ∀ {X : 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
Y : C
e : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e (f ≫ g) = F.map f.op (e g)
e' : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he' : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e' (f ≫ g) = F.map f.op (e' g)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 Y) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 Y)
this :
  ∀ {X : 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' }