Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
⊢ (if j✝ ∈ some (if i✝ = i then j else if i✝ = j then i else i✝) then 1 else 0) =
    ((((if i✝ = j✝ then 1 else 0) - if j✝ ∈ if i✝ = i then some i else none then 1 else 0) -
          if j✝ ∈ if i✝ = j then some j else none then 1 else 0) +
        if j✝ ∈ if i✝ = i then some j else none then 1 else 0) +
      if j✝ ∈ if i✝ = j then some i else none then 1 else 0

Tactic:
split_ifs

Goal state after:
case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∈ some j
h✝² : i✝ = j✝
h✝¹ : j✝ ∈ some i
h✝ : i✝ = j
⊢ 1 = 1 - 1 - 1 + 1 + 1

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 1 = 1 - 1 - 1 + 1 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 1 = 1 - 1 - 0 + 1 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∈ some j
h✝² : i✝ = j✝
h✝¹ : j✝ ∉ some i
h✝ : i✝ = j
⊢ 1 = 1 - 0 - 1 + 1 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 1 = 1 - 0 - 1 + 1 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 1 = 1 - 0 - 0 + 1 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∈ some j
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∈ some i
h✝ : i✝ = j
⊢ 1 = 0 - 1 - 1 + 1 + 1

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 1 = 0 - 1 - 1 + 1 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 1 = 0 - 1 - 0 + 1 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∈ some j
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∉ some i
h✝ : i✝ = j
⊢ 1 = 0 - 0 - 1 + 1 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 1 = 0 - 0 - 1 + 1 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 1 = 0 - 0 - 0 + 1 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∉ some j
h✝² : i✝ = j✝
h✝¹ : j✝ ∈ some i
h✝ : i✝ = j
⊢ 0 = 1 - 1 - 0 + 0 + 1

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 0 = 1 - 1 - 1 + 0 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 0 = 1 - 1 - 0 + 0 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∉ some j
h✝² : i✝ = j✝
h✝¹ : j✝ ∉ some i
h✝ : i✝ = j
⊢ 0 = 1 - 0 - 0 + 0 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 0 = 1 - 0 - 1 + 0 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 0 = 1 - 0 - 0 + 0 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∉ some j
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∈ some i
h✝ : i✝ = j
⊢ 0 = 0 - 1 - 0 + 0 + 1

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 0 = 0 - 1 - 1 + 0 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 0 = 0 - 1 - 0 + 0 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∉ some j
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∉ some i
h✝ : i✝ = j
⊢ 0 = 0 - 0 - 0 + 0 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 0 = 0 - 0 - 1 + 0 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 0 = 0 - 0 - 0 + 0 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∈ some j
⊢ 1 = 1 - 1 - 1 + 1 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∉ some j
⊢ 1 = 1 - 1 - 0 + 1 + 1

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∈ some j
⊢ 1 = 1 - 0 - 1 + 0 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∉ some j
⊢ 1 = 1 - 0 - 0 + 0 + 1

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∈ some j
⊢ 1 = 0 - 1 - 1 + 1 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∉ some j
⊢ 1 = 0 - 1 - 0 + 1 + 1

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∈ some j
⊢ 1 = 0 - 0 - 1 + 0 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∉ some j
⊢ 1 = 0 - 0 - 0 + 0 + 1

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∈ some j
⊢ 0 = 1 - 1 - 1 + 1 + 0

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∉ some j
⊢ 0 = 1 - 1 - 0 + 1 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∈ some j
⊢ 0 = 1 - 0 - 1 + 0 + 0

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∉ some j
⊢ 0 = 1 - 0 - 0 + 0 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∈ some j
⊢ 0 = 0 - 1 - 1 + 1 + 0

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∉ some j
⊢ 0 = 0 - 1 - 0 + 1 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∈ some j
⊢ 0 = 0 - 0 - 1 + 0 + 0

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∉ some j
⊢ 0 = 0 - 0 - 0 + 0 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∈ some i✝
h✝¹ : i✝ = j✝
h✝ : j✝ ∈ none
⊢ 1 = 1 - 1 - 1 + 1 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∈ some i✝
h✝¹ : i✝ = j✝
h✝ : j✝ ∉ none
⊢ 1 = 1 - 0 - 0 + 0 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∈ some i✝
h✝¹ : ¬i✝ = j✝
h✝ : j✝ ∈ none
⊢ 1 = 0 - 1 - 1 + 1 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∈ some i✝
h✝¹ : ¬i✝ = j✝
h✝ : j✝ ∉ none
⊢ 1 = 0 - 0 - 0 + 0 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∉ some i✝
h✝¹ : i✝ = j✝
h✝ : j✝ ∈ none
⊢ 0 = 1 - 1 - 1 + 1 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∉ some i✝
h✝¹ : i✝ = j✝
h✝ : j✝ ∉ none
⊢ 0 = 1 - 0 - 0 + 0 + 0

case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∉ some i✝
h✝¹ : ¬i✝ = j✝
h✝ : j✝ ∈ none
⊢ 0 = 0 - 1 - 1 + 1 + 1

case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∉ some i✝
h✝¹ : ¬i✝ = j✝
h✝ : j✝ ∉ none
⊢ 0 = 0 - 0 - 0 + 0 + 0