-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
pos : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
pos₁ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
neg : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 1 - 0 + 1 + 0
pos₂ : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∉ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 0
pos₃ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∉ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 1
neg₁ :
  i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∉ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 0 - 0 + 1 + 0
pos₄ : i_1 = i → j_1 ∈ some j → ¬i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1
pos₅ :
  i_1 = i →
    j_1 ∈ some j →
      ¬i_1 = j_1 →
        j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1
neg₂ :
  i_1 = i → j_1 ∈ some j → ¬i_1 = j_1 → j_1 ∈ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 0 1 - 0 + 1 + 0
pos₆ : i_1 = i → j_1 ∈ some j → ¬i_1 = j_1 → j_1 ∉ some i → i_1 = j → 1 = HSub.hSub (α := α) 0 0 - 1 + 1 + 0
pos₇ :
  i_1 = i →
    j_1 ∈ some j →
      ¬i_1 = j_1 →
        j_1 ∉ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 0 0 - 1 + 1 + 1
neg₃ :
  i_1 = i → j_1 ∈ some j → ¬i_1 = j_1 → j_1 ∉ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 0 0 - 0 + 1 + 0
pos₈ : i_1 = i → j_1 ∉ some j → i_1 = j_1 → j_1 ∈ some i → i_1 = j → 0 = HSub.hSub (α := α) 1 1 - 0 + 0 + 1
pos₉ :
  i_1 = i →
    j_1 ∉ some j →
      i_1 = j_1 →
        j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 0 = HSub.hSub (α := α) 1 1 - 1 + 0 + 1
neg₄ :
  i_1 = i → j_1 ∉ some j → i_1 = j_1 → j_1 ∈ some i → ¬i_1 = j → j_1 ∉ none → 0 = HSub.hSub (α := α) 1 1 - 0 + 0 + 0
pos₁₀ : i_1 = i → j_1 ∉ some j → i_1 = j_1 → j_1 ∉ some i → i_1 = j → 0 = HSub.hSub (α := α) 1 0 - 0 + 0 + 0
pos₁₁ :
  i_1 = i →
    j_1 ∉ some j →
      i_1 = j_1 →
        j_1 ∉ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 0 = HSub.hSub (α := α) 1 0 - 1 + 0 + 1
neg₅ :
  i_1 = i → j_1 ∉ some j → i_1 = j_1 → j_1 ∉ some i → ¬i_1 = j → j_1 ∉ none → 0 = HSub.hSub (α := α) 1 0 - 0 + 0 + 0
pos₁₂ : i_1 = i → j_1 ∉ some j → ¬i_1 = j_1 → j_1 ∈ some i → i_1 = j → 0 = HSub.hSub (α := α) 0 1 - 0 + 0 + 1
pos₁₃ :
  i_1 = i →
    j_1 ∉ some j →
      ¬i_1 = j_1 →
        j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 0 = HSub.hSub (α := α) 0 1 - 1 + 0 + 1
neg₆ :
  i_1 = i → j_1 ∉ some j → ¬i_1 = j_1 → j_1 ∈ some i → ¬i_1 = j → j_1 ∉ none → 0 = HSub.hSub (α := α) 0 1 - 0 + 0 + 0
pos₁₄ : i_1 = i → j_1 ∉ some j → ¬i_1 = j_1 → j_1 ∉ some i → i_1 = j → 0 = HSub.hSub (α := α) 0 0 - 0 + 0 + 0
pos₁₅ :
  i_1 = i →
    j_1 ∉ some j →
      ¬i_1 = j_1 →
        j_1 ∉ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 0 = HSub.hSub (α := α) 0 0 - 1 + 0 + 1
neg₇ :
  i_1 = i → j_1 ∉ some j → ¬i_1 = j_1 → j_1 ∉ some i → ¬i_1 = j → j_1 ∉ none → 0 = HSub.hSub (α := α) 0 0 - 0 + 0 + 0
pos₁₆ :
  ¬i_1 = i →
    i_1 = j →
      j_1 ∈ some i →
        i_1 = j_1 → Membership.mem (γ := Option n) none j_1 → j_1 ∈ some j → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
neg₈ :
  ¬i_1 = i →
    i_1 = j →
      j_1 ∈ some i →
        i_1 = j_1 → Membership.mem (γ := Option n) none j_1 → j_1 ∉ some j → 1 = HSub.hSub (α := α) 1 1 - 0 + 1 + 1
pos₁₇ :
  ¬i_1 = i → i_1 = j → j_1 ∈ some i → i_1 = j_1 → j_1 ∉ none → j_1 ∈ some j → 1 = HSub.hSub (α := α) 1 0 - 1 + 0 + 1
neg₉ :
  ¬i_1 = i → i_1 = j → j_1 ∈ some i → i_1 = j_1 → j_1 ∉ none → j_1 ∉ some j → 1 = HSub.hSub (α := α) 1 0 - 0 + 0 + 1
pos₁₈ :
  ¬i_1 = i →
    i_1 = j →
      j_1 ∈ some i →
        ¬i_1 = j_1 → Membership.mem (γ := Option n) none j_1 → j_1 ∈ some j → 1 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1
neg₁₀ :
  ¬i_1 = i →
    i_1 = j →
      j_1 ∈ some i →
        ¬i_1 = j_1 → Membership.mem (γ := Option n) none j_1 → j_1 ∉ some j → 1 = HSub.hSub (α := α) 0 1 - 0 + 1 + 1
pos₁₉ :
  ¬i_1 = i → i_1 = j → j_1 ∈ some i → ¬i_1 = j_1 → j_1 ∉ none → j_1 ∈ some j → 1 = HSub.hSub (α := α) 0 0 - 1 + 0 + 1
neg₁₁ :
  ¬i_1 = i → i_1 = j → j_1 ∈ some i → ¬i_1 = j_1 → j_1 ∉ none → j_1 ∉ some j → 1 = HSub.hSub (α := α) 0 0 - 0 + 0 + 1
pos₂₀ :
  ¬i_1 = i →
    i_1 = j →
      j_1 ∉ some i →
        i_1 = j_1 → Membership.mem (γ := Option n) none j_1 → j_1 ∈ some j → 0 = HSub.hSub (α := α) 1 1 - 1 + 1 + 0
neg₁₂ :
  ¬i_1 = i →
    i_1 = j →
      j_1 ∉ some i →
        i_1 = j_1 → Membership.mem (γ := Option n) none j_1 → j_1 ∉ some j → 0 = HSub.hSub (α := α) 1 1 - 0 + 1 + 0
pos₂₁ :
  ¬i_1 = i → i_1 = j → j_1 ∉ some i → i_1 = j_1 → j_1 ∉ none → j_1 ∈ some j → 0 = HSub.hSub (α := α) 1 0 - 1 + 0 + 0
neg₁₃ :
  ¬i_1 = i → i_1 = j → j_1 ∉ some i → i_1 = j_1 → j_1 ∉ none → j_1 ∉ some j → 0 = HSub.hSub (α := α) 1 0 - 0 + 0 + 0
pos₂₂ :
  ¬i_1 = i →
    i_1 = j →
      j_1 ∉ some i →
        ¬i_1 = j_1 → Membership.mem (γ := Option n) none j_1 → j_1 ∈ some j → 0 = HSub.hSub (α := α) 0 1 - 1 + 1 + 0
neg₁₄ :
  ¬i_1 = i →
    i_1 = j →
      j_1 ∉ some i →
        ¬i_1 = j_1 → Membership.mem (γ := Option n) none j_1 → j_1 ∉ some j → 0 = HSub.hSub (α := α) 0 1 - 0 + 1 + 0
pos₂₃ :
  ¬i_1 = i → i_1 = j → j_1 ∉ some i → ¬i_1 = j_1 → j_1 ∉ none → j_1 ∈ some j → 0 = HSub.hSub (α := α) 0 0 - 1 + 0 + 0
neg₁₅ :
  ¬i_1 = i → i_1 = j → j_1 ∉ some i → ¬i_1 = j_1 → j_1 ∉ none → j_1 ∉ some j → 0 = HSub.hSub (α := α) 0 0 - 0 + 0 + 0
pos₂₄ :
  ¬i_1 = i →
    ¬i_1 = j →
      j_1 ∈ some i_1 → i_1 = j_1 → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
⊢ (if j_1 ∈ some (if i_1 = i then j else if i_1 = j then i else i_1) then 1 else 0) =
    ((HSub.hSub (α := α) (if i_1 = j_1 then 1 else 0) (if j_1 ∈ if i_1 = i then some i else none then 1 else 0) -
          if j_1 ∈ if i_1 = j then some j else none then 1 else 0) +
        if j_1 ∈ if i_1 = i then some j else none then 1 else 0) +
      if j_1 ∈ if i_1 = j then some i else none then 1 else 0
have neg₁₆ : ¬i_1 = i → ¬i_1 = j → j_1 ∈ some i_1 → i_1 = j_1 → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 0 - 0 + 0 + 0
Tactic: split_ifs