∀ {V : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : One α] {A : Matrix V V α},
  autoParam (∀ (i j : V), A i j = 0 ∨ A i j = 1) Matrix.IsAdjMatrix.zero_or_one._autoParam →
    autoParam A.IsSymm Matrix.IsAdjMatrix.symm._autoParam →
      autoParam (∀ (i : V), A i i = 0) Matrix.IsAdjMatrix.apply_diag._autoParam → A.IsAdjMatrix