Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

Tactic:
<;>

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