-- Mathlib/CategoryTheory/Bicategory/Grothendieck.lean
@[ext (iff := false)]
lemma Hom.ext (f g : a ⟶ b) (hfg₁ : f.base = g.base)
    (hfg₂ : f.fiber = g.fiber ≫ eqToHom (hfg₁ ▸ rfl)) : f = g

Proof state:
case mk.mk.h.e_7
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat
a b : ∫ F
base✝¹ : a.base ⟶ b.base
fiber✝¹ : a.fiber ⟶ (F.map base✝¹.op.toLoc).obj b.fiber
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).obj b.fiber
hfg₁ : base✝¹ = base✝
hfg₂ : { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber ≫ eqToHom ⋯
⊢ HEq fiber✝¹ fiber✝

Tactic:
rw [← conj_eqToHom_iff_heq _ _ rfl (hfg₁ ▸ rfl)]

Result:
case mk.mk.h.e_7
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat
a b : ∫ F
base✝¹ : a.base ⟶ b.base
fiber✝¹ : a.fiber ⟶ (F.map base✝¹.op.toLoc).obj b.fiber
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).obj b.fiber
hfg₁ : base✝¹ = base✝
hfg₂ : { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber ≫ eqToHom ⋯
⊢ fiber✝¹ = eqToHom ⋯ ≫ fiber✝ ≫ eqToHom ⋯

Proof state:
case mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat
a b : ∫ F
g : a ⟶ b
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).obj b.fiber
hfg₁ : { base := base✝, fiber := fiber✝ }.base = g.base
hfg₂ : { base := base✝, fiber := fiber✝ }.fiber = g.fiber ≫ eqToHom ⋯
⊢ { base := base✝, fiber := fiber✝ } = g

Tactic:
cases g

Result:
case mk.mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat
a b : ∫ F
base✝¹ : a.base ⟶ b.base
fiber✝¹ : a.fiber ⟶ (F.map base✝¹.op.toLoc).obj b.fiber
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).obj b.fiber
hfg₁ : { base := base✝¹, fiber := fiber✝¹ }.base = { base := base✝, fiber := fiber✝ }.base
hfg₂ : { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber ≫ eqToHom ⋯
⊢ { base := base✝¹, fiber := fiber✝¹ } = { base := base✝, fiber := fiber✝ }

Proof state:
case mk.mk.h.e_7
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat
a b : ∫ F
base✝¹ : a.base ⟶ b.base
fiber✝¹ : a.fiber ⟶ (F.map base✝¹.op.toLoc).obj b.fiber
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).obj b.fiber
hfg₁ : base✝¹ = base✝
hfg₂ : { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber ≫ eqToHom ⋯
⊢ fiber✝¹ = eqToHom ⋯ ≫ fiber✝ ≫ eqToHom ⋯

Tactic:
simpa only [eqToHom_refl, id_comp] using hfg₂

Result:
no goals

Proof state:
case mk.mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat
a b : ∫ F
base✝¹ : a.base ⟶ b.base
fiber✝¹ : a.fiber ⟶ (F.map base✝¹.op.toLoc).obj b.fiber
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).obj b.fiber
hfg₁ : { base := base✝¹, fiber := fiber✝¹ }.base = { base := base✝, fiber := fiber✝ }.base
hfg₂ : { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber ≫ eqToHom ⋯
⊢ { base := base✝¹, fiber := fiber✝¹ } = { base := base✝, fiber := fiber✝ }

Tactic:
congr

Result:
case mk.mk.h.e_7
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat
a b : ∫ F
base✝¹ : a.base ⟶ b.base
fiber✝¹ : a.fiber ⟶ (F.map base✝¹.op.toLoc).obj b.fiber
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).obj b.fiber
hfg₁ : { base := base✝¹, fiber := fiber✝¹ }.base = { base := base✝, fiber := fiber✝ }.base
hfg₂ : { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber ≫ eqToHom ⋯
⊢ HEq fiber✝¹ fiber✝

Proof state:
case mk.mk.h.e_7
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat
a b : ∫ F
base✝¹ : a.base ⟶ b.base
fiber✝¹ : a.fiber ⟶ (F.map base✝¹.op.toLoc).obj b.fiber
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).obj b.fiber
hfg₁ : { base := base✝¹, fiber := fiber✝¹ }.base = { base := base✝, fiber := fiber✝ }.base
hfg₂ : { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber ≫ eqToHom ⋯
⊢ HEq fiber✝¹ fiber✝

Tactic:
dsimp at hfg₁

Result:
case mk.mk.h.e_7
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat
a b : ∫ F
base✝¹ : a.base ⟶ b.base
fiber✝¹ : a.fiber ⟶ (F.map base✝¹.op.toLoc).obj b.fiber
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).obj b.fiber
hfg₁ : base✝¹ = base✝
hfg₂ : { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber ≫ eqToHom ⋯
⊢ HEq fiber✝¹ fiber✝

Proof state:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat
a b : ∫ F
f g : a ⟶ b
hfg₁ : f.base = g.base
hfg₂ : f.fiber = g.fiber ≫ eqToHom ⋯
⊢ f = g

Tactic:
cases f

Result:
case mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat
a b : ∫ F
g : a ⟶ b
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).obj b.fiber
hfg₁ : { base := base✝, fiber := fiber✝ }.base = g.base
hfg₂ : { base := base✝, fiber := fiber✝ }.fiber = g.fiber ≫ eqToHom ⋯
⊢ { base := base✝, fiber := fiber✝ } = g