-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[ext (iff := false)]
lemma ext {p q : YonedaCollection F X} (h : p.fst = q.fst)
    (h' : F.map (eqToHom <| by rw [h]) q.snd = p.snd) : p = q

Proof state:
case mk
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
q : YonedaCollection F X
p : A.obj (op X)
p' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))
h : fst ⟨p, p'⟩ = q.fst
h' : F.map (eqToHom ⋯) q.snd = snd ⟨p, p'⟩
⊢ ⟨p, p'⟩ = q

Tactic:
rcases q with ⟨q, q'⟩

Result:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p : A.obj (op X)
p' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))
q : A.obj (op X)
q' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm q)))
h : fst ⟨p, p'⟩ = fst ⟨q, q'⟩
h' : F.map (eqToHom ⋯) (snd ⟨q, q'⟩) = snd ⟨p, p'⟩
⊢ ⟨p, p'⟩ = ⟨q, q'⟩

Proof state:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p : A.obj (op X)
p' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))
q : A.obj (op X)
q' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm q)))
h : fst ⟨p, p'⟩ = fst ⟨q, q'⟩
h' : F.map (eqToHom ⋯) (snd ⟨q, q'⟩) = snd ⟨p, p'⟩
⊢ ⟨p, p'⟩ = ⟨q, q'⟩

Tactic:
obtain rfl : p = q := yonedaEquiv.symm.injective h

Result:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p : A.obj (op X)
p' q' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))
h : fst ⟨p, p'⟩ = fst ⟨p, q'⟩
h' : F.map (eqToHom ⋯) (snd ⟨p, q'⟩) = snd ⟨p, p'⟩
⊢ ⟨p, p'⟩ = ⟨p, q'⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p q : YonedaCollection F X
h : p.fst = q.fst
h' : F.map (eqToHom ⋯) q.snd = p.snd
⊢ p = q

Tactic:
rcases p with ⟨p, p'⟩

Result:
case mk
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
q : YonedaCollection F X
p : A.obj (op X)
p' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))
h : fst ⟨p, p'⟩ = q.fst
h' : F.map (eqToHom ⋯) q.snd = snd ⟨p, p'⟩
⊢ ⟨p, p'⟩ = q

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p q : YonedaCollection F X
h : p.fst = q.fst
⊢ op (CostructuredArrow.mk q.fst) = op (CostructuredArrow.mk p.fst)

Tactic:
rw [h]

Result:
no goals

Proof state:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p : A.obj (op X)
p' q' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))
h : fst ⟨p, p'⟩ = fst ⟨p, q'⟩
h' : F.map (eqToHom ⋯) (snd ⟨p, q'⟩) = snd ⟨p, p'⟩
⊢ ⟨p, p'⟩ = ⟨p, q'⟩

Tactic:
exact Sigma.ext rfl (by simpa [snd] using h'.symm)

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p : A.obj (op X)
p' q' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))
h : fst ⟨p, p'⟩ = fst ⟨p, q'⟩
h' : F.map (eqToHom ⋯) (snd ⟨p, q'⟩) = snd ⟨p, p'⟩
⊢ HEq ⟨p, p'⟩.snd ⟨p, q'⟩.snd

Tactic:
simpa [snd] using h'.symm

Result:
no goals