-- Mathlib/CategoryTheory/Grothendieck.lean
theorem ext {X Y : Grothendieck F} (f g : Hom X Y) (w_base : f.base = g.base)
    (w_fiber : eqToHom (by rw [w_base]) ≫ f.fiber = g.fiber) : f = g

Proof state:
case mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
g : X.Hom Y
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).obj X.fiber ⟶ Y.fiber
w_base : { base := base✝, fiber := fiber✝ }.base = g.base
w_fiber : eqToHom ⋯ ≫ { base := base✝, fiber := fiber✝ }.fiber = g.fiber
⊢ { base := base✝, fiber := fiber✝ } = g

Tactic:
cases g

Result:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
base✝¹ : X.base ⟶ Y.base
fiber✝¹ : (F.map base✝¹).obj X.fiber ⟶ Y.fiber
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).obj X.fiber ⟶ Y.fiber
w_base : { base := base✝¹, fiber := fiber✝¹ }.base = { base := base✝, fiber := fiber✝ }.base
w_fiber : eqToHom ⋯ ≫ { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber
⊢ { base := base✝¹, fiber := fiber✝¹ } = { base := base✝, fiber := fiber✝ }

Proof state:
case mk.mk.h.e_7
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
base✝¹ : X.base ⟶ Y.base
fiber✝¹ : (F.map base✝¹).obj X.fiber ⟶ Y.fiber
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).obj X.fiber ⟶ Y.fiber
w_base : base✝¹ = base✝
w_fiber : eqToHom ⋯ ≫ { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber
⊢ HEq fiber✝¹ fiber✝

Tactic:
aesop_cat

Result:
no goals

Proof state:
case mk.mk.h.e_7
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
base✝¹ : X.base ⟶ Y.base
fiber✝¹ : (F.map base✝¹).obj X.fiber ⟶ Y.fiber
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).obj X.fiber ⟶ Y.fiber
w_base : { base := base✝¹, fiber := fiber✝¹ }.base = { base := base✝, fiber := fiber✝ }.base
w_fiber : eqToHom ⋯ ≫ { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber
⊢ HEq fiber✝¹ fiber✝

Tactic:
dsimp at w_base

Result:
case mk.mk.h.e_7
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
base✝¹ : X.base ⟶ Y.base
fiber✝¹ : (F.map base✝¹).obj X.fiber ⟶ Y.fiber
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).obj X.fiber ⟶ Y.fiber
w_base : base✝¹ = base✝
w_fiber : eqToHom ⋯ ≫ { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber
⊢ HEq fiber✝¹ fiber✝

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f g : X.Hom Y
w_base : f.base = g.base
w_fiber : eqToHom ⋯ ≫ f.fiber = g.fiber
⊢ f = g

Tactic:
cases f

Result:
case mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
g : X.Hom Y
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).obj X.fiber ⟶ Y.fiber
w_base : { base := base✝, fiber := fiber✝ }.base = g.base
w_fiber : eqToHom ⋯ ≫ { base := base✝, fiber := fiber✝ }.fiber = g.fiber
⊢ { base := base✝, fiber := fiber✝ } = g

Proof state:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
base✝¹ : X.base ⟶ Y.base
fiber✝¹ : (F.map base✝¹).obj X.fiber ⟶ Y.fiber
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).obj X.fiber ⟶ Y.fiber
w_base : { base := base✝¹, fiber := fiber✝¹ }.base = { base := base✝, fiber := fiber✝ }.base
w_fiber : eqToHom ⋯ ≫ { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber
⊢ { base := base✝¹, fiber := fiber✝¹ } = { base := base✝, fiber := fiber✝ }

Tactic:
congr

Result:
case mk.mk.h.e_7
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
base✝¹ : X.base ⟶ Y.base
fiber✝¹ : (F.map base✝¹).obj X.fiber ⟶ Y.fiber
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).obj X.fiber ⟶ Y.fiber
w_base : { base := base✝¹, fiber := fiber✝¹ }.base = { base := base✝, fiber := fiber✝ }.base
w_fiber : eqToHom ⋯ ≫ { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber
⊢ HEq fiber✝¹ fiber✝

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f g : X.Hom Y
w_base : f.base = g.base
⊢ (F.map g.base).obj X.fiber = (F.map f.base).obj X.fiber

Tactic:
rw [w_base]

Result:
no goals