-- Mathlib/CategoryTheory/Iso.lean
theorem ext ⦃α β : X ≅ Y⦄ (w : α.hom = β.hom) : α = β :=
  suffices α.inv = β.inv by
    cases α
    cases β
    cases w
    cases this
    rfl
  calc
    α.inv = α.inv ≫ β.hom ≫ β.inv

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ (α.inv ≫ α.hom) ≫ β.inv = β.inv

Tactic:
rw [Iso.inv_hom_id, Category.id_comp]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ α.inv = α.inv ≫ β.hom ≫ β.inv

Tactic:
rw [Iso.hom_inv_id, Category.comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α β : X ≅ Y
w : α.hom = β.hom
this : α.inv = β.inv
⊢ α = β

Tactic:
cases α

Result:
case mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
β : X ≅ Y
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
w : { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }.hom = β.hom
this : { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }.inv = β.inv
⊢ { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ } = β

Proof state:
case mk.mk.refl.refl
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝¹ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝¹ : inv✝ ≫ hom✝ = 𝟙 Y
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
⊢ { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝¹, inv_hom_id := inv_hom_id✝¹ } =
    { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hom✝¹ : X ⟶ Y
inv✝¹ : Y ⟶ X
hom_inv_id✝¹ : hom✝¹ ≫ inv✝¹ = 𝟙 X
inv_hom_id✝¹ : inv✝¹ ≫ hom✝¹ = 𝟙 Y
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
w :
  { hom := hom✝¹, inv := inv✝¹, hom_inv_id := hom_inv_id✝¹, inv_hom_id := inv_hom_id✝¹ }.hom =
    { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }.hom
this :
  { hom := hom✝¹, inv := inv✝¹, hom_inv_id := hom_inv_id✝¹, inv_hom_id := inv_hom_id✝¹ }.inv =
    { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }.inv
⊢ { hom := hom✝¹, inv := inv✝¹, hom_inv_id := hom_inv_id✝¹, inv_hom_id := inv_hom_id✝¹ } =
    { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }

Tactic:
cases w

Result:
case mk.mk.refl
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hom✝ : X ⟶ Y
inv✝¹ : Y ⟶ X
hom_inv_id✝¹ : hom✝ ≫ inv✝¹ = 𝟙 X
inv_hom_id✝¹ : inv✝¹ ≫ hom✝ = 𝟙 Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
this :
  { hom := hom✝, inv := inv✝¹, hom_inv_id := hom_inv_id✝¹, inv_hom_id := inv_hom_id✝¹ }.inv =
    { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }.inv
⊢ { hom := hom✝, inv := inv✝¹, hom_inv_id := hom_inv_id✝¹, inv_hom_id := inv_hom_id✝¹ } =
    { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }

Proof state:
case mk.mk.refl
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hom✝ : X ⟶ Y
inv✝¹ : Y ⟶ X
hom_inv_id✝¹ : hom✝ ≫ inv✝¹ = 𝟙 X
inv_hom_id✝¹ : inv✝¹ ≫ hom✝ = 𝟙 Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
this :
  { hom := hom✝, inv := inv✝¹, hom_inv_id := hom_inv_id✝¹, inv_hom_id := inv_hom_id✝¹ }.inv =
    { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }.inv
⊢ { hom := hom✝, inv := inv✝¹, hom_inv_id := hom_inv_id✝¹, inv_hom_id := inv_hom_id✝¹ } =
    { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }

Tactic:
cases this

Result:
case mk.mk.refl.refl
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝¹ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝¹ : inv✝ ≫ hom✝ = 𝟙 Y
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
⊢ { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝¹, inv_hom_id := inv_hom_id✝¹ } =
    { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }

Proof state:
case mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
β : X ≅ Y
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
w : { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }.hom = β.hom
this : { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }.inv = β.inv
⊢ { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ } = β

Tactic:
cases β

Result:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hom✝¹ : X ⟶ Y
inv✝¹ : Y ⟶ X
hom_inv_id✝¹ : hom✝¹ ≫ inv✝¹ = 𝟙 X
inv_hom_id✝¹ : inv✝¹ ≫ hom✝¹ = 𝟙 Y
hom✝ : X ⟶ Y
inv✝ : Y ⟶ X
hom_inv_id✝ : hom✝ ≫ inv✝ = 𝟙 X
inv_hom_id✝ : inv✝ ≫ hom✝ = 𝟙 Y
w :
  { hom := hom✝¹, inv := inv✝¹, hom_inv_id := hom_inv_id✝¹, inv_hom_id := inv_hom_id✝¹ }.hom =
    { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }.hom
this :
  { hom := hom✝¹, inv := inv✝¹, hom_inv_id := hom_inv_id✝¹, inv_hom_id := inv_hom_id✝¹ }.inv =
    { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }.inv
⊢ { hom := hom✝¹, inv := inv✝¹, hom_inv_id := hom_inv_id✝¹, inv_hom_id := inv_hom_id✝¹ } =
    { hom := hom✝, inv := inv✝, hom_inv_id := hom_inv_id✝, inv_hom_id := inv_hom_id✝ }

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ α.inv ≫ β.hom ≫ β.inv = (α.inv ≫ α.hom) ≫ β.inv

Tactic:
rw [Category.assoc, ← w]

Result:
no goals