Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂✝ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
h₁ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
⊢ ∀ (a : Fin (n + 2 + 1)) (b : Fin (n + 1 + 1)),
    ((∃ a_1, ∃ b_1 ≤ a_1.castSucc, b_1.castSucc = a ∧ a_1.succ = b) ∨
        ∃ a_1 b_1, a_1.castSucc < b_1 ∧ b_1.succ = a ∧ a_1.castSucc = b) →
      ∀ (a_2 : Fin (n + 2 + 1)) (b_1 : Fin (n + 1 + 1)),
        ((∃ a, a.castSucc.succ = a_2 ∧ a.succ = b_1) ∨ ∃ a, a.castSucc.succ = a_2 ∧ a.castSucc = b_1) ∨
            a_2 = 0 ∧ b_1 = 0 ∨ a_2 = Fin.last (n + 2) ∧ b_1 = Fin.last (n + 1) →
          a = a_2 → ¬b = b_1

Tactic:
rintro ⟨a, _⟩ ⟨b, _⟩ (⟨⟨j, _⟩, ⟨k, _⟩, h₁, h₂, h₃⟩ | ⟨⟨j, _⟩, ⟨k, _⟩, h₁, h₂, h₃⟩) _ _
      ((⟨⟨i, _⟩, h₄, h₅⟩ | ⟨⟨i, _⟩, h₄, h₅⟩) | (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩))

Goal state after:
case inl.inl.inl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂✝¹ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
h₁✝ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂✝ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃✝ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂✝)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt✝⁴ : a < n + 2 + 1
b : ℕ
isLt✝³ : b < n + 1 + 1
j : ℕ
isLt✝² : j < n + 1
k : ℕ
isLt✝¹ : k < n + 2
h₁ : ⟨k, isLt✝¹⟩ ≤ ⟨j, isLt✝²⟩.castSucc
h₂ : ⟨k, isLt✝¹⟩.castSucc = ⟨a, isLt✝⁴⟩
h₃ : ⟨j, isLt✝²⟩.succ = ⟨b, isLt✝³⟩
a✝ : Fin (n + 2 + 1)
b✝ : Fin (n + 1 + 1)
i : ℕ
isLt✝ : i < n + 1
h₄ : ⟨i, isLt✝⟩.castSucc.succ = a✝
h₅ : ⟨i, isLt✝⟩.succ = b✝
⊢ ⟨a, isLt✝⁴⟩ = a✝ → ¬⟨b, isLt✝³⟩ = b✝

case inl.inl.inr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂✝¹ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
h₁✝ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂✝ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃✝ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂✝)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt✝⁴ : a < n + 2 + 1
b : ℕ
isLt✝³ : b < n + 1 + 1
j : ℕ
isLt✝² : j < n + 1
k : ℕ
isLt✝¹ : k < n + 2
h₁ : ⟨k, isLt✝¹⟩ ≤ ⟨j, isLt✝²⟩.castSucc
h₂ : ⟨k, isLt✝¹⟩.castSucc = ⟨a, isLt✝⁴⟩
h₃ : ⟨j, isLt✝²⟩.succ = ⟨b, isLt✝³⟩
a✝ : Fin (n + 2 + 1)
b✝ : Fin (n + 1 + 1)
i : ℕ
isLt✝ : i < n + 1
h₄ : ⟨i, isLt✝⟩.castSucc.succ = a✝
h₅ : ⟨i, isLt✝⟩.castSucc = b✝
⊢ ⟨a, isLt✝⁴⟩ = a✝ → ¬⟨b, isLt✝³⟩ = b✝

case inl.inr.inl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂✝¹ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
h₁✝ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂✝ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃✝ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂✝)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt✝³ : a < n + 2 + 1
b : ℕ
isLt✝² : b < n + 1 + 1
j : ℕ
isLt✝¹ : j < n + 1
k : ℕ
isLt✝ : k < n + 2
h₁ : ⟨k, isLt✝⟩ ≤ ⟨j, isLt✝¹⟩.castSucc
h₂ : ⟨k, isLt✝⟩.castSucc = ⟨a, isLt✝³⟩
h₃ : ⟨j, isLt✝¹⟩.succ = ⟨b, isLt✝²⟩
⊢ ⟨a, isLt✝³⟩ = 0 → ¬⟨b, isLt✝²⟩ = 0

case inl.inr.inr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂✝¹ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
h₁✝ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂✝ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃✝ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂✝)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt✝³ : a < n + 2 + 1
b : ℕ
isLt✝² : b < n + 1 + 1
j : ℕ
isLt✝¹ : j < n + 1
k : ℕ
isLt✝ : k < n + 2
h₁ : ⟨k, isLt✝⟩ ≤ ⟨j, isLt✝¹⟩.castSucc
h₂ : ⟨k, isLt✝⟩.castSucc = ⟨a, isLt✝³⟩
h₃ : ⟨j, isLt✝¹⟩.succ = ⟨b, isLt✝²⟩
⊢ ⟨a, isLt✝³⟩ = Fin.last (n + 2) → ¬⟨b, isLt✝²⟩ = Fin.last (n + 1)

case inr.inl.inl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂✝¹ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
h₁✝ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂✝ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃✝ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂✝)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt✝⁴ : a < n + 2 + 1
b : ℕ
isLt✝³ : b < n + 1 + 1
j : ℕ
isLt✝² : j < n + 1
k : ℕ
isLt✝¹ : k < n + 2
h₁ : ⟨j, isLt✝²⟩.castSucc < ⟨k, isLt✝¹⟩
h₂ : ⟨k, isLt✝¹⟩.succ = ⟨a, isLt✝⁴⟩
h₃ : ⟨j, isLt✝²⟩.castSucc = ⟨b, isLt✝³⟩
a✝ : Fin (n + 2 + 1)
b✝ : Fin (n + 1 + 1)
i : ℕ
isLt✝ : i < n + 1
h₄ : ⟨i, isLt✝⟩.castSucc.succ = a✝
h₅ : ⟨i, isLt✝⟩.succ = b✝
⊢ ⟨a, isLt✝⁴⟩ = a✝ → ¬⟨b, isLt✝³⟩ = b✝

case inr.inl.inr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂✝¹ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
h₁✝ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂✝ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃✝ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂✝)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt✝⁴ : a < n + 2 + 1
b : ℕ
isLt✝³ : b < n + 1 + 1
j : ℕ
isLt✝² : j < n + 1
k : ℕ
isLt✝¹ : k < n + 2
h₁ : ⟨j, isLt✝²⟩.castSucc < ⟨k, isLt✝¹⟩
h₂ : ⟨k, isLt✝¹⟩.succ = ⟨a, isLt✝⁴⟩
h₃ : ⟨j, isLt✝²⟩.castSucc = ⟨b, isLt✝³⟩
a✝ : Fin (n + 2 + 1)
b✝ : Fin (n + 1 + 1)
i : ℕ
isLt✝ : i < n + 1
h₄ : ⟨i, isLt✝⟩.castSucc.succ = a✝
h₅ : ⟨i, isLt✝⟩.castSucc = b✝
⊢ ⟨a, isLt✝⁴⟩ = a✝ → ¬⟨b, isLt✝³⟩ = b✝

case inr.inr.inl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂✝¹ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
h₁✝ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂✝ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃✝ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂✝)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt✝³ : a < n + 2 + 1
b : ℕ
isLt✝² : b < n + 1 + 1
j : ℕ
isLt✝¹ : j < n + 1
k : ℕ
isLt✝ : k < n + 2
h₁ : ⟨j, isLt✝¹⟩.castSucc < ⟨k, isLt✝⟩
h₂ : ⟨k, isLt✝⟩.succ = ⟨a, isLt✝³⟩
h₃ : ⟨j, isLt✝¹⟩.castSucc = ⟨b, isLt✝²⟩
⊢ ⟨a, isLt✝³⟩ = 0 → ¬⟨b, isLt✝²⟩ = 0

case inr.inr.inr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂✝¹ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
h₁✝ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂✝ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃✝ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂✝)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt✝³ : a < n + 2 + 1
b : ℕ
isLt✝² : b < n + 1 + 1
j : ℕ
isLt✝¹ : j < n + 1
k : ℕ
isLt✝ : k < n + 2
h₁ : ⟨j, isLt✝¹⟩.castSucc < ⟨k, isLt✝⟩
h₂ : ⟨k, isLt✝⟩.succ = ⟨a, isLt✝³⟩
h₃ : ⟨j, isLt✝¹⟩.castSucc = ⟨b, isLt✝²⟩
⊢ ⟨a, isLt✝³⟩ = Fin.last (n + 2) → ¬⟨b, isLt✝²⟩ = Fin.last (n + 1)