-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem ext_aux (I J : HasZeroMorphisms C)
    (w : ∀ X Y : C, (I.zero X Y).zero = (J.zero X Y).zero) : I = J

Proof state:
case mk
C : Type u
inst✝ : Category.{v, u} C
J : HasZeroMorphisms C
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ mk comp_zero✝ zero_comp✝ = J

Tactic:
cases J

Result:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
zero✝¹ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ mk comp_zero✝¹ zero_comp✝¹ = mk comp_zero✝ zero_comp✝

Proof state:
case mk.mk.h.e_4
C : Type u
inst✝ : Category.{v, u} C
zero✝¹ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ HEq comp_zero✝¹ comp_zero✝

Tactic:
apply proof_irrel_heq

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
⊢ zero = zero

Tactic:
funext X Y

Result:
case h.h
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
X Y : C
⊢ zero X Y = zero X Y

Proof state:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
zero✝¹ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ mk comp_zero✝¹ zero_comp✝¹ = mk comp_zero✝ zero_comp✝

Tactic:
congr

Result:
case mk.mk.h.e_4
C : Type u
inst✝ : Category.{v, u} C
zero✝¹ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ HEq comp_zero✝¹ comp_zero✝

case mk.mk.h.e_5
C : Type u
inst✝ : Category.{v, u} C
zero✝¹ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ HEq zero_comp✝¹ zero_comp✝

Proof state:
case h.h
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
w : Zero.zero = Zero.zero
⊢ zero X Y = zero X Y

Tactic:
apply congrArg Zero.mk w

Result:
no goals

Proof state:
case h.h
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
X Y : C
⊢ zero X Y = zero X Y

Tactic:
specialize w X Y

Result:
case h.h
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
w : Zero.zero = Zero.zero
⊢ zero X Y = zero X Y

Proof state:
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
⊢ I = J

Tactic:
have : I.zero = J.zero := by
  funext X Y
  specialize w X Y
  apply congrArg Zero.mk w

Result:
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ I = J

Proof state:
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ I = J

Tactic:
cases I

Result:
case mk
C : Type u
inst✝ : Category.{v, u} C
J : HasZeroMorphisms C
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ mk comp_zero✝ zero_comp✝ = J

Proof state:
case mk.mk.h.e_5
C : Type u
inst✝ : Category.{v, u} C
zero✝¹ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ HEq zero_comp✝¹ zero_comp✝

Tactic:
apply proof_irrel_heq

Result:
no goals