-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
lemma biprod_ext {X₁ X₂ : C} {α β : Ext (X₁ ⊞ X₂) Y n}
    (h₁ : (mk₀ biprod.inl).comp α (zero_add n) = (mk₀ biprod.inl).comp β (zero_add n))
    (h₂ : (mk₀ biprod.inr).comp α (zero_add n) = (mk₀ biprod.inr).comp β (zero_add n)) :
    α = β

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ : (singleFunctor C 0).map biprod.inl ≫ α.hom = (singleFunctor C 0).map biprod.inl ≫ β.hom
h₂ : (singleFunctor C 0).map biprod.inr ≫ α.hom = (singleFunctor C 0).map biprod.inr ≫ β.hom
⊢ α.hom = β.hom

Tactic:
apply BinaryCofan.IsColimit.hom_ext
  (isBinaryBilimitOfPreserves (singleFunctor C 0)
    (BinaryBiproduct.isBilimit X₁ X₂)).isColimit

Result:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ : (singleFunctor C 0).map biprod.inl ≫ α.hom = (singleFunctor C 0).map biprod.inl ≫ β.hom
h₂ : (singleFunctor C 0).map biprod.inr ≫ α.hom = (singleFunctor C 0).map biprod.inr ≫ β.hom
⊢ BinaryCofan.inl ((singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ α.hom =
    BinaryCofan.inl ((singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ β.hom

case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ : (singleFunctor C 0).map biprod.inl ≫ α.hom = (singleFunctor C 0).map biprod.inl ≫ β.hom
h₂ : (singleFunctor C 0).map biprod.inr ≫ α.hom = (singleFunctor C 0).map biprod.inr ≫ β.hom
⊢ BinaryCofan.inr ((singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ α.hom =
    BinaryCofan.inr ((singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ β.hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
h₁ : (mk₀ biprod.inl).comp α ⋯ = (mk₀ biprod.inl).comp β ⋯
h₂ : (mk₀ biprod.inr).comp α ⋯ = (mk₀ biprod.inr).comp β ⋯
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α = β

Tactic:
rw [Ext.ext_iff] at h₁ h₂ ⊢

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₂ : ((mk₀ biprod.inr).comp α ⋯).hom = ((mk₀ biprod.inr).comp β ⋯).hom
h₁ : ((mk₀ biprod.inl).comp α ⋯).hom = ((mk₀ biprod.inl).comp β ⋯).hom
⊢ α.hom = β.hom

Proof state:
case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ : (singleFunctor C 0).map biprod.inl ≫ α.hom = (singleFunctor C 0).map biprod.inl ≫ β.hom
h₂ : (singleFunctor C 0).map biprod.inr ≫ α.hom = (singleFunctor C 0).map biprod.inr ≫ β.hom
⊢ BinaryCofan.inr ((singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ α.hom =
    BinaryCofan.inr ((singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ β.hom

Tactic:
assumption

Result:
no goals

Proof state:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ : (singleFunctor C 0).map biprod.inl ≫ α.hom = (singleFunctor C 0).map biprod.inl ≫ β.hom
h₂ : (singleFunctor C 0).map biprod.inr ≫ α.hom = (singleFunctor C 0).map biprod.inr ≫ β.hom
⊢ BinaryCofan.inl ((singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ α.hom =
    BinaryCofan.inl ((singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ β.hom

case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ : (singleFunctor C 0).map biprod.inl ≫ α.hom = (singleFunctor C 0).map biprod.inl ≫ β.hom
h₂ : (singleFunctor C 0).map biprod.inr ≫ α.hom = (singleFunctor C 0).map biprod.inr ≫ β.hom
⊢ BinaryCofan.inr ((singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ α.hom =
    BinaryCofan.inr ((singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ β.hom

Tactic:
all_goals assumption

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₂ : ((mk₀ biprod.inr).comp α ⋯).hom = ((mk₀ biprod.inr).comp β ⋯).hom
h₁ : ((mk₀ biprod.inl).comp α ⋯).hom = ((mk₀ biprod.inl).comp β ⋯).hom
⊢ α.hom = β.hom

Tactic:
simp only [comp_hom, mk₀_hom, ShiftedHom.mk₀_comp] at h₁ h₂

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ : (singleFunctor C 0).map biprod.inl ≫ α.hom = (singleFunctor C 0).map biprod.inl ≫ β.hom
h₂ : (singleFunctor C 0).map biprod.inr ≫ α.hom = (singleFunctor C 0).map biprod.inr ≫ β.hom
⊢ α.hom = β.hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
h₁ : (mk₀ biprod.inl).comp α ⋯ = (mk₀ biprod.inl).comp β ⋯
h₂ : (mk₀ biprod.inr).comp α ⋯ = (mk₀ biprod.inr).comp β ⋯
⊢ α = β

Tactic:
letI := HasDerivedCategory.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
h₁ : (mk₀ biprod.inl).comp α ⋯ = (mk₀ biprod.inl).comp β ⋯
h₂ : (mk₀ biprod.inr).comp α ⋯ = (mk₀ biprod.inr).comp β ⋯
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α = β