-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
lemma descSigma_ext_iff {φ : F ⟶ G} {K : HomologicalComplex C c}
    (x y : Σ (α : G ⟶ K), Homotopy (φ ≫ α) 0) :
    x = y ↔ x.1 = y.1 ∧ (∀ (i j : ι) (_ : c.Rel j i), x.2.hom i j = y.2.hom i j)

Proof state:
case mpr.mk.mk.intro.hom.h.h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
i j : ι
⊢ x₂.hom i j = y₂.hom i j

Tactic:
by_cases hij : c.Rel j i

Result:
case pos
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
i j : ι
hij : c.Rel j i
⊢ x₂.hom i j = y₂.hom i j

case neg
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
i j : ι
hij : ¬c.Rel j i
⊢ x₂.hom i j = y₂.hom i j

Proof state:
case mpr.mk.mk
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₁ : G ⟶ K
y₂ : Homotopy (φ ≫ y₁) 0
⊢ (⟨x₁, x₂⟩.fst = ⟨y₁, y₂⟩.fst ∧ ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨y₁, y₂⟩.snd.hom i j) →
    ⟨x₁, x₂⟩ = ⟨y₁, y₂⟩

Tactic:
rintro ⟨rfl, h⟩

Result:
case mpr.mk.mk.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
⊢ ⟨x₁, x₂⟩ = ⟨⟨x₁, x₂⟩.fst, y₂⟩

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
⊢ x.fst = x.fst ∧ ∀ (i j : ι), c.Rel j i → x.snd.hom i j = x.snd.hom i j

Tactic:
tauto

Result:
no goals

Proof state:
case mpr.mk.mk.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
⊢ ⟨x₁, x₂⟩ = ⟨⟨x₁, x₂⟩.fst, y₂⟩

Tactic:
simp only [Sigma.mk.inj_iff, heq_eq_eq, true_and]

Result:
case mpr.mk.mk.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
⊢ x₂ = y₂

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
⊢ x = y → x.fst = y.fst ∧ ∀ (i j : ι), c.Rel j i → x.snd.hom i j = y.snd.hom i j

Tactic:
rintro rfl

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
⊢ x.fst = x.fst ∧ ∀ (i j : ι), c.Rel j i → x.snd.hom i j = x.snd.hom i j

Proof state:
case pos
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
i j : ι
hij : c.Rel j i
⊢ x₂.hom i j = y₂.hom i j

Tactic:
exact h _ _ hij

Result:
no goals

Proof state:
case neg
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
i j : ι
hij : ¬c.Rel j i
⊢ x₂.hom i j = y₂.hom i j

Tactic:
simp only [Homotopy.zero _ _ _ hij]

Result:
no goals

Proof state:
case mpr.mk.mk.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
⊢ x₂ = y₂

Tactic:
ext i j

Result:
case mpr.mk.mk.intro.hom.h.h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
i j : ι
⊢ x₂.hom i j = y₂.hom i j

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
⊢ x = y ↔ x.fst = y.fst ∧ ∀ (i j : ι), c.Rel j i → x.snd.hom i j = y.snd.hom i j

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
⊢ x = y → x.fst = y.fst ∧ ∀ (i j : ι), c.Rel j i → x.snd.hom i j = y.snd.hom i j

case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
⊢ (x.fst = y.fst ∧ ∀ (i j : ι), c.Rel j i → x.snd.hom i j = y.snd.hom i j) → x = y

Proof state:
case mpr.mk
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
⊢ (⟨x₁, x₂⟩.fst = y.fst ∧ ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = y.snd.hom i j) → ⟨x₁, x₂⟩ = y

Tactic:
obtain ⟨y₁, y₂⟩ := y

Result:
case mpr.mk.mk
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₁ : G ⟶ K
y₂ : Homotopy (φ ≫ y₁) 0
⊢ (⟨x₁, x₂⟩.fst = ⟨y₁, y₂⟩.fst ∧ ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨y₁, y₂⟩.snd.hom i j) →
    ⟨x₁, x₂⟩ = ⟨y₁, y₂⟩