-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}
a₁ :
  (↑((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) ↦
              (match (motive :=
                  (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)) x_1 with
                | ⟨(a, b), h⟩ =>
                  Subtype.mk (p := fun (x_2 : ℤ × ℤ) ↦ x_2 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a + x, b) ⋯ :
                (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)))
            ((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)) ↦
                (match (motive :=
                    (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type))
                    x_1 with
                  | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a - x, b) ⋯ :
                  (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)))
              (Subtype.mk (p := fun (x_1 : ℤ × ℤ) ↦ x_1 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a, b) h))) :
        ℤ × ℤ).1 =
    (↑(Subtype.mk (p := fun (x_1 : ℤ × ℤ) ↦ x_1 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a, b) h) : ℤ × ℤ).1
⊢ (fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) ↦
        (match (motive := (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type))
            x_1 with
          | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x_2 : ℤ × ℤ) ↦ x_2 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a + x, b) ⋯ :
          (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)))
      ((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)) ↦
          (match (motive := (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type))
              x_1 with
            | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a - x, b) ⋯ :
            (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)))
        (Subtype.mk (p := fun (x_1 : ℤ × ℤ) ↦ x_1 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a, b) h)) =
    Subtype.mk (p := fun (x_1 : ℤ × ℤ) ↦ x_1 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a, b) h
have a₂ : (↑((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) ↦
            (match (motive :=
                (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)) x_1 with
              | ⟨(a, b), h⟩ =>
                Subtype.mk (p := fun (x_2 : ℤ × ℤ) ↦ x_2 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a + x, b) sorry :
              (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)))
          ((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)) ↦
              (match (motive :=
                  (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) x_1 with
                | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a - x, b) sorry :
                (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)))
            (Subtype.mk (p := fun (x_1 : ℤ × ℤ) ↦ x_1 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a, b) h))) :
      ℤ × ℤ).2 =
  (↑(Subtype.mk (p := fun (x_1 : ℤ × ℤ) ↦ x_1 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a, b) h) : ℤ × ℤ).2
Tactic: ext