V : Type u_2
α : Type u_1
β : Type ?u.12780
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ (if i = j then 0 else if A i j = 0 then 1 else 0) = 0 ∨ (if i = j then 0 else if A i j = 0 then 1 else 0) = 1
V : Type u_2
α : Type u_1
β : Type ?u.12780
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ compl A i j = 0 ∨ compl A i j = 1
unfold compl
no goals
V : Type u_2
α : Type u_1
β : Type ?u.12780
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ (if i = j then 0 else if A i j = 0 then 1 else 0) = 0 ∨ (if i = j then 0 else if A i j = 0 then 1 else 0) = 1
split_ifs <;> simp